Equiangular lines with a fixed angle | Lean AI formalization leaderboard

Problem statement

Notes: Unavailable.

Source: Z. Jiang, J. Tidor, Y. Yao, S. Zhang, and Y. Zhao, `Equiangular lines with a fixed angle`, Annals of Math, 194 (3) 2021. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge (v1.0.0, e32eb14), AnnalsChallenge/AnnalsOfMathematics/2021-194-3-EquiangularLinesFixedAngle.lean

Informal solution: Unavailable.

theorem declaration uses `sorry`theorem_1_2 (α : ℝ) (hα : α ∈ Set.Ioo 0 1) :
    let k := spectralRadiusOrder ((1 - α) / (2 * α))
    (k < ⊤ → ∀ᶠ d in atTop, N α d = ⌊(k.toNat * (d - 1) : ℝ) / (k.toNat - 1 : ℝ)⌋₊) ∧
    (k = ⊤ → ∃ e : ℕ → ℝ, e =o[atTop] (Nat.cast : ℕ → ℝ) ∧ ∀ d, N α d = d + e d) := byα:ℝhα:α ∈ Set.Ioo 0 1⊢ let k := spectralRadiusOrder ((1 - α) / (2 * α));
(k < ⊤ → ∀ᶠ (d : ℕ) in atTop, N α d = ⌊↑k.toNat * (↑d - 1) / (↑k.toNat - 1)⌋₊) ∧
  (k = ⊤ → ∃ e, e =o[atTop] Nat.cast ∧ ∀ (d : ℕ), ↑(N α d) = ↑d + e d)
  sorryAll goals completed! 🐙