perf(row-reduce): optimize prepared helpers and complete Phase 4 evidence

[kim-em]

library: HexRowReduce

Problem

HexRowReduce advertises executable row reduction, rank, nullspace, and span-coefficient operations, but has no compiled Phase-4 benchmark coverage. Premise validation also found two avoidable costs that must be fixed before scientific complexity evidence can be accepted:

• IsEchelonForm.freeColsList filters every column using linear membership in the sorted pivot list, making the complement quadratic instead of linear.
• IsRowReduced.nullspaceMatrix performs the linear pivotIndex? scan for every output entry, making the prepared constructor cubic instead of quadratic.

This issue therefore includes the prerequisite implementation work; it is not a documentation-only Phase-4 promotion.

Deliverables

• Implement a linear sorted complement for free columns and prove it equivalent to the existing definition.
• Keep the public pivotIndex? behavior unchanged, but build a private column-to-pivot-row lookup once inside nullspaceMatrix, use constant-time entry lookup, and prove equivalence.
• Repair downstream HexBerlekamp/PackedKernel.lean proofs that currently rely on definitional unfolding of these implementations.
• Add direct mode-1 registrations for all 12 advertised executable operations, with independently derived models, prepared-state isolation, fixed schedules, default tolerance 0.15, and the normal signal floor/time budget.
• Add an informational persistent python-flint comparison for the directly comparable rank result only. Keep full RREF/nullspace correctness in conformance and give exact non-comparability reasons for the remaining operations.
• Add Phase-4 input-family metadata, scientific evidence, representative profiles, an empty-Concerns headline report, and set the release manifest bench flag.

Initial schedules may be calibrated before evidence is frozen only to obtain adequate signal or avoid a documented runtime/allocation transition. Do not change the expected model or tolerance, omit difficult rungs, or retune after accepting a clean evidence run.

Context

• audit: reconcile completed Phase-4 reports with the ordered complexity modes #9797
• HexRowReduce/SPEC/hex-row-reduce.md
• reports/hex-row-reduce-performance.md
• PLAN/Phase4.md §Evidence tracks and §Exit criteria
• SPEC/benchmarking.md §Choosing the complexity claim
• Premise evidence: perf(row-reduce): optimize prepared helpers and complete Phase 4 evidence #9811 (comment)

Verification

• lake build HexRowReduce
• lake build HexBerlekamp
• lake build
• lake exe hexrowreduce_bench list
• lake exe hexrowreduce_bench verify
• fixed scientific runs, FLINT informational comparison, and representative profiles
• python3 scripts/check_phase4.py
• python3 scripts/check_dag.py
• git diff --check

[kim-em]

Premise validation found that this Phase-4-only directive cannot be completed soundly against the current implementation.

Concrete evidence:

• IsRowReduced.nullspaceMatrix in HexRowReduce/Nullspace.lean constructs m * (m - r) entries and calls the linear pivotIndex? scan inside the per-entry lambda. On the declared fixed-rank family this is Theta(m * (m - r) * r), hence cubic. A pivot-column-to-row lookup can be built once in Theta(mr) or better and then indexed in O(1), giving the intended quadratic output construction. Declaring n^3 merely matches the avoidable current scan, which SPEC/benchmarking.md explicitly forbids.
• IsEchelonForm.freeColsList in HexRowReduce/RowEchelon/Contracts.lean filters all m columns with membership in D.pivotCols.toList, giving Theta(mr) work even though the proved-sorted pivot vector admits a linear sorted-complement merge. Declaring n^2 would likewise ratify the current implementation rather than test the independently expected linear algorithm.
• The scientific run for prepared nullspaceMatrix measured beta = -0.166352. It is inconclusive under the mode-1 default tolerance 0.15; the current PR only reports a pass after widening that tolerance to 0.20. This is not acceptable evidence under the verdict-fitting rule.
• pivotIndex? is public, separable, and asymptotically significant, so the attribution rule also requires its own registration if it remains part of the implementation.

Therefore the requested empty-Concerns Phase-4 promotion needs earlier-phase algorithm work first: precompute pivot lookup for nullspace construction and replace the repeated-membership free-column scan with a sorted complement, then derive and measure the quadratic, linear, and pivot-lookup models. I am not filing a decomposition issue because the repository directive policy says to report a defective premise on the directive itself. PR #9865 has been stopped and should not merge in its current form.