Freiman.lowerHistory_quad_sign_value
ProvedFreiman.lowerHistory_quad_sign_valuehall-raynumber-theory
Specialized quadratic sign comparison for d=3; no false d=0 generalization.
Preamble
import Definitions.Def_Freiman_lowerHistoryVerification import Mathlib.Tactic open Freiman
Formal statement
theorem Freiman.lowerHistory_quad_sign_value (a b : ℚ) :
(lowerHistoryQuadSign a b 3 = 0 ↔ (a:ℝ)+b*Real.sqrt 3 = 0) ∧
(0 < lowerHistoryQuadSign a b 3 ↔ 0 < (a:ℝ)+b*Real.sqrt 3) := by
sorrySource
Freiman's Hall ray: Proof report and corrected English text (8 September 2026); lower_core.tex, eq:lc-difference and eq:lc-full-width; history_certificates.tex, app:all-suffix-histories; verification/families/section15_late/independent_engine.py and verification/families/target_selection/verify_h5_original_independent.py; role: certificate field arithmetic