feat/refactor(Hachi): ring switching subprotocol

[tobias-rothmann]

Ring switching for hachi as a proper subprotocol :)

[github-actions]

🤖 PR Summary

⚠️ PR title does not follow conventional commit format type[(scope)]: subject. Got: feat/refactor(Hachi): ring switching subprotocol

sorry delta: -4 (5 removed, 1 added) — net proof progress

The user provides detailed instructions for writing a high-level PR overview for a Lean 4 formal verification project, along with a PR title, body, and per-file summaries. The assistant must produce a self-contained, objective overview that describes the scope, structure, and relevance of the PR without critiquing code. The assistant must surface any new sorry/admit placeholders, organize under relevant headers, and critically evaluate the PR body against the per-file summaries. The output must be clean Markdown without meta prefaces.

---

Statistics

Metric	Count
📝 Files Changed	54
✅ Lines Added	3250
❌ Lines Removed	4881

---

Lean Declarations

✏️ Removed: 7 declaration(s)

ArkLib/Commitments/Functional/Hachi/RingSwitch/Reduction.lean (5)

• def liftProver (WitIn : Type)
• def liftVerifier :
• noncomputable def evalAt (φF : ZMod q →+* F) (a : F) : Polynomial (ZMod q) →+* F
• noncomputable def rowSum (s : RlinStatement Φ n μ) (z : PolyVec (Rq Φ) μ) (i : Fin n) :
• theorem lift_coordinateWiseSpecialSound

ArkLib/Commitments/Functional/Hachi/ZeroCheck/Constraints.lean (2)

• theorem hAlpha_degreeOf_le (φF : ZMod q →+* F) (b : ℕ) (s : RlinStatement Φ n μ) (a : F)
• theorem hZero_degreeOf_le (φF : ZMod q →+* F) (b : ℕ) (w : LiftedWitness Φ μ n)

✏️ Added: 105 declaration(s)

ArkLib/Commitments/Functional/Hachi/RingSwitch/Reduction.lean (8)

• abbrev LiftCom (W E : Type) (Short : W → Prop)
• abbrev LiftedWitness (Φ : CyclotomicModulus (ZMod q)) (μ n : ℕ)
• def liftCheckAt (φF : ZMod q →+* F) (s : RlinStatement Φ n μ) (a : F)
• example (bound ρBound : ℕ) :
• noncomputable def cyclotomicPresentation : Lift.Presentation (ZMod q) (Rq Φ) where
• theorem cyclotomicPresentation_modulus_natDegree :
• theorem isPresentation_cyclotomic (hd : 0 < Φ.φ.natDegree) :
• theorem vecLInftyNorm_le_of_liftShort (s : RlinStatement Φ n μ) (w : LiftedWitness Φ μ n)

ArkLib/Commitments/Functional/Hachi/RingSwitch/Rlin.lean (23)

• @[simp] theorem flattenBlocks_unflatten {P : Type} {blocks width : Nat}
• @[simp] theorem stack_unstack
• @[simp] theorem unflatten_flattenBlocks {P : Type} {blocks width : Nat}
• @[simp] theorem unstack_stack
• abbrev rlinCT (innerRows innerDigits r : Nat) : Nat
• abbrev rlinCW (messageDigits r : Nat) : Nat
• abbrev rlinCZ (messageDigits zDigits m : Nat) : Nat
• def stack (resp : QuadEvalResponse Φ innerRows (2 ^ m) messageDigits (2 ^ r) innerDigits zDigits) :
• def tensorGMatrix (base : ZMod q) (k digits blocks : Nat)
• def unflatten {P : Type} {blocks width : Nat} (v : ArkLib.Lattices.PolyVec P (blocks * width)) :
• theorem dot_append {m n : ℕ} (u : ArkLib.Lattices.PolyVec P m) (v : ArkLib.Lattices.PolyVec P n)
• theorem dot_matVecMul_transpose {a b : ℕ} (A : ArkLib.Lattices.PolyMatrix P a b)
• theorem dot_neg_left {k : ℕ} (u w : ArkLib.Lattices.PolyVec P k) :
• theorem dot_zero_left {k : ℕ} (w : ArkLib.Lattices.PolyVec P k) :
• theorem forall_fin_add {m n : ℕ} {motive : Fin (m + n) → Prop} :
• theorem funext_fin_add_iff {α : Type*} {m n : ℕ} {f g : Fin (m + n) → α} :
• theorem matVecMul_append_rows {a b c : ℕ} (M₁ : ArkLib.Lattices.PolyMatrix P a c)
• theorem mem_relRlinE_of_relOutE (base : ZMod q) (ω γ : ℕ) (esc : Set E)
• theorem rlin_iff_relOut (base : ZMod q) (ω γ : ℕ)
• theorem rlin_linear_iff (base : ZMod q) (ω γ : ℕ)
• theorem rlin_norm_iff (base : ZMod q) (ω γ : ℕ)
• theorem tensorGMatrix_mulVec (base : ZMod q) (k digits blocks : Nat)
• theorem vecLInftyNorm_append {a b : Nat} (u : ArkLib.Lattices.PolyVec (Rq Φ) a)

ArkLib/Commitments/Functional/Hachi/ZeroCheck/Constraints.lean (5)

• def rangeProduct (b : ℕ) (v : F) : F
• def rowPoint (hn : n ≤ 2 ^ m₁) (i : Fin n) : Fin (2 ^ m₁)
• noncomputable def hAlphaEvals (φF : ZMod q →+* F) (_b : ℕ) (s : RlinStatement Φ n μ) (α : F)
• theorem hAlphaEvals_rowPoint (φF : ZMod q →+* F) (b : ℕ) (s : RlinStatement Φ n μ) (α : F)
• theorem rangeProduct_eq_zero_iff {b : ℕ} {v : F} :

ArkLib/Data/Lattices/CyclotomicRing/QuotientLift.lean (3)

• theorem modulus_dvd_toPoly_add_sub (a b : Rq Φ) :
• theorem modulus_dvd_toPoly_mul_sub (a b : Rq Φ) :
• theorem val_toPoly_injective : Function.Injective (fun a : Rq Φ => a.1.toPoly)

ArkLib/Data/Lattices/CyclotomicRing/Rq.lean (1)

• theorem natDegree_val_toPoly_lt' (hd : 0 < Φ.φ.natDegree) (a : Rq Φ) :

ArkLib/OracleReduction/Security/CoordinateWiseSpecialSoundness/CommittedScalar.lean (10)

• @[simp] theorem responseOpening_inl [Nonempty W] (w : W) :
• abbrev Statement (Stmt TCom Challenge : Type) : Type
• def package [Nonempty W] {ι : Type} {oSpec : OracleSpec ι} {σ : Type}
• def prover {ι : Type} {oSpec : OracleSpec ι} (K : BindingCommitment W E Short)
• def rel (K : BindingCommitment W E Short) (checkAt : Stmt → Challenge → W → Prop) :
• def verifier {ι : Type} {oSpec : OracleSpec ι} (K : BindingCommitment W E Short) :
• noncomputable def buildWitness [Nonempty W] {k : ℕ} (hk : 2 ≤ k)
• noncomputable def responseOpening [Nonempty W] (r : W ⊕ E) : W
• theorem buildWitness_mem [Nonempty W] {k : ℕ} (hk : 2 ≤ k)
• theorem coordinateWiseSpecialSound [Nonempty W] {ι : Type} {oSpec : OracleSpec ι} {σ : Type}

ArkLib/OracleReduction/Security/CoordinateWiseSpecialSoundness/ScalarRound.lean (20)

• @[simp] theorem readChallenges_tree2 (v : Msg)
• @[simp] theorem readPre_tree2 (v : Msg)
• def branchPath (v : Msg)
• def branchTr (v : Msg)
• def chalsAux : {a : Fin 3} → ChallengeTree (pSpecScalar Msg C) arity a → a = (1 : Fin 3) →
• def readChallenges (tree : ChallengeTree (pSpecScalar Msg C) arity 0) :
• def readPre (tree : ChallengeTree (pSpecScalar Msg C) arity 0) :
• def topMsgAux : {a : Fin 3} → ChallengeTree (pSpecScalar Msg C) arity a → a = (0 : Fin 3) →
• def tree2 (v : Msg)
• noncomputable def treeExtractor {StmtIn WitOut WitIn : Type} [Nonempty WitOut] {k : ℕ}
• theorem branch_challenge (v : Msg)
• theorem branch_mem (v : Msg)
• theorem branch_pre (v : Msg)
• theorem branch_relOut_language (init : ProbComp σ)
• theorem chal_shape : {a : Fin 3} → (t : ChallengeTree (pSpecScalar Msg C) arity a) →
• theorem eq_leaf : {a : Fin 3} → (t : ChallengeTree (pSpecScalar Msg C) arity a) →
• theorem injective_of_nodeOk {k : ℕ} {hk : 2 ≤ k}
• theorem scalarStructure_arity {k : ℕ} (hk : 2 ≤ k) :
• theorem tree_shape (tree : ChallengeTree (pSpecScalar Msg C) arity 0) :
• theorem tree_shape_aux : {a : Fin 3} → (t : ChallengeTree (pSpecScalar Msg C) arity a) →

ArkLib/ProofSystem/RingSwitching/Lift/Presentation.lean (15)

• noncomputable def rowSum (M : PolyMatrix S n μ) (z : PolyVec S μ) (i : Fin n) :
• theorem eq_of_modulus_dvd {a b : S} (h : P.modulus ∣ P.rep a - P.rep b) : a = b
• theorem eq_zero_of_modulus_dvd_of_natDegree_lt {p : Polynomial R} (h : P.modulus ∣ p)
• theorem exists_rowSum_eq_of_mulVec_eq {M : PolyMatrix S n μ} {z : PolyVec S μ}
• theorem modulus_dvd_rep_mulVec_sub_rowSum (M : PolyMatrix S n μ) (z : PolyVec S μ)
• theorem modulus_dvd_rep_sum {ι : Type*} (t : Finset ι) (f : ι → S) :
• theorem modulus_dvd_rep_zero : P.modulus ∣ P.rep 0
• theorem mulVec_eq_of_evalAt_rowSum {F : Type*} [Field F] {φF : R →+* F}
• theorem mulVec_eq_of_rowSum_eq {M : PolyMatrix S n μ} {z : PolyVec S μ}
• theorem natDegree_modulus_pos : 0 < P.modulus.natDegree
• theorem natDegree_rowSum_le (M : PolyMatrix S n μ) (z : PolyVec S μ) (i : Fin n) :
• theorem rep_add (a b : S) : P.rep (a + b) = P.rep a + P.rep b
• theorem rep_neg (a : S) : P.rep (-a) = -P.rep a
• theorem rep_sum {ι : Type*} (t : Finset ι) (f : ι → S) :
• theorem rep_zero : P.rep (0 : S) = 0

ArkLib/ProofSystem/RingSwitching/Lift/Reduction.lean (11)

• def checkAt (P : Presentation R S) (φF : R →+* F)
• def package [IsPresentation P] (hφF : Function.Injective φF)
• def prover (WitIn : Type) (computeW : Stmt → WitIn → LiftedWitness R S d μ n) :
• def relLin (getM : Stmt → PolyMatrix S n μ) (getY : Stmt → PolyVec S n)
• def relOut : Set (CommittedScalar.Statement Stmt K.TCom F × LiftedWitness R S d μ n)
• def relOutE :
• def verifier :
• noncomputable def buildWitness [IsPresentation P] (hd : P.modulus.natDegree = d)
• theorem buildWitness_mem [IsPresentation P] (hφF : Function.Injective φF)
• theorem coordinateWiseSpecialSound [IsPresentation P] (hφF : Function.Injective φF)
• theorem recover [IsPresentation P] (hφF : Function.Injective φF)

ArkLib/ProofSystem/RingSwitching/Packing/Prelude.lean (1)

• def eqWeightedCoordSum (c : (Fin κ → Fin 2) → L) (r : Fin κ → L) : L

ArkLib/ProofSystem/RingSwitching/RoundVerifiers.lean (3)

• @[reducible] def pSpecMessage (Msg : Type) : ProtocolSpec 1
• def messageRoundOracleVerifier
• def scalarRoundOracleVerifier

ArkLib/ProofSystem/RingSwitching/Transport/Coeffs.lean (2)

• noncomputable def embedCoeffs (φ : R →+* T) (p : R⦃≤ d⦄[X σ]) : T⦃≤ d⦄[X σ]
• theorem embedCoeffs_eval (φ : R →+* T) (p : R⦃≤ d⦄[X σ]) (x : σ → R) :

ArkLib/ProofSystem/RingSwitching/Transport/Eval.lean (3)

• noncomputable def evalAt {F : Type*} [CommSemiring F] (φF : R →+* F) (a : F) :
• theorem eq_of_evalAt_eq {R : Type*} [CommRing R] {F : Type*} [CommRing F] [IsDomain F]
• theorem evalAt_apply {F : Type*} [CommSemiring F] (φF : R →+* F) (a : F) (p : Polynomial R) :

✏️ Affected: 11 declaration(s) (line number changed)

• noncomputable def liftPackage (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp)) in ArkLib/Commitments/Functional/Hachi/RingSwitch/Reduction.lean moved from L231 to L172
• def relRlin {n μ : ℕ} : in ArkLib/Commitments/Functional/Hachi/RingSwitch/Rlin.lean moved from L79 to L171
• def unstack in ArkLib/Commitments/Functional/Hachi/RingSwitch/Rlin.lean moved from L108 to L236
• noncomputable def rlinPackage (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp)) in ArkLib/Commitments/Functional/Hachi/RingSwitch/Rlin.lean moved from L136 to L467
• noncomputable def rlinStmt (base : ZMod q) (ω γ : ℕ) in ArkLib/Commitments/Functional/Hachi/RingSwitch/Rlin.lean moved from L95 to L275
• noncomputable def hAlpha (φF : ZMod q →+* F) (b : ℕ) (s : RlinStatement Φ n μ) (α : F) in ArkLib/Commitments/Functional/Hachi/ZeroCheck/Constraints.lean moved from L115 to L177
• noncomputable def hZero (φF : ZMod q →+* F) (b : ℕ) (w : LiftedWitness Φ μ n) : in ArkLib/Commitments/Functional/Hachi/ZeroCheck/Constraints.lean moved from L106 to L168
• noncomputable def wTable (φF : ZMod q →+* F) (_b : ℕ) (w : LiftedWitness Φ μ n) : in ArkLib/Commitments/Functional/Hachi/ZeroCheck/Constraints.lean moved from L93 to L117
• noncomputable def wTableMleEval (φF : ZMod q →+* F) (b : ℕ) (w : LiftedWitness Φ μ n) in ArkLib/Commitments/Functional/Hachi/ZeroCheck/Constraints.lean moved from L98 to L124
• theorem natDegree_val_toPoly_lt (α : ℕ) (a : Rq (powTwoCyclotomic (R in ArkLib/Data/Lattices/CyclotomicRing/Rq.lean moved from L298 to L308
• def pSpecFinalSumcheck : ProtocolSpec 1 in ArkLib/ProofSystem/RingSwitching/Packing/Spec.lean moved from L54 to L77

---

sorry Tracking

✅ Removed: 5 `sorry`(s)

ArkLib/Commitments/Functional/Hachi/RingSwitch/Reduction.lean (1)

• theorem lift_coordinateWiseSpecialSound (L226)

ArkLib/Commitments/Functional/Hachi/RingSwitch/Rlin.lean (3)

• def rlinStmt (base : ZMod q) (ω γ : ℕ) (L101)
• def unstack (L111)
• theorem mem_relOutE_of_relRlinE (base : ZMod q) (ω γ : ℕ) (esc : Set E) (L129)

ArkLib/OracleReduction/Security/CoordinateWiseSpecialSoundness/ScalarRound.lean (1)

• theorem coordinateWiseSpecialSound_of_mkWitness_scalar (L102)

❌ Added: 1 `sorry`(s)

ArkLib/Commitments/Functional/Hachi/ZeroCheck/Constraints.lean (1)

• theorem rangeProduct_eq_zero_iff {b : ℕ} {v : F} : (L102)

---

Coverage Notes

• AI file summarization partially analyzed 1 file(s) because their individual diffs exceeded the per-file size budget. Statistics and Lean signal tracking still cover the full PR.

Partially Analyzed Files

• HACHI_GENERIC_RING_SWITCH_PLAN.md (+0/-1079)

* Additional-instructions analysis was skipped because the full diff exceeded the analysis size budget, and partial results would be misleading.

---

📄 **Per-File Summaries**

• ArkLib.lean: Added imports for ArkLib.Data.Lattices.CyclotomicRing.QuotientLift and ArkLib.OracleReduction.Security.CoordinateWiseSpecialSoundness.CommittedScalar. Restructured ArkLib.ProofSystem.RingSwitching imports: the six flat files (BatchingPhase, General, Prelude, Profile, Spec, SumcheckPhase) are replaced by fifteen imports organized under new submodules Basic, Lift (with Presentation and Reduction), Packing (with sub‑files for the previous six), RoundVerifiers, and Transport (with Coeffs and Eval). This reflects a major refactor of the RingSwitching module into a package of sub‑directories and the addition of two new files elsewhere.
• ArkLib/Commitments/Functional/Hachi/Composition.lean: The diff updates ArkLib/Commitments/Functional/Hachi/Composition.lean with four notable changes. First, module-level comments are revised: references to the generic guarded-append composition theorem are simplified by removing the 'B4' label; the explicit pointers to HACHI_RING_SWITCHING_PLAN.md, HACHI_LEMMA10_GAP.md, and HACHI_RECURSION_GAP.md are replaced with inline descriptions; and the 'Sorry inventory' section is rewritten to reflect that rows 1–4 of the table (the R^lin adapter and the HMZ25 lift via Lemma 9, liftPackage.isCWSS, scalar-round engine coordinateWiseSpecialSound_of_mkWitness_scalar, and QuotientLift) are now proven and axiom-clean, removing them from the inventory of sorried per-link math. Second, the function openCore gains three new explicit hypotheses (hρ : b - 1 ≤ ρBound, hcov : (μ₀ + n₀) * (𝓜(q, α)).φ.natDegree ≤ 2 ^ m₀, and hn : n₀ ≤ 2 ^ m₁), and these are threaded into its call to batchPackage. Third, openingChain similarly adds the same three hypotheses (hρ, hcov which now uses (mLow + κ) as the exponent bound, hn), threading them into its call to openCore and storing them for the isCWSS proof; its docstring removes a HACHI_RECURSION_GAP.md reference. Fourth, the theorem hachi_iteration_coordinateWiseSpecialSound adds the same three hypotheses (hρ, hcov, hn) and passes them to openingChain.
• ArkLib/Commitments/Functional/Hachi/Escape.lean: The comments in Escape.lean were updated to remove milestone markers ((sumcheck-track milestone F2.0), (F2.0), and (design decision G1)) from the module docstring and the sorried theorem annotation. No code, definitions, or logical content changed; the file remains a skeleton with the same bridgePackageE definition and sorried HachiLemma8 proof.
• ArkLib/Commitments/Functional/Hachi/Recursion/PartialEval.lean: The file removes '(milestone G2)' from the module docstring and '(design D7)' from two comments, updates a docstring to no longer mention 'design D7', adds IsEmpty and SampleableType instances for pSpecPartialEval (the partial-evaluation protocol spec with no challenge round), and adds a docstring to the partialEvalVerifier definition. The file also removes the reference to 'HACHI_RECURSION_GAP.md' from the module-level documentation. All three defined functions (partialEvalAt, eqWeight, deriveFamily) and the theorem wTableMleEval_split remain sorried (marked sorry), and the CWSS theorem partialEvalE_cwss also remains sorried.
• ArkLib/Commitments/Functional/Hachi/Recursion/TraceHandoff.lean: The diff updates comments and docstrings throughout TraceHandoff.lean to remove milestone markers (e.g., “(milestone G3)”, “(gate G1)”, “(design D6)”, “(Phase G)”) and to simplify the “sorried” annotations from “Sorried (G3)” to just “Sorried”. No definitions, theorems, or proofs are changed; the file continues to contain the same sorried declarations (traceCheck, toNextQuadEvalStatement, handoffProver, and handoff_coordinateWiseSpecialSound).
• ArkLib/Commitments/Functional/Hachi/Recursion/ZBatchBridge.lean: Removes two explicit references to an external gap-analysis note (HACHI_RECURSION_GAP.md) — one in a top-level comment describing the soundness gap in the batching-bridge construction, and another in the docstring of the toHatEvalStatement definition, which remains marked as an open soundness question. Also changes the docstring of hatEval from marking the definition as Sorried (G3-adjacent) to simply Sorried, generalizing the annotation. No definitions, theorems, or signatures are added, removed, or refactored; the file's core content — the hatEval function (still sorry), the HatEvalStatement structure, and the toHatEvalStatement pull-back — is unchanged.
• ArkLib/Commitments/Functional/Hachi/RingSwitch.lean: The diff updates ArkLib/Commitments/Functional/Hachi/RingSwitch.lean, the umbrella file for Hachi's ring-switching lift. The module-level docstring has been significantly rewritten: the explanatory text now clarifies that the Lift instance is the cyclotomic instance of the generic Lift from ProofSystem/RingSwitching/Lift/ (with the packing reduction planned as a separate RingSwitchingProfile instance under ProofSystem/RingSwitching/Packing/), and it adds a new paragraph distinguishing the algebraic meaning of "Lift" (lifting equality modulo Xᵈ + 1 to an exact polynomial equation) versus "Packing" (grouping small-field coefficients into one R_q element). The folder-structure description for RingSwitch/Rlin.lean is updated: previously it mentioned "sorried pieces" for block-matrix assembly/unstacking and block-row equivalence; it now states these are "proven — sorry-free". The description for RingSwitch/Reduction.lean is also updated: it formerly referred to a "sorried" plain-special-sound CWSS theorem lift_coordinateWiseSpecialSound; it now reports that the composable CWSS package liftPackage at k = 2d with certificate liftPackage.isCWSS is "proven, sorry-free and axiom-clean", assembled wholesale from the generic Lift.package, and that the IsPresentation law-discharge lemmas live in Data/Lattices/CyclotomicRing/QuotientLift.lean while Hachi keeps only its norms, statement bound convention, commitment interface, and the norm implication vecLInftyNorm_le_of_liftShort. The diff thus reflects progress from sorried to fully proven declarations in the sibling modules, and adds architectural context about the generic lift and its relationship to the planned packing instance.
• ArkLib/Commitments/Functional/Hachi/RingSwitch/Reduction.lean: The file was rewritten to instantiate the generic Lift framework for Hachi's cyclotomic ring-switching, replacing the previous custom structures (LiftedWitness, LiftCom, LiftStatement, relLift, relLiftE, liftVerifier, liftProver) with abbreviations or definitions that delegate to Lift.LiftedWitness, CoordinateWise.BindingCommitment, CommittedScalar.Statement, and Lift.checkAt/CommittedScalar.rel. A new cyclotomicPresentation and isPresentation_cyclotomic theorem provide the presentation data, and the sorried lift_coordinateWiseSpecialSound theorem is removed; instead, the file supplies the Hachi-specific norm implication vecLInftyNorm_le_of_liftShort and constructs liftPackage using Lift.package (which provides the CWSS certificate). Imports and namespace opens are updated to reflect the new dependencies (ArkLib.Data.Lattices.CyclotomicRing.QuotientLift and ArkLib.ProofSystem.RingSwitching.Lift.Reduction), and an example showing that LiftCom is non-vacuous is added.
• ArkLib/Commitments/Functional/Hachi/RingSwitch/Rlin.lean: This pull request completes the previously skeleton Rlin.lean by replacing sorry placeholders with concrete definitions and proofs, thereby realizing the R^lin adapter (Hachi §4.3 entry). It adds: (1) the block-row equivalence theorem rlin_iff_relOut (and its components rlin_linear_iff for rows c1–c5 and rlin_norm_iff for row c6), which states that an R^lin witness at the assembled statement rlinStmt is equivalent to an Eq. (20)-valid QuadEvalResponse; (2) the previously sorried functions rlinStmt (statement assembly), unstack (witness unstacking), and mem_relOutE_of_relRlinE (the pull-back), plus a new completeness direction mem_relRlinE_of_relOutE; (3) several generic helper theorems (forall_fin_add, funext_fin_add_iff, dot_append, dot_matVecMul_transpose, matVecMul_append_rows, vecLInftyNorm_append), the stack/unstack inverses (stack, unstack, stack_unstack, unstack_stack), the tensorGMatrix definition and its identity tensorGMatrix_mulVec, and the rlinCW/rlinCT/rlinCZ width abbreviations. The type RlinStatement and relation relRlin are updated to use ArkLib.Lattices.PolyMatrix/PolyVec and the definition RlinStatement no longer depends on Φ. The rlinPackage is updated to be noncomputable and to include the new completeness proof.
• ArkLib/Commitments/Functional/Hachi/Sumcheck/FinalEval.lean: This diff makes several documentation and in-code annotation changes to ArkLib/Commitments/Functional/Hachi/Sumcheck/FinalEval.lean, updating references to match the current project state. Specifically, it: (1) removes the placeholder 'milestone F8' from the module header comment and from the finalCheck and relWEvalClaimE docstrings, (2) removes the design-notation reference 'design D6' from the module-level comment, (3) removes the tag 'F5' from a comment describing 'sorried sumcheck polynomials', and (4) adds two instance docstrings clarifying that pSpecFinalEval has no challenge rounds — one stating it has no challenges and one noting each (vacuously) is sampleable. No definitions, signatures, or logic are altered; the diff is purely cosmetic and documentary.
• ArkLib/Commitments/Functional/Hachi/Sumcheck/Rounds.lean: The docstrings and comments in this file were revised to remove internal design and milestone identifiers (e.g., "F7", "D9", "R10", "B4", "R8", "G3") and streamline explanatory text, making the module more readable for external reviewers. No changes were made to the code or sorried status (round_coordinateWiseSpecialSound remains sorried).
• ArkLib/Commitments/Functional/Hachi/ZeroCheck.lean: The diff updates two comments in the file's header documentation: it removes the reference to the external analysis document HACHI_LEMMA10_GAP.md and replaces the type name MvPolynomial with CMlPolynomialEval in the description of the batching bridge (ZeroCheck/Batch.lean). These changes align the documentation with the current codebase, removing an outdated reference and correcting the type name used in the actual implementation.
• ArkLib/Commitments/Functional/Hachi/ZeroCheck/Batch.lean: The diff updates the module-level documentation to describe the batched identities as CMlPolynomialEval instead of MvPolynomial, and revises the proof plan for the sorried theorem mem_relLiftE_of_relBatchedE to explicitly state that relBatched omits liftShort and that H₀ is load-bearing for deriving shortness, referencing lemmas hAlphaEvals_rowPoint and rangeProduct_eq_zero_iff. The theorem's signature gains three new hypotheses (hρ, hcov, hn) necessary for the planned proof, and the batchPackage definition is updated accordingly to require and pass these hypotheses.
• ArkLib/Commitments/Functional/Hachi/ZeroCheck/Constraints.lean: The file was significantly refactored. The constraint polynomials hZero and hAlpha were changed from MvPolynomial to CMlPolynomialEval (multilinear polynomial in eval/Lagrange form), and the corresponding degree‑of lemmas hZero_degreeOf_le and hAlpha_degreeOf_le were removed (multilinearity is now structural). A new definition rangeProduct (the per‑entry range factor polynomial) and a new sorried theorem rangeProduct_eq_zero_iff were added. The table definition wTable now takes a ring homomorphism φF and returns F‑valued results; it was also made noncomputable. Two new definitions rowPoint (encoding a row index into the batching cube) and hAlphaEvals (the per‑row linear‑constraint values) were introduced, together with a new sorried theorem hAlphaEvals_rowPoint that links them to the ring‑switching evaluations. The relation roundRel now includes a liftShort shortness condition. The sum‑of‑sumcheck theorems sum_sumcheckPolyZero and sum_sumcheckPolyAlpha were updated to use CMlPolynomialEval.eval with Vector.ofFn instead of MvPolynomial.eval. All existing sorried definitions (wTable, wTableMleEval, hZero, hAlpha, sumcheckPolyZero, sumcheckPolyAlpha, zcTargetAlpha, hypercubeSum, and the three sum‑theorems) remain sorried, and the new rangeProduct_eq_zero_iff and hAlphaEvals_rowPoint theorems are also sorried. Docstrings were cleaned up to remove milestone markers (e.g. “F5”, “R8”) and references to HACHI_LEMMA10_GAP.md.
• ArkLib/Commitments/Functional/Hachi/ZeroCheck/Reduction.lean: Updated ArkLib/Commitments/Functional/Hachi/ZeroCheck/Reduction.lean to correct the polynomial evaluation predicates in relZeroCheck: replaced MvPolynomial.eval with CMlPolynomialEval.eval against (Vector.ofFn (kroneckerPoint ...)) for both hZero and hAlpha, and added a liftShort precondition to the relation. Added the SampleableType instance for the challenge type pSpecZeroCheck F. Removed the cross-reference to the gap analysis file from the module docstring and the theorem docstring. The proof of zeroCheck_coordinateWiseSpecialSound remains sorried.
• ArkLib/Commitments/Functional/Hachi/hachi-overview.html: Updated hachi-overview.html to reflect that the Ring-Switching Lift (Section 4.3, Lemma 9) and its Rˡⁱⁿ adapter (row 3) are now fully proven and axiom-clean, advancing the 'rows 1–4 sorry-free' status, reducing the open sorries count from approximately 24 to 20, and updating the status source from the hachi-skeleton branch to the tr/ring-switching-subprotocol branch. The corresponding status in the INDEX array for the files RingSwitch/Rlin.lean and RingSwitch/Reduction.lean was changed from wip to proven and their sorries reset to 0.
• ArkLib/Data/Lattices/CyclotomicRing/QuotientLift.lean: This new file supplies the law-discharge lemmas for the cyclotomic quotient presentation Rq Φ needed by the HMZ25 ring-switching lift. It adds val_toPoly_injective (injectivity of the canonical representative map), modulus_dvd_toPoly_add_sub (coset law for addition: Φ.φ.toPoly divides (a+b).1.toPoly - (a.1.toPoly + b.1.toPoly)), and modulus_dvd_toPoly_mul_sub (coset law for multiplication: Φ.φ.toPoly divides (a*b).1.toPoly - a.1.toPoly * b.1.toPoly), each proved via the quotientHom bridge. The remaining degree-reduction law is already in Rq.lean.
• ArkLib/Data/Lattices/CyclotomicRing/Rq.lean: Added a new theorem natDegree_val_toPoly_lt' (signature: (hd : 0 < Φ.φ.natDegree) (a : Rq Φ) → a.1.toPoly.natDegree < Φ.φ.natDegree) that generalizes the existing natDegree_val_toPoly_lt from the power-of-two cyclotomic ring to any modulus Φ with a positive degree hypothesis. The original natDegree_val_toPoly_lt is redefined as a corollary of the new theorem, using powTwoCyclotomic_natDegree to provide the positivity condition; its docstring is updated to reflect this derivation. The proof of natDegree_val_toPoly_lt' uses Φ.degree_toPoly_lt_of_reduced instead of the earlier powTwoCyclotomic-specific lemma.
• ArkLib/OracleReduction/Security/CoordinateWiseSpecialSoundness/CommittedScalar.lean: This file adds CommittedScalar, a new generic module in the CoordinateWiseSpecialSound hierarchy that formalizes a recurring two-round commit-then-challenge protocol shape. It defines the BindingCommitment structure (a deterministic commitment with binding restricted to Short openings, producing an escape element from collisions), the output statement type CommittedScalar.Statement, the anchored relation CommittedScalar.rel, a pure statement-extending verifier CommittedScalar.verifier, and an honest prover shell CommittedScalar.prover. The file also provides extractor logic via CommittedScalar.buildWitness (a three-way assembler that passes through escapes, produces binding escapes from distinct openings, or projects a common opening) with its correctness theorem buildWitness_mem, parameterized by an instance-specific recover hypothesis. Finally, it bundles these components into a generic CWSS theorem coordinateWiseSpecialSound and a CWSSPackage (package), both parameterized by the same recover hypothesis, ready for composition with ▷.
• ArkLib/OracleReduction/Security/CoordinateWiseSpecialSoundness/Escape.lean: The module docstring is edited to remove the parenthetical reference to 'design decision G1 of the sumcheck-track plan'. A new Nonempty instance is added for the sum type A ⊕ E when A is nonempty, using .inl (Classical.arbitrary A), which is intended for the escape‑threaded witness types (Wit ⊕ Escape) used in the file.
• ArkLib/OracleReduction/Security/CoordinateWiseSpecialSoundness/Guarded.lean: The module docstring and several theorem/definition docstrings (IsGuardedWith, IsGuarded.append, append_coordinateWiseSpecialSound_of_guardedLeft, GCWSSPackage.toGuarded, GCWSSPackage.append) were updated to remove explicit references to the Hachi sumcheck track plan and milestone labels (B4, B4.1, B4.3, B4.4), making the file self-contained. A new instance was added: instance (V) [h : V.IsPure] : V.IsGuarded := IsGuarded.of_isPure V h, providing automatic typeclass inference that pure verifiers are guarded. These changes do not alter the logic or introduce new sorry—the pre-existing sorried theorems (IsGuarded.append, append_coordinateWiseSpecialSound_of_guardedLeft) remain unsolved.
• ArkLib/OracleReduction/Security/CoordinateWiseSpecialSoundness/ScalarRound.lean: This change completes the file, which previously contained only a sorried theorem. It adds the full tree-navigation kit (topMsgAux, readPre, chalsAux, readChallenges), the star-tree constructor tree2 and its shape theorem (tree_shape), per-branch transcript definitions (branchPath, branchTr, branch_challenge, branch_pre, branch_mem), the arity equality scalarStructure_arity and collapse of the node predicate to injectivity (injective_of_nodeOk), a pure-acceptance bridge (branch_relOut_language), and a noncomputable generic extractor (treeExtractor) parameterized over witness types. The formerly sorried theorem coordinateWiseSpecialSound_of_mkWitness_scalar is now proved using this infrastructure, removing the sorry. The module docstring is updated to note the new protocols that use the scalar-round pattern (DP24/Binius ring‑switching batching, HMZ25, paired sumcheck) and adds a TODO about deduplicating the tree-navigation code with SingleRound.lean.
• ArkLib/ProofSystem/Binius/FRIBinius/General.lean: Updated the import path for BatchingPhase from ArkLib.ProofSystem.RingSwitching.BatchingPhase to ArkLib.ProofSystem.RingSwitching.Packing.BatchingPhase, reflecting a reorganization of the RingSwitching module into a Packing subdirectory.
• ArkLib/ProofSystem/Binius/FRIBinius/Prelude.lean: The file now imports ArkLib.ProofSystem.RingSwitching.Packing.Prelude instead of ArkLib.ProofSystem.RingSwitching.Prelude, reflecting a refactor that organized ring-switching definitions into a Packing submodule.
• ArkLib/ProofSystem/RingSwitching/Basic.lean: This diff adds the new file ArkLib/ProofSystem/RingSwitching/Basic.lean, which serves as the top-level umbrella module for the RingSwitching/ folder. The file does not introduce any executable Lean code, theorems, definitions, or instances; it consists entirely of a module-level docstring (/-! ... -/) that provides a comprehensive taxonomy of the ring-switching constructions in the project. The docstring defines two main construction families — Packing (small ring B to large ring L, with interactive and planned deterministic relocation) and Lift (quotient ring S ≅ R[X]/(φ) to a field F ⊇ R) — and clarifies the shared infrastructure (RoundVerifiers.lean, Transport/, the committed-scalar seam) that belongs to neither family. It also explicitly states what is not shared (e.g., the two data layers do not unify under a common parent structure). No sorry or admit appears in this diff.
• ArkLib/ProofSystem/RingSwitching/Lift.lean: This diff creates a new module ArkLib/ProofSystem/RingSwitching/Lift.lean that serves as the umbrella documentation and entry point for the ring-switch lifting subdirectory. It outlines the purpose of the Lift family — converting linear claims over a quotient ring S ≅ R[X]/(φ) into lifted R[X] identities with a quotient witness ρ, which are then checked via field evaluation at a single challenge point α. The module documents the folder structure (Presentation.lean for the algebraic layer and Reduction.lean for the protocol layer), instance examples (notably cyclotomic rings), and security model (coordinate-wise special soundness with extractor). No theorems, definitions, sorry, or admit are added; the file contains only documentation and import statements.
• ArkLib/ProofSystem/RingSwitching/Lift/Presentation.lean: This file introduces the Presentation structure and IsPresentation class that abstract a ring S as a quotient R[X]/(φ) with a monic modulus φ and a canonical representative map rep. It proves the exactness layer (rep_zero, rep_add, rep_neg, rep_sum) — derived from the coset laws and the vanishing kernel lemma eq_zero_of_modulus_dvd_of_natDegree_lt. The file defines rowSum for lifted rows and proves the quotient-witness correspondence: mulVec_eq_of_rowSum_eq (descent) and exists_rowSum_eq_of_mulVec_eq (lift with an explicit quotient polynomial of bounded degree). Finally, mulVec_eq_of_evalAt_rowSum provides a per-row recovery engine that uses evaluation at many pairwise-distinct points to descend lifted identities over a field.
• ArkLib/ProofSystem/RingSwitching/Lift/Reduction.lean: This new file defines the two-round Lift reduction protocol. It introduces the LiftedWitness structure (holding the S‑witness z and per‑row quotient polynomials ρ) and the core relations relLin (input linear relation over S), checkAt (polynomial evaluation at a challenge a), and relOut/relOutE (output relations with an escape budget). It provides a verifier and prover built from the committed‑scalar shell, together with the key theorems recover (generic recovery of the input relation from 2d pairwise‑distinct challenges, using the presentation’s interpolation engine), buildWitness and buildWitness_mem (extractor and its correctness), and coordinateWiseSpecialSound (CWSS at plain k = 2d special soundness). Finally, it assembles everything into a composable package of type CWSSPackage. No sorry or admit appear in the code.
• ArkLib/ProofSystem/RingSwitching/Packing.lean: This is the initial creation of ArkLib/ProofSystem/RingSwitching/Packing.lean, a module-level documentation file that introduces the Packing family of ring-switching protocols. It adds a module docstring (/-!) explaining: the problem of relocating an evaluation claim from a small ring B into a large ring L by packing blocks of 2^κ coordinates into single L-elements via packMLE, the separation of packing data (RingSwitchingProfile from Profile.lean) and per-instance relocation logic (interactive for general points, deterministic for subring-valued points), and the folder structure (Profile.lean, Prelude.lean, Spec.lean, BatchingPhase.lean, SumcheckPhase.lean, General.lean). The file also imports ArkLib.ProofSystem.RingSwitching.Packing.Profile and ArkLib.ProofSystem.RingSwitching.Packing.General, and references three planned or existing instantiations (Binius, Hachi §3, and an opposite-direction Lift construction).
• ArkLib/ProofSystem/RingSwitching/Packing/BatchingPhase.lean: The file BatchingPhase.lean was moved into a new Packing/ subdirectory, and its imports were updated to the Packing-scoped versions of Prelude and Spec. The module-level docstring was completely rewritten to describe the phase as the first part of an interactive packing reduction rather than the initial phase of a ring-switching IOP, and now explains the two goals (relocate and batch) and the security rationale. The oracleVerifier was refactored: it is no longer a custom verify implementation but is now defined as an instance of scalarRoundOracleVerifier (from RingSwitching's RoundVerifiers) by providing separate check, accept, and reject functions; the old inline steps 1–5 were replaced by calls to performCheckOriginalEvaluation (in check), compute_s0 (inside accept), and failureState (in reject). A batchingRbrExtractor and associated knowledge-state function, per-challenge knowledge error, completeness/soundness statements, and references to [DP24] were added, with the leaf proofs left as sorry. The input relation batchingInputRelationProp was reformatted but not semantically changed.
• ArkLib/ProofSystem/RingSwitching/Packing/General.lean: The file was renamed from ArkLib/ProofSystem/RingSwitching/General.lean to ArkLib/ProofSystem/RingSwitching/Packing/General.lean and its imports updated accordingly. The module docstring was rewritten to describe the composed interactive packing reduction (batching, relocation sumcheck, downstream opening) with error analysis, and now notes that leaf proofs are left as sorry. Comments on the existing definitions (batchingCoreVerifier, fullOracleVerifier, etc.) were updated to refer to the "DP24 ring-switching protocol" instead of "Binary Basefold protocol". The docstring also adds a reference to the umbrella file ArkLib/ProofSystem/RingSwitching/Basic.lean.
• ArkLib/ProofSystem/RingSwitching/Packing/Prelude.lean: This commit renames the file from ArkLib/ProofSystem/RingSwitching/Prelude.lean to ArkLib/ProofSystem/RingSwitching/Packing/Prelude.lean, updating its module docstring and content focus to define the 'Packing' protocol's algebraic vocabulary. It adds three new definitions: eqWeightedCoordSum, a verifier subroutine computing an eq̃-weighted sum over a 2^κ-indexed coordinate family; compute_A_func, which computes a batched-multiplier function on the cube by decomposing evaluations into basis coordinates; and compute_A_MLE, the multilinear extension of compute_A_func. It replaces the inline implementation of componentWise_embed_MLE with a call to embedCoeffs from the new import ArkLib/ProofSystem/RingSwitching/Transport/Coeffs. The existing definitions performCheckOriginalEvaluation, compute_s0, and compute_final_eq_value are refactored to use eqWeightedCoordSum. The docstrings for TensorAlgebra, φ₁Embed, decompose_tensor_algebra_rows, decompose_tensor_algebra_columns, packMLE, unpackMLE, embedded_MLP_eval, performCheckOriginalEvaluation, compute_A_func, compute_A_MLE, compute_s0, and compute_final_eq_tensor are updated. No sorry or admit are present.
• ArkLib/ProofSystem/RingSwitching/Packing/Profile.lean: Renamed ArkLib/ProofSystem/RingSwitching/Profile.lean to ArkLib/ProofSystem/RingSwitching/Packing/Profile.lean, entirely rewriting the docstring to frame the RingSwitchingProfile structure specifically as the data layer for the Packing ring-switch protocol. The new documentation explicitly names each field (basis, A, φ₀, φ₁, decomposeRows, decomposeColumns) and spells out what they mean; replaces the earlier table of two instantiations with a corrected one that distinguishes Binius (DP24) and Hachi (NOZ26), adds an explicit note that the Lift construction does not instantiate this profile, and includes proper bibliography references. The design-notes discussion of explicit vs. instance-based structure and the CommRing-over-Field constraint is preserved; the remark that the reconstruction laws are a data-layer boundary, not a standalone soundness theorem, is restated more concretely.
• ArkLib/ProofSystem/RingSwitching/Packing/Spec.lean: The file was renamed into the Packing/ subdirectory and its module docstring rewritten to describe the ‘Wire formats of the interactive packing reduction’. pSpecBatching now delegates to CoordinateWise.ScalarRound.pSpecScalar P.A (Fin κ → L) and pSpecFinalSumcheck to pSpecMessage L (both imported from ArkLib.ProofSystem.RingSwitching.RoundVerifiers and ArkLib.OracleReduction.Security.CoordinateWiseSpecialSoundness.ScalarRound), replacing manual ProtocolSpec tuples. The explicit per-index OracleInterface and SampleableType instances for those two specs have been removed, with comments stating that the generic instances from ScalarRound and RoundVerifiers are used instead; the analogous instances for pSpecSumcheckLoop and pSpecCoreInteractionWithDegree remain unchanged.
• ArkLib/ProofSystem/RingSwitching/Packing/SumcheckPhase.lean: The file was renamed from SumcheckPhase.lean to Packing/SumcheckPhase.lean and its imports updated to Packing.Prelude and Packing.Spec. The module-level docstring was completely rewritten to describe this as the second phase of the interactive packing reduction (relocation sumcheck and final consistency step), with explicit protocol steps 6–9 and references to [DP24]. The finalSumcheckVerifier definition was refactored: it is now defined as an instance of messageRoundOracleVerifier (from RingSwitching), replacing the previous manual implementation of the query-and-check logic. The new definition takes explicit check, accept, and reject functions, where the check and acceptance both use compute_final_eq_value multiplied by s', while rejection outputs a dummy statement. The old code comments describing steps 7–9 were removed as they are superseded by the docstring. The docstring explicitly notes that leaf proofs are open (sorry).
• ArkLib/ProofSystem/RingSwitching/RoundVerifiers.lean: This pull request introduces a new file ArkLib/ProofSystem/RingSwitching/RoundVerifiers.lean in the Lean 4 formal verification project. It defines a generic "check-then-update" verifier pattern for two common round structures in the ring-switching proof system: the one-message wire (pSpecMessage) and the message-then-scalar-challenge wire (pSpecScalar from CoordinateWise.ScalarRound). Specifically, it provides two new OracleVerifier definitions: messageRoundOracleVerifier for the one-message round (which performs a deterministic local check and returns either an accept or reject statement update) and scalarRoundOracleVerifier for the scalar-challenge round (which additionally incorporates the challenge into the statement update, with the check-free limit corresponding to CoordinateWise.CommittedScalar.verifier). The file also includes the necessary OracleInterface and SampleableType instances for the new pSpecMessage protocol wire format. No sorry or admit placeholders are present.
• ArkLib/ProofSystem/RingSwitching/Transport.lean: Added ArkLib/ProofSystem/RingSwitching/Transport.lean as a module-documentation file that introduces the ring-switching transport layer. It describes the two submodules Eval.lean (univariate evaluation and interpolation via evalAt and eq_of_evalAt_eq) and Coeffs.lean (multivariate coefficient embedding via embedCoeffs and embedCoeffs_eval), and explains how they support claim transport through ring homomorphisms. The file also notes how Lift and Packing instantiate these components.
• ArkLib/ProofSystem/RingSwitching/Transport/Coeffs.lean: This new file Coeffs.lean defines embedCoeffs, a function that transports a degree-bounded multivariate polynomial over R to one over T by applying a ring homomorphism φ : R →+* T coefficient-wise via MvPolynomial.map, and proves it preserves the degree bound d. It also proves the theorem embedCoeffs_eval, which states that evaluating the transported polynomial at transported arguments equals transporting the original evaluation.
• ArkLib/ProofSystem/RingSwitching/Transport/Eval.lean: This new file Eval.lean adds the transport mechanism for evaluating base-ring polynomials in a target carrier F via a ring homomorphism φF : R →+* F. It defines evalAt φF a : R[X] →+* F as a bundled ring homomorphism using Polynomial.eval₂RingHom, along with the lemma evalAt_apply expressing it as (p.map φF).eval a. The key theorem eq_of_evalAt_eq (the
• ArkLib/ProofSystem/Sumcheck/Structured/SingleRound.lean: The file ArkLib/ProofSystem/Sumcheck/Structured/SingleRound.lean had its module-level docstring updated to reflect a refactoring: the former dependencies RingSwitching.Spec and RingSwitching.SumcheckPhase are now RingSwitching.Packing.Spec and RingSwitching.Packing.SumcheckPhase, respectively. The docstring also clarifies that the ring-switching wrappers specialize Context and OStmtIn back to "the DP24 ring-switching types" instead of the less specific "the ring-switching types." These are purely documentation changes—no code, theorems, definitions, or API signatures were modified.
• HACHI_GENERIC_RING_SWITCH_PLAN.md: This plan (HACHI_GENERIC_RING_SWITCH_PLAN.md) was deleted entirely (1079 lines removed). It was a detailed reconciliation and implementation plan for integrating Hachi's §3.1 packing head into the Generic/ ring-switching layer on the feat/generic-ring-switch branch. The plan spanned seven phases (branch setup, generic layer stage addition, lattice glue, unpack algebra, head reduction with CWSS, guarded composition framework, and chain assembly) and was superseded by the new document HACHI_RING_SWITCHING_PLAN.md. Its removal cleans up the repository's set of planning documents and eliminates an obsolete roadmap that prescribed a specific implementation strategy involving a PackedClaim.lean stage, psiLinearEquiv, unpackPoly, guarded verifier composition, and a GuardedCWSSPackage — all of which are no longer part of the active plan.
• HACHI_LEMMA10_GAP.md: Removed the HACHI_LEMMA10_GAP.md document, which had analyzed a soundness gap in Lemma 10 of the Hachi protocol and proposed multiple repair approaches (including Kronecker-curve challenges and coordinate-zipped sequential CWSS rounds). Its deletion indicates that this analysis is no longer maintained as a separate document, likely because the gap has been addressed elsewhere or the information has been integrated into the formalization plan.
• HACHI_RECURSION_GAP.md: The file HACHI_RECURSION_GAP.md, which contained a detailed analysis of a partial‑evaluation gap in the Hachi protocol and the adopted CWSS‑native repair, has been deleted. This removal eliminates the documentation of the gap, its explicit counterexample, and the planned formalization impact from the repository.
• HACHI_RING_SWITCHING_COMPARISON.md: This file was deleted; it documented design rationale and architectural differences between Hachi's ring-switching protocol and the one formalized as ProofSystem/RingSwitching/. The deletion removes extensive prose (Sections 1–8) that explained why the formalized Packing/ submodule's interactive batching and sumcheck phases are not reusable for Hachi, why Hachi uses a different deterministic trace-check reduction (§3) and a separate sumcheck over a field (§4.3) for a different purpose, and how the codebase has since added a distinct Lift/ submodule (with Presentation.lean, Reduction.lean) to capture Hachi's style of ring switch. The file also documented shared layers (Transport/, RoundVerifiers.lean) and negative design results. Since this is documentation, the deletion removes information that is either outdated (the taxonomy and negative results are now encoded in the folder structure itself and in docstrings within the .lean files) or duplicated in in-repo comments. No theorems, definitions, or APIs are changed; only an explanatory Markdown document is removed.
• HACHI_RING_SWITCHING_PLAN.md: The file HACHI_RING_SWITCHING_PLAN.md was deleted, removing the detailed formalization plan (v2) for the Hachi ring-switching and sumcheck protocols, including milestones, design decisions, and acceptance criteria. This change eliminates the document that served as the roadmap for the proof project, likely indicating that the plan has been superseded, integrated elsewhere, or is no longer needed.
• HACHI_SUMCHECK_TRACK_PLAN.md: The file HACHI_SUMCHECK_TRACK_PLAN.md was deleted from the repository. This document contained a sequential, implementation-ready plan for completing the first four milestones (B4, F2, F3, F4) of the sumcheck track within the HACHI project. It provided detailed specifications for adding guarded composition for the CWSSPackage, creating the R^lin adapter via a Set.withEscape design, formalizing the quotient-lift algebra in QuotientLift.lean, and implementing the HMZ25 lift. The plan also outlined broader context, including its relationship to the existing codebase, dependencies, and acceptance criteria for each milestone.
• blueprint/src/references.bib: Two new BibTeX entries were added to the bibliography: @misc{HMZ25} (Huang, Mao, and Zhang, "Sublinear Proofs over Polynomial Rings", ePrint 2025/199) and @misc{NOZ26} (Nguyen, O'Rourke, and Zhang, "Hachi: Efficient Lattice-Based Multilinear Polynomial Commitments over Extension Fields", ePrint 2026/156). These are cryptology ePrint papers that will be cited in the blueprint.
• docs/kb/concepts/ring-switching.md: The documentation page for ring switching has been substantially reorganized and expanded. It now clearly distinguishes two construction families in ArkLib — Packing/ (small→large, based on RingSwitchingProfile) and Lift/ (large quotient ring→field, based on Presentation/IsPresentation) — and adds a dedicated section "The three constructions" detailing the DP24 packing switch, the planned Hachi §3 packing head, and the HMZ25 Lift construction, each with their algebraic direction, profile, determinism, and soundness notes. The soundness cost formula is corrected from O(1/|L|) to O(ℓ/|L|) (with O(1/|L|) per challenge). The abstraction section is updated to clarify that it formalizes only the packing data layer, not the whole protocol, and the protocol description now references per-construction subdirectories. File paths in "Main ArkLib Touchpoints" are revised to point to the new umbrella Basic.lean, shared RoundVerifiers.lean and Transport.lean, and the per-construction files. The "Notes" section now explicitly states that DP24 leaf completeness/soundness proofs are open (sorry) and adds a note on soundness reuse limitations for non-domain rings.
• docs/kb/papers/DP24.md: The DP24.md documentation page was updated to reflect a reorganization of the ring-switching code in the ArkLib subtree. The related_modules list and the Main ArkLib Touchpoints section now point to Packing/Profile.lean and Packing/General.lean (previously RingSwitching/Profile.lean and RingSwitching/General.lean). The prose description was revised to state that the ring-switching reduction is now housed under ProofSystem/RingSwitching/Packing/, parameterized over the RingSwitchingProfile abstraction from Packing/Profile.lean, and a reference to the taxonomy umbrella file ProofSystem/RingSwitching/Basic.lean was added.
• docs/kb/papers/HMZ25.md: Added a new documentation page docs/kb/papers/HMZ25.md summarizing the paper 'Sublinear Proofs over Polynomial Rings' by Huang, Mao, and Zhang. The page explains the paper's core contribution—a ring-switching lift that turns quotient-ring linear relations into polynomial identities over Z_q[X], then evaluates them at a random point in an extension field for sumcheck—and documents how ArkLib formalizes this: the generic quotient-witness correspondence in ArkLib/Data/Lattices/CyclotomicRing/QuotientLift.lean; the two-round subprotocol with k = 2d special soundness generically in ArkLib/ProofSystem/RingSwitching/Lift/ over any monic-modulus presentation; and the Hachi-specific instance, norms, local predicate, interpolation recovery, liftPackage, and lift_coordinateWiseSpecialSound in ArkLib/Commitments/Functional/Hachi/RingSwitch/Reduction.lean. It also lists known divergences from the paper (e.g., ArkLib never sends the lifted witness in the clear, uses norm-conditioned weak binding instead of plain binding, defers digit encoding to Hachi's constraint layer, and generalizes modulus to arbitrary monic cyclotomic Φ.φ and the extension field to an abstract embedding).
• docs/kb/papers/NOZ26.md: This update documents the formalization of the cyclotomic-ring → extension-field lift (Lemma 9) from §4.3 of NOZ26, which is now sorry-free and axiom-clean as liftPackage / lift_coordinateWiseSpecialSound in Hachi/RingSwitch/Reduction.lean, the cyclotomic instance of the generic Lift construction over the committed-scalar shell, with law-discharge lemmas in CyclotomicRing/QuotientLift.lean, consumed at row 4 of the Hachi opening chain in Hachi/Composition.lean. The path to the ring-switching profile is updated from RingSwitching/Profile.lean to RingSwitching/Packing/Profile.lean. The open gaps are refined: the packing-head profile for §3 remains to be done, while the Lemma 9 lift (rows 1–4 of the opening chain) is marked complete; Lemmas 10–11 and recursion adapters are noted as skeletons in Composition.lean; the previous 'sumcheck / ring-switching evaluation' gap is removed.
• docs/kb/sources/HMZ25/metadata.yml: Added a new metadata file for the HMZ25 source (bibkey HMZ25) in docs/kb/sources/HMZ25/metadata.yml. It records the source as bibliography-only, provides its canonical URL (https://eprint.iacr.org/2025/199), and notes that it was scaffolded from references.bib for the paper "Sublinear Proofs over Polynomial Rings."
• docs/skills/prove-milestone.md: The documentation at docs/skills/prove-milestone.md has been updated with several notable changes. A new scope-conflict resolution rule was added before Stage 1 design work, requiring explicit surfacing and recording of conflicts between a user's approach and the repo's verified design notes. Two global invariants were refined: invariant 6 now clarifies that Classical.choice arriving through Mathlib or unmodified generic combinators (e.g., ReduceClaim.verifier_coordinateWiseSpecialSound) is acceptable and need not be eliminated, with results called "axiom-clean against the baseline" rather than "axiom-free"; and invariant 7 implicitly references the new baseline. A Hachi-specific attack was added for escape-threaded links, noting that treeSpecialSound is an ∃-extractor statement and requiring the buildWitness/liftBuildWitness pattern to be public, named, and cited. The build/tooling guidance in the Stage 2 section was expanded with three Hachi mechanics: running lake build <module> before lake env lean, checking long lines with lake env lean -Dlinter.style.longLine=true, and silencing unusedSectionVars with omit placed before the docstring (with a warning that the lint does not fire on sorry-bodied declarations). Stage 3 now allows transcribing verbatim verified bodies from spike files one file at a time, and its axiom check (step 6) now explicitly requires the axiom set to stay within invariant 6's baseline. The clean-room review and finalization steps were updated to match the baseline language, and the citation workflow was extended to require completing blueprint/src/references.bib entries and docs/kb/papers/ pages per docs/wiki/blueprint-and-citations.md, with regeneration via ./scripts/update-lib.sh after git add-ing new files.
• docs/wiki/repo-map.md: Updated the RingSwitch/ entry to note that RingSwitch/Reduction is now the proven cyclotomic instance of the generic Lift switch (Lemma 9 CWSS proven), and clarified that the §3 packing reduction lives under ProofSystem/RingSwitching/Packing/ (distinct, no committed-scalar seam). Corrected the ZeroCheck/ Lemma 10 reference from HACHI_LEMMA10_GAP.md to [NOZ26] Lemma 10. Replaced the `HACHI_RECURSION_GAP.md

---

Last updated: 2026-07-24 10:58 UTC.

[github-actions]

Build Timing Report

• Commit: 215b886
• Message: feat/refactor(Hachi): ring switching subprotocol
• Ref: tr/ring-switching-subprotocol
• Comparison baseline: 1c73b9a from the previous successful PR update.
• Measured on ubuntu-latest with /usr/bin/time -p.
• Commands: clean build rm -rf .lake/build && lake build; warm rebuild lake build; validation wrapper ./scripts/validate.sh.

Measurement	Baseline (s)	Current (s)	Delta (s)	Status
Clean build	1379.21	1395.96	+16.75	ok
Warm rebuild	2.60	2.38	-0.22	ok
Validation wrapper	2.86	2.75	-0.11	ok

Incremental Rebuild Signal

• Warm rebuild saved 1393.58s vs clean (586.54x faster).

This compares a clean project build against an incremental rebuild in the same CI job; it is a lightweight variability signal, not a full cross-run benchmark.

Slowest Current Clean-Build Files

Showing 20 slowest current targets, with comparison against the selected baseline when available.

Current (s)	Baseline (s)	Delta (s)	Path
68.00	66.00	+2.00	ArkLib/Data/CodingTheory/ProximityGap/DG25/MainResults.lean
64.00	63.00	+1.00	ArkLib/ProofSystem/Stir/Combine.lean
61.00	64.00	-3.00	ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean
59.00	58.00	+1.00	ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/AffineSpaces.lean
57.00	55.00	+2.00	ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/AffineLines/BWMatrix.lean
51.00	56.00	-5.00	ArkLib/Data/CodingTheory/JohnsonBound/Lemmas.lean
47.00	47.00	+0.00	ArkLib/Data/CodingTheory/ProximityGap/AHIV22.lean
40.00	38.00	+2.00	ArkLib/Data/CodingTheory/BerlekampWelch/Condition.lean
40.00	42.00	-2.00	ArkLib/Data/CodingTheory/ProximityGap/Folding.lean
39.00	29.00	+10.00	ArkLib/OracleReduction/Security/RoundByRound.lean
38.00	38.00	+0.00	ArkLib/OracleReduction/LiftContext/Reduction.lean
37.00	28.00	+9.00	ArkLib/Commitments/Functional/KZG/FunctionBinding/EvaluationBindingConflict.lean
36.00	38.00	-2.00	ArkLib/Data/CodingTheory/JohnsonBound/Basic.lean
33.00	33.00	+0.00	ArkLib/Data/CodingTheory/DivergenceOfSets.lean
29.00	19.00	+10.00	ArkLib/Commitments/Functional/KZG/FunctionBinding/DegreeConflict.lean
29.00	28.00	+1.00	ArkLib/ProofSystem/Sumcheck/Spec/SingleRound.lean
28.00	24.00	+4.00	ArkLib/ToCompPoly/Univariate/Basic.lean
26.00	19.00	+7.00	ArkLib/Data/Domain/CosetFftDomain/Subdomain.lean
24.00	24.00	+0.00	ArkLib/Data/Polynomial/FoldingPolynomial.lean
23.00	19.00	+4.00	ArkLib/Data/CodingTheory/ReedSolomon.lean

[alexanderlhicks]

🤖 AI-generated review (Claude Code). These comments were produced by an AI assistant reviewing this PR against the Hachi paper (NOZ26, ePrint 2026/156) and ArkLib conventions; claims were spot-checked in a built worktree but please verify before acting.

[github-actions]

🤖 PR Summary

⚠️ PR title does not follow conventional commit format type[(scope)]: subject. Got: feat/refactor(Hachi): ring switching subprotocol

sorry delta: -4 (5 removed, 1 added) — net proof progress

Failed to generate AI summary. Please check the per-file summaries and statistics below.

---

Statistics

Metric	Count
📝 Files Changed	54
✅ Lines Added	3250
❌ Lines Removed	4881

---

Lean Declarations

✏️ Removed: 7 declaration(s)

ArkLib/Commitments/Functional/Hachi/RingSwitch/Reduction.lean (5)

• def liftProver (WitIn : Type)
• def liftVerifier :
• noncomputable def evalAt (φF : ZMod q →+* F) (a : F) : Polynomial (ZMod q) →+* F
• noncomputable def rowSum (s : RlinStatement Φ n μ) (z : PolyVec (Rq Φ) μ) (i : Fin n) :
• theorem lift_coordinateWiseSpecialSound

ArkLib/Commitments/Functional/Hachi/ZeroCheck/Constraints.lean (2)

• theorem hAlpha_degreeOf_le (φF : ZMod q →+* F) (b : ℕ) (s : RlinStatement Φ n μ) (a : F)
• theorem hZero_degreeOf_le (φF : ZMod q →+* F) (b : ℕ) (w : LiftedWitness Φ μ n)

✏️ Added: 105 declaration(s)

ArkLib/Commitments/Functional/Hachi/RingSwitch/Reduction.lean (8)

• abbrev LiftCom (W E : Type) (Short : W → Prop)
• abbrev LiftedWitness (Φ : CyclotomicModulus (ZMod q)) (μ n : ℕ)
• def liftCheckAt (φF : ZMod q →+* F) (s : RlinStatement Φ n μ) (a : F)
• example (bound ρBound : ℕ) :
• noncomputable def cyclotomicPresentation : Lift.Presentation (ZMod q) (Rq Φ) where
• theorem cyclotomicPresentation_modulus_natDegree :
• theorem isPresentation_cyclotomic (hd : 0 < Φ.φ.natDegree) :
• theorem vecLInftyNorm_le_of_liftShort (s : RlinStatement Φ n μ) (w : LiftedWitness Φ μ n)

ArkLib/Commitments/Functional/Hachi/RingSwitch/Rlin.lean (23)

• @[simp] theorem flattenBlocks_unflatten {P : Type} {blocks width : Nat}
• @[simp] theorem stack_unstack
• @[simp] theorem unflatten_flattenBlocks {P : Type} {blocks width : Nat}
• @[simp] theorem unstack_stack
• abbrev rlinCT (innerRows innerDigits r : Nat) : Nat
• abbrev rlinCW (messageDigits r : Nat) : Nat
• abbrev rlinCZ (messageDigits zDigits m : Nat) : Nat
• def stack (resp : QuadEvalResponse Φ innerRows (2 ^ m) messageDigits (2 ^ r) innerDigits zDigits) :
• def tensorGMatrix (base : ZMod q) (k digits blocks : Nat)
• def unflatten {P : Type} {blocks width : Nat} (v : ArkLib.Lattices.PolyVec P (blocks * width)) :
• theorem dot_append {m n : ℕ} (u : ArkLib.Lattices.PolyVec P m) (v : ArkLib.Lattices.PolyVec P n)
• theorem dot_matVecMul_transpose {a b : ℕ} (A : ArkLib.Lattices.PolyMatrix P a b)
• theorem dot_neg_left {k : ℕ} (u w : ArkLib.Lattices.PolyVec P k) :
• theorem dot_zero_left {k : ℕ} (w : ArkLib.Lattices.PolyVec P k) :
• theorem forall_fin_add {m n : ℕ} {motive : Fin (m + n) → Prop} :
• theorem funext_fin_add_iff {α : Type*} {m n : ℕ} {f g : Fin (m + n) → α} :
• theorem matVecMul_append_rows {a b c : ℕ} (M₁ : ArkLib.Lattices.PolyMatrix P a c)
• theorem mem_relRlinE_of_relOutE (base : ZMod q) (ω γ : ℕ) (esc : Set E)
• theorem rlin_iff_relOut (base : ZMod q) (ω γ : ℕ)
• theorem rlin_linear_iff (base : ZMod q) (ω γ : ℕ)
• theorem rlin_norm_iff (base : ZMod q) (ω γ : ℕ)
• theorem tensorGMatrix_mulVec (base : ZMod q) (k digits blocks : Nat)
• theorem vecLInftyNorm_append {a b : Nat} (u : ArkLib.Lattices.PolyVec (Rq Φ) a)

ArkLib/Commitments/Functional/Hachi/ZeroCheck/Constraints.lean (5)

• def rangeProduct (b : ℕ) (v : F) : F
• def rowPoint (hn : n ≤ 2 ^ m₁) (i : Fin n) : Fin (2 ^ m₁)
• noncomputable def hAlphaEvals (φF : ZMod q →+* F) (_b : ℕ) (s : RlinStatement Φ n μ) (α : F)
• theorem hAlphaEvals_rowPoint (φF : ZMod q →+* F) (b : ℕ) (s : RlinStatement Φ n μ) (α : F)
• theorem rangeProduct_eq_zero_iff {b : ℕ} {v : F} :

ArkLib/Data/Lattices/CyclotomicRing/QuotientLift.lean (3)

• theorem modulus_dvd_toPoly_add_sub (a b : Rq Φ) :
• theorem modulus_dvd_toPoly_mul_sub (a b : Rq Φ) :
• theorem val_toPoly_injective : Function.Injective (fun a : Rq Φ => a.1.toPoly)

ArkLib/Data/Lattices/CyclotomicRing/Rq.lean (1)

• theorem natDegree_val_toPoly_lt' (hd : 0 < Φ.φ.natDegree) (a : Rq Φ) :

ArkLib/OracleReduction/Security/CoordinateWiseSpecialSoundness/CommittedScalar.lean (10)

• @[simp] theorem responseOpening_inl [Nonempty W] (w : W) :
• abbrev Statement (Stmt TCom Challenge : Type) : Type
• def package [Nonempty W] {ι : Type} {oSpec : OracleSpec ι} {σ : Type}
• def prover {ι : Type} {oSpec : OracleSpec ι} (K : BindingCommitment W E Short)
• def rel (K : BindingCommitment W E Short) (checkAt : Stmt → Challenge → W → Prop) :
• def verifier {ι : Type} {oSpec : OracleSpec ι} (K : BindingCommitment W E Short) :
• noncomputable def buildWitness [Nonempty W] {k : ℕ} (hk : 2 ≤ k)
• noncomputable def responseOpening [Nonempty W] (r : W ⊕ E) : W
• theorem buildWitness_mem [Nonempty W] {k : ℕ} (hk : 2 ≤ k)
• theorem coordinateWiseSpecialSound [Nonempty W] {ι : Type} {oSpec : OracleSpec ι} {σ : Type}

ArkLib/OracleReduction/Security/CoordinateWiseSpecialSoundness/ScalarRound.lean (20)

• @[simp] theorem readChallenges_tree2 (v : Msg)
• @[simp] theorem readPre_tree2 (v : Msg)
• def branchPath (v : Msg)
• def branchTr (v : Msg)
• def chalsAux : {a : Fin 3} → ChallengeTree (pSpecScalar Msg C) arity a → a = (1 : Fin 3) →
• def readChallenges (tree : ChallengeTree (pSpecScalar Msg C) arity 0) :
• def readPre (tree : ChallengeTree (pSpecScalar Msg C) arity 0) :
• def topMsgAux : {a : Fin 3} → ChallengeTree (pSpecScalar Msg C) arity a → a = (0 : Fin 3) →
• def tree2 (v : Msg)
• noncomputable def treeExtractor {StmtIn WitOut WitIn : Type} [Nonempty WitOut] {k : ℕ}
• theorem branch_challenge (v : Msg)
• theorem branch_mem (v : Msg)
• theorem branch_pre (v : Msg)
• theorem branch_relOut_language (init : ProbComp σ)
• theorem chal_shape : {a : Fin 3} → (t : ChallengeTree (pSpecScalar Msg C) arity a) →
• theorem eq_leaf : {a : Fin 3} → (t : ChallengeTree (pSpecScalar Msg C) arity a) →
• theorem injective_of_nodeOk {k : ℕ} {hk : 2 ≤ k}
• theorem scalarStructure_arity {k : ℕ} (hk : 2 ≤ k) :
• theorem tree_shape (tree : ChallengeTree (pSpecScalar Msg C) arity 0) :
• theorem tree_shape_aux : {a : Fin 3} → (t : ChallengeTree (pSpecScalar Msg C) arity a) →

ArkLib/ProofSystem/RingSwitching/Lift/Presentation.lean (15)

• noncomputable def rowSum (M : PolyMatrix S n μ) (z : PolyVec S μ) (i : Fin n) :
• theorem eq_of_modulus_dvd {a b : S} (h : P.modulus ∣ P.rep a - P.rep b) : a = b
• theorem eq_zero_of_modulus_dvd_of_natDegree_lt {p : Polynomial R} (h : P.modulus ∣ p)
• theorem exists_rowSum_eq_of_mulVec_eq {M : PolyMatrix S n μ} {z : PolyVec S μ}
• theorem modulus_dvd_rep_mulVec_sub_rowSum (M : PolyMatrix S n μ) (z : PolyVec S μ)
• theorem modulus_dvd_rep_sum {ι : Type*} (t : Finset ι) (f : ι → S) :
• theorem modulus_dvd_rep_zero : P.modulus ∣ P.rep 0
• theorem mulVec_eq_of_evalAt_rowSum {F : Type*} [Field F] {φF : R →+* F}
• theorem mulVec_eq_of_rowSum_eq {M : PolyMatrix S n μ} {z : PolyVec S μ}
• theorem natDegree_modulus_pos : 0 < P.modulus.natDegree
• theorem natDegree_rowSum_le (M : PolyMatrix S n μ) (z : PolyVec S μ) (i : Fin n) :
• theorem rep_add (a b : S) : P.rep (a + b) = P.rep a + P.rep b
• theorem rep_neg (a : S) : P.rep (-a) = -P.rep a
• theorem rep_sum {ι : Type*} (t : Finset ι) (f : ι → S) :
• theorem rep_zero : P.rep (0 : S) = 0

ArkLib/ProofSystem/RingSwitching/Lift/Reduction.lean (11)

• def checkAt (P : Presentation R S) (φF : R →+* F)
• def package [IsPresentation P] (hφF : Function.Injective φF)
• def prover (WitIn : Type) (computeW : Stmt → WitIn → LiftedWitness R S d μ n) :
• def relLin (getM : Stmt → PolyMatrix S n μ) (getY : Stmt → PolyVec S n)
• def relOut : Set (CommittedScalar.Statement Stmt K.TCom F × LiftedWitness R S d μ n)
• def relOutE :
• def verifier :
• noncomputable def buildWitness [IsPresentation P] (hd : P.modulus.natDegree = d)
• theorem buildWitness_mem [IsPresentation P] (hφF : Function.Injective φF)
• theorem coordinateWiseSpecialSound [IsPresentation P] (hφF : Function.Injective φF)
• theorem recover [IsPresentation P] (hφF : Function.Injective φF)

ArkLib/ProofSystem/RingSwitching/Packing/Prelude.lean (1)

• def eqWeightedCoordSum (c : (Fin κ → Fin 2) → L) (r : Fin κ → L) : L

ArkLib/ProofSystem/RingSwitching/RoundVerifiers.lean (3)

• @[reducible] def pSpecMessage (Msg : Type) : ProtocolSpec 1
• def messageRoundOracleVerifier
• def scalarRoundOracleVerifier

ArkLib/ProofSystem/RingSwitching/Transport/Coeffs.lean (2)

• noncomputable def embedCoeffs (φ : R →+* T) (p : R⦃≤ d⦄[X σ]) : T⦃≤ d⦄[X σ]
• theorem embedCoeffs_eval (φ : R →+* T) (p : R⦃≤ d⦄[X σ]) (x : σ → R) :

ArkLib/ProofSystem/RingSwitching/Transport/Eval.lean (3)

• noncomputable def evalAt {F : Type*} [CommSemiring F] (φF : R →+* F) (a : F) :
• theorem eq_of_evalAt_eq {R : Type*} [CommRing R] {F : Type*} [CommRing F] [IsDomain F]
• theorem evalAt_apply {F : Type*} [CommSemiring F] (φF : R →+* F) (a : F) (p : Polynomial R) :

✏️ Affected: 11 declaration(s) (line number changed)

• noncomputable def liftPackage (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp)) in ArkLib/Commitments/Functional/Hachi/RingSwitch/Reduction.lean moved from L231 to L172
• def relRlin {n μ : ℕ} : in ArkLib/Commitments/Functional/Hachi/RingSwitch/Rlin.lean moved from L79 to L171
• def unstack in ArkLib/Commitments/Functional/Hachi/RingSwitch/Rlin.lean moved from L108 to L236
• noncomputable def rlinPackage (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp)) in ArkLib/Commitments/Functional/Hachi/RingSwitch/Rlin.lean moved from L136 to L467
• noncomputable def rlinStmt (base : ZMod q) (ω γ : ℕ) in ArkLib/Commitments/Functional/Hachi/RingSwitch/Rlin.lean moved from L95 to L275
• noncomputable def hAlpha (φF : ZMod q →+* F) (b : ℕ) (s : RlinStatement Φ n μ) (α : F) in ArkLib/Commitments/Functional/Hachi/ZeroCheck/Constraints.lean moved from L115 to L177
• noncomputable def hZero (φF : ZMod q →+* F) (b : ℕ) (w : LiftedWitness Φ μ n) : in ArkLib/Commitments/Functional/Hachi/ZeroCheck/Constraints.lean moved from L106 to L168
• noncomputable def wTable (φF : ZMod q →+* F) (_b : ℕ) (w : LiftedWitness Φ μ n) : in ArkLib/Commitments/Functional/Hachi/ZeroCheck/Constraints.lean moved from L93 to L117
• noncomputable def wTableMleEval (φF : ZMod q →+* F) (b : ℕ) (w : LiftedWitness Φ μ n) in ArkLib/Commitments/Functional/Hachi/ZeroCheck/Constraints.lean moved from L98 to L124
• theorem natDegree_val_toPoly_lt (α : ℕ) (a : Rq (powTwoCyclotomic (R in ArkLib/Data/Lattices/CyclotomicRing/Rq.lean moved from L298 to L308
• def pSpecFinalSumcheck : ProtocolSpec 1 in ArkLib/ProofSystem/RingSwitching/Packing/Spec.lean moved from L54 to L77

---

sorry Tracking

✅ Removed: 5 `sorry`(s)

ArkLib/Commitments/Functional/Hachi/RingSwitch/Reduction.lean (1)

• theorem lift_coordinateWiseSpecialSound (L226)

ArkLib/Commitments/Functional/Hachi/RingSwitch/Rlin.lean (3)

• def rlinStmt (base : ZMod q) (ω γ : ℕ) (L101)
• def unstack (L111)
• theorem mem_relOutE_of_relRlinE (base : ZMod q) (ω γ : ℕ) (esc : Set E) (L129)

ArkLib/OracleReduction/Security/CoordinateWiseSpecialSoundness/ScalarRound.lean (1)

• theorem coordinateWiseSpecialSound_of_mkWitness_scalar (L102)

❌ Added: 1 `sorry`(s)

ArkLib/Commitments/Functional/Hachi/ZeroCheck/Constraints.lean (1)

• theorem rangeProduct_eq_zero_iff {b : ℕ} {v : F} : (L102)

---

Coverage Notes

• AI file summarization partially analyzed 1 file(s) because their individual diffs exceeded the per-file size budget. Statistics and Lean signal tracking still cover the full PR.

Partially Analyzed Files

• HACHI_GENERIC_RING_SWITCH_PLAN.md (+0/-1079)

* Additional-instructions analysis was skipped because the full diff exceeded the analysis size budget, and partial results would be misleading.

---

📄 **Per-File Summaries**

• ArkLib.lean: The import list in ArkLib.lean was updated with two new module imports – ArkLib.Data.Lattices.CyclotomicRing.QuotientLift and ArkLib.OracleReduction.Security.CoordinateWiseSpecialSoundness.CommittedScalar – and the ArkLib.ProofSystem.RingSwitching imports were restructured: the previous six entries (BatchingPhase, General, Prelude, Profile, Spec, SumcheckPhase) were replaced by fourteen more granular modules organized under the new subdirectories Basic, Lift (with Presentation and Reduction), Packing (containing the former BatchingPhase, General, Prelude, Profile, Spec, SumcheckPhase), RoundVerifiers, and Transport (with Coeffs and Eval). This reflects a reorganization of the ring‑switching proof system into a more modular hierarchy and the addition of new functionality in the lattice and oracle‑reduction areas.
• ArkLib/Commitments/Functional/Hachi/Composition.lean: This change updates the module-level documentation and the signature of several definitions in Composition.lean. It removes specific cross-references to external design documents (HACHI_RING_SWITCHING_PLAN.md, HACHI_LEMMA10_GAP.md, HACHI_RECURSION_GAP.md) and a generic machinery reference (B4), replacing them with more concise descriptions. It adds two new hypotheses (hρ : b - 1 ≤ ρBound and hd bounds) to openCore, openingChain, and hachi_iteration_coordinateWiseSpecialSound, and passes these through the function bodies. The docstring for openCore is updated to mark rows 3–4 (the R^lin adapter and HMZ25 lift) as proven and axiom-clean, and the **Sorried** warning is removed from the coordinateWiseSpecialSound_of_mkWitness_scalar entry. The hachi_iteration_coordinateWiseSpecialSound theorem’s signature is updated to accept and use these new arguments.
• ArkLib/Commitments/Functional/Hachi/Escape.lean: Updated bridgePackageE to pass the escape budget E and set esc explicitly as parameters, replacing former hard-coded or implicit references. The module-level docstring was simplified by removing the parenthetical 'sumcheck-track milestone F2.0' and the '(design decision G1)' annotation on the escape-budget remark. The sorried Lemma 8 comment lost its 'F2.0' qualifier, now reading only 'Sorried.' with the proof plan unchanged.
• ArkLib/Commitments/Functional/Hachi/Recursion/PartialEval.lean: The file’s documentation and comments were updated to remove the (milestone G2) label from the header and the (G2) suffix from the Sorried annotations on partialEvalAt, eqWeight, wTableMleEval_split, and deriveFamily; the reference to HACHI_RECURSION_GAP.md in the header comment was removed; and the mention of design D7 was dropped from the docstrings of pSpecPartialEval, deriveFamily, and partialEvalVerifier. Two new instances were added for pSpecPartialEval — IsEmpty on its challenge index type and a SampleableType instance for each challenge — together with their documentation comments, making the protocol spec ready for use in the generic verifier framework. The relPartialEvalE definition and the CWSS theorem’s docstring were also updated to remove the (G2) milestone marker.
• ArkLib/Commitments/Functional/Hachi/Recursion/TraceHandoff.lean: The module-level docstring and the docstrings of traceCheck, toNextQuadEvalStatement, and handoff_coordinateWiseSpecialSound were updated to remove milestone labels (G3, D6, D5, Phase G, gate G1) and the parenthetical (G3) from Sorried annotations. These are purely cosmetic/docstring changes; no definitions, implementations, or sorry statuses were modified.
• ArkLib/Commitments/Functional/Hachi/Recursion/ZBatchBridge.lean: The diff removes references to the external gap-note file HACHI_RECURSION_GAP.md from the module-level docstring and from the docstring of toHatEvalStatement. It also drops the parenthetical "(G3-adjacent)" from the docstring of hatEval, which remains annotated with sorry. No code, definitions, or theorem statements are changed; only in-file documentation is adjusted.
• ArkLib/Commitments/Functional/Hachi/RingSwitch.lean: This pull request updates the documentation and metadata in ArkLib/Commitments/Functional/Hachi/RingSwitch.lean. The module-level docstring was rewritten to clarify the name "Lift" as referring to the algebraic operation of lifting a quotient-ring equation to an exact polynomial equation, contrasting it with the separate "Packing" concept. It also revises the folder structure documentation to report significant proof-completion progress: RingSwitch/Rlin.lean is now fully proven and sorry-free, and RingSwitch/Reduction.lean now contains a proven, sorry-free and axiom-clean composable CWSS package liftPackage (the cyclotomic instance of a generic Lift protocol), alongside updated references to proof components in Data/Lattices/CyclotomicRing/QuotientLift.lean and the generic ProofSystem/RingSwitching/Lift/. No Lean definitions, theorems, or signatures were added, removed, or modified in this file itself.
• ArkLib/Commitments/Functional/Hachi/RingSwitch/Reduction.lean: The file is rewritten from a custom, sorried implementation of Hachi's ring-switching lift (Figure 4 / Lemma 9) into a cyclotomic instance of the generic Lift framework (ProofSystem/RingSwitching/Lift/). LiftedWitness and LiftCom are repurposed as abbreviations (Lift.LiftedWitness, CoordinateWise.BindingCommitment) instead of standalone structures; relLift and relLiftE are re-expressed via CommittedScalar.rel / Lift.checkAt. The definitions cyclotomicPresentation, cyclotomicPresentation_modulus_natDegree, isPresentation_cyclotomic, and liftCheckAt are added to provide the presentation data and evaluation predicate. The sorried theorem lift_coordinateWiseSpecialSound is removed, replaced by a liftPackage constructed via Lift.package that delegates the CWSS certificate to generic infrastructure; the sole Hachi-specific obligation is the new theorem vecLInftyNorm_le_of_liftShort. liftVerifier and liftProver are deleted.
• ArkLib/Commitments/Functional/Hachi/RingSwitch/Rlin.lean: The file, previously a skeleton with three sorried declarations, is now implemented sorry-free. Key changes include: the addition of the generic helper theorems forall_fin_add, funext_fin_add_iff, dot_append, dot_zero_left, dot_neg_left, dot_matVecMul_transpose, and matVecMul_append_rows; the concrete definitions rlinCW, rlinCT, rlinCZ, unflatten, flattenBlocks_unflatten, unflatten_flattenBlocks, tensorGMatrix, tensorGMatrix_mulVec, stack, unstack, unstack_stack, and stack_unstack; the noncomputable definition rlinStmt for statement assembly; the theorems rlin_linear_iff, vecLInftyNorm_append, rlin_norm_iff, and rlin_iff_relOut establishing the block-row equivalence; the now-proved lemmas mem_relOutE_of_relRlinE and the new completeness direction mem_relRlinE_of_relOutE; and the noncomputable rlinPackage definition. The RlinStatement structure was also updated to remove the binder (Φ : CyclotomicModulus (ZMod q)). All sorrys have been replaced with implementations.
• ArkLib/Commitments/Functional/Hachi/Sumcheck/FinalEval.lean: Updated documentation strings throughout ArkLib/Commitments/Functional/Hachi/Sumcheck/FinalEval.lean to remove milestone markers ((F8), (milestone F8), (sorried F5)) from comments and theorem docstrings — the file is no longer labeled as a skeleton tied to a specific milestone. Added two new instance declarations (IsEmpty and SampleableType) for pSpecFinalEval with full doc strings, establishing that the final-evaluation protocol step has no challenge round. All other definitions (pSpecFinalEval, finalCheck, relWEvalClaimE, and the CWSS theorem) remain unchanged in signature and body but have had their doc-strings cleaned of milestone references.
• ArkLib/Commitments/Functional/Hachi/Sumcheck/Rounds.lean: This diff updates Rounds.lean, which implements the paired sumcheck round loop of Hachi (Lemma 11). The moduledoc strings have been cleaned up: milestone label (milestone F7), design reference (design D9), plan-risk reference (plan risk R10), skeleton reference B4 skeleton, pin reference R8 pins, design reference (design G3), and the F7 sorried label are removed. A minor rewording in the round_coordinateWiseSpecialSound documentation replaces F4.1 + B4.1's with using. No definitions, theorems, signatures, or proof bodies are changed; no sorry or admit is introduced.
• ArkLib/Commitments/Functional/Hachi/ZeroCheck.lean: Updated comments in ArkLib/Commitments/Functional/Hachi/ZeroCheck.lean: removed the reference to HACHI_LEMMA10_GAP.md from the introductory paragraph, and corrected the type name from MvPolynomial to CMlPolynomialEval in the description of ZeroCheck/Batch.lean. These changes reflect updated documentation alignment with the codebase.
• ArkLib/Commitments/Functional/Hachi/ZeroCheck/Batch.lean: Summary unavailable — AI generation failed.
• ArkLib/Commitments/Functional/Hachi/ZeroCheck/Constraints.lean: This diff moves the ZeroCheck file past a preliminary skeleton by adding rangeProduct and its characterizing theorem rangeProduct_eq_zero_iff (both sorried), turning the earlier wTable signature from ZMod q-valued to F-valued and adding a φF parameter to align with the field embedding used downstream, and likewise reworking hZero and hAlpha from MvPolynomial types to the richer CMlPolynomialEval type while adding the new hAlphaEvals function (for per-row Lagrange values) and its companion sorried theorem hAlphaEvals_rowPoint. The diff also adds the liftShort conjunct to roundRel, updates the two sum_sumcheck… theorems to use CMlPolynomialEval.eval instead of MvPolynomial.eval, and introduces rowPoint as the index encoding from Fin n to Fin (2 ^ m₁) needed by the batching scheme. All new definitions and theorems other than rangeProduct, rowPoint, and roundDegAlpha/roundDegZero are marked sorry.
• ArkLib/Commitments/Functional/Hachi/ZeroCheck/Reduction.lean: The file Reduction.lean refines three definitions and removes a cross-reference to a gap-analysis document. relZeroCheck now additionally requires liftShort Φ bound ρBound p.2 (the shortness precondition of the commitment's weak binding) and evaluates the two constraint polynomials via CMlPolynomialEval.eval applied to a Vector.ofFn of the Kronecker point, rather than with MvPolynomial.eval. The zeroCheck_coordinateWiseSpecialSound theorem’s docstring deletes the specific citation to HACHI_LEMMA10_GAP.md and the plan-risk tag, leaving the extraction plan described but marked Sorried. A new docstring on the SampleableType instance for the zero-check challenge briefly documents that F × F is sampleable when F is.
• ArkLib/Commitments/Functional/Hachi/hachi-overview.html: This update to hachi-overview.html reflects progress in the proof formalization for the Hachi protocol. The status of two rows has been upgraded from 'wip' to 'proven': the 'Rˡⁱⁿ adapter' (row 3) in RingSwitch/Rlin.lean is now marked as sorry-free and axiom-clean, with its block-matrix assembly and the rlin_iff_relOut equivalence proven; the 'HMZ25 lift' (row 4) in RingSwitch/Reduction.lean is now also sorry-free and axiom-clean, with the liftBuildWitness extractor and Lemma 9's CWSS fully established. Consequently, the header chip count updated from 'rows 1–2 sorry-free' to 'rows 1–4 sorry-free', and the total open sorries decreased from '≈24' to '≈20'. The footnotes and proof-status legend were also revised to mention Lemma 9's axiom-clean status and to reflect that the count of open sorries now only includes proof terms in the files listed on this page, excluding those in the Recursion/ directory. The summary tile for 'Proven' was expanded to include the new proven rows 3 and 4.
• ArkLib/Data/Lattices/CyclotomicRing/QuotientLift.lean: This new file provides three law-discharge lemmas for the cyclotomic quotient presentation Rq Φ with canonical representatives a.1.toPoly and modulus Φ.φ.toPoly. val_toPoly_injective establishes that the canonical representative mapping is injective. modulus_dvd_toPoly_add_sub and modulus_dvd_toPoly_mul_sub prove the coset laws: the modulus divides the difference between the representative of a sum/product and the sum/product of representatives. No sorry or admit appears in any of the three proofs.
• ArkLib/Data/Lattices/CyclotomicRing/Rq.lean: Refactored natDegree_val_toPoly_lt into a general lemma natDegree_val_toPoly_lt' that works for any cyclotomic modulus Φ given a positivity hypothesis 0 < Φ.φ.natDegree, then re-derived natDegree_val_toPoly_lt for the power-of-two cyclotomic ring as an immediate corollary by supplying that hypothesis via powTwoCyclotomic_natDegree. The general version now uses Φ.degree_toPoly_lt_of_reduced instead of a powTwoCyclotomic-specific variant, and the proof handles zero polynomials by using the explicit hypothesis hd rather than a dimension computation.
• ArkLib/OracleReduction/Security/CoordinateWiseSpecialSoundness/CommittedScalar.lean: This new file CommittedScalar.lean introduces a reusable two-round protocol shape (commit then scalar challenge) within the coordinate-wise special-soundness framework. It defines the structures and theorems that instantiate the generic scalar round for any commitment satisfying BindingCommitment W E Short (a deterministic commitment whose binding guarantee is restricted to Short openings, with an escape set E for weak binding). The file defines:

• Statement (output type Stmt × TCom × Challenge) and rel (the anchored output relation fixing commitment consistency, a checkAt predicate, and the Short condition).
• verifier and prover (the pure statement-extending verifier and honest prover shell).
• responseOpening (extracting the real opening from an escaped response) with the simplification lemma responseOpening_inl.
• buildWitness (a three-way extraction assembler: escape pass-through, commitment-collision escape, or common-opening projection) and its correctness theorem buildWitness_mem, parameterized by the instance-specific recover hypothesis.
• The generic coordinateWiseSpecialSound theorem and the bundled CWSSPackage (package), ready for ▷ composition.

Notably, no sorry or admit is present in the diff.

• ArkLib/OracleReduction/Security/CoordinateWiseSpecialSoundness/Escape.lean: The change removes a parenthetical reference to a design-decision label from the module-level docstring ((design decision G1 of the sumcheck-track plan)) and adds a new Nonempty instance: instance {A E : Type*} [Nonempty A] : Nonempty (A ⊕ E), ensuring that any sum type with a left-inhabited component is itself nonempty (using Classical.arbitrary). This utility instance supports the escape-threaded witness types used throughout the file. No sorry or admit are present.
• ArkLib/OracleReduction/Security/CoordinateWiseSpecialSoundness/Guarded.lean: The diff updates only comments and documentation in Guarded.lean. Milestone references (B4, B4.3, B4.4, B4.1) and the HACHI_SUMCHECK_TRACK_PLAN.md citation are removed from the module docstring, the IsGuardedWith docstring, the contents list, and the docstrings of IsGuarded.append, Verifier.append_coordinateWiseSpecialSound_of_guardedLeft, and GCWSSPackage.append. The instance IsGuarded.of_isPure now has a doc comment. No definitions, theorems, or sorry statements are added or removed; the only functional change is purely cosmetic.
• ArkLib/OracleReduction/Security/CoordinateWiseSpecialSoundness/ScalarRound.lean: Added the full scalar-round tree-navigation kit (topMsgAux/readPre, chalsAux/readChallenges, tree2, shape-recovery theorems eq_leaf, chal_shape, tree_shape_aux, and tree_shape; branch transcript constructors branchPath, branchTr, and accessors branch_challenge, branch_pre, branch_mem), the arity lemma scalarStructure_arity, the node‑predicate‑to‑injectivity link injective_of_nodeOk, the pure‑acceptance bridge branch_relOut_language, and a noncomputable extractor treeExtractor. The previously sorried theorem coordinateWiseSpecialSound_of_mkWitness_scalar is now fully proved (removing sorry), with the [SampleableType C] requirement dropped from its context.
• ArkLib/ProofSystem/Binius/FRIBinius/General.lean: The import path for BatchingPhase was updated from ArkLib.ProofSystem.RingSwitching.BatchingPhase to ArkLib.ProofSystem.RingSwitching.Packing.BatchingPhase, reflecting a reorganization of the RingSwitching module into a Packing subdirectory. No other changes were made to the file; the rest of the code remains identical.
• ArkLib/ProofSystem/Binius/FRIBinius/Prelude.lean: The import statement was updated from ArkLib.ProofSystem.RingSwitching.Prelude to ArkLib.ProofSystem.RingSwitching.Packing.Prelude, reflecting a more specific module path for the ring-switching packing definitions. This change ensures that the file uses the dedicated packing submodule rather than the broader ring-switching prelude, presumably to access packing-specific utilities without unnecessary dependencies.
• ArkLib/ProofSystem/RingSwitching/Basic.lean: This new file acts as the top-level umbrella and taxonomy document for the RingSwitching/ folder in the ArkLib proof system. It provides a detailed, non-code orientation that distinguishes the two construction families (Packing/ and Lift/) by their algebraic direction (small-to-large ring vs. quotient-to-field), their concrete protocol instances and references ([DP24], [HMZ25], [NOZ26]), and their shared but separate infrastructure (RoundVerifiers.lean, Transport/). The file explicitly states that no generic ring-switching reduction exists, documents the folder structure, and lists the relevant wire formats and security machinery (CommittedScalar) that live under OracleReduction/ rather than here.
• ArkLib/ProofSystem/RingSwitching/Lift.lean: Introduced the umbrella file Lift.lean that defines the top-level module for the 'RingSwitching/Lift/' subsystem. The file provides the orientation documentation describing the purpose and architecture of the lift ring switch, which moves linear claims from a quotient ring S ≅ R[X]/(φ) down to field evaluations by lifting to polynomial identities and then evaluating at a challenge scalar α. It enumerates the submodules (Presentation.lean for the data/presentation layer and Reduction.lean for the protocol/committed-scalar shell), explains the coordinate-wise special soundness with security parameter k = 2·deg φ, names the relevant concrete instances (cyclotomic rings via cyclotomicPresentation), and gives usage guidance for instantiators. No new Lean definitions, theorems, or sorry/admit annotations are present in this file itself – it consists solely of the module docstring and import statements.
• ArkLib/ProofSystem/RingSwitching/Lift/Presentation.lean: This file adds the Presentation structure and IsPresentation class, which model a ring S as a quotient R[X]/(phi) with a monic modulus and a canonical representative map. It proves that the representative map is exactly additive (rep_zero, rep_add, rep_neg, rep_sum), strictly stronger than the coset laws. It defines rowSum and establishes the quotient–witness correspondence via mulVec_eq_of_rowSum_eq and exists_rowSum_eq_of_mulVec_eq, which equate row equations in S with exact polynomial identities over R[X]. Finally, mulVec_eq_of_evalAt_rowSum provides an engine that recovers a row equation from evaluations at 2d distinct points, implementing the algebra of Lemma 9 in the cited references.
• ArkLib/ProofSystem/RingSwitching/Lift/Reduction.lean: This is the initial creation of RingSwitching/Lift/Reduction.lean, a protocol-layer module that orchestrates the Lift reduction for the committed-scalar shell. The file defines: the LiftedWitness structure (holding an S-witness z : Fin μ → S and per-row quotient polynomials ρ : Fin n → Polynomial R with a degree bound hρ); the input relation relLin (capturing getM s *ᵥ z = getY s and the zOk admissibility predicate); the challenge-local predicate checkAt (evaluating lifted row identities at a challenge point a plus sideCond); the output relations relOut (commitment consistency plus checkAt) and its escape-threaded variant relOutE; the pure verifier and honest prover derived from the committed-scalar shell; the generic recovery theorem recover (if a short opening passes checkAt at 2d pairwise-distinct challenges, the input linear relation holds); the extractor buildWitness and its correctness theorem buildWitness_mem; the coordinate-wise special-soundness theorem coordinateWiseSpecialSound at plain k = 2d; and the composable package CWSSPackage. No sorry or admit are present.
• ArkLib/ProofSystem/RingSwitching/Packing.lean: Added a new module documentation file Packing.lean that serves as the top-level orientation for the RingSwitching/Packing/ folder. It explains that the packing family of ring switches moves evaluation claims from a small ring B to a large ring L by encoding blocks of 2^κ small-ring coefficients as single large-ring elements, outlines the two ingredients (the shared RingSwitchingProfile in Profile.lean and per-instance relocation logic), enumerates the folder's subfiles (Profile.lean, Prelude.lean, Spec.lean, BatchingPhase.lean, SumcheckPhase.lean, General.lean) with their responsibilities, and notes planned instantiations such as the binary-tower case (Binius) and a subfield-valued one-message variant (Hachi). No new theorems, definitions, or proofs are introduced; the file is purely documentation.
• ArkLib/ProofSystem/RingSwitching/Packing/BatchingPhase.lean: The file was renamed and moved from ArkLib/ProofSystem/RingSwitching/BatchingPhase.lean to ArkLib/ProofSystem/RingSwitching/Packing/BatchingPhase.lean, with imports updated to ArkLib.ProofSystem.RingSwitching.Packing.Prelude and ArkLib.ProofSystem.RingSwitching.Packing.Spec. The module docstring was completely rewritten to describe the phase as “relocating the claim into the carrier”, referencing [DP24] Construction 3.1, and explicitly stating that leaf proofs remain open (sorry). The oracleVerifier definition was refactored from a manual verify method to an instance of scalarRoundOracleVerifier (from RingSwitching.scalarRoundOracleVerifier), with separate check, accept, and reject arguments that delegate the protocol steps (Check 1, batching-scalar absorption, and failure state). The batchingInputRelationProp definition had a minor formatting change, splitting the conjunction onto two lines. The docstring also introduces new security scaffolding (batchingRbrExtractor) and clarifies the tensor factor ordering in the protocol steps.
• ArkLib/ProofSystem/RingSwitching/Packing/General.lean: The file was renamed from ArkLib/ProofSystem/RingSwitching/General.lean to ArkLib/ProofSystem/RingSwitching/Packing/General.lean, and its imports were updated to point to the new Packing submodule (Packing.Spec, Packing.BatchingPhase, Packing.SumcheckPhase). The module-level docstring was rewritten to describe the file as “The composed interactive packing reduction” rather than the full ring-switching protocol, detailing the three-phase sequential composition (batching, relocation sumcheck, downstream opening), the perfect completeness and round-by-round knowledge soundness composition with error bounds, and noting that leaf proofs are open (sorry). The inline comments on batchingCoreVerifier, fullOracleVerifier, batchingCoreReduction, fullOracleReduction, and fullOracleProof were updated from “Binary Basefold protocol” to “DP24 ring-switching protocol”. These changes reflect a reorganization of the ring-switching code into a dedicated Packing variant, with clearer documentation of the construction and its security composition.
• ArkLib/ProofSystem/RingSwitching/Packing/Prelude.lean: This diff refactors ArkLib/ProofSystem/RingSwitching/Prelude.lean into a new file ArkLib/ProofSystem/RingSwitching/Packing/Prelude.lean with a focused scope on packing algebra and protocol vocabulary. The file-level module documentation is rewritten to describe the pack/unpack pair (packMLE/unpackMLE), carrier operations on L ⊗[K] L with embeddings φ₀/φ₁, protocol subroutines (embedded_MLP_eval, eqWeightedCoordSum, compute_A_func/compute_A_MLE), and protocol types/relations. The import of ArkLib.ProofSystem.RingSwitching.Profile is changed to ArkLib.ProofSystem.RingSwitching.Packing.Profile, and a new import ArkLib.ProofSystem.RingSwitching.Transport.Coeffs is added. The implementation of componentWise_embed_MLE is replaced with a single call to embedCoeffs φ t' from the new transport module. Three new definitions are added: eqWeightedCoordSum (the eq̃-weighted sum for coordinate families), compute_s0 (batched sumcheck target), and compute_final_eq_value (final eq̃ value); all use eqWeightedCoordSum rather than inline sums. The definitions performCheckOriginalEvaluation, compute_A_func, compute_s0, and compute_final_eq_value are updated to use eqWeightedCoordSum internally. No sorry or admit are introduced.
• ArkLib/ProofSystem/RingSwitching/Packing/Profile.lean: Renamed from Profile.lean to Packing/Profile.lean under RingSwitching/Packing/ and substantially rewritten its module-level doc-comment. The file still defines the RingSwitchingProfile structure (the data required for a packing-based ring switch: basis, carrier A, embeddings φ₀ and φ₁, coordinate maps decomposeRows/decomposeColumns, and their reconstruction laws), but the documentation now frames it as the data layer of Packing rather than a general ring-switching profile, clarifies that the Lift construction does not use this profile, and adds formal references to [DP24] and [NOZ26]. No Lean code other than the comment block was changed.
• ArkLib/ProofSystem/RingSwitching/Packing/Spec.lean: The file was renamed from ArkLib/ProofSystem/RingSwitching/Spec.lean to ArkLib/ProofSystem/RingSwitching/Packing/Spec.lean, reorganized into a new Packing namespace, and its module-level comment was rewritten to describe the interactive packing reduction wire formats. The pSpecBatching definition was refactored to use CoordinateWise.ScalarRound.pSpecScalar (replacing the manual Direction and message-type arrays), and pSpecFinalSumcheck was refactored to use pSpecMessage. Correspondingly, the hand-written OracleInterface and SampleableType instances for pSpecBatching, pSpecSumcheckLoop, and pSpecFinalSumcheck were replaced with comments referring to the generic instances from CoordinateWise.ScalarRound and RingSwitching.RoundVerifiers, and several earlier manual instances were removed.
• ArkLib/ProofSystem/RingSwitching/Packing/SumcheckPhase.lean: This diff relocates SumcheckPhase.lean into a new Packing/ subdirectory and rewrites its module-level docstring to describe the file as covering the relocation sumcheck (iterated rounds plus final consistency step) of the interactive packing reduction, referencing [DP24] Construction 3.1 steps 6–9. The finalSumcheckVerifier definition is refactored from an explicit verify method to an instantiation of messageRoundOracleVerifier, using named check, accept, and reject functions. The docstring now explicitly notes that leaf proofs are left open (sorry).
• ArkLib/ProofSystem/RingSwitching/RoundVerifiers.lean: This new file defines two reusable check-then-update verifier combinators for common round shapes in ring-switching proofs: messageRoundOracleVerifier for a one-message wire (using the new pSpecMessage protocol spec) and scalarRoundOracleVerifier for a message-then-scalar-challenge wire (using CoordinateWise.ScalarRound.pSpecScalar). Both verifiers query the prover message, run a deterministic check, and produce an updated statement via accept or reject. The file also provides the necessary OracleInterface and SampleableType instances for pSpecMessage.
• ArkLib/ProofSystem/RingSwitching/Transport.lean: Added a new umbrella documentation module Transport.lean that describes the purpose and structure of the RingSwitching/Transport/ subfolder. It imports the Eval and Coeffs modules, explains how the transport layer moves claims between rings via a ring homomorphism, and documents the univariate (evalAt, eq_of_evalAt_eq) and multivariate (embedCoeffs, embedCoeffs_eval) legs. It also notes how Lift and Packing instantiate these components, providing orientation for the reviewer.
• ArkLib/ProofSystem/RingSwitching/Transport/Coeffs.lean: The new file Coeffs.lean defines embedCoeffs (a noncomputable function transporting coefficients of a degree‑bounded multivariate polynomial along a ring homomorphism φ : R →+* T while preserving the degree bound) and the theorem embedCoeffs_eval, which states that evaluating the transported polynomial at the transported input equals the transported evaluation. This is the multivariate leg of the ring‑switching transport layer and complements the univariate leg in Eval.lean.
• ArkLib/ProofSystem/RingSwitching/Transport/Eval.lean: Summary unavailable — AI generation failed.
• ArkLib/ProofSystem/Sumcheck/Structured/SingleRound.lean: The file comment block was updated to reflect that the single-round primitives originated from RingSwitching.Packing.Spec and RingSwitching.Packing.SumcheckPhase (previously RingSwitching.Spec and RingSwitching.SumcheckPhase). The documentation now states that the promoton allows reuse by other protocols like Hachi's §4.3 sumcheck and Galois-ring PCS, and that RingSwitching.Packing.SumcheckPhase contains @[reducible] wrappers specializing Context and OStmtIn to the DP24 ring-switching types. No definitions, theorems, or proofs were modified; the change is exclusively to the module-level docstring.
• HACHI_GENERIC_RING_SWITCH_PLAN.md: The file HACHI_GENERIC_RING_SWITCH_PLAN.md was deleted. This document contained a detailed reconciliation and implementation plan for extending the generic ring‑switching layer to accommodate Hachi’s packing head, including phases, design decisions, and dependencies. Its removal eliminates this planning document from the repository.
• HACHI_LEMMA10_GAP.md: This .md file was deleted in its entirety (852 lines removed). The file contained an in-depth analysis of a gap in Lemma 10 of the Hachi protocol, a detailed refutation of the paper's coordinate-wise special-soundness (CWSS) claim, and a survey of possible repairs. It presented a constructive protocol-level counterexample based on the range-check polynomial, diagnosed the root cause (degree confusion and the failure of cross-vanishing to imply the polynomial is zero for multilinear polynomials in at least two challenge variables), and evaluated multiple repair strategies (Kronecker-curve challenges, coordinate-zipped sequential CWSS rounds, tensor grids, scalar power fingerprints, etc.), ultimately recommending a one-round Kronecker-curve encoding. The file also included formalization-ready theorem statements, parameter accounting, and a roadmap for adapting the protocol's zero-check round.
• HACHI_RECURSION_GAP.md: Deleted HACHI_RECURSION_GAP.md entirely. The file documented a confirmed algebraic gap in the partial-evaluation step of the Hachi protocol (§3.2/§4.5), where the reduction from per-slice well-formedness claims to a single packed claim is not knowledge-sound, and detailed an adopted CWSS-native repair involving post-yᵢ scalar fingerprinting, a degree-two relocation sumcheck, and reuse of the existing p element. Its removal indicates that the analysis and proposed repair have been either resolved or superseded.
• HACHI_RING_SWITCHING_COMPARISON.md: The file HACHI_RING_SWITCHING_COMPARISON.md was deleted entirely (246 lines removed). It contained a detailed architectural comparison between the Hachi protocol's ring-switching and the DP24/Binius ring-switching implemented in the ProofSystem/RingSwitching/ directory. Its removal suggests that the comparison is no longer maintained as a standalone document—the structural taxonomy it described (distinguishing Packing/ from Lift/ folders, the shared RoundVerifiers skeletons, the Transport/ algebra, and the conclusion that Hachi uses a different protocol interaction) has been absorbed into the project's in-code documentation or is handled by the two updated construction folders mentioned in §7–8 of the deleted file itself.
• HACHI_RING_SWITCHING_PLAN.md: The file HACHI_RING_SWITCHING_PLAN.md was deleted in its entirety. This document contained the detailed formalization plan for Hachi's ring switching and sumcheck protocols (v2). Its removal indicates that the planning phase has concluded, and the content is either superseded by the actual implementation or has been absorbed into other documentation. For reviewers, this means that the planning document is no longer available; orientation should instead rely on the committed code, the existing HACHI_RING_SWITCHING_COMPARISON.md, and the TODO blocks in the relevant Lean files for the current state of the formalization.
• HACHI_SUMCHECK_TRACK_PLAN.md: The file HACHI_SUMCHECK_TRACK_PLAN.md has been deleted in its entirety. This file contained a detailed, sequential implementation plan for milestones B4, F2, F3, and F4 of the Hachi sumcheck track, including code sketches, proof plans, acceptance criteria, and risk analysis. Its removal means that this plan will no longer serve as a starting point for reviewers or as an implementation guide for those milestones.
• blueprint/src/references.bib: Added two new bibliography entries: HMZ25 (Huang, Mao, Zhang, "Sublinear Proofs over Polynomial Rings", ePrint 2025/199) and NOZ26 (Nguyen, O'Rourke, Zhang, "Hachi: Efficient Lattice-Based Multilinear Polynomial Commitments over Extension Fields", ePrint 2026/156). These references support newly cited cryptographic constructions or proof systems in the formalization.
• docs/kb/concepts/ring-switching.md: The documentation page for ring switching was rewritten to clarify that ring switching is a family of constructions, adding a taxonomy umbrella (Basic.lean) and explicitly naming two construction folders: Packing/ (small→large packing via RingSwitchingProfile) and Lift/ (large quotient ring→field via Lift.Presentation for the HMZ25 switch). The “Instances” section was restructured into “The three constructions”, detailing the DP24 packing switch (previously Binius), the Hachi §3 packing head (newly described as planned), and the HMZ25 Lift construction (new). The soundness cost in the Overview was updated from O(1/|L|) to O(ℓ/|L|) (with O(1/|L|) per challenge). The “Main ArkLib Touchpoints” section was expanded with more specific file paths, including new entries for Basic.lean, RoundVerifiers.lean, Transport.lean, Packing/Profile.lean, Packing/Prelude.lean, Packing/General.lean, Lift/Presentation.lean, Lift/Reduction.lean, and OracleReduction/Security/CoordinateWiseSpecialSoundness/CommittedScalar.lean. The Notes now explicitly state that the DP24 protocol leaf completeness/soundness proofs are open (sorry) and tracked as follow-up.
• docs/kb/papers/DP24.md: Updated the DP24 paper page to reflect the reorganization of the ring-switching files: the two RingSwitching/ (Profile.lean, General.lean) moved into a subdirectory Packaging/, and the page now describes the ring-switching reduction as parameterized over the RingSwitchingProfile in the packing-algebra layer, notes that it belongs to a larger family of ring-switching constructions documented in a new taxonomy umbrella (RingSwitching/Basic.lean), and updates the related-modules paths and touchpoints table accordingly. No theorems, definitions, or proofs were added or changed—only documentation paths and conceptual framing were corrected.
• docs/kb/papers/HMZ25.md: This commit adds a new knowledge-base entry for the paper "Sublinear Proofs over Polynomial Rings" (HMZ25), documenting its core ring-switching lift technique and how ArkLib formalizes it. The page provides a high-level summary of the paper's identity (relating a quotient-ring equation to a lifted polynomial equation with a quotient vector), identifies the key formalized modules and their roles (the generic Presentation/Reduction lift in ArkLib/ProofSystem/RingSwitching/, the interpolation kernel in ArkLib/Data/Lattices/CyclotomicRing/QuotientLift.lean, and the Hachi instantiation in ArkLib/Commitments/Functional/Hachi/RingSwitch/Reduction.lean), and notes divergences between the paper's plain construction and ArkLib's implementation (e.g., the use of weak/norm-conditioned binding, an abstract monic cyclotomic modulus instead of X^d+1, and abstract extension embeddings).
• docs/kb/papers/NOZ26.md: Updated docs/kb/papers/NOZ26.md to reflect that the §4.3 HMZ25 lift (Lemma 9) is now formalized and proven (sorry-free, axiom-clean) as liftPackage/lift_coordinateWiseSpecialSound in Hachi/RingSwitch/Reduction.lean, consuming the generic Lift construction under ProofSystem/RingSwitching/Lift/. The related module path was corrected from Profile.lean to Packing/Profile.lean. The Open Formalization Gaps section was revised: the §4.3 lift is marked done, the §3 packing head remains open, and Lemmas 10–11 plus recursion adapters are noted as still being skeletons. The status of the sumcheck/ring-switching evaluation machinery was also changed from 'not yet formalized' to removed entirely.
• docs/kb/sources/HMZ25/metadata.yml: Adds a new metadata file docs/kb/sources/HMZ25/metadata.yml that registers the HMZ25 bibliography entry with source kind bibliography-only, a canonical URL to the eprint (https://eprint.iacr.org/2025/199), an empty list of committed artifacts, and a note that it was scaffolded from references.bib for the paper “Sublinear Proofs over Polynomial Rings.” This makes the source available in the project’s knowledge base for referencing and linking.
• docs/skills/prove-milestone.md: The change makes several targeted updates to the prove-milestone.md workflow document for the Hachi project. It refines Global invariant 6 to clarify that Classical.choice is acceptable when inherited through Mathlib or through an unmodified generic combinator (e.g., ReduceClaim.verifier_coordinateWiseSpecialSound), and introduces the concept of "axiom-clean against the baseline" with the set {propext, Classical.choice, Quot.sound}. It adds a new requirement before Stage 1 design work to surface conflicts between a user's requested approach and the repo's verified design notes (from KB analyses), recording the user's decision in the scope manifest. It adds documentation for Hachi-specific attacks regarding treeSpecialSound as an ∃-extractor, requiring that its buildWitness/liftBuildWitness constructive anchor be public and cited. It also adds a new block of practical development guidance covering lake build <module> before spike files, linter flags (longLine, unusedSectionVars with the omit pattern), and a note that the unusedSectionVars lint does not fire on sorry-bodied declarations. It revises the Stage 3 workflow to allow transcribing verified spike-file bodies one file at a time, and updates the axiom-check steps in both Stage 3 and the public review section to reference invariant 6's new baseline. It revises the milestone finalization section to require completing the citation workflow (blueprint/src/references.bib entry + docs/kb/papers/ page, per docs/wiki/blueprint-and-citations.md) and to note the KB linter in validate.sh and the regeneration command ./scripts/update-lib.sh.
• docs/wiki/repo-map.md: The RingSwitch/ entry was updated to reflect that RingSwitch/Reduction is now the cyclotomic instance of the generic Lift switch, with Lemma 9 marked as proven, and the distinct §3 packing reduction is now explicitly located under ProofSystem/RingSwitching/Packing/. The ZeroCheck/ entry now references the corrected Lemma 10 directly instead of a gap file, and the Recursion/ entry points to a local gap reference (Recursion/ZBatchBridge) rather than a separate document. In the CoordinateWiseSpecialSoundness section, ScalarRound and CommittedScalar are now marked as proven (previously ScalarRound was sorried), with details on their components, instantiation, and the completed CWSS theorem. The overview of ring switching was rewritten to clarify that it is a family of two constructions (Packing/ and Lift/) with shared top-level verifiers and transport algebra, replacing the previous description of a single generic compiler; this reflects the architectural separation and the completed proofs for the lift.

---

Last updated: 2026-07-26 07:15 UTC.