inductive Hex.RCF.Sign : Type

The three possible signs stored by an RCF sign matrix.

• neg : Sign

  A negative value.

• zero : Sign

  A zero value.

• pos : Sign

  A positive value.

@[instance_reducible]

instance Hex.RCF.instDecidableEqSign : DecidableEq Sign

Equations

• Hex.RCF.instDecidableEqSign x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Hex.RCF.instReprSign.repr : Sign → Nat → Std.Format

Equations

• Hex.RCF.instReprSign.repr Hex.RCF.Sign.neg prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hex.RCF.Sign.neg")).group prec✝
• Hex.RCF.instReprSign.repr Hex.RCF.Sign.zero prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hex.RCF.Sign.zero")).group prec✝
• Hex.RCF.instReprSign.repr Hex.RCF.Sign.pos prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hex.RCF.Sign.pos")).group prec✝

@[instance_reducible]

instance Hex.RCF.instReprSign : Repr Sign

Equations

• Hex.RCF.instReprSign = { reprPrec := Hex.RCF.instReprSign.repr }

def Hex.RCF.Sign.toInt : Sign → Int

Canonical integer representative of a stored sign.

Equations

• Hex.RCF.Sign.neg.toInt = -1
• Hex.RCF.Sign.zero.toInt = 0
• Hex.RCF.Sign.pos.toInt = 1

def Hex.RCF.Sign.ofInt (value : Int) : Sign

Collapse an arbitrary integer to its three-way sign.

Equations

• Hex.RCF.Sign.ofInt value = if value < 0 then Hex.RCF.Sign.neg else if 0 < value then Hex.RCF.Sign.pos else Hex.RCF.Sign.zero

def Hex.RCF.evalSign (p : ZPoly) (x : Dyadic) : Sign

Exact executable sign of an integer polynomial at a dyadic point.

Equations

• Hex.RCF.evalSign p x = Hex.RCF.Sign.ofInt (Hex.dyadicSign (p.evalDyadic x))

def Hex.RCF.containsPoly (p : ZPoly) : List ZPoly → Bool

Coefficient-equality membership test for literal polynomials. This avoids the derived array equality that does not kernel-reduce through modules.

Equations

• Hex.RCF.containsPoly p [] = false
• Hex.RCF.containsPoly p (q :: qs) = (Hex.DensePoly.beqCoeffs p q || Hex.RCF.containsPoly p qs)

theorem Hex.RCF.containsPoly_iff {p : ZPoly} {ps : List ZPoly} : containsPoly p ps = true ↔ p ∈ ps

Coefficient-based polynomial membership agrees with list membership.

theorem Hex.RCF.containsPoly_eq_false_iff {p : ZPoly} {ps : List ZPoly} : containsPoly p ps = false ↔ ¬p ∈ ps

The coefficient-equality membership test is false exactly on nonmembership.

def Hex.RCF.dedupPolysAux (seen : List ZPoly) : List ZPoly → List ZPoly

First-occurrence-preserving duplicate removal with an explicit seen set.

Equations

• Hex.RCF.dedupPolysAux seen [] = []
• Hex.RCF.dedupPolysAux seen (q :: qs) = if Hex.RCF.containsPoly q seen = true then Hex.RCF.dedupPolysAux seen qs else q :: Hex.RCF.dedupPolysAux (q :: seen) qs

def Hex.RCF.dedupPolys (ps : List ZPoly) : List ZPoly

Deterministic first-occurrence-preserving duplicate removal using only coefficient equality.

Equations

• Hex.RCF.dedupPolys ps = Hex.RCF.dedupPolysAux [] ps

theorem Hex.RCF.mem_dedupPolysAux {p : ZPoly} {seen ps : List ZPoly} : p ∈ dedupPolysAux seen ps ↔ p ∈ ps ∧ ¬p ∈ seen

A polynomial survives duplicate removal exactly when it occurs in the input and has not already occurred in seen.

theorem Hex.RCF.mem_dedupPolys {p : ZPoly} {ps : List ZPoly} : p ∈ dedupPolys ps ↔ p ∈ ps

Duplicate removal preserves polynomial membership.

theorem Hex.RCF.dedupPolysAux_nodup (seen ps : List ZPoly) : (dedupPolysAux seen ps).Nodup

Duplicate removal with an initial seen list produces no duplicate entries.

theorem Hex.RCF.dedupPolys_nodup (ps : List ZPoly) : (dedupPolys ps).Nodup

Duplicate removal produces no duplicate entries.

def Hex.RCF.checkCommon (carrier : ZPoly) : List ZPoly → List CommonRootCert → Bool

Pair a recomputed polynomial order with common-root packages and validate every package. Length mismatches and malformed packages are rejected.

Equations

• Hex.RCF.checkCommon carrier [] [] = true
• Hex.RCF.checkCommon carrier (p :: ps) (common :: commons) = (Hex.RCF.CommonRootCert.check p carrier common && Hex.RCF.checkCommon carrier ps commons)
• Hex.RCF.checkCommon carrier x✝¹ x✝ = false

def Hex.RCF.findCommon? (p : ZPoly) : List ZPoly → List CommonRootCert → Option CommonRootCert

Positional lookup in an aligned common-root package list.

Equations

• Hex.RCF.findCommon? p (q :: qs) (common :: commons) = if Hex.DensePoly.beqCoeffs p q = true then some common else Hex.RCF.findCommon? p qs commons
• Hex.RCF.findCommon? p x✝¹ x✝ = none

theorem Hex.RCF.findCommon?_of_check {carrier p : ZPoly} {ps : List ZPoly} {commons : List CommonRootCert} (hcheck : checkCommon carrier ps commons = true) (hmem : p ∈ ps) : ∃ (common : CommonRootCert), findCommon? p ps commons = some common ∧ CommonRootCert.check p carrier common = true

Checked alignment makes positional lookup total and validates the package against the requested external polynomial.

structure Hex.RCF.SignMatrixCert : Type

Common-root data carried by the sign-matrix layer. No signs or formula truth values are trusted fields: both are recomputed exactly.

• commonRoots : List CommonRootCert

  Proposed common-root certificates. The checker aligns them with the distinct nonconstant atom polynomials in their recomputed order.

def Hex.RCF.openSign? (p : ZPoly) (isolations : IsolationCert) (cut : Fin (isolations.intervals.size + 1)) : Option Sign

Exact sign on an open cell, rejecting zero for a nonconstant atom of a valid carrier decomposition.

Equations

• Hex.RCF.openSign? p isolations cut = match Hex.RCF.evalSign p (isolations.openPoint cut) with | Hex.RCF.Sign.zero => none | sign => some sign

def Hex.RCF.rootSign? (p : ZPoly) (common : CommonRootCert) (isolations : IsolationCert) (i : Fin isolations.intervals.size) : Option Sign

Exact sign on a root cell from the cached common-root zero test, or from the canonical left open sample when the atom does not vanish.

Equations

• Hex.RCF.rootSign? p common isolations i = match common.hasRoot isolations.intervals[i] with | true => some Hex.RCF.Sign.zero | false => Hex.RCF.openSign? p isolations i.castSucc

theorem Hex.RCF.openSign?_eq_some {p : ZPoly} {isolations : IsolationCert} {cut : Fin (isolations.intervals.size + 1)} (hnonzero : evalSign p (isolations.openPoint cut) ≠ Sign.zero) : openSign? p isolations cut = some (evalSign p (isolations.openPoint cut))

A nonzero open-cell evaluation is returned unchanged by openSign?.

def Hex.RCF.openCellSign? (p : ZPoly) (isolations : IsolationCert) (cut : Fin (isolations.intervals.size + 1)) : Option Sign

Exact sign on an open cell, with constant polynomials evaluated once at zero and nonconstant polynomials guarded against an impossible zero sample.

Equations

• Hex.RCF.openCellSign? p isolations cut = if 0 < Hex.DensePoly.natDegree p then Hex.RCF.openSign? p isolations cut else some (Hex.RCF.evalSign p 0)

structure Hex.RCF.SignEntry : Type

One cached sign associated with its literal polynomial.

• poly : ZPoly

  The polynomial whose sign is cached.

• sign : Sign

  The cached sign of the polynomial.

def Hex.RCF.findSign? (p : ZPoly) : List SignEntry → Option Sign

Coefficient-equality lookup in a cached sign row.

Equations

• Hex.RCF.findSign? p [] = none
• Hex.RCF.findSign? p (entry :: entries) = if Hex.DensePoly.beqCoeffs p entry.poly = true then some entry.sign else Hex.RCF.findSign? p entries

def Hex.RCF.buildSigns? (signOf : ZPoly → Option Sign) : List ZPoly → Option (List SignEntry)

Materialize a sign row once for each polynomial in a recomputed distinct order. Any missing sign fails the whole row.

Equations

• Hex.RCF.buildSigns? signOf [] = some []
• Hex.RCF.buildSigns? signOf (q :: qs) = do let sign ← signOf q let entries ← Hex.RCF.buildSigns? signOf qs pure ({ poly := q, sign := sign } :: entries)

theorem Hex.RCF.findSign?_of_build {signOf : ZPoly → Option Sign} {ps : List ZPoly} {entries : List SignEntry} (hbuild : buildSigns? signOf ps = some entries) {p : ZPoly} (hmem : p ∈ ps) : findSign? p entries = signOf p

A row built from an option-valued environment returns exactly that environment on every polynomial included in the row order.

theorem Hex.RCF.buildSigns?_total {signOf : ZPoly → Option Sign} {ps : List ZPoly} (htotal : ∀ (p : ZPoly), p ∈ ps → ∃ (sign : Sign), signOf p = some sign) : ∃ (entries : List SignEntry), buildSigns? signOf ps = some entries

A total option-valued environment builds a complete cached row.

def Hex.RCF.SignMatrixCert.check (sentence : Sentence) (carrier : CarrierCert) (cert : SignMatrixCert) : Bool

Recompute the distinct nonconstant atom order and validate exact package alignment against the checked carrier.

Equations

• Hex.RCF.SignMatrixCert.check sentence carrier cert = Hex.RCF.checkCommon carrier.carrier (Hex.RCF.dedupPolys sentence.polys) cert.commonRoots

def Hex.RCF.SignMatrixCert.findCommon? (sentence : Sentence) (cert : SignMatrixCert) (p : ZPoly) : Option CommonRootCert

Look up the package associated with one nonconstant atom.

Equations

• Hex.RCF.SignMatrixCert.findCommon? sentence cert p = Hex.RCF.findCommon? p (Hex.RCF.dedupPolys sentence.polys) cert.commonRoots

theorem Hex.RCF.SignMatrixCert.findCommon?_of_check {sentence : Sentence} {carrier : CarrierCert} {cert : SignMatrixCert} (hcheck : check sentence carrier cert = true) {p : ZPoly} (hmem : p ∈ sentence.polys) : ∃ (common : CommonRootCert), findCommon? sentence cert p = some common ∧ CommonRootCert.check p carrier.carrier common = true

Every recomputed nonconstant atom has a checked package after successful alignment.

def Hex.RCF.SignMatrixCert.signWith? (cert : SignMatrixCert) (commonPolys : List ZPoly) (isolations : IsolationCert) (cell : Cell isolations.intervals.size) (p : ZPoly) : Option Sign

Recompute one atom sign on one carrier cell using a precomputed distinct nonconstant order. Constants use evaluation at zero and consume no common-root package.

Equations

• One or more equations did not get rendered due to their size.
• cert.signWith? commonPolys isolations (Hex.RCF.Cell.open cut) p = Hex.RCF.openCellSign? p isolations cut

def Hex.RCF.SignMatrixCert.sign? (cert : SignMatrixCert) (sentence : Sentence) (isolations : IsolationCert) (cell : Cell isolations.intervals.size) (p : ZPoly) : Option Sign

Public atom-sign lookup, recomputing the deterministic package order.

Equations

• cert.sign? sentence isolations cell p = cert.signWith? (Hex.RCF.dedupPolys sentence.polys) isolations cell p

def Hex.RCF.Cmp.evalSign (cmp : Cmp) (sign : Sign) : Bool

Evaluate a comparison from the sign of its left-hand side.

Equations

• Hex.RCF.Cmp.lt.evalSign sign = (sign == Hex.RCF.Sign.neg)
• Hex.RCF.Cmp.le.evalSign sign = (sign != Hex.RCF.Sign.pos)
• Hex.RCF.Cmp.eq.evalSign sign = (sign == Hex.RCF.Sign.zero)
• Hex.RCF.Cmp.ge.evalSign sign = (sign != Hex.RCF.Sign.neg)
• Hex.RCF.Cmp.gt.evalSign sign = (sign == Hex.RCF.Sign.pos)
• Hex.RCF.Cmp.ne.evalSign sign = (sign != Hex.RCF.Sign.zero)

def Hex.RCF.Formula.evalSigns (signOf : ZPoly → Option Sign) : Formula → Option Bool

Evaluate a formula from an option-valued polynomial-sign environment. Every Boolean branch evaluates both children, so any missing sign fails closed.

Equations

• Hex.RCF.Formula.evalSigns signOf (Hex.RCF.Formula.atom a) = do let sign ← signOf a.p pure (a.cmp.evalSign sign)
• Hex.RCF.Formula.evalSigns signOf Hex.RCF.Formula.tt = some true
• Hex.RCF.Formula.evalSigns signOf Hex.RCF.Formula.ff = some false
• Hex.RCF.Formula.evalSigns signOf φ.not = do let value ← Hex.RCF.Formula.evalSigns signOf φ pure !value
• Hex.RCF.Formula.evalSigns signOf (φ.and ψ) = do let left ← Hex.RCF.Formula.evalSigns signOf φ let right ← Hex.RCF.Formula.evalSigns signOf ψ pure (left && right)
• Hex.RCF.Formula.evalSigns signOf (φ.or ψ) = do let left ← Hex.RCF.Formula.evalSigns signOf φ let right ← Hex.RCF.Formula.evalSigns signOf ψ pure (left || right)
• Hex.RCF.Formula.evalSigns signOf (φ.imp ψ) = do let left ← Hex.RCF.Formula.evalSigns signOf φ let right ← Hex.RCF.Formula.evalSigns signOf ψ pure (!left || right)

def Hex.RCF.Formula.evalConstants? (formula : Formula) : Option Bool

Evaluate a formula whose atoms are all constant, without constructing a carrier decomposition.

Equations

• formula.evalConstants? = Hex.RCF.Formula.evalSigns (fun (p : Hex.ZPoly) => some (Hex.RCF.evalSign p 0)) formula

def Hex.RCF.SignMatrixCert.evalCell? (cert : SignMatrixCert) (sentence : Sentence) (isolations : IsolationCert) (cell : Cell isolations.intervals.size) : Option Bool

Recompute the formula truth value on one carrier cell after materializing one exact sign per distinct polynomial. Repeated atom occurrences reuse the cached row entry.

Equations

• One or more equations did not get rendered due to their size.