Source-pinned research

Research proof index

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 423 research declarations. Search 10,000 more complete Mathlib declarations.

All topics

423 results

Clear filters
Project-declaredLean 4.31.0

Binding Advantage le module SIS of short Closure

ArkLib.Lattices.Ajtai.Simple.bindingAdvantage_le_moduleSIS_of_shortClosure

Plain-language statement

Binding reduces to Module-SIS for any commitment/Module-SIS shortness predicates closed under differences.

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

Zmod Digit nat Abs le

ArkLib.Lattices.Ajtai.zmodDigit_natAbs_le

Plain-language statement

Core digit bound. Each base-b digit of zmodDigitDecomposition, viewed as a centered residue, has absolute value at most b - 1 , provided b - 1 ≤ q/2, so the digit (a natural number < b) does not wrap to a negative centered representative.

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

Card fixed Subring le

ArkLib.Lattices.CyclotomicModulus.card_fixedSubring_le

Plain-language statement

|R_q^H| ≤ q^k, from ψ : (R_q^H)^{d/k} ↪ R_q injective and |R_q| = q^{2^α}: |R_q^H|^{d/k} ≤ q^{2^α} = (q^k)^{d/k}.

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

C Inf Norm psi le

ArkLib.Lattices.CyclotomicModulus.cInfNorm_psi_le

Plain-language statement

Hachi [NOZ26, §3, Lemma 6]: ‖ψ(a)‖∞ ≤ 2β. If every entry of the vector a : (R_q^H)^{d/k} has centered coefficient ℓ∞-norm at most β (i.e. ‖a‖∞ ≤ β in the mod± q convention of [NOZ26, §2.1]), then the packed ring element ψ(a) ∈ R_q satisfies ‖ψ(a)‖∞ ≤ 2β. The hypotheses are the standing assumptions of [NOZ26, §3]: k = 2^κ divides `d/2...

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

Coeff psi abs le two vec CInf Norm

ArkLib.Lattices.CyclotomicModulus.coeff_psi_abs_le_two_vecCInfNorm

Project documentation

Main combinatorial bound (at most two contributions per position). For p < d, the p-th coefficient of ψ(a) is ± c₁ ± c₂ where c₁, c₂ are coefficients of the (at most two) entries of a whose index matches p's residue class mod d/2k (j₁ := p mod d/2k from the first half, j₂ := d/2k + p mod d/2k from the second); all other summands...

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

Conj Aut Xpow eq neg

ArkLib.Lattices.CyclotomicModulus.conjAut_Xpow_eq_neg

Plain-language statement

σ_{-1}(X^e) = -X^{d-e} for 0 < e < d: the conjugate of a sub-d/2 monomial is minus the complementary monomial. The only nonzero coefficient of σ_{-1}(X^e) sits at d - e, with sign -1: from e·conjExp ≡ 2^{α+1} - e (mod 2^{α+1}) we get σ_{-1}(X^e) = X^{d + (d-e)} = -X^{d-e}.

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record