Freiman late: late fork endpoints
ProvedFreiman.late_fork_endpointsfinite-certificatesfreimanhall-raylate
Actual incoming-order alignment of every source goodness fork. When the right side was wider, lowerChild swaps the pair before appending, while the source endpoint record retains physical order. This lemma must justify the resulting endpoint equality, including any child width tie; no unconditional swap identity is assumed.
Preamble
import Definitions.Def_Freiman_lateGeometry import Mathlib.Tactic set_option maxRecDepth 8000 set_option maxHeartbeats 0 open Freiman
Formal statement
theorem Freiman.late_fork_endpoints (p : LowerPair) (path : LatePath) (hm : lateMatches p path.right3) (hv : latePathValid lateCatalog path) (hn : ∀ n ∈ path.normalizations, lateNormalizationHolds p n) : lateForkAlignment p path := 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.