ArkLib

The gadget product, evaluated at row i, is the base-weighted sum of the digits slots of block i.

Core recomposition coefficient bound. Each centered coefficient of an entry of the gadget product G_{b,rows} ·ᵥ v is at most (∑_{u<digits} bᵘ) · γ whenever ‖v‖∞ ≤ γ. The wraparound of the ZMod q powers bᵘ is immaterial: the integer ∑ₑ bᵉ·valMinAbs(vₑ.coeff k) is an explicit representative of the output coefficient, and the centered represe...

The J-recomposition ℓ₂² chain. From the range check ‖ẑ‖∞ ≤ γ (Eq. (20)'s ẑ ∈ S_b, symmetric model), the recomposed z = J·ẑ satisfies ‖z‖₂² ≤ zRecomposeL2SqBound γ b τ (deg φ) rows , no primitive ‖z‖₂² verifier check is needed.

The witness assembler is correct , the hmk input to the generic assembly coordinateWiseSpecialSound_of_mkWitness (SingleRound.lean), and the mathematical content of Hachi Lemma 8's three-case split: at every star-shaped family of relOut-accepting branches, buildWitness lands in relIn.

Eval-consistency of the extracted opening (Hachi Lemma 8, case (C), part 2 , Eq. (15)): the shared-ŵ c3 row plus the coordinate-isolated, unit-divided c4 rows discharge the w/c3/c4 hypotheses of evalConsistency_of_star at the shared recomposed carrier w := G_{2^r} *ᵥ ŵ.

Honest message decompositions pass the message gadget checks.

The c5-side unit-cancellation of the subtract-and-divide extraction (Hachi Lemma 8, case (C)): from the c5-subtract chain c̄ᵢ •ᵥ (G_{n_A} t̂ᵢ) = A *ᵥ Δz and IsUnit c̄ᵢ, the extracted message block sᵢ := Ring.inverse c̄ᵢ •ᵥ Δz satisfies the weak-opening inner gadget relation (VerifiedBlock.inner_eq).

Pull-back lemma (the hRel for the bridge's CWSS): a QuadEvalWitness accepted by QuadEval's relIn at the reinterpreted statement toQuadEvalStatement Φ s is accepted by relPolyEval at the polynomial-level statement s. The MSIS disjuncts are preserved verbatim (toQuadEvalStatement keeps pp); the opening disjunct converts the matrix-leve...