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

1 topic

35 results

Clear filters
Project-declaredLean 4.31.0

F₂ eq zero

f₂_eq_zero

Plain-language statement

From g = 0 and h = 0, deduce f₂ = 0. Proof: From g = 0 we get a relation between f₂ and f₄. Combined with h = 0, we show f₄² · (3 · H_sum_sq) = 0. Since H_sum_sq → 1 ≠ 0, we get f₄ = 0, then f₂ = 0 follows from h = f₂² = 0.

sphere packingFourier analysismodular forms

Source project: Sphere Packing in Dimension 8

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

F₂ S action

f₂_S_action

Plain-language statement

f₂ transforms under S as f₂|S = -f₄. Proof outline using serre_D_slash_equivariant: 1. (serre_D 2 H₂)|[4]S = serre_D 2 (H₂|[2]S) = serre_D 2 (-H₄) = -serre_D 2 H₄ 2. (H₂(H₂ + 2H₄))|[4]S = (-H₄)((-H₄) + 2(-H₂)) = H₄(H₄ + 2H₂) 3. f₂|[4]S = -serre_D 2 H₄ - (1/6)H₄(H₄ + 2H₂) = -f₄ Key lemmas used: - serre_D_slash_equivariant: (serre_D k F)|[k+2]γ = serre_D k...

sphere packingFourier analysismodular forms

Source project: Sphere Packing in Dimension 8

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

F₂ T action

f₂_T_action

Plain-language statement

f₂ transforms under T as f₂|T = -f₂. Proof outline: 1. (serre_D 2 H₂)|[4]T = serre_D 2 (H₂|[2]T) = serre_D 2 (-H₂) = -serre_D 2 H₂ 2. (H₂(H₂ + 2H₄))|[4]T = (-H₂)((-H₂) + 2H₃) Using Jacobi H₃ = H₂ + H₄: -H₂ + 2H₃ = -H₂ + 2(H₂ + H₄) = H₂ + 2H₄ So: (H₂(H₂ + 2H₄))|[4]T = (-H₂)(H₂ + 2H₄) 3. f₂|[4]T = -serre_D 2 H₂ - (1/6)(-H₂)(H₂ + 2H₄) = -serre_D 2 H₂ + (1/6)...

sphere packingFourier analysismodular forms

Source project: Sphere Packing in Dimension 8

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

F₂ tendsto at Im Infty

f₂_tendsto_atImInfty

Plain-language statement

f₂ tends to 0 at infinity. Proof: f₂ = serre_D 2 H₂ - (1/6)H₂(H₂ + 2H₄) Since H₂ → 0, both serre_D 2 H₂ → 0 and H₂(H₂ + 2H₄) → 0, so f₂ → 0.

sphere packingFourier analysismodular forms

Source project: Sphere Packing in Dimension 8

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

F₄ S action

f₄_S_action

Plain-language statement

f₄ transforms under S as f₄|S = -f₂. Proof outline (symmetric to f₂_S_action): 1. (serre_D 2 H₄)|[4]S = serre_D 2 (H₄|[2]S) = serre_D 2 (-H₂) = -serre_D 2 H₂ 2. (H₄(2H₂ + H₄))|[4]S = (-H₂)(2(-H₄) + (-H₂)) = H₂(H₂ + 2H₄) 3. f₄|[4]S = -serre_D 2 H₂ + (1/6)H₂(H₂ + 2H₄) = -f₂

sphere packingFourier analysismodular forms

Source project: Sphere Packing in Dimension 8

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

F₄ sq mul eq

f₄_sq_mul_eq

Plain-language statement

Key algebraic identity for proving f₂ = f₄ = 0. Given Af₂ + Bf₄ = 0, we have f₄² * (A² - AB + B²) = A² * (f₂² + f₂f₄ + f₄²).

sphere packingFourier analysismodular forms

Source project: Sphere Packing in Dimension 8

Person-level attribution pending.

View proof record