Freiman late: late endpoint from width cf
ProvedFreiman.late_endpoint_from_width_cffinite-certificatesfreimanhall-raylate
Selected-mode endpoint identity for actual outward prefixes. Reconstruct the source strict-normalization alternatives and 7/5 shortening from the shared continuant and width identities. The old odd–odd case uses the increasing coordinate −t and flips lower/upper; right suffix 1 or 2 shares the 31 representative only because every queried right addition is nonempty.
Preamble
import Definitions.Def_Freiman_lateGeometry import Mathlib.Tactic set_option maxRecDepth 8000 set_option maxHeartbeats 0 open Freiman
Formal statement
theorem Freiman.late_endpoint_from_width_cf (hcf : ∀ (w : List ℕ+) (z : CertField), 0 ≤ certFieldVal z → certFieldVal (lowerHistoryCF w z) = prefixEval w (certFieldVal z)) (hw : LowerHistoryWidthLaw) : lateEndpointLaw := by sorry
Source
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.