Prove2Me

middle endpoint order

Proved
Freiman.middle_endpoint_order

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

continued-fractionsformalizationlagrange-spectrum

The exact shortened/normal endpoint alternatives are ordered; for mixed parity, the C01 and C10 alternatives meet, including normalization and shortening equalities.

Preamble
import Definitions.Def_Freiman_middleRoots
Formal statement
namespace Freiman

theorem middle_endpoint_order :
    ∀ c : MiddleCore, middleRegular c → (middleBounds c).1  ≤  (middleBounds c).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, cover convention, before m2b:sec:good

View graph