Research proof index

ℓ₂² shortness of G⁻¹. The full gadget decomposition has centered squared-ℓ₂ norm at most (rows·digits)·(deg φ)·(b-1)².

The gadget entry at the flattened index finProdFinEquiv (i', e) is constRq (base^e) on the diagonal block and 0 elsewhere.

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.