theorem Hex.RCF.Sign.ofInt_spec (value : ℤ) : SignType.sign ↑(ofInt value).toInt = SignType.sign ↑value

Collapsing an integer preserves its mathematical sign.

theorem Polynomial.sign_eq_of_noRoot {p : Polynomial ℝ} {s : Set ℝ} (hs : IsPreconnected s) (hnz : ∀ z ∈ s, ¬p.IsRoot z) {x y : ℝ} (hx : x ∈ s) (hy : y ∈ s) : SignType.sign (eval x p) = SignType.sign (eval y p)

The sign of a continuous polynomial evaluation is constant on a preconnected set containing no root of the polynomial.

theorem Hex.RCF.evalSign_spec (p : ZPoly) (x : Dyadic) : SignType.sign ↑(evalSign p x).toInt = SignType.sign (Polynomial.eval (HexRealRootsMathlib.Dyadic.toReal x) (HexRealRootsMathlib.toPolyℝ p))

Exact dyadic Horner evaluation computes the sign of the corresponding real-polynomial evaluation.

theorem Hex.RCF.eval_eq_at_zero (p : ZPoly) (hdegree : ¬0 < DensePoly.natDegree p) (x : ℝ) : Polynomial.eval x (HexRealRootsMathlib.toPolyℝ p) = Polynomial.eval 0 (HexRealRootsMathlib.toPolyℝ p)

A polynomial whose executable degree is not positive is constant after casting, including the zero polynomial.

theorem Hex.RCF.sign_eval_eq_open {carrier : ZPoly} {replay : SturmReplay} (hreplay : SturmReplay.check carrier replay = true) {isolations : IsolationCert} (hstrict : IsolationCert.checkStrict replay isolations = true) {atom : ZPoly} (hroot : ∀ (z : ℝ), (HexRealRootsMathlib.toPolyℝ atom).IsRoot z → (HexRealRootsMathlib.toPolyℝ carrier).IsRoot z) (cut : Fin (isolations.intervals.size + 1)) {x : ℝ} (hx : Cell.Sem (isolations.rootModel hreplay hstrict) (Cell.open cut) x) : SignType.sign (Polynomial.eval (HexRealRootsMathlib.Dyadic.toReal (isolations.openPoint cut)) (HexRealRootsMathlib.toPolyℝ atom)) = SignType.sign (Polynomial.eval x (HexRealRootsMathlib.toPolyℝ atom))

Sign constancy on an open carrier cell from root containment.

theorem Hex.RCF.evalSign_open_spec {carrier : ZPoly} {replay : SturmReplay} (hreplay : SturmReplay.check carrier replay = true) {isolations : IsolationCert} (hstrict : IsolationCert.checkStrict replay isolations = true) {atom : ZPoly} (hroot : ∀ (z : ℝ), (HexRealRootsMathlib.toPolyℝ atom).IsRoot z → (HexRealRootsMathlib.toPolyℝ carrier).IsRoot z) (cut : Fin (isolations.intervals.size + 1)) {x : ℝ} (hx : Cell.Sem (isolations.rootModel hreplay hstrict) (Cell.open cut) x) : SignType.sign ↑(evalSign atom (isolations.openPoint cut)).toInt = SignType.sign (Polynomial.eval x (HexRealRootsMathlib.toPolyℝ atom))

The exact dyadic sign is valid at every point of an open carrier cell.

theorem Hex.RCF.evalSign_open_of_atom {sentence : Sentence} {carrier : CarrierCert} (hcarrier : CarrierCert.check sentence carrier = true) {isolations : IsolationCert} (hstrict : IsolationCert.checkStrict carrier.replay isolations = true) {atom : ZPoly} (hatom : atom ∈ sentence.polys) (cut : Fin (isolations.intervals.size + 1)) {x : ℝ} (hx : Cell.Sem (isolations.rootModel ⋯ hstrict) (Cell.open cut) x) : SignType.sign ↑(evalSign atom (isolations.openPoint cut)).toInt = SignType.sign (Polynomial.eval x (HexRealRootsMathlib.toPolyℝ atom))

Every nonconstant sentence atom has its exact sampled sign throughout an open cell of an accepted carrier decomposition.

theorem Hex.RCF.sign_eval_eq_leftRoot {carrier atom : ZPoly} {cert : IsolationCert} (model : RootModel carrier cert) (hroot : ∀ (z : ℝ), (HexRealRootsMathlib.toPolyℝ atom).IsRoot z → (HexRealRootsMathlib.toPolyℝ carrier).IsRoot z) (i : Fin cert.intervals.size) (hnonzero : ¬(HexRealRootsMathlib.toPolyℝ atom).IsRoot (model.root i)) {sample : ℝ} (hsample : Cell.Sem model (Cell.open i.castSucc) sample) : SignType.sign (Polynomial.eval sample (HexRealRootsMathlib.toPolyℝ atom)) = SignType.sign (Polynomial.eval (model.root i) (HexRealRootsMathlib.toPolyℝ atom))

A nonzero atom has the same sign at carrier root i as on the open cell immediately to its left.

theorem Hex.RCF.evalSign_leftRoot {carrier atom : ZPoly} {replay : SturmReplay} {isolations : IsolationCert} (hreplay : SturmReplay.check carrier replay = true) (hstrict : IsolationCert.checkStrict replay isolations = true) (hroot : ∀ (z : ℝ), (HexRealRootsMathlib.toPolyℝ atom).IsRoot z → (HexRealRootsMathlib.toPolyℝ carrier).IsRoot z) (i : Fin isolations.intervals.size) (hnonzero : ¬(HexRealRootsMathlib.toPolyℝ atom).IsRoot ((isolations.rootModel hreplay hstrict).root i)) : SignType.sign ↑(evalSign atom (isolations.openPoint i.castSucc)).toInt = SignType.sign (Polynomial.eval ((isolations.rootModel hreplay hstrict).root i) (HexRealRootsMathlib.toPolyℝ atom))

Exact left-open sample sign at a carrier root where the atom does not vanish.

theorem Hex.RCF.evalSign_commonLeft {sentence : Sentence} {carrier : CarrierCert} (hcarrier : CarrierCert.check sentence carrier = true) {isolations : IsolationCert} (hstrict : IsolationCert.checkStrict carrier.replay isolations = true) {atom : ZPoly} (hatom : atom ∈ sentence.polys) {common : CommonRootCert} (hcommon : CommonRootCert.check atom carrier.carrier common = true) (i : Fin isolations.intervals.size) (hnonroot : common.hasRoot isolations.intervals[i] = false) : SignType.sign ↑(evalSign atom (isolations.openPoint i.castSucc)).toInt = SignType.sign (Polynomial.eval ((isolations.rootModel ⋯ hstrict).root i) (HexRealRootsMathlib.toPolyℝ atom))

A false cached common-root query certifies the exact nonzero root-cell sign using the canonical left open sample.

theorem Hex.RCF.evalSign_ne_zero (p : ZPoly) (x : Dyadic) (hroot : ¬(HexRealRootsMathlib.toPolyℝ p).IsRoot (HexRealRootsMathlib.Dyadic.toReal x)) : evalSign p x ≠ Sign.zero

Exact evaluation cannot report zero at a certified nonroot.

theorem Hex.RCF.openCellSign_spec {sentence : Sentence} {carrier : CarrierCert} (hcarrier : CarrierCert.check sentence carrier = true) {isolations : IsolationCert} (hstrict : IsolationCert.checkStrict carrier.replay isolations = true) {p : ZPoly} (hp : p ∈ sentence.formula.polys) (cut : Fin (isolations.intervals.size + 1)) {x : ℝ} (hx : Cell.Sem (isolations.rootModel ⋯ hstrict) (Cell.open cut) x) : ∃ (sign : Sign), openCellSign? p isolations cut = some sign ∧ SignType.sign ↑sign.toInt = SignType.sign (Polynomial.eval x (HexRealRootsMathlib.toPolyℝ p))

The shared open-cell lookup is total and exact for every formula atom of a checked carrier, including constants.

theorem Hex.RCF.SignMatrixCert.signWith?_spec {sentence : Sentence} {carrier : CarrierCert} {cert : SignMatrixCert} {isolations : IsolationCert} (hcarrier : CarrierCert.check sentence carrier = true) (hstrict : IsolationCert.checkStrict carrier.replay isolations = true) (hmatrix : check sentence carrier cert = true) {commonPolys : List ZPoly} (hpolys : commonPolys = dedupPolys sentence.polys) {p : ZPoly} (hp : p ∈ sentence.formula.polys) (cell : Cell isolations.intervals.size) : ∃ (sign : Sign), cert.signWith? commonPolys isolations cell p = some sign ∧ ∀ (x : ℝ), Cell.Sem (isolations.rootModel ⋯ hstrict) cell x → SignType.sign ↑sign.toInt = SignType.sign (Polynomial.eval x (HexRealRootsMathlib.toPolyℝ p))

A checked sign-matrix package returns a total exact sign for every atom on every semantic carrier cell when given the checker-derived package order.

theorem Hex.RCF.SignMatrixCert.sign?_spec {sentence : Sentence} {carrier : CarrierCert} {cert : SignMatrixCert} {isolations : IsolationCert} (hcarrier : CarrierCert.check sentence carrier = true) (hstrict : IsolationCert.checkStrict carrier.replay isolations = true) (hmatrix : check sentence carrier cert = true) {p : ZPoly} (hp : p ∈ sentence.formula.polys) (cell : Cell isolations.intervals.size) : ∃ (sign : Sign), cert.sign? sentence isolations cell p = some sign ∧ ∀ (x : ℝ), Cell.Sem (isolations.rootModel ⋯ hstrict) cell x → SignType.sign ↑sign.toInt = SignType.sign (Polynomial.eval x (HexRealRootsMathlib.toPolyℝ p))

Public atom-sign lookup is total and exact under the combined checker.

theorem Hex.RCF.Cmp.evalSign_iff {cmp : Cmp} {sign : Sign} {value : ℝ} (hsign : SignType.sign ↑sign.toInt = SignType.sign value) : cmp.evalSign sign = true ↔ cmp.toProp value 0

Comparison evaluation depends only on the mathematical sign.

theorem Hex.RCF.Atom.toProp_iff_eval (a : Atom) (x : ℝ) : a.toProp x ↔ a.cmp.toProp (Polynomial.eval x (HexRealRootsMathlib.toPolyℝ a.p)) 0

Relate the reflected atom semantics to real-cast polynomial evaluation.

theorem Hex.RCF.Formula.evalSigns_spec {formula : Formula} {signOf : ZPoly → Option Sign} {x : ℝ} (hlookup : ∀ p ∈ formula.polys, ∃ (sign : Sign), signOf p = some sign ∧ SignType.sign ↑sign.toInt = SignType.sign (Polynomial.eval x (HexRealRootsMathlib.toPolyℝ p))) : ∃ (value : Bool), evalSigns signOf formula = some value ∧ (value = true ↔ formula.toProp x)

Formula evaluation returns a Boolean whose truth is exactly the semantic formula, provided every referenced polynomial lookup carries its exact sign. The existential result also supplies the false direction required by negation and implication.

theorem Hex.RCF.Formula.evalSigns_eq_true_iff {formula : Formula} {signOf : ZPoly → Option Sign} {x : ℝ} (hlookup : ∀ p ∈ formula.polys, ∃ (sign : Sign), signOf p = some sign ∧ SignType.sign ↑sign.toInt = SignType.sign (Polynomial.eval x (HexRealRootsMathlib.toPolyℝ p))) : evalSigns signOf formula = some true ↔ formula.toProp x

Successful true formula evaluation is equivalent to the reflected semantics at the point.

theorem Hex.RCF.Formula.evalConstants_eq_true_iff {formula : Formula} (hconstant : ∀ p ∈ formula.polys, ¬0 < DensePoly.natDegree p) (x : ℝ) : formula.evalConstants? = some true ↔ formula.toProp x

Constant-only formula evaluation is exact at every real point, including formulas containing the zero polynomial.

theorem Hex.RCF.SignMatrixCert.evalCell_spec {sentence : Sentence} {carrier : CarrierCert} {cert : SignMatrixCert} {isolations : IsolationCert} (hcarrier : CarrierCert.check sentence carrier = true) (hstrict : IsolationCert.checkStrict carrier.replay isolations = true) (hmatrix : check sentence carrier cert = true) (cell : Cell isolations.intervals.size) : ∃ (value : Bool), cert.evalCell? sentence isolations cell = some value ∧ ∀ (x : ℝ), Cell.Sem (isolations.rootModel ⋯ hstrict) cell x → (value = true ↔ sentence.formula.toProp x)

A checked package computes one Boolean valid uniformly throughout each semantic carrier cell.

theorem Hex.RCF.SignMatrixCert.evalCell_eq_true_iff {sentence : Sentence} {carrier : CarrierCert} {cert : SignMatrixCert} {isolations : IsolationCert} (hcarrier : CarrierCert.check sentence carrier = true) (hstrict : IsolationCert.checkStrict carrier.replay isolations = true) (hmatrix : check sentence carrier cert = true) {cell : Cell isolations.intervals.size} {x : ℝ} (hx : Cell.Sem (isolations.rootModel ⋯ hstrict) cell x) : cert.evalCell? sentence isolations cell = some true ↔ sentence.formula.toProp x

The computed true value is exactly the reflected formula semantics at every point of the checked cell.