Report convention repair: middleRepair_good_gap_bound

Proved

Freiman.middleRepair_good_gap_bound

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

continued-fractionsformalizationlagrange-spectrum

Because each child cover lies in its compatible sum hull, child intersection forces the narrower width to be at least the wider-side separating gap. 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_good_gap_bound :
    ∀ c : MiddleCore, middleRegular c → middleRepairGood c →
      middleGapFraction (middleParameter (middleNormalized c).left) * middleWidth (middleNormalized c).left  ≤  middleWidth (middleNormalized c).right := 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:good5 Repair: active m2b_body.tex lines 46–48 and §11 physical-cylinder argument.

View graph