feat(sparse-poly): dense conversions with the multiplicative transport - #9388
Merged
Conversation
kim-em
force-pushed
the
sparse-poly-arith
branch
from
August 22, 2026 04:08
de973f0 to
62c31c0
Compare
kim-em
force-pushed
the
sparse-poly-dense
branch
from
August 22, 2026 04:08
33a00b4 to
b5c4fb5
Compare
kim-em
force-pushed
the
sparse-poly-arith
branch
from
August 22, 2026 04:10
62c31c0 to
93e42b4
Compare
kim-em
force-pushed
the
sparse-poly-dense
branch
from
August 22, 2026 04:10
b5c4fb5 to
c1f28fb
Compare
kim-em
force-pushed
the
sparse-poly-arith
branch
from
August 22, 2026 04:10
93e42b4 to
1830102
Compare
kim-em
force-pushed
the
sparse-poly-dense
branch
from
August 22, 2026 04:11
c1f28fb to
ace969a
Compare
kim-em
force-pushed
the
sparse-poly-arith
branch
from
August 22, 2026 04:36
1830102 to
c0582c2
Compare
kim-em
force-pushed
the
sparse-poly-dense
branch
from
August 22, 2026 04:36
ace969a to
563529b
Compare
kim-em
force-pushed
the
sparse-poly-arith
branch
from
August 22, 2026 05:17
c0582c2 to
586ded3
Compare
kim-em
force-pushed
the
sparse-poly-dense
branch
from
August 22, 2026 05:17
563529b to
52b84c3
Compare
kim-em
force-pushed
the
sparse-poly-arith
branch
from
August 23, 2026 12:38
586ded3 to
5dfd8be
Compare
kim-em
force-pushed
the
sparse-poly-dense
branch
from
August 23, 2026 12:38
52b84c3 to
bbe7d12
Compare
kim-em
force-pushed
the
sparse-poly-arith
branch
from
August 23, 2026 13:05
5dfd8be to
589aa37
Compare
kim-em
force-pushed
the
sparse-poly-dense
branch
from
August 23, 2026 13:05
bbe7d12 to
796f7dc
Compare
coeffsOfTerms and termsOfCoeffs workers, toDense, ofDense with the proved array-pass @[csimp] twin, coefficient preservation, both array-level and bundled round trips, homomorphism laws in both directions including toDense_mul via the mulMonomial-fold decomposition, coeff_mul by transport, the degree/leadingCoeff/Monic transport, and the multiplicative ring laws (moved from Arith.lean: their SPEC-prescribed transport proofs need this layer). The library is now sorry-free through milestone 3. Progress: progress/20260822T035252Z_sparse-poly-dense.md Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_014CvkL7tZHMnLN53fXCAjiq
kim-em
force-pushed
the
sparse-poly-dense
branch
from
August 23, 2026 13:28
796f7dc to
5fa8bba
Compare
kim-em
enabled auto-merge (squash)
August 23, 2026 13:29
auto-merge was automatically disabled
August 23, 2026 13:30
Pull request was closed
kim-em
enabled auto-merge (squash)
August 23, 2026 13:31
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 land milestone 3 of the hex-sparse-poly SPEC: the array-level workers
coeffsOfTerms(indexed writes whose last-write-wins behaviour on non-canonical input matches the SPEC's negative-case bullets) andtermsOfCoeffs;toDensethroughDensePoly.ofCoeffsandofDenseas the ordered list-walk specification compiled through a proved@[csimp]array pass;coeff_toDense/coeff_ofDense; both round trips at the array level (each under exactly its necessity hypothesis) and at the bundled level; the homomorphism laws in both directions, withtoDense_mulproved by decomposing the pairwise product into a fold ofmulMonomials and matching it against a fold of dense monomial multiples;coeff_mulby transport; and the degree-boundary transport (degree?_toDense,leadingCoeff_toDense,Monic,monic_toDense). The eight multiplicative ring laws move here fromArith.leanand are proved through the injectivetoDense, atLean.Grind.CommRingwhere the dense side proves them. The library is sorry-free through milestone 3.🤖 Prepared with Claude Code