middle secondary four separations

Proved

Freiman.middle_secondary_four_separations

by tp · Sep 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

continued-fractionsformalizationlagrange-spectrum

The eight two-4 roots have strictly larger exterior left tail x than right tail y for every allowed completion; the eight exact positive lower bounds are in the dominance table.

Preamble

import Definitions.Def_Freiman_middleRoots

Formal statement

namespace Freiman

theorem middle_secondary_four_separations :
    ∀ (r : Fin 15) (a : ℤ→ℕ+), middleCompatible (middleRoot r) a → (r.val∈[5,6,7,8,9,10,11,13]) →
      cfValue (fun n : ℕ => a (-(n:ℤ)-1)) > cfValue (fun n : ℕ => a ((n:ℤ)+2)) := by
  sorry

end Freiman

Source

Freiman's Hall ray: Proof report and corrected English text, 8 September 2026, Part III, active source staging/m2b/m2b_body.tex, m2b:sec:centers, dominance table

View graph