trunk endpoint strict mixed
OpenFreiman.trunk_endpoint_strict_mixedalgebracontinued-fractionsformalization
For opposite whole-word parity, compare the natural endpoint with the virtual endpoint after appending1 to the actual wider side. The exact ordered tail ranges give strict endpoint order in both normalization branches, retaining the incoming side at equality.
Preamble
import Definitions.Def_Freiman_trunkGeometry import Mathlib.Tactic.FinCases import Mathlib.Tactic.Linarith open Freiman
Formal statement
theorem Freiman.trunk_endpoint_strict_mixed (p : LowerPair) (hp : p.1.length % 2 ≠ p.2.length % 2) :
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.