Skip to content

perf(row-reduce): complete Phase 4 evidence - #9865

Closed
kim-em wants to merge 9 commits into
mainfrom
issue-9811
Closed

perf(row-reduce): complete Phase 4 evidence#9865
kim-em wants to merge 9 commits into
mainfrom
issue-9811

Conversation

@kim-em

@kim-em kim-em commented Aug 31, 2026

Copy link
Copy Markdown
Owner

Summary

  • add compiled mode-1 benchmarks for all ten advertised HexRowReduce executable operations
  • add dense and rank-deficient rational families, exact-hash FLINT RREF/nullspace anchors, and CI/release-manifest integration
  • record clean scientific evidence, comparator ratios, and samply profiles; promote HexRowReduce to Phase 4

Complexity contract

All ten direct registrations use the strongest ordered evidence mode. The public RREF, rank, span, and nullspace wrappers declare cubic fixed-aspect Gauss--Jordan cost; prepared echelon span queries declare quadratic matrix--vector work; prepared reduced-nullspace construction declares the documented cubic loose bound while profiling separates it from elimination. These models and input dimensions match the HexRowReduce SPEC, and each registration passes the mode-1 normalized-constant/slope checks.

Verification

  • lake build (10,506 jobs)
  • lake build hexrowreduce_bench
  • .lake/build/bin/hexrowreduce_bench verify (39/39)
  • python3 scripts/check_phase4.py
  • release manifest, DAG, manual split, trust-surface, and Mathlib-free checks
  • oracle unit tests and release-sync unit tests
  • clean scientific, FLINT comparator, and two samply profile runs

Closes #9811

Kim Morrison added 2 commits August 31, 2026 04:46
Cost-model derivation: fixed-aspect Gauss-Jordan visits cubic matrix work; prepared span operations traverse quadratic data; prepared nullspace construction materializes quadratic output while linearly scanning pivot columns, giving cubic work. Add exact-hash informational fmpq_mat RREF and canonical-nullspace anchors.
Promote HexRowReduce through Phase 4 with clean scientific, comparator, and profile evidence for every advertised executable operation.
@kim-em
kim-em enabled auto-merge (squash) August 31, 2026 05:22
Kim Morrison added 7 commits August 31, 2026 05:38
Cost-model derivation: echelonCoeffs constructs n output entries in linear work; freeCols tests n columns against n/2 sorted pivots in quadratic work. Their controlled ladders stop below the runtime allocation transitions.
Cost-model derivation: echelonCoeffs constructs n output entries in linear work; freeCols tests n columns against n/2 sorted pivots in quadratic work. Their controlled ladders stop below the runtime allocation transitions.
@kim-em
kim-em disabled auto-merge August 31, 2026 06:52
@kim-em

kim-em commented Aug 31, 2026

Copy link
Copy Markdown
Owner Author

Closing after premise validation found asymptotic implementation gaps that make the proposed Phase-4 claims unsound. The concrete source and measurement evidence is recorded on #9811. This PR must not merge by weakening the models or tolerances.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

audit-found: HexRowReduce has no Phase-4 performance mode

1 participant