Freiman late: late parameter case
ProvedFreiman.late_parameter_casefinite-certificatesfreimanhall-raylate
The actual normalized continuant ratios lie in the full closed late rectangle [13/17,4/5]×[1/4,4/5], or its right-suffix-3 subrectangle with s≤1/3. This is a finite suffix/continuant fact; hr is the unchanged long-route hypothesis.
Preamble
import Definitions.Def_Freiman_lateGeometry import Mathlib.Tactic set_option maxRecDepth 8000 set_option maxHeartbeats 0 open Freiman
Formal statement
theorem Freiman.late_parameter_case (t : ℝ) (p : LowerPair) (hs : lowerState t p)
(hd : ¬ lowerMixed p ∧ ¬ lowerA p 3 ∧ ¬ lowerA p 9 ∧ lowerL p ∧ ¬ lowerLStar p)
(hr : (13/17 : ℝ) ≤ lowerRatio (lowerNormalize p).1) :
∃ right3 : Bool, lateMatches p right3 ∧
certRectangleMem (lateRootRectangle right3) (lateR p) (lateS p) := by
sorrySource
Freiman report, §15, printed source pages 140–144; active lower_140_144.tex and Appendix Complete finite certificates for printed pages 140–144 (late_certificates.tex); exact late_readable_certificates.json with both original cover_*_certificate.json trees.