Freiman late: late checks from endpoint comparison
ProvedFreiman.late_checks_from_endpoint_comparisonfinite-certificatesfreimanhall-raylate
Finite-list transfer: use a validated active endpoint mode for each comparison, derive tail nonnegativity from the directed bounds, and apply the exact strict/weak comparison law. Membership in the eighteen-label family guarantees both queried additions are 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_checks_from_endpoint_comparison (he : lateEndpointLaw) (hg : lateGreaterLaw) (hl : ∀ z : CertField, (certFieldLower z : ℝ) ≤ certFieldVal z) : lateChecksLaw := 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.