Research proof index

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...

Unconditional perfect correctness with the concrete binary decomposition. Both message and inner decompositions are the genuine base-b digit decomposition of ZMod q (zmodDigitDecomposition, the Hachi gadget inverse G⁻¹). All weak-verifier side conditions are discharged automatically: the trivial challenge cᵢ = 1 is short (Rq.l1Norm_one), a...

Perfect correctness of the inner-outer Ajtai commitment for lawful decompositions. The honest opening uses the trivial challenge cᵢ = 1, under which verify_weak reduces to the ordinary honest check. Correctness therefore needs, beyond gadget lawfulness: * the trivial challenge is an admissible challenge: 0 < ‖1‖₁ and ‖1‖₁ ≤ κ; * each honest me...