Freiman late: late proof sound
ProvedFreiman.late_proof_soundfinite-certificatesfreimanhall-raylate
The late arithmetic forest is sound relative to the shared Bernstein checker.
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_sound : ∀ 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.