perf(row-reduce): optimize prepared helpers and complete Phase 4 evidence - #9880
Merged
Conversation
added 7 commits
September 1, 2026 01:25
Cost-model derivation: public elimination and nullspace wrappers are cubic; prepared span and nullspace materialization are quadratic; prepared coefficient and free-column traversals are linear.
Cost-model derivation: public row reduction, rank, span, and nullspace are cubic because dense elimination performs n pivots by n rows by n entries. Prepared span and nullspace materialization are quadratic, while prepared coefficient selection and the sorted free-column complement are linear.
Cost-model derivation: nullspace construction performs dense Gauss--Jordan elimination before basis materialization, so benchmark it against n^3 across 8, 12, 16, 24, 32, 48, and 64. The restored low-to-high ladder directly tests the claimed regime instead of sampling only the high endpoint. Document checksum attribution and comparator limitations identified by independent review.
added 2 commits
September 1, 2026 02:35
Record a pristine full-ladder run after restoring the cubic nullspace schedule. All twelve parametric targets pass their declared models, fixed hashes agree, and the report now includes comparator eligibility and checksum attribution.
# Conflicts: # .github/workflows/ci.yml
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Closes #9811
Summary
Validation
Scientific artifact: reports/bench-results/hex-row-reduce-phase4-scientific.json, SHA-256 ecc174e4ac710fa928f6e31464251ca5a0484d0ef3073992246af1f3e9a5e2f2.
Review and release prerequisite
A fresh Claude Opus review found substantive evidence and release-readiness gaps. This revision restores the full cubic nullspace ladder, discloses checksum profile cost and comparator eligibility/work mismatch, and records the refreshed pristine artifact. The required unmanaged benchmark sidecar skeleton is merged in leanprover/hex-row-reduce#2, and release-sync-baseline now records mirror main at 52cd2d3a156207bb5b16f00ab872a1055adf580f.