Freiman late: late proof from witness
ProvedFreiman.late_proof_from_witnessfinite-certificatesfreimanhall-raylate
Generic semantics of the indexed arithmetic proof forest: a pair cites only present premises and its exact rectangle; each rectangle split covers its closed parent. Fuel is consumed at each descent, so a cycle cannot certify a contradiction.
Preamble
import Definitions.Def_Freiman_lateGeometry import Mathlib.Tactic set_option maxRecDepth 8000 set_option maxHeartbeats 0 open Freiman
Formal statement
theorem Freiman.late_proof_from_witness (hw : ∀ w : CertWitness, certWitnessValid w → ∀ r s q : ℝ, certRectangleMem w.rectangle r s → ¬ (certBoundHolds w.lowerBound r s q ∧ certBoundHolds w.upperBound r s q)) : ∀ C : LateCatalog, lateAllWitnesses C → lateProofSound C := 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.