perf(row-reduce): complete Phase 4 evidence

.github/workflows/ci.yml

@@ -170,7 +170,7 @@ jobs:
       - name: Define the hex-dev cache + build target sets
         run: |
           echo "HEX_LIB_TARGETS=HexBasic HexTruncatedSeries HexTruncatedSeriesMathlib HexArith HexPoly HexPolyFast HexMvPoly HexModArith HexGF2 HexPolyZ HexRoots HexResultant HexInterval HexIntervalExperiment HexIntervalMathlib HexIntervalMathlibExperiment HexIntervalReplayProbe HexIntervalMathlibReplayProbe HexRealRootsMathlibReplayProbe HexRCFProofProbe HexPolyFp HexGFqRing HexGFqField HexBerlekamp HexHensel HexConway HexGFq HexPrimality HexIntFactor HexPrimalityKernelProbe HexPrimalityElabProbe HexPrimalityMathlibProofProbe HexIntFactorKernelProbe HexMvGcdKernelProbe HexBerlekampZassenhaus HexRealRoots HexMatrix HexRowReduce HexDeterminant HexBareiss HexHermite HexSmith HexCharPoly HexMinPoly HexPolySmith HexGramSchmidt HexLLL HexMatrixMathlib HexHermiteMathlib HexSmithMathlib HexSmithTests HexCharPolyMathlib HexMinPolyMathlib HexPolySmithMathlib HexGramSchmidtMathlib HexLLLMathlib HexBerlekampZassenhausMathlib HexBerlekampZassenhausMathlibProofProbe HexBerlekampMathlibProofProbe HexPrimalityMathlib HexIntFactorMathlib HexPolyFpMathlib HexFactorizationModules HexRealRootsMathlib HexGF2Mathlib HexGFqMathlib HexMvPolyMathlib HexMvPolyMathlibProofProbe HexRCF HexRCFTests HexRootsMathlib HexResultantMathlib HexNumberField HexNumberFieldMathlib HexNumberFieldTower HexNumberFieldTowerMathlib HexReleaseTests HexReleaseExamples HexAggregateCheck" >> "$GITHUB_ENV"
-          echo "HEX_EXE_TARGETS=hextruncatedseries_bench hexarith_bench hexpoly_bench hexpolyfast_bench hexpolysmith_bench hexmvpoly_bench hexmvgcd_bench hexsparsepoly_bench hexpolyz_bench hexpolyfp_bench hexmodarith_bench hexmodular_bench hexgf2_bench hexgfqring_bench hexgfqfield_bench hexgfq_bench hexhensel_bench hexprimality_bench hexprimality_policy_probe hexprimality_fuel_probe hexintfactor_bench hexberlekamp_bench hexbz_bench hexconway_bench hexmatrix_bench hexstrassen_compare hexdeterminant_bench hexbareiss_bench hexcharpoly_bench hexminpoly_bench hexgramschmidt_bench hexhermite_bench hexsmith_bench hexrealroots_bench hexrcf_bench hexroots_bench hexresultant_bench hexnumberfield_bench hexnumberfieldtower_bench hexinterval_decision_bench hexroots_demo hex_interval_representation_spike hex_interval_center_spike hex_interval_scale_spike hex_interval_scheduler_spike hex_interval_policy_frontier_spike hex_arith_floor hexlll_bench hexlll_gram_bench hexlll_external_reduction hexbz_factor_service" >> "$GITHUB_ENV"
+          echo "HEX_EXE_TARGETS=hextruncatedseries_bench hexarith_bench hexpoly_bench hexpolyfast_bench hexpolysmith_bench hexmvpoly_bench hexmvgcd_bench hexsparsepoly_bench hexpolyz_bench hexpolyfp_bench hexmodarith_bench hexmodular_bench hexgf2_bench hexgfqring_bench hexgfqfield_bench hexgfq_bench hexhensel_bench hexprimality_bench hexprimality_policy_probe hexprimality_fuel_probe hexintfactor_bench hexberlekamp_bench hexbz_bench hexconway_bench hexmatrix_bench hexstrassen_compare hexrowreduce_bench hexdeterminant_bench hexbareiss_bench hexcharpoly_bench hexminpoly_bench hexgramschmidt_bench hexhermite_bench hexsmith_bench hexrealroots_bench hexrcf_bench hexroots_bench hexresultant_bench hexnumberfield_bench hexnumberfieldtower_bench hexinterval_decision_bench hexroots_demo hex_interval_representation_spike hex_interval_center_spike hex_interval_scale_spike hex_interval_scheduler_spike hex_interval_policy_frontier_spike hex_arith_floor hexlll_bench hexlll_gram_bench hexlll_external_reduction hexbz_factor_service" >> "$GITHUB_ENV"
       # Shared build. The libraries, bench exes, conformance #guard drivers, and
       # emit-fixture exes are all elaborated here so the two verification tails
       # below only *run* things, never rebuild them -- which is what lets the
@@ -239,7 +239,7 @@ jobs:
             hexmodular_bench \
             hexgf2_bench hexgfqring_bench hexgfqfield_bench hexgfq_bench \
             hexhensel_bench hexintfactor_bench hexberlekamp_bench hexbz_bench \
-            hexconway_bench hexdeterminant_bench hexmatrix_bench \
+            hexconway_bench hexdeterminant_bench hexmatrix_bench hexrowreduce_bench \
             hexhermite_bench hexsmith_bench \
             hexcharpoly_bench hexminpoly_bench \
             hexgramschmidt_bench hexlll_gram_bench \

HexRowReduce/SPEC/hex-row-reduce.md

@@ -73,6 +73,8 @@ def IsRowReduced.nullspaceMatrix [Ring R] (E : IsRowReduced M D) : Matrix R m (m
 def IsRowReduced.nullspace [Ring R] (E : IsRowReduced M D) : Vector (Vector R m) (m - D.rank)
 def Matrix.nullspace [Field R] [DecidableEq R] (M : Matrix R n m) :
     Vector (Vector R m) (m - rowReduce_rank)
+def Matrix.nullspaceBasisMatrix [Field R] [DecidableEq R] (M : Matrix R n m) :
+    Matrix R m (m - rowReduce_rank)
 ```
 
 **Key properties:**
@@ -106,11 +108,49 @@ with `colPartition` (free columns telescope to `v[freeCols[l]]`; pivot columns
 follow from `pivot_one` / `above_pivot_zero` / `below_pivot_zero` / `zero_row`);
 package into `E.nullspaceMatrix * c = v`.
 
+## Complexity and benchmark contract
+
+For an `n × m` matrix of rank `r`, the executable Gauss--Jordan loop performs
+at most `r` pivot steps, and each step visits `O(n(n + m))` entries across the
+echelon and transform updates.  Thus the field-operation bound is
+`O(rn(n + m))`; it is cubic for the fixed-aspect square families below.  This
+is an arithmetic-operation bound, not unrestricted bit complexity: exact
+rational cost also depends on numerator and denominator growth.
+
+`bench/HexRowReduce/Bench.lean` registers every advertised executable surface
+directly in mode 1:
+
+| Operation | Controlled family | Declared wall model |
+| --- | --- | --- |
+| `Matrix.rowReduce`, `Matrix.rowReduce_rank` | `dense-rational-rref` | `n³` |
+| `Matrix.spanCoeffs`, `Matrix.spanContains` | `dense-rational-rref` | `n³` |
+| `IsEchelonForm.echelonCoeffs` on prepared RREF | `rank-deficient-rational-nullspace` | `n` |
+| `IsEchelonForm.spanCoeffs`, `IsEchelonForm.spanContains` on prepared RREF | `dense-rational-rref` | `n²` |
+| `IsEchelonForm.freeCols` on prepared RREF | `rank-deficient-rational-nullspace` | `n²` |
+| `Matrix.nullspaceBasisMatrix`, `Matrix.nullspace` | `rank-deficient-rational-nullspace` | `n³` |
+| `IsRowReduced.nullspaceMatrix`, `IsRowReduced.nullspace` on prepared RREF | `rank-deficient-rational-nullspace` | `n³` |
+
+The dense family is `I + J`, so all pivots fire while intermediate rational
+heights stay bounded by `O(log n)` bits on the scheduled ladder.  The
+rank-deficient family repeats the rows and columns of `I + J` at half size,
+giving rank and nullity `n / 2`.  Prepared span targets exclude RREF and visit
+quadratically many entries.  Prepared nullspace targets use an already-reduced
+rank-`n / 2` projection to exclude RREF setup; constructing `Θ(n²)` output
+entries calls a pivot lookup that scans up to `n / 2` columns, giving the
+declared cubic model.  Preparation and result forcing are outside and inside
+the timed region, respectively.
+
 ## External comparators
 
-The `rank`, `rowReduce`, and `nullspace` operations are cross-checked for correctness
-against python-flint's `fmpz_mat` / `fmpq_mat` through the conformance oracle
-(`scripts/oracle/matrix_flint.py`, driven by `hexrowreduce_emit_fixtures`).
-There is no Phase-4 performance comparator: row reduction is an exact rational
-computation validated for correctness, not timed against an external tool. See
-`reports/hex-row-reduce-performance.md`.
+No external Phase-4 timing comparator is declared.  python-flint exposes
+FLINT's exact rational RREF, but the public Python interface must decode and
+encode every rational matrix entry for each request; that transport dominates
+the shared practical ladder and therefore cannot support a meaningful kernel
+ratio.  Moreover, Hex's `rowReduce` returns the complete row-operation
+transform while python-flint's RREF omits it, and `spanCoeffs` returns a
+transform-dependent witness with no canonical counterpart.
+
+FLINT remains the independent correctness oracle for `rank`, `rowReduce`, and
+`nullspace` through `scripts/oracle/matrix_flint.py`, driven by
+`hexrowreduce_emit_fixtures`.  It is conformance evidence, not timing evidence.
+See `reports/hex-row-reduce-performance.md`.