Freiman late: late greater from sign

Proved

Freiman.late_greater_from_sign

by tp · Sep 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

finite-certificatesfreimanhall-raylate

One continuant-difference identity transfers the scalar threshold comparison to actual endpoint values, including strict comparisons. All four tails are nonnegative, so the omitted denominators are positive; an identical pair of tails cannot justify strictness.

Preamble

import Definitions.Def_Freiman_lateGeometry
import Mathlib.Tactic

set_option maxRecDepth 8000
set_option maxHeartbeats 0

open Freiman

Formal statement

theorem Freiman.late_greater_from_sign (hsg : ∀ z : CertField, (lowerHistorySign z = 0 ↔ certFieldVal z = 0) ∧ (0 < lowerHistorySign z ↔ 0 < certFieldVal z)) : lateGreaterLaw := 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.

View graph