trunk endpoint strict order
OpenFreiman.trunk_endpoint_strict_orderalgebracontinued-fractionsformalization
Every ordinary source cover has distinct correctly ordered endpoints; this strict own-interval order is separate from crossed contact inequalities.
Preamble
import Definitions.Def_Freiman_trunkGeometry import Mathlib.Tactic.FinCases import Mathlib.Tactic.Linarith open Freiman
Formal statement
theorem Freiman.trunk_endpoint_strict_order (p : LowerPair) :
lowerEndpoint p false < lowerEndpoint p true := by
sorrySource
Report Proposition4.1 s15:trunk, printed report p28; original source pp120–126. Complete sixteen-state trunk certificate,58230 records,90 case plans, with three explicitly unfilled interfaces.