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

1 topic

5 results

Clear filters
Project-declaredLean 4.31.0

Galois Aut fixed of mem

ArkLib.Lattices.CyclotomicModulus.galoisAut_fixed_of_mem

Plain-language statement

Every σ_m with m ∈ Hexp fixes R_q^H: modulo 2d, m is ±(4k+1)^a, and the two generators σ_{4k+1}, σ_{-1} fix R_q^H (so does any composite).

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

Psi injective

ArkLib.Lattices.CyclotomicModulus.psi_injective

Plain-language statement

ψ is injective (Hachi [NOZ26, §3, Theorem 2]). The trace form (a,b) ↦ ⟨a,b⟩ is non-degenerate (testing against b = eⱼ recovers aⱼ), and d/k is a unit in R_q (it is a power of 2, invertible since q is odd). So ψ(a) = ψ(b) forces ⟨a,eⱼ⟩ = ⟨b,eⱼ⟩, i.e. aⱼ = bⱼ, for every j.

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
Project-declaredLean 4.31.0

Trace H psi mul conj

ArkLib.Lattices.CyclotomicModulus.traceH_psi_mul_conj

Plain-language statement

Hachi [NOZ26, §3, Theorem 2]: Tr_H(ψ(a)·σ_{-1}(ψ(b))) = (d/k)·⟨a,b⟩, where ⟨a,b⟩ = Σ_i a_i b_i is the inner product over R_q^H. Expand the product as a double sum, pull the R_q^H-coefficients out of Tr_H (traceH_smul_fixed), evaluate the monomial kernel (traceH_kernel, which is (d/k)·[p=q]), and collapse the diagonal.

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

Trace H sum

ArkLib.Lattices.CyclotomicModulus.traceH_sum

Plain-language statement

Tr_H distributes over finite sums (it is additive).

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record