Progress on Walsh-Hadamard Transform#1
Open
porkboi wants to merge 1042 commits into
Open
Conversation
* feat: computable additive NTT * name changes * more name changes * more name change --------- Co-authored-by: Quang Dao <quang.dao@layerzerolabs.org>
* feat: implement SkeletonNodeIndex.path * Clean up TODO comments in SkeletonNodeIndex.path Removed TODO comments regarding ancestor node inclusion. --------- Co-authored-by: Alexander Hicks <25369263+alexanderlhicks@users.noreply.github.com>
Section 6 and 7 of the proximity gap paper
* feat: WHIR [WHIR2024] and Proximity Gap papers [BCIKS20] introduced to references and cited in a standard way. * fix: WHIR2024 to ACFY24 * feat: systematically add reference and standardize the style of citation * fix: clean up some small cases * feat: document in contributing * fix: reverse over-eager deleting * fix: adapt the standards of Arklib and CSlib more precisely * fix: minor fixes to formatting and wording
…rleaved code, code distances, proximity gaps (#265) * feat: proximity gaps in interleaved codes - DG25 * feat: refactor interleaved codes * update: distFromCode'_eq_distFromCode * update: generalizations of rate & dist lemmas for RS code to arbitrary index type * fix: generic symbol index for DG25 * update: refactor probability lemmas * feat: unify distance definitions * feat: AHIV22 refactor and definition updates --------- Co-authored-by: Quang Dao <qvd@andrew.cmu.edu>
…into BF128Ghash
feat: BF128Ghash
* feat: statement of the ring-switching and FRI-Binius protocols * fix: address review comments
Bumps [actions/checkout](https://github.com/actions/checkout) from 5 to 6. - [Release notes](https://github.com/actions/checkout/releases) - [Changelog](https://github.com/actions/checkout/blob/main/CHANGELOG.md) - [Commits](actions/checkout@v5...v6) --- updated-dependencies: - dependency-name: actions/checkout dependency-version: '6' dependency-type: direct:production update-type: version-update:semver-major ... Signed-off-by: dependabot[bot] <support@github.com> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
Bumps [actions/cache](https://github.com/actions/cache) from 4 to 5. - [Release notes](https://github.com/actions/cache/releases) - [Changelog](https://github.com/actions/cache/blob/main/RELEASES.md) - [Commits](actions/cache@v4...v5) --- updated-dependencies: - dependency-name: actions/cache dependency-version: '5' dependency-type: direct:production update-type: version-update:semver-major ... Signed-off-by: dependabot[bot] <support@github.com> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
…ess (#569) `Verifier.knowledgeSoundness` was vacuously satisfiable: the straightline extractor returns `OptionT (OracleComp oSpec) WitIn`, and the knowledge game bound it inside the surrounding `OptionT` execution. In VCV-io semantics, `OptionT` failure contributes to the failure mass of the computation, which `probEvent` excludes (it only measures `some '' {x | p x}`). Hence the always-failing extractor `fun _ _ _ _ _ => failure` drove the game's bad-event probability to exactly 0, discharging knowledge soundness at error 0 for ANY verifier and ANY relations. (Verified by a Lean proof of `verifier.knowledgeSoundness init impl relIn relOut 0` for arbitrary `verifier`, `relIn`, `relOut`, depending only on the standard axioms; reproduced in the PR description.) Fix: run the extractor's `OptionT` layer explicitly (`.run`) and keep the resulting `Option WitIn` in the game's output, changing the bad event to (∀ extractedWitIn ∈ extractedWitIn?, (stmtIn, extractedWitIn) ∉ relIn) ∧ (stmtOut, witOut) ∈ relOut so extractor failure now counts as an adversary win, matching the cryptographic definition (the extractor must succeed whenever the prover convinces the verifier). This keeps `Extractor.Straightline`'s type, the definition's signature, and the error type unchanged, so no downstream statement changes; failures of the protocol execution itself (verifier aborts) remain excluded, consistent with plain soundness. The rbr variant (`rbrKnowledgeSoundness`) uses a pure-function extractor and is unaffected. Also prove the previously-sorried `Verifier.id_knowledgeSoundness` (via `Extractor.Straightline.id`), which both removes a sorry and witnesses that the strengthened definition remains satisfiable; as a result `OracleVerifier.id_knowledgeSoundness` is now sorry-free as well (both depend only on [propext, Classical.choice, Quot.sound]). Blueprint prose for `def:knowledge_soundness` updated to match. Known follow-up (out of scope): `Verifier.StateRestoration.knowledgeSoundness` has the same trap (its extractor's `OracleComp` may fail inside the game). Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
…#565) * docs(lattices): add proof plan for LS short-element invertibility (#549) Replace the vague 'deferred' note in LyubashevskySeiler.lean with a phased decomposition of the Lyubashevsky-Seiler invertibility proof (k=2 splitting case) into provable sub-lemmas: (A) order of q mod 2^(a+1) and the two-factor splitting of X^(2^a)+1, (B) CRT unit criterion, (C) ideal-lattice minimum- distance bound, (D) l2 <= l1^2 norm bridge and assembly. Theorem still sorry. * feat(lattices): prove Phase D norm bridge; switch LS plan to elementary proof Discovered an elementary proof of isUnit_of_l1Norm_le that avoids ideal lattices / canonical embedding entirely: a non-unit forces q | (c_j^2 + c_{n/2+j}^2) for every coefficient pair (via a root of X^n+1, s=zeta^{n/2} with s^2=-1, and the n/2-degree independence of powers of zeta), and the sum equals l2NormSq <= l1Norm^2 <= k^2 < q, forcing c=0. - Prove Rq.l2NormSq_le_l1Norm_sq (Phase D, axiom-clean). - Rewrite the module-docstring plan to the elementary argument with the exact Mathlib lemmas (Int.two_pow_sub_pow', ZMod.exists_sq_eq_neg_one_iff, natDegree_of_dvd_cyclotomic_of_irreducible). Main theorem still sorry (phases A-C to formalize). * feat(lattices): prove Lyubashevsky–Seiler short-element invertibility Discharge the `sorry` in `isUnit_of_l1Norm_le` (LS18 Cor. 1.2 / Hachi Lemma 3): over `powTwoCyclotomic α` (`X^{2^α}+1`) with prime `q ≡ 5 (mod 8)`, a nonzero element of centered `ℓ₁` norm `≤ κ` with `κ² < q` is a unit. Add `NormBounds/LSCore.lean` with the reusable building blocks: - `Rq.equivQuotient` / `Rq.not_isUnit_toQuotientHom_of_not_isUnit` — surjectivity of `toQuotientHom`, giving the ring iso `Rq Φ ≃+* Φ.CyclotomicRing` and unit transfer. - `orderOf_q_mod_two_pow` — lifting-the-exponent (`v₂(q^{2^k}-1) = k+2`) ⇒ the multiplicative order of `q` mod `2^{α+1}` is `2^{α-1}`. - `irreducible_X_pow_sub_C_r` — Phase A: the splitting factor `X^{2^{α-1}} - r` is irreducible over `ZMod q` (factor degree = order, via cyclotomic). - `dvd_sq_add_sq` — Phase C: the abstract coefficient-extraction kernel. In `NormBounds/LyubashevskySeiler.lean`, assemble the core lemma `q_dvd_l2NormSq_of_not_isUnit`: a non-unit's quotient image is non-coprime to `X^{2^α}+1`, so an irreducible factor divides its lift; evaluating at the `AdjoinRoot` and using the degree-`2^{α-1}` power-basis independence yields `q ∣ (c̃_j² + c̃_{n/2+j}²)` per coefficient pair, summing to `q ∣ ‖c‖₂²`. With the elementary `‖c‖₂² ≤ ‖c‖₁² ≤ κ² < q` bridge this forces `c = 0`, a contradiction. Also proves the explicit splitting, the `√-1` existence, the zero-norm characterization, and the `α = 0` field edge case. * fix: cleanup doc comments Remove the proof-plan phase scaffolding (Phase A/B/C/D, "phases A–C", "grouped by phase") from the module and lemma docstrings, replacing the plan with a label-free mathematical overview, and drop the proof-internal enumeration from the maxHeartbeats justification comment. * style(lattices): address review bot naming and formatting feedback Rename LSCore.lean -> LsCore.lean (acronyms treated as words), expand the emult_* lemma names to emultiplicity_*, rename exists_sq_eq_neg_one_of_q5 to exists_sq_eq_neg_one_of_mod_eight_eq_five, switch fun ... => binders to fun ... ↦, and add a ## References section to the LsCore module docstring.
* refactor: migrate prime power-of-two cyclotomic ring into Data/Lattices
Move hachiModulus/HachiRing out of Ajtai/InnerOuter into
CyclotomicRing/PowTwo.lean as primePowTwoModulus/PrimePowTwoRing (neutral,
shared with the §3 extension-field algebra). Ajtai/InnerOuter/Arithmetic
becomes a thin re-export keeping the names + scoped notation, so the
inner-outer correctness/security files are unchanged.
* feat: Galois automorphism layer for power-of-two cyclotomic ring (Hachi §3)
Add CyclotomicRing/Galois/ with the computable Galois automorphisms σ_i and
supporting structure for Hachi §3:
- Automorphism.lean: computable galoisAut (X^k ↦ X^{ki}, reduced), semantic
galoisAutₛ via Mathlib aeval + Ideal.Quotient.lift, soundness bridge, and
the galoisRingHom bundling. Rq.mk_add/mk_sum/galoisAut_zero/galoisAut_add
proven; well-definedness, soundness, map_mul/map_one sorried.
- Group.lean: generators σ_{-1}, σ_{4k+1} (oddness proven), exponent set Hexp;
composition law, σ_1=id, |H|=d/k sorried.
- Trace.lean: traceOver/traceH; additivity proven; fixed-image sorried.
- FixedSubring.lean: R_q^H via RingHom.eqLocus of the two generators
(sorry-free Subring) + membership characterization.
All files compile. Hard algebraic/number-theoretic lemmas are sorried per
scope; easy lemmas proven.
* feat: computable trace variant + discharge tractable Galois sorries
- Trace.lean: add computable traceOverComp/traceHComp (sum at the
CPolynomial level, reduce once) with traceOverComp_eq/traceHComp_eq
proving equivalence to the noncomputable traceOver/traceH.
- Automorphism.lean: prove powTwo_galoisAeval_mem (aeval(X^i) fixes the
modulus ideal for odd i, via X^d+1 ∣ X^{di}+1) and galoisAut_map_one
(σ_i fixes 1), wiring the latter into galoisRingHom.map_one'. Add
helpers powTwoCyclotomic_toPoly, monomial_eq_zero.
- Register new modules in ArkLib.lean; regenerate KB caches.
Remaining sorries (all rated 6+, documented): galoisAut_toQuotient (8,
soundness bridge), galoisRingHom.map_mul' (8), galoisAut_one_eq (6),
galoisAut_comp (8), Hexp_card (8), traceH_mem_fixed (7).
* feat: prove galoisAut_toQuotient soundness bridge + galoisRingHom.map_mul'
Implement the soundness-bridge blueprint as separate lemmas in
Automorphism.lean, making the rated-8 gap tractable by routing through
Ideal.Quotient.mk (reduction becomes invisible) so it collapses to a plain
polynomial identity:
- S0 powTwoCyclotomic_natDegree, S3 coeff_toPoly, S4 natDegree_val_toPoly_lt
- galoisAeval_apply, S2 aeval_X_pow_monomial
- S1 galoisAutₛ_toQuotient, S5 galoisAut_sum_toPoly_eq_aeval
- S6 galoisAut_toQuotient (was sorry, rated 8)
- galoisAut_mul → galoisRingHom.map_mul' (was sorry, rated 8)
Automorphism.lean is now sorry-free. Galois/ sorries: 6 → 4 (remaining:
galoisAut_one_eq, galoisAut_comp, Hexp_card, traceH_mem_fixed).
* feat: prove galoisAut_one_eq and galoisAut_comp via soundness bridge
With galoisAut_toQuotient available, the two semantic-routed group laws are
now provable:
- galoisAut_one_eq (σ_1 = id): aeval X is the identity (was rated 6).
- galoisAut_comp (σ_i∘σ_j=σ_{ij}, odd i,j): transported through the bridge
via new helpers galoisAutₛ_mk and aeval_X_pow_aeval_X_pow (was rated 8).
Added the necessary Odd i/Odd j hypotheses (false for even exponents).
Galois/ sorries: 4 → 2 (only Hexp_card and traceH_mem_fixed remain).
* Galois Automorphism and Ring Subfield
* computable packing map psi + theorem 2 (algebraic core)
* fix kb
* fix build errors
* fix build
* cleanup
* Section 3
* fix build
* fix build again
* update make-pr-ready.md skill
* build fix
…ments (#582) * refactor commitments into ordinary and functional commitments * build? * github build fix * another try * build regenerate * add knowledge base entry and update repo map * add SimpleRO disclaimer
* initial work factoring out binius' sumcheck/ringswitch * move ringswitch * more * minor clean up * generalise sumcheck round polynomial * add sumcheck domain asbtraction * integrate sumcheckdomain * integrate concrete hypercube into binius * prismalinear and booldomain * proofsystem/ringswitch * prismalinear * more prismalinear * prismalinear clean up * clean up * clean up * address pre-existing soundness sorries * Prove ReduceClaim.oracleVerifier_rbrKnowledgeSoundness (close relocated sorry) The oracle-reduction RBR-knowledge-soundness theorem appeared closed but its `oracleKnowledgeStateFunction.toFun_full` carried a `sorry`, so the theorem transitively depended on `sorryAx`. Port the complete non-oracle `knowledgeStateFunction.toFun_full` proof to the oracle case: extract `relOut` membership from the positive-probability hypothesis (the zero-round oracle verifier deterministically returns `(mapStmt stmtIn, mapOStmt … oStmtIn)`), then apply the unchanged `hRel`. The theorem statement, `hRel`, `relIn`, `relOut`, `mapWitInv`, and `toFun` are unchanged. Verified: `#print axioms` on both `oracleKnowledgeStateFunction` and `oracleVerifier_rbrKnowledgeSoundness` → [propext, Classical.choice, Quot.sound] (no sorryAx); full `lake build` green (4104 jobs). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * Add RingSwitchingProfile structure + Binius instance (packing-layer abstraction) Introduce `ProofSystem/RingSwitching/Profile.lean`: a `RingSwitchingProfile B L κ` structure bundling the packing-layer data every ring-switching reduction needs (rank-2^κ basis, pack/trace carrier `A` with embeddings `φ₀,φ₁ : L →+* A`, and the row/column decompositions), plus `binaryTowerProfile`, the Binius instance built from the existing tensor-algebra defs (`A := L ⊗[K] L`, `φ₀ = ·⊗1`, `φ₁ = 1⊗·`). Passed explicitly (a `structure`, not a `class`) since profiles may share `(B,L,κ)`; stated over `CommRing` (not `Field`) so Hachi's `L = R_q` fits. Data-only for now; the eq̃/trace law is added when the protocol code is rewired through the profile. Pre-validated against both instantiations: the field shape fills for Binius (this instance, compiles) and for Hachi (B=R_q^H, L=R_q, A=R_q, φ₀=id, φ₁=σ₋₁, basis=ψ, law=Theorem 2 of ePrint 2026/156) — see GENERIC_RING_SWITCHING_PROFILE_PLAN.md §3. Verified: full lake build green (4104 jobs); #print axioms binaryTowerProfile = [propext, Classical.choice, Quot.sound] (no sorryAx); sorry count unchanged (285); top-level Binius theorems' axiom set unchanged. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * Profile: make binaryTowerProfile reducible; correct decompose docstrings Address findings from the adversarial re-review of 708c0c3: - Mark `binaryTowerProfile` `@[reducible]` so `(binaryTowerProfile …).A` unfolds to `L ⊗[K] L` at reducible transparency when the protocol code is later rewired through the profile, preserving the existing rfl/instance-driven Binius proofs. - Replace the backwards `φ₀/φ₁`-side attribution on `decomposeRows`/`Columns` with accurate operational docstrings, and record that `decomposeColumns` uses the *right* L-module structure (distinct from `algLA` = left action) — so the profile will need to carry that right-side structure + a connecting law before the Step-3 rewire (the data-only structure is necessary but not sufficient for soundness). Build green; #print axioms binaryTowerProfile = [propext, Classical.choice, Quot.sound]. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * make more generic * docs * Generalize structured sumcheck degree errors Derive BinaryBasefold fold errors from protocol composition and expose degree-parametric ring-switching core error maps while preserving the degree-2 aliases. * chore(kb): drop generated KB files from PR (CI guard) docs/kb/_generated/** is auto-regenerated on main by the KB workflow and must not be committed in feature PRs; the CI "Reject generated KB updates" guard rejects any PR that touches it. Restore these 4 files to main's content so the Lean build can actually run. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * fix(Binius): close scope-leaking proof in nonLastBlock{Verifier,Reduction} `nonLastBlockOracleVerifier`/`nonLastBlockOracleReduction` are defined without an explicit return type, so Lean infers it from the body. The generic-ring-switch refactor changed the `pSpec₂` argument of the inner `OracleVerifier/Reduction.append` from a closed inline proof to the let-local `h1`. Since `append`'s result `pSpec` (`pSpec₁ ++ₚ pSpec₂`) is exposed in the def's type, referencing the inner local `h1` leaked it out of scope: the return-type metavariable `?m bIdx` could not be solved, the def failed to elaborate, and its name became unknown at the `seqCompose` use sites (CoreInteractionPhase.lean:375/562). Restore the closed inline proof (exactly main's pre-refactor term) for that `Fin ℓ` index. By proof irrelevance the index ⟨bIdx*ϑ+(ϑ-1), _⟩ is unchanged, so the non-last-block reduction is still (ϑ-1) fold-relay + 1 fold-commit rounds (= `pSpecFullNonLastBlock`); no protocol, theorem, or sorry is changed (the file's 2 pre-existing RBR-soundness sorries are untouched). Module and its 3 downstream consumers (BinaryBasefold/FRIBinius General) build clean. This error was masked until now: the CI KB-guard aborted the build before it ran. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * chore(ci): exclude docs/kb/_generated from docs-integrity link check The docs-integrity check validated every markdown link, including the line-anchored source links in the generated docs/kb/_generated/dedup-report.md. For any PR that moves Lean files, those generated links go stale, yet the KB guard forbids committing a regenerated _generated tree in the PR — making the two checks mutually unsatisfiable for file-moving PRs (this PR relocates the RingSwitching subtree). _generated is machine-owned and refreshed on main, so its internal links are excluded here; staleness self-heals when main regenerates. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * chore(Data): use non-deprecated Finsupp.finsetSum_apply RestrictDegreeVar.lean used the deprecated alias `Finsupp.finset_sum_apply`, tripping the ArkLib/Data non-sorry warning budget in CI. Rename to the current `Finsupp.finsetSum_apply` (the deprecated name is a plain alias for it, so the proofs are unchanged). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…duct (#593) * refactor commitments into ordinary and functional commitments * build? * github build fix * another try * build regenerate * poly eval as mat vec * docstring
* CWSS
* fix distinctness bug
* docs(security): add citations and regenerate generated files for CWSS
Make the coordinate-wise special soundness PR review-ready per CONTRIBUTING.md:
- Replace prose paper references in the CWSS module/declaration docstrings with
citation keys ([FMN24], [NOZ26], [AFK22]) and add a `## References` section.
- Add BibTeX entries for the three papers to blueprint/src/references.bib.
- Scaffold and fill in docs/kb/papers/{FMN24,NOZ26,AFK22}.md and their source
metadata so cited keys have paper pages (kb lint --strict-cited-pages).
- Regenerate references.json, lean-citations.json, declarations.json, the
dedup report, and ArkLib.lean to reflect the new files and citations.
- Fix a double-negative typo in TranscriptTree.lean.
* in the middle of forking
* CWSS with composition
* docs
* cleanup files
* refactor special soundness + generalization lemma SS to CWSS
---------
Co-authored-by: Alexander Hicks <25369263+alexanderlhicks@users.noreply.github.com>
* ci: update PR summary workflow to OpenRouter interface The lean-summary-workflow action is now a single OpenRouter-backed gateway. Update summary.yml inputs: api_key takes the OpenRouter key (secrets.OPENROUTER_KEY), drop the removed `provider` input, use an OpenRouter model slug, rename style_guide_path -> additional_instructions_path, and add contents:read for the action's checkout. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * ci: standardize deployment (inherit default model, add upstream_path/reopened/timeout) Omit `model` so the workflow inherits the action's default (deepseek/deepseek-v4-flash) — the fleet model can then be changed in one place. Also add the `reopened` trigger, a job timeout, and (where applicable) upstream_path for upstream-bound directories. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Bumps [actions/checkout](https://github.com/actions/checkout) from 6 to 7. - [Release notes](https://github.com/actions/checkout/releases) - [Changelog](https://github.com/actions/checkout/blob/main/CHANGELOG.md) - [Commits](actions/checkout@v6...v7) --- updated-dependencies: - dependency-name: actions/checkout dependency-version: '7' dependency-type: direct:production update-type: version-update:semver-major ... Signed-off-by: dependabot[bot] <support@github.com> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
Bumps [actions/cache](https://github.com/actions/cache) from 5 to 6. - [Release notes](https://github.com/actions/cache/releases) - [Changelog](https://github.com/actions/cache/blob/main/RELEASES.md) - [Commits](actions/cache@v5...v6) --- updated-dependencies: - dependency-name: actions/cache dependency-version: '6' dependency-type: direct:production update-type: version-update:semver-major ... Signed-off-by: dependabot[bot] <support@github.com> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
Discharge the two remaining `sorry`s in `ArkLib/Data/Fin/Tuple/TakeDrop.lean`: * `drop_update_of_ge`: `Fin.drop` commutes with `Function.update` for indices at or after the drop point. * `take_drop_addCases'`: `Fin.addCases'` of `take`/`drop` reconstructs the tuple. Both dependent `eqRec`/`dcast` coherence goals are reduced to `_root_.cast` via `eqRec_eq_cast`, merged with `_root_.cast_cast`, and closed by proof irrelevance (`cast_eq`), matching the existing `drop_addCases_right` proof style. Co-authored-by: Alexander Hicks <25369263+alexanderlhicks@users.noreply.github.com>
Discharge the remaining `sorry` for `Fin.happend_assoc` (associativity of the dependent heterogeneous append `happend`), adding two reusable helper lemmas: * `happend_heq_left` / `happend_heq_right`: access into `happend u v j` by value (`HEq (happend u v j) (u/v ⟨...⟩)` for `↑j < m` / `m ≤ ↑j`). They rewrite the whole application rather than the index, avoiding the dependent-motive issues of reindexing inside `happend`. The associativity proof splits on where the index lands (u / v / w): the first two regions reduce by `castAdd`/`natAdd` decomposition + staged `simp`, and the third (`natAdd ∘ natAdd`) goes through the `HEq` helpers. Co-authored-by: Alexander Hicks <25369263+alexanderlhicks@users.noreply.github.com>
Discharge two `sorry`s in `Data/Fin/Sigma.lean`: the functorial-flatten analogues of the already-proven `dflatten_embedSum`. They state that flattening a nested tuple and indexing at `embedSum i j` recovers the `(i, j)` entry, up to the canonical `cast` along `vflatten_embedSum`. Both proofs mirror `dflatten_embedSum`: induct on `m`, case on `i` via `Fin.cases`, reduce with `fflatten_succ`/`fflatten₂_succ` + `fappend_left`/`fappend_right` (resp. `fappend₂_*`), and reconcile the nested casts with `cast_cast`.
Co-authored-by: Alexander Hicks <25369263+alexanderlhicks@users.noreply.github.com>
…s-only pilot) (#620) * ci(review): switch to consolidated lean4repo-utils/review@0.1 (chatops-only pilot) * Refine comments in review.yml for clarity Updated comments and formatting in the AI review step.
Changed concurrency cancel-in-progress setting to false.
* removed unused theorem * move lemmas to Rq
Comment out llm_max_run_tokens and llm_budget_mode settings in review.yml.
* feat(Data/Lattices): prove cInfNorm_psi_le (Hachi §3 Lemma 6) Fill the `cInfNorm_psi_le` sorry in ArkLib/Data/Lattices/CyclotomicRing/Subfield/NormBound.lean: the norm bound `‖ψ(a)‖∞ ≤ 2β` of Hachi [NOZ26, §3, Lemma 6]. Adds 7 supporting lemmas: - conjAut_Xpow_eq_neg, vElt_coeff_full — full coefficient/support of the vElt basis - mk_monomial_mul_Xpow, mk_monomial_coeff_full, Xpow_mul_coeff — monomial shift / coeff - coeff_eq_zero_of_size_le — CPolynomial coeff past size is 0 - fixedSubring_coeff_eq_zero — fixed elements supported on multiples of d/2k lake build green, 0 sorries, lint-clean. * refactor(Data/Lattices): relocate NormBound.lean support lemmas per review Address tobias-rothmann's review on #591: keep NormBound.lean focused on the final cInfNorm_psi_le proof and move general-purpose lemmas to their natural homes. - Basis.lean: conjAut_Xpow_eq_neg, mk_monomial_coeff_full, mk_monomial_mul_Xpow, Xpow_mul_coeff, vElt_coeff_full - Cardinality.lean: fixedSubring_coeff_eq_zero (not Basis.lean as literally requested - it needs fixedBasisMap/card_fixedSubring_eq, which only exist in Cardinality.lean; Basis.lean is upstream of Cardinality.lean in the import graph, so it cannot see them) - ToCompPoly/Univariate/Basic.lean: coeff_eq_zero_of_size_le - Packing.lean: new named index lemmas packExp_lt, packExp_mod_eq, eq_or_eq_of_mod_eq (replacing inline modular arithmetic) NormBound.lean now extracts psi_summand_coeff_eq_zero_of_ne_mod and coeff_psi_abs_le_two_vecCInfNorm; cInfNorm_psi_le is a short 7-line proof: unfold cInfNorm, Finset.sup_le, apply the extracted bound, done. No more maxHeartbeats bump needed. lake build green across all touched files (incl. the Subfield aggregator), 0 sorries, lint-clean. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> --------- Co-authored-by: Claude Sonnet 5 <noreply@anthropic.com> Co-authored-by: Alexander Hicks <25369263+alexanderlhicks@users.noreply.github.com> Co-authored-by: Tobias Rothmann <Tobias.rothmann@outlook.com>
* Introduce blocks as in the WHIR paper * More * Docs * Add block at 1 * Add more helpers for blockIdx * Fix `k` issue and docstring
* chore: start Lean 4.31 migration * chore: adapt ArkLib to VCVio 4.31 APIs * fix: complete Lean 4.31 migration * refactor: tighten v4.31 compatibility fixes * fix: clear Lean 4.31 Data warnings * docs: make pre-push validation explicit * refactor: fix root causes behind v4.31 linter suppressions Replace all 12 `set_option <linter> false` escapes added during the 4.31 migration with fixes of what the linters actually flagged: - JohnsonBound/Lemmas: drop `@[simp]` on `Fis_cover_B` (variable-head LHS; its only use is an explicit `rw`) and the `warning.simp.varHead` suppression. - Prelims: `omit [Nontrivial F]` on `rank_eq_if_det_ne_zero` (implied by its `[IsDomain F]`) instead of `linter.overlappingInstances`. - ProximityGap/Basic: give `δ_ε_multilinearCorrelatedAgreement` a nested section with a single `[CommRing F]` scalar structure. The previous signature carried both the section `[Ring F]` and a local `[CommRing F]` — a genuine instance diamond the new linter caught. - DG25/Basic: delete duplicate local `[Module F A]` / `[CommRing F]` binders already supplied by section variables. - DG25/MainResults: extend the `omit` lists with the genuinely unused `[DecidableEq ι]` / `[DecidableEq κ]` instead of three unused-variable linter suppressions per lemma. - CosetFftDomain/Log: make the two non-terminal `simp`s in `log_right_inverse'` terminal via `show ... by simp` step equations instead of `linter.flexible`. Validated with a full `lake build` (4094 jobs) and `./scripts/validate.sh`. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> --------- Co-authored-by: Alexander Hicks <alexander.hicks@ethereum.org> Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
* delete duplicate lemma * unused variable * move lemma that was common to different files * add new file to Arklib.lean * fix for Lean 4.31
…quivalences for seqCompose (6 sorries removed) (#641) - Transcript.fst / Transcript.snd: uniform cast-based definitions along two new transport lemmas append_Type_castAdd / append_Type_natAdd (no if-split, no Nat subtraction in types; signatures unchanged) - FullTranscript.rtake_append_right: dissolve the eqRec/cast residue via HEq - seqComposeChallengeEquiv.left_inv / seqComposeMessageEquiv.left_inv: rw! (castMode := .all) [Fin.splitSum_embedSum] + rfl Verified: full lake build ArkLib (4048 jobs) green; file now sorry-free. Co-authored-by: Richard Goodman <rgoodman@apoth3osis.io>
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
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
20 participants
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.
in ZKLib/Data/MIPoly/Basic.lean