rank_exact

std.linalg.rank_exact · Level L4

The rank of an integer matrix, decided exactly by fraction-free Gaussian elimination: a Scan of bareiss_step over the columns, every entry an integer and every division exact. Unlike matrix_rank, which reads singular values against a tolerance, there is no threshold; the entries must stay below 2⁵³, which the intermediate minors (Hadamard's bound) make the limit.

rank A, exactly

Signature

rank_exact(A: f64[m, n]) → f64[]

Structure

The function as NOVA stores it: one box per input, operation and output, and arrows that carry values. A double border marks another library function this one runs — called once, or by Scan once per element; select it to open that function.

input
operation
constant
call
output

Verification

Signature proven by NOVA’s shape solver, for every size.
Equal to the reference Gaussian elimination over the rationals (Python fractions) in exact rational arithmetic, on all 40 test cases.
All 40 float64 results are exact: the error is zero.
Interpreter and NumPy backend return bit-identical results.
At float32 too: the 40 test cases rounded to float32, and 40 of them exact, with zero error.

Accuracy in detail

correctly rounded (the float64 nearest the exact value): 100%
bit-equal to the NumPy formula in float64: 100%
largest error, in units in the last place: 0

Identity

Calls

bareiss_step

Called by

direct_sum in_span independence kernel_dimension same_coset

sha256:c4bd1d5c3e3f59265aef0449493baa38dbe7be84ada7313a97def0c0f3caa22b

The semantic hash of the graph. It changes when the program changes, and never when only its documentation does.

Control handle

Symbol: Ω:std.linalg.rank_exact · Ω:rank_exact
Pins: sha256:8fe0ec5406b6a5de34878d387989316ba003335c418664647712dd78c302d4aathis graph and the 1 it reaches through calls
Evidence: sha256:5de9cb6b4e00114934136334de5aab12480f2c341e92fdc7b25efaa46fe3fa88the hash of its verification record
Needs: no capability: a pure function

Through NOVA’s control layer, the symbol launches this function only while the program still matches what it pins: a change to this graph, or to any graph it reaches, needs a migration first.