Research proof index

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

Weak binding reduces to Module-SIS. The Hachi/Greyhound weak-binding advantage (over 𝓜(q, α)) is bounded by the sum of the inner and outer extracted Module-SIS advantages.