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.

1 topic

423 results

Clear filters
Project-declaredLean 4.31.0

Vec LInfty Norm flatten Blocks le

ArkLib.Lattices.CyclotomicModulus.vecLInftyNorm_flattenBlocks_le

Plain-language statement

The ℓ∞ norm of a flattened block vector is bounded by γ as soon as every block is: the ℓ∞ norm of flattenBlocks is the supremum of the per-block ℓ∞ norms.

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

V Elt coeff

ArkLib.Lattices.CyclotomicModulus.vElt_coeff

Plain-language statement

Coefficient of the basis element: v_j has coefficient [s = j]·(2 if j=0 else 1) at the position (d/2k)·s. The two basis exponents of v_j are (d/2k)·j (degree < d/2) and its conjugate (degree > d/2); only the former can equal (d/2k)·s < d/2, except at j=0 where the conjugate coincides (giving the doubling).

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

V Elt coeff full

ArkLib.Lattices.CyclotomicModulus.vElt_coeff_full

Plain-language statement

Full coefficient formula for the basis element v_j. For every position p < d, the p-th coefficient of v_j = X^{(d/2k)·j} + σ_{-1}(X^{(d/2k)·j}) is: 2 at p = 0 when j = 0; otherwise +1 at p = (d/2k)·j, -1 at the complementary position p = d - (d/2k)·j, and 0 elsewhere. This extends vElt_coeff (which only covers the positions `...

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

Xpow coeff of lt

ArkLib.Lattices.CyclotomicModulus.Xpow_coeff_of_lt

Plain-language statement

For i < 2^α (below the modulus degree), X^i is already reduced, so its j-th coefficient is the Kronecker delta [j = i].

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

Xpow mul coeff

ArkLib.Lattices.CyclotomicModulus.Xpow_mul_coeff

Plain-language statement

Coefficient of an X^e-shift of a reduced element. For e < d, p < d and any x : R_q, the p-th coefficient of x·X^e is the (p-e)-th coefficient of x (no wrap, e ≤ p), or minus the (p+d-e)-th coefficient (one wrap past X^d = -1, p < e). This is the only place the proof needs the ring's multiplication; everything downstream is coef...

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

Xpow mul conj Exp

ArkLib.Lattices.CyclotomicModulus.Xpow_mul_conjExp

Plain-language statement

Conjugation negates a square-root-of--1 monomial: if X^{2j} = -1 then σ_{-1}(X^j) = X^{j·conjExp} = -X^j. The exponent j·conjExp ≡ -j, so X^{j·conjExp} is the inverse of X^j; and X^j·(-X^j) = -(X^j)² = -X^{2j} = 1, so the inverse is -X^j.

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record