Report convention repair: middleRepair_mixed31_width_from_real_bounds

Proved

Freiman.middleRepair_mixed31_width_from_real_bounds

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

continued-fractionsformalizationlagrange-spectrum

Specialize the real C31 comparisons using the exact full width identity K/q; check positive q and parameter denominators, both physical orientations and the post-child normalization. This draft uses the report-normalized child convention, preserving actual incoming order at equal widths.

Preamble

import Definitions.Def_Freiman_middleRepair

open Freiman

Formal statement

theorem Freiman.middleRepair_mixed31_width_from_real_bounds :
    (∀ p s : ℝ, p ∈ Set.Icc (1/4:ℝ) (4/5) → s ∈ Set.Icc (1/4:ℝ) (4/5) → middleScalarA p s (55/100)<(19/5:ℝ)*middleMixedK p s ∧ (5/19:ℝ)*middleMixedK p s<middleScalarB p s (328/1000)) →
    ∀ c : MiddleCore, middleRegular c → middleRowCondition c .mixedC →
      middleRatio (middleRepairChild c [3] [1]) < (19/5:ℝ) := by
  sorry

Source

Freiman's Hall ray: Proof report and corrected English text, 8 September 2026, Part III, active source staging/m2b/m2b_body.tex, m2b:lem:mixed31width Repair: active m2b_body.tex lines 46–48 and §11 physical-cylinder argument.

View graph