Report convention repair: middleRepair_j_endpoint_limit

Proved

Freiman.middleRepair_j_endpoint_limit

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

continued-fractionsformalizationlagrange-spectrum

Both endpoints of J_k tend to the common compatible all-3 completion. The report uses |φ3′|≤1/9 and the fixed point (sqrt 13−3)/2. 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_j_endpoint_limit :
    ∀ c : MiddleCore,
      Filter.Tendsto (fun k : ℕ => (middleBounds (middleRepairJ c k)).1) Filter.atTop (nhds (middleLimitValue c)) ∧
      Filter.Tendsto (fun k : ℕ => (middleBounds (middleRepairJ c k)).2) Filter.atTop (nhds (middleLimitValue c)) := 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:sec:jfamily, limiting point Repair: active m2b_body.tex lines 46–48 and §11 physical-cylinder argument.

View graph