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

Is Unit of l1Norm le

ArkLib.Lattices.CyclotomicModulus.isUnit_of_l1Norm_le

Plain-language statement

Lyubashevsky–Seiler: short elements are invertible (LS18, Cor. 1.2; Hachi, Lemma 3). Over the power-of-two cyclotomic modulus powTwoCyclotomic α (φ = X^{2^α}+1) with a prime q ≡ 5 (mod 8), a nonzero element of Rq (powTwoCyclotomic α) with centered ℓ₁ norm ≤ κ and κ² < q is a unit: by the algebraic core a non-unit forces q ∣ ‖c‖₂², whil...

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

Mem fixed symm

ArkLib.Lattices.CyclotomicModulus.mem_fixed_symm

Plain-language statement

X^e + σ_{-1}(X^e) ∈ R_q^H when d/2k ∣ e: X^e is then σ_{4k+1}-fixed (its exponent is a multiple of d/2k), and the sum is symmetric under σ_{-1} (which has order 2).

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

Mk aeval X pow periodic

ArkLib.Lattices.CyclotomicModulus.mk_aeval_X_pow_periodic

Plain-language statement

(C-3 helper) aeval (X^n) and aeval (X^{n mod 2^{α+1}}) agree in the quotient.

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

Mk monomial coeff full

ArkLib.Lattices.CyclotomicModulus.mk_monomial_coeff_full

Plain-language statement

Full coefficient of a (possibly high-degree) scaled monomial. For p < d, the p-th coefficient of the reduced c·X^m is (-1)^{m/d}·c at the folded position p = m mod d, and 0 elsewhere , the sign records how many times the exponent wrapped past X^d = -1.

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

Mk monomial coeff lt

ArkLib.Lattices.CyclotomicModulus.mk_monomial_coeff_lt

Plain-language statement

The j-th coefficient of the reduced c·X^i (for i < d) is c·[j = i].

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

Mk monomial eq

ArkLib.Lattices.CyclotomicModulus.mk_monomial_eq

Plain-language statement

The scaled monomial c·X^j ∈ Rq Φ factors as (constant c)·X^j.

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record