Freiman.lowerHistory_sign_from_quadratic

import Definitions.Def_Freiman_lowerHistoryVerification
import Mathlib.Tactic

open Freiman

theorem Freiman.lowerHistory_sign_from_quadratic (hq : ∀ a b : ℚ, (lowerHistoryQuadSign a b 3 = 0 ↔ (a:ℝ)+b*Real.sqrt 3=0) ∧ (0<lowerHistoryQuadSign a b 3 ↔ 0<(a:ℝ)+b*Real.sqrt 3)) (z : CertField) :
    (lowerHistorySign z = 0 ↔ certFieldVal z = 0) ∧ (0 < lowerHistorySign z ↔ 0 < certFieldVal z) := by
  sorry