Source-pinned research
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 5 research declarations. Search 10,000 more complete Mathlib declarations.
5 results
Clear filtersArkLib.Lattices.Ajtai.InnerOuter.generateDecomps_message_checks
Plain-language statement
Honest message decompositions pass the message gadget checks.
Source project: ArkLib
Person-level attribution pending.
ArkLib.Lattices.Ajtai.InnerOuter.perfectlyCorrect
Plain-language statement
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...
Source project: ArkLib
Person-level attribution pending.
ArkLib.Lattices.Ajtai.InnerOuter.perfectlyCorrect_of_lawful
Plain-language statement
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...
Source project: ArkLib
Person-level attribution pending.
KZG.CommitmentScheme.correctness
Plain-language statement
The KZG scheme satisfies perfect correctness as defined in CommitmentScheme.
Source project: ArkLib
Person-level attribution pending.
KZG.correctness
Plain-language statement
Algebraic correctness of one KZG opening for a coefficient vector.
Source project: ArkLib
Person-level attribution pending.