Freiman §14: section14 parameter state
ProvedFreiman.section14_parameter_statefinite-certificatesfreimanhall-raysection14
An admissible mixed parent has one of the sixteen geometry states and its actual continuant ratios lie in that closed rectangle. The language states 313 and 3131 preserve every future natural-shortening flag and are covered by the respective 3 and 31 geometry states.
Preamble
import Definitions.Def_Freiman_section14Geometry import Mathlib.Tactic.FinCases open Freiman
Formal statement
theorem Freiman.section14_parameter_state (t : ℝ) (p : LowerPair) (hs : lowerState t p) (hm : lowerMixed p) : ∃ i : Fin 16, section14Matches p (section14State section14Catalog (i.val+1)) ∧ certRectangleMem (section14State section14Catalog (i.val+1)).rectangle (section14R p) (section14S p) := by sorry
Source
Freiman report, active §14; Appendix Complete finite certificates for the scalar geometry of §14; full_readable_model.json.