feat(sparse-poly-mathlib): activate the companion with the complete Equiv surface - #9481
Merged
Conversation
kim-em
force-pushed
the
sparse-poly-proofs
branch
from
August 23, 2026 12:38
2f278c0 to
d08634f
Compare
kim-em
force-pushed
the
sparse-poly-mathlib
branch
2 times, most recently
from
August 23, 2026 12:39
0bee145 to
e87f134
Compare
kim-em
force-pushed
the
sparse-poly-proofs
branch
from
August 23, 2026 13:05
d08634f to
dfd070c
Compare
kim-em
force-pushed
the
sparse-poly-mathlib
branch
from
August 23, 2026 13:05
792f75d to
cf0babf
Compare
kim-em
force-pushed
the
sparse-poly-proofs
branch
from
August 23, 2026 13:28
dfd070c to
38c3318
Compare
kim-em
force-pushed
the
sparse-poly-mathlib
branch
from
August 23, 2026 13:28
cf0babf to
57302e0
Compare
kim-em
force-pushed
the
sparse-poly-proofs
branch
from
August 23, 2026 13:55
38c3318 to
96fd9d2
Compare
kim-em
force-pushed
the
sparse-poly-mathlib
branch
from
August 23, 2026 13:55
57302e0 to
0ec46e8
Compare
kim-em
force-pushed
the
sparse-poly-proofs
branch
from
August 23, 2026 14:19
96fd9d2 to
82c4817
Compare
kim-em
force-pushed
the
sparse-poly-mathlib
branch
from
August 23, 2026 14:19
0ec46e8 to
9621904
Compare
kim-em
force-pushed
the
sparse-poly-proofs
branch
from
August 23, 2026 15:11
82c4817 to
95ab0fb
Compare
kim-em
force-pushed
the
sparse-poly-mathlib
branch
from
August 23, 2026 15:11
9621904 to
36460aa
Compare
kim-em
force-pushed
the
sparse-poly-proofs
branch
from
August 23, 2026 15:56
95ab0fb to
e37a267
Compare
kim-em
force-pushed
the
sparse-poly-mathlib
branch
from
August 23, 2026 15:56
36460aa to
072d1c4
Compare
kim-em
force-pushed
the
sparse-poly-proofs
branch
from
August 23, 2026 16:24
e37a267 to
15c6fce
Compare
kim-em
force-pushed
the
sparse-poly-mathlib
branch
from
August 23, 2026 16:24
072d1c4 to
9b39388
Compare
…quiv surface The companion SPEC with its headline correctness theorem section, the denseEquiv/equiv ring equivalences at Mathlib CommRing, and all seven correspondence lemmas including the equiv_support headline. Core gains mem_support_iff. Progress: progress/20260823T123004Z_sparse-poly-mathlib.md Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_014CvkL7tZHMnLN53fXCAjiq
…nces, and the token Independent review verdict pass-with-gaps: dense eval helpers move to HexPolyMathlib as simp lemmas, equiv_monomial/C/X/natDegree/ leadingCoeff/monic close the constructor/observer gaps, equiv_apply loses simp so the correspondence lemmas fire first, and the parent SPEC's RingEquiv field description is corrected. substScale transport is issue 9482. done_through: 2 Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_014CvkL7tZHMnLN53fXCAjiq
Companion-import regression guards plus the theorem-level transport surface at a generic CommRing, wired into the HexConformance globs. Phase 4 holds by the correspondence-only-layer declaration (zero bench targets, no phase4 block), Phase 5 by zero sorries; done_through: 5. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_014CvkL7tZHMnLN53fXCAjiq
kim-em
force-pushed
the
sparse-poly-mathlib
branch
from
August 23, 2026 16:50
9b39388 to
ea2a79c
Compare
kim-em
enabled auto-merge (squash)
August 23, 2026 16:50
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.
This PR activate HexSparsePolyMathlib and bring it through phases 1-5, fully proven throughout: the companion SPEC (with the headline correctness theorem section naming
equiv,coeff_equiv, andequiv_support), thedenseEquivring equivalence packaging the core'stoDense/ofDenseconversions and homomorphism laws,equiv := denseEquiv.trans HexPolyMathlib.equiv, and one correspondence lemma per public core operation (coeff_equiv,equiv_toDense,equiv_support,equiv_eval,equiv_derivative,equiv_compose,equiv_substPow,equiv_monomial,equiv_C,equiv_X,equiv_natDegree,equiv_leadingCoeff,equiv_monic). Both equivalences are stated at Mathlib[CommRing R]becausedenseEquiv.map_mul'reuses the core'stoDense_mul, which the parent SPEC's law-placement note records atLean.Grind.CommRing; the parent SPEC's Mathlib-layer section is updated to match, with the semiring weakening path recorded. HexPolyMathlib gains the denseeval_toPolynomialsimp lemma, and the core gainsHex.SparsePoly.mem_support_iff. An independent Phase-2 review ran against the SPEC and PLAN/Phase2.md (token committed); the conformance module carries companion-import regression guards plus the theorem-level transport surface at a genericCommRing; Phase 4 holds by the correspondence-only-layer declaration and Phase 5 by zero sorries. The one scheduled gap,substScaletransport, is #9482.done_through: 5.🤖 Prepared with Claude Code