docs: specify Schönhage radix-3 multiplication and operation-count bounds - #9888
Open
kim-em wants to merge 2 commits into
Open
docs: specify Schönhage radix-3 multiplication and operation-count bounds#9888kim-em wants to merge 2 commits into
kim-em wants to merge 2 commits into
Conversation
…ty companion This commit specifies Schönhage's 1977 radix-3 multiplication algorithm across three SPECs: triadic reference semantics, the fixed-length carrier, the proof-carrying schedule, and the generic plan as hex-poly-fast amendments; the packed F_2[x] kernel, the schoolbook/Karatsuba/Schönhage dispatch ladder, and the dense-correspondence refinement ladder as hex-gf2 amendments; and hex-poly-fast-cslib, the first -cslib companion library, holding operation-count bounds in cslib's query-complexity framework with operation-parametric workers, specialization theorems, and proved cost obliviousness. Index, future-work, and design-principles entries updated. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018S4hrFX6e8B8s56182nAp4
…lassification This commit revises the Schönhage SPECs: the operation bounds are stated for the operation-parametric workers only, with the raw @[csimp] runtimes related by output equality and explicitly outside the claims; the schedule gains chooser obligations (bounded padding, two-sided sqrt-N balance for K and L, recursive completeness) and the per-schedule recurrence carries the K*L*k transform term; cost obliviousness is stated for constructor- determined weights; the Schönhage bound fixes its base to the counted Karatsuba worker; the Triadic carrier carries 0 < L and exact-order claims take Nontrivial R; hex-gf2 states the ladder as a planned amendment with milestones, targets DensePoly (ZMod64 2) directly, gives the exact packed twiddle rule, and corrects the oracle attribution (python-flint conforms, NTL remains an informational comparator). SPEC/benchmarking.md and SPEC/testing.md gain the normative complexity_layer classification the companion cites. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018S4hrFX6e8B8s56182nAp4
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 specifies Schönhage's 1977 radix-3 multiplication algorithm for F_2[x] and the project's first proved operation-count bounds, across three SPECs plus supporting doctrine. hex-poly-fast gains triadic reference semantics (the third family beside the cyclic and negacyclic folds), the fixed-length positive
Triadiccarrier, the proof-carryingSchoenhageSchedulewith chooser obligations (bounded padding, two-sided sqrt-N balance for K and L, recursive completeness),schoenhagePlan, and theCoeffOpsoperation-parametric worker convention whoseidOpsinstantiations are the proof-facing definitions. hex-gf2 specifies a planned schoolbook/Karatsuba/Schönhage dispatch ladder behind a proof-backed@[csimp]replacement, Mathlib-free conversions toDensePoly (ZMod64 2), a four-stage refinement proof ending on its own convolution semantics, the exact packed twiddle rule for non-word-aligned L, and ladder milestones with the publication-order constraint. hex-poly-fast-cslib is the first-cslibcompanion, playing the role for complexity that the-mathlibcompanions play for correspondence: it instantiates the workers atFreeM (ArithQuery R)from cslib#401, proves specialization and constructor-weight cost obliviousness, and states a dispatcher-covering Karatsuba bound and the Schönhage recurrence with its K·L·k transform term and clog-form global bound, base fixed to the counted Karatsuba worker. The bounds apply to the workers; the raw@[csimp]runtimes stay related by output equality and are explicitly outside the claims, as are word-level and wall-clock statements. cslib#401's Query modules were verified to build against hex-dev's Mathlib revision and the pin policy records the result. SPEC/benchmarking.md and SPEC/testing.md gain the normativecomplexity_layerclassification, SPEC/design-principles.md extends the external-dependency boundary to cslib, and the index and future-work residuals are updated. Nolibraries.yml, lakefile, or release-manifest changes land with this SPEC-only change.🤖 Prepared with Claude Code