[tcoratger]

This adds the Lagrange decomposition of a polynomial across a regular cyclic-coset partition, giving the algebra behind reconstructing a STARK quotient from chunk openings.

For positive c, m, a primitive root w of order c * m, and nonzero s, chunk i < c consists of {s * w^(i + c*t) : t < m}. The module proves that the normalized factors select their respective chunks, that the interpolants reconstruct every polynomial of degree strictly below c * m, and that the weighted masks cancel. These are algebraic identities; the PR does not define a protocol or establish zero-knowledge.

chunkWeight is executable field arithmetic, with a theorem identifying it with the polynomial normalization product. The formal-polynomial definitions remain mathematical views, with their Mathlib representation blocker documented.

Acceptance examples cover shifted two-chunk reconstruction, three-chunk masking, the single-chunk case, and failure at the excluded degree boundary. Ordinary executable callers check concrete normalization weights over ZMod 5 and ZMod 13.

References and paper-to-code mappings are recorded in the bibliography and KB: ethSTARK documentation (2021/582), Haböck's FRI summary (2022/1216), and Haböck–Al Kindi (2024/1037, §4.2). The last is specialized from arbitrary disjoint cosets to this regular cyclic partition.

Validation: ./scripts/validate.sh --axioms passed, including the full library and acceptance builds, warning budgets, source-policy checks, runtime checks, and axiom regression gate. No new admissions or native trust constructs; the axiom baseline and generated KB files are unchanged. Citation keys and documentation links were checked directly.

Original contribution generated with Claude Code.

[github-actions]

🤖 PR Summary

A new module ArkLib/Data/Polynomial/CosetChunks.lean formalizes the splitting and recombination of a polynomial over a partition of a coset of a cyclic group into smaller cosets (chunks), targeting STARK proof verification applications. The core contribution is a self-contained set of definitions and proofs (no external dependencies beyond mathlib) establishing the algebraic identities that underpin polynomial decomposition, zero-knowledge masking, and out-of-domain recovery in the STARK setting.

Mathematical Formalization

The file defines the following primary objects and results:

• point: the map (s, w, i, t) -> s * w^(i + c * t) that indexes chunk elements.
• chunkZ: for each chunk i, the vanishing polynomial (X / s_i)^m - 1, where s_i is the first element of the chunk.
• chunkL: the Lagrange-like factor that evaluates to 1 on chunk i and 0 on all other chunks.
• chunkInterp: the interpolating polynomial of degree < m for a chunk.
• chunkWeight: a scalar equal to the product of the evaluation of the other chunks' Z_i polynomials at the start point s_i (nonzero by chunkWeight_ne_zero).
• mask: an auxiliary polynomial used for zero-knowledge masking.

Key theorems:

• eval_chunkZ, eval_chunkZ_point, eval_chunkZ_first, eval_chunkL_point: evaluation properties of the chunk vanishing and Lagrange factors.
• natDegree_chunkZ_le, natDegree_chunkL_le, natDegree_chunkInterp_le: degree bounds for the above polynomials.
• point_injective: the chunk-index map is injective, ensuring the chunks are disjoint.
• chunkWeight_eq_prod_inv_eval: explicit expression for chunkWeight.
• sum_chunkL_mul_chunkInterp: the central decomposition theorem: any polynomial of degree below c*m can be expressed as the sum over chunks of L_i * q_i, where q_i is its chunk interpolant. This is the identity used by a STARK verifier to recover the quotient polynomial at an out-of-domain point from chunk openings.
• chunkL_mul_chunkZ: product factorization relating L_i and Z_i.
• sum_chunkL_mul_masked: the mask-cancellation identity: adding weighted masks to the chunk interpolants leaves the overall sum unchanged when the weights are balanced. This formalizes the reason why zero-knowledge masking of chunks preserves the verifier's ability to check the sum.

All definitions except point and chunkWeight are marked noncomputable, reflecting the abstract polynomial-ring setting. No sorry or admit placeholders appear in this file.

Documentation

Two new reference documentation files have been added:

• docs/kb/papers/EthStark21.md: summary of the ethSTARK paper (eprint 2021/582).
• docs/kb/papers/HK24.md: summary of the chunk-masking construction from eprint 2024/1037, Section 4.2.

Infrastructure / Library

• ArkLib.lean: a single import line ArkLib.Data.Polynomial.CosetChunks has been added, making the new module available to downstream users.

Testing

• ArkLibTest/Data/Polynomial/CosetChunks.lean: a test file exists, but its content could not be summarized (AI generation failed). The file is not analyzed further here.

---

Statistics

Metric	Count
📝 Files Changed	10
✅ Lines Added	554
❌ Lines Removed	0

---

Lean Declarations

✏️ Added: 37 declaration(s)

ArkLib/Data/Polynomial/CosetChunks.lean (20)

• def chunkWeight (s w : K) (c m i : ℕ) : K
• def point (s w : K) (c : ℕ) (i t : ℕ) : K
• noncomputable def chunkInterp (s w : K) (c m : ℕ) (Q : K[X]) (i : ℕ) : K[X]
• noncomputable def chunkL (s w : K) (c m i : ℕ) : K[X]
• noncomputable def chunkZ (s w : K) (m i : ℕ) : K[X]
• noncomputable def mask (s w : K) (c m : ℕ) (t : ℕ → K[X]) (i : ℕ) : K[X]
• theorem chunkL_mul_chunkZ {i : ℕ} (hi : i < c) :
• theorem chunkWeight_eq_prod_inv_eval (i : ℕ) :
• theorem chunkWeight_ne_zero {i : ℕ} (hi : i < c) : chunkWeight s w c m i ≠ 0
• theorem eval_chunkL_point {i i' : ℕ} (hi : i < c) (hi' : i' < c) (t : ℕ) :
• theorem eval_chunkZ (j : ℕ) (x : K) :
• theorem eval_chunkZ_first {i j : ℕ} (hi : i < c) (hj : j < c) :
• theorem eval_chunkZ_point (i j t : ℕ) :
• theorem natDegree_chunkInterp_le (Q : K[X]) {i : ℕ} (hi : i < c) :
• theorem natDegree_chunkL_le {i : ℕ} (hi : i < c) :
• theorem natDegree_chunkZ_le (j : ℕ) : (chunkZ s w m j).natDegree ≤ m
• theorem point_injective {i : ℕ} (hi : i < c) :
• theorem point_lt {i t : ℕ} (hi : i < c) (ht : t < m) : i + c * t < c * m
• theorem sum_chunkL_mul_chunkInterp (Q : K[X]) (hQ : Q.degree < (c * m : ℕ)) :
• theorem sum_chunkL_mul_masked (q t : ℕ → K[X]) :

ArkLibTest/Data/Polynomial/CosetChunks.lean (17)

• example (t : ℕ → (ZMod 13)[X]) : mask (2 : ZMod 13) 4 3 2 t 2 = -(t 0 + t 1)
• example (t : ℕ → (ZMod 5)[X]) : mask (3 : ZMod 5) 2 2 2 t 1 = -t 0
• example : chunkInterp (3 : ZMod 5) (-1) 1 2 (X + 1) 0 = X + 1
• example : chunkL (3 : ZMod 5) 2 2 2 0 * (C 4 * X) +
• example : ∑ i ∈ range 2, chunkL (3 : ZMod 5) 2 2 2 i *
• example :
• example {K : Type*} [Field K] (s w : K) (i : ℕ) : chunkZ s w 0 i = 0
• example {K : Type*} [Field K] (s w : K) (m : ℕ) (t : ℕ → K[X]) :
• example {K : Type*} [Field K] {s w : K} {c m : ℕ}
• private def weightRuntimeChecks : IO Unit
• private lemma interp_degree (i : ℕ) (hi : i < 2) :
• private lemma interp_one : chunkInterp (3 : ZMod 5) 2 2 2 cubic 1 = X + C 2
• private lemma interp_vanisher (i : Fin 2) :
• private lemma interp_zero : chunkInterp (3 : ZMod 5) 2 2 2 cubic 0 = C 4 * X
• private lemma primitive_root_four_zmod_thirteen : IsPrimitiveRoot (4 : ZMod 13) 6
• private lemma primitive_root_two_zmod_five : IsPrimitiveRoot (2 : ZMod 5) 4
• private noncomputable def cubic : (ZMod 5)[X]

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

Lean Quality Signals

• ⚠️ #eval debug command left in code in ArkLibTest/Data/Polynomial/CosetChunks.lean (L160)

---

📋 **Additional Analysis**

Review of pull-request diff against ArkLib contribution guidelines

Documentation

• Several theorems in ArkLib/Data/Polynomial/CosetChunks.lean lack docstrings, violating the requirement that "every definition and major theorem should have a docstring". Notably: eval_chunkZ, chunkWeight_eq_prod_inv_eval, natDegree_chunkZ_le, natDegree_chunkL_le, point_lt, point_injective, eval_chunkZ_point, eval_chunkZ_first, eval_chunkL_point, natDegree_chunkInterp_le, sum_chunkL_mul_chunkInterp, chunkL_mul_chunkZ, chunkWeight_ne_zero, sum_chunkL_mul_masked. All should have /-- ... -/ docstrings to state their purpose and assumptions.

Naming and Formatting

• Some lines exceed 100 characters, e.g. the call to eq_of_degree_sub_lt_of_eval_finset_eq in sum_chunkL_mul_chunkInterp and the simp line in sum_chunkL_mul_masked. These should be wrapped or shortened.
• Otherwise naming follows the Mathlib conventions and variable naming is appropriate for algebraic code.

Module System

• The new file ArkLib/Data/Polynomial/CosetChunks.lean correctly uses the module system: module after copyright, public imports, then the module docstring, then @[expose] public section. This satisfies the requirement for files under ArkLib/.

Computability

• The design distinguishes between noncomputable polynomial views (chunkZ, chunkL, chunkInterp, mask) and a computable scalar weight (chunkWeight). The module docstring explains the rationale, and the test file exercises chunkWeight at runtime, which satisfies the computability guidelines.

Citation Standards

• The module docstring includes a References section with proper citation keys and the BibTeX entries have been added to blueprint/src/references.bib. New knowledge-base pages for EthStark21 and HK24 are provided with statement correspondence and scope. This follows the citation standards.

Test Coverage

• ArkLibTest/Data/Polynomial/CosetChunks.lean includes acceptance examples, degree-boundary cases, a single-chunk check, mask cancellation tests, and a run-time #eval of scalar weights. This provides adequate coverage of the stated properties.

No Other Violations

• No sorry/admit introduced.
• No new axioms or sorryAx debt.
• No forbidden set_option or nolint directives.
• File names, directory structure, and namespace hierarchy are correct.

---

📄 **Per-File Summaries**

• ArkLib.lean: The public import line for ArkLib.Data.Polynomial.CosetChunks has been added, making the definitions from that module available to users of ArkLib. This is a new module in the polynomial library, likely providing functionality related to coset chunking.
• ArkLib/Data/Polynomial/CosetChunks.lean: This new file introduces a formalization of polynomial splitting and recombination over a cyclic-coset partition, targeting STARK proof applications. It defines the fundamental point map, normalized chunk polynomials (chunkZ), Lagrange-like chunk factors (chunkL), chunk interpolants (chunkInterp), scalar chunk weights (chunkWeight), and masks (mask), along with key theorems establishing their evaluation properties (eval_chunkZ, eval_chunkZ_point, eval_chunkZ_first, eval_chunkL_point), degree bounds (natDegree_chunkZ_le, natDegree_chunkL_le, natDegree_chunkInterp_le), the point-injectivity lemma (point_injective), the scalar-weight identity (chunkWeight_eq_prod_inv_eval), the sum decomposition theorem (sum_chunkL_mul_chunkInterp), a product factorization (chunkL_mul_chunkZ), a nonzeroness condition (chunkWeight_ne_zero), and a mask-cancellation identity (sum_chunkL_mul_masked). All definitions except point and chunkWeight are noncomputable, and no sorries or admits are present.
• ArkLibTest/Data/Polynomial/CosetChunks.lean: Summary unavailable — AI generation failed.
• docs/kb/papers/EthStark21.md: Summary unavailable — AI generation failed.
• docs/kb/papers/HK24.md: Summary unavailable — AI generation failed.
• 5 file(s) filtered as noise (lockfiles, generated, or trivial): blueprint/src/references.bib, docs/kb/index.md, docs/kb/papers/FRI1216.md, docs/kb/sources/EthStark21/metadata.yml, docs/kb/sources/HK24/metadata.yml

---

Last updated: 2026-10-24 02:27 UTC.

[github-actions]

Build Timing Report

• PR head: 8215036
• Message: feat(Polynomial): split a polynomial over coset chunks and recombine it
• Ref: stark-coset-chunks
• Measured checkout: 396abde (workflow head 8215036).
• Build cache: restored the main build of 45f0255; Lake rebuilt only modules whose source or imports differ from it.
• Runner: ubuntu24 20261012.334.1, X64, 4 cores.
• Dependency cache: exact hit (Linux-lean-deps-242376a597a93d6e5528b31f4ec941d759eea025ee2e52878c0b2f83dc95e539); manifest 2c4edd1c8e0f.
• Measured on the pinned ubuntu-24.04 runner with /usr/bin/time -p.
• Commands: library build lake build; native build lake build toyproblem-runtime hachi-runtime sumcheck-runtime fri-extractor-runtime lint-style; validation wrapper ./scripts/validate.sh.
• The rows run in order against one tree, so native build and validation wrapper both measure an already-built library: validation wrapper is the cost of the gate itself, not of a cold ./scripts/validate.sh. CI passes it no flags, so --docs, --site and --axioms contribute nothing.

Measurement	Wall (s)	CPU work (s)	Status
Library build	12.86	12.99	ok
Native build	3.48	5.75	ok
Validation wrapper	60.98	74.80	ok

CPU work is user + sys. Wall time depends on which modules this run had to rebuild, so compare it across runs only together with the module section below.

Rebuilt Modules

Rebuilt 3 modules (2 without an earlier time). The 1 with an earlier time took 4s here against 3s when main last built them (+1s (+41.4%)).

Estimated clean-build compile time, summed over all 1288 modules: 5938s before, 5946s after (+8s (+0.1%)).

Per-module times are wall-clock under whatever parallel load the run had, so treat small differences as noise; a large change on one module is the signal.

Showing 3 slowest of 3 rebuilt modules.

Current (s)	Earlier (s)	Delta (s)	Path
4.6	-	-	ArkLib/Data/Polynomial/CosetChunks.lean
4.1	2.9	+1.2	ArkLib.lean
2.7	-	-	ArkLibTest/Data/Polynomial/CosetChunks.lean

[alexanderlhicks]

The chunk selection, strict degree bound, reconstruction, and weighted mask cancellation check out. I applied the requested readiness fixes: executable scalar weights with a polynomial-view agreement theorem; explicit hypotheses and scope; bibliography/KB mappings; and acceptance examples covering shifted two-chunk reconstruction, three chunks, the single-chunk case, and the sharp degree boundary. Ordinary callers also execute the finite-field weight checks.

./scripts/validate.sh --axioms passed, including the full build and test warning budgets, source policy, runtime checks, fixture certification, and axiom regression gate. No new admissions, custom axioms, or native trust; no baseline or generated-KB drift. The documented noncomputable polynomial definitions are mathematical views, and the cancellation theorem is not a protocol or zero-knowledge proof. Ready to merge.