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

Xpow nat Degree

ArkLib.Lattices.CyclotomicModulus.Xpow_natDegree

Plain-language statement

The key relation X^{2^α} = -1 (X^d = -1), proven via the quotient: X^d + 1 is the modulus, so it vanishes in the quotient.

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

Xpow sub one is Unit

ArkLib.Lattices.CyclotomicModulus.Xpow_sub_one_isUnit

Plain-language statement

X^c - 1 is a unit whenever some X^{c·2^t} = -1. Then (∑_{j<2^t} (X^c)^j)·(X^c - 1) = (X^c)^{2^t} - 1 = -2, a unit (isUnit_two), so X^c - 1 is a unit. This is the crux of the trace-of-monomial vanishing (Hachi [NOZ26, §3, Claim 2]): it makes the geometric sum collapse without a domain.

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

Eval Split eq eval

ArkLib.Lattices.Hachi.evalSplit_eq_eval

Plain-language statement

The split. Evaluating a multilinear polynomial equals the vector–matrix–vector product of its reshaped coefficient matrix with the monomial bases of the low and high evaluation points (Hachi [NOZ26, §4]).

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

Eval Split Eval eq eval

ArkLib.Lattices.Hachi.evalSplitEval_eq_eval

Plain-language statement

The split (Lagrange representation). Evaluating a multilinear polynomial given by its hypercube values equals the vector–matrix–vector product of its reshaped value matrix with the Lagrange bases of the low and high evaluation points.

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

Tensor G coord diff

ArkLib.Lattices.Hachi.tensorG_coord_diff

Plain-language statement

Coordinate isolation (Hachi Lemma 8, case (C), the c5 subtract-and-divide crux): if c ≡ⱼ c', the challenge-difference sum collapses to the j-th block, tensorG (c − c') x = (cⱼ − c'ⱼ) •ᵥ (G_k *ᵥ xⱼ).

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

Tensor G1 coord diff

ArkLib.Lattices.Hachi.tensorG1_coord_diff

Project documentation

Coordinate isolation at k = 1 (Hachi Lemma 8, case (C), the c4 subtract-and-divide crux): if c ≡ⱼ c', then tensorG1 (c − c') ŵ = (cⱼ − c'ⱼ) · wⱼ where w := G_blocks *ᵥ ŵ is the recomposed carrier.

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record