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

All topics

2569 results

Project-declaredLean 4.31.0

Scalar Vec Mul mul l2Norm Sq le

ArkLib.Lattices.CyclotomicModulus.scalarVecMul_mul_l2NormSq_le

Plain-language statement

Micciancio/Young product bound. Over the power-of-two cyclotomic modulus powTwoCyclotomic α (φ = X^{2^α}+1), scaling an already-c-scaled vector by a further ring element d of bounded centered ℓ₁ norm grows the squared ℓ₂ norm by at most κ² (the honest Young/Micciancio inequality ‖(c·d)·v‖₂² ≤ ‖d‖₁² · ‖c·v‖₂² over the negacyclic convolu...

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

Sub l2Norm Sq le

ArkLib.Lattices.CyclotomicModulus.sub_l2NormSq_le

Plain-language statement

Subtraction bound. The squared ℓ₂ norm of a difference of two vectors, each within boundSq, is within subL2NormSqBound boundSq = 4·boundSq.

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

Sub l Infty Norm le

ArkLib.Lattices.CyclotomicModulus.sub_lInftyNorm_le

Plain-language statement

ℓ∞ subtraction bound. The ℓ∞ norm of a difference of two vectors, each within bound, is within subLInftyNormBound bound = 2·bound.

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

Sum eq half Sum

ArkLib.Lattices.CyclotomicModulus.sum_eq_halfSum

Plain-language statement

Splitting the degree-2^α sum into low/high halves and factoring ζ^{2^{α-1}} = s collects the coefficient of ζ^j as a_j + s·a_{2^{α-1}+j}.

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

Trace H fixed of smul

ArkLib.Lattices.CyclotomicModulus.traceH_fixed_of_smul

Plain-language statement

If multiplication by g permutes Hexp (Hexp_generator_smul), then σ_g fixes Tr_H. The per-term step uses σ_g(σ_i a) = σ_{g·i} a = σ_{(g·i) mod 2^{α+1}} a (composition + exponent-periodicity, both proven); the sum then reindexes along the permutation.

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

Trace H kernel

ArkLib.Lattices.CyclotomicModulus.traceH_kernel

Plain-language statement

The kernel Tr_H(X^{e_p + e_q·σ_{-1}}) = (d/k)·[p = q] (Hachi [NOZ26, §3, Theorem 2]). With e_v = packExp v and n = d/2k: on the diagonal the exponent is e_p·2d, so X^{…} = 1 and the trace is d/k; off the diagonal, n ∣ (e_p + e_q·σ_{-1}) ↔ p ≡ q mod n, so when p ≢ q mod n Claim 2 applies, and when p ≡ q mod n (but p ≠ q) the exponen...

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record