def Hex.RCF.OptionFold.all {α : Type u_1} (f : α → Option Bool) : List α → Option Bool

Universal option fold that does not Boolean-short-circuit a false value.

Equations

• Hex.RCF.OptionFold.all f [] = some true
• Hex.RCF.OptionFold.all f (x_1 :: xs) = do let head ← f x_1 let tail ← Hex.RCF.OptionFold.all f xs pure (head && tail)

def Hex.RCF.OptionFold.any {α : Type u_1} (f : α → Option Bool) : List α → Option Bool

Existential option fold that does not Boolean-short-circuit a true value.

Equations

• Hex.RCF.OptionFold.any f [] = some false
• Hex.RCF.OptionFold.any f (x_1 :: xs) = do let head ← f x_1 let tail ← Hex.RCF.OptionFold.any f xs pure (head || tail)

def Hex.RCF.OptionFold.allArray {α : Type u_1} (xs : Array α) (f : α → Option Bool) : Option Bool

Universal fold over an array.

Equations

• Hex.RCF.OptionFold.allArray xs f = Hex.RCF.OptionFold.all f xs.toList

def Hex.RCF.OptionFold.anyArray {α : Type u_1} (xs : Array α) (f : α → Option Bool) : Option Bool

Existential fold over an array.

Equations

• Hex.RCF.OptionFold.anyArray xs f = Hex.RCF.OptionFold.any f xs.toList

def Hex.RCF.OptionFold.allWhereArray {α : Type u_1} (xs : Array α) (relevant : α → Bool) (f : α → Option Bool) : Option Bool

Filter irrelevant entries before a strict universal fold.

Equations

• Hex.RCF.OptionFold.allWhereArray xs relevant f = Hex.RCF.OptionFold.all f (List.filter relevant xs.toList)

def Hex.RCF.OptionFold.anyWhereArray {α : Type u_1} (xs : Array α) (relevant : α → Bool) (f : α → Option Bool) : Option Bool

Filter irrelevant entries before a strict existential fold.

Equations

• Hex.RCF.OptionFold.anyWhereArray xs relevant f = Hex.RCF.OptionFold.any f (List.filter relevant xs.toList)

structure Hex.RCF.DecompCert : Type

Carrier and isolation data for a carrier with no real roots.

• carrier : CarrierCert

  Certificate data for the proposed square-free carrier.

• isolations : IsolationCert

  Proposed carrier isolation data. The root-free replay branch requires this array to contain no intervals.

structure Hex.RCF.CellsCert : Type

Full positive-root decomposition data. Endpoint comparisons are present exactly for bounded sentences.

• carrier : CarrierCert

  Certificate data for the proposed square-free carrier.

• isolations : IsolationCert

  Proposed carrier isolation data. Cell replay requires at least one interval.

• signs : SignMatrixCert

  Common-root data used to compute atom signs on every cell.

• iocCmps : Option (IocCmps self.isolations.intervals.size)

  Endpoint comparisons for bounded sentences, or none for sentences over the whole real line.

inductive Hex.RCF.Certificate : Type

The four disjoint replay branches.

• emptyIoc : Certificate

  Equal or reversed bounded endpoints.

• constants : Certificate

  A formula containing no nonconstant atom polynomial.

• noRoots (data : DecompCert) : Certificate

  A checked carrier with no real roots.

• cells (data : CellsCert) : Certificate

  A checked carrier with at least one real root.

def Hex.RCF.Sentence.evalOpen? (s : Sentence) (isolations : IsolationCert) (cut : Fin (isolations.intervals.size + 1)) : Option Bool

Evaluate one open cell without constructing common-root packages.

Equations

• s.evalOpen? isolations cut = Hex.RCF.Formula.evalSigns (fun (p : Hex.ZPoly) => Hex.RCF.openCellSign? p isolations cut) s.formula

def Hex.RCF.Sentence.replayConstants? (s : Sentence) : Option Bool

Replay the carrier-free constant branch. Nonempty bounded domains are checked here. Empty domains belong to Certificate.emptyIoc.

Equations

• (Hex.RCF.Sentence.forallReal formula).replayConstants? = if (Hex.RCF.Sentence.forallReal formula).polys.isEmpty = true then formula.evalConstants? else none
• (Hex.RCF.Sentence.existsReal formula).replayConstants? = if (Hex.RCF.Sentence.existsReal formula).polys.isEmpty = true then formula.evalConstants? else none
• (Hex.RCF.Sentence.forallIoc a b formula).replayConstants? = if (Hex.RCF.Sentence.forallIoc a b formula).polys.isEmpty = true then if a < b then formula.evalConstants? else none else none
• (Hex.RCF.Sentence.existsIoc a b formula).replayConstants? = if (Hex.RCF.Sentence.existsIoc a b formula).polys.isEmpty = true then if a < b then formula.evalConstants? else none else none

def Hex.RCF.Sentence.replayNoRoots? (s : Sentence) (data : DecompCert) : Option Bool

Replay a checked decomposition whose carrier has no real roots.

Equations

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

def Hex.RCF.Sentence.replayCells? (s : Sentence) (data : CellsCert) : Option Bool

Replay a checked positive-root decomposition. Real sentences forbid endpoint data. Bounded sentences require and verify it.

Equations

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

def Hex.RCF.Certificate.replay? (s : Sentence) : Certificate → Option Bool

Three-valued certificate replay.

Equations

• Hex.RCF.Certificate.replay? (Hex.RCF.Sentence.forallIoc a b φ) Hex.RCF.Certificate.emptyIoc = if a < b then none else some true
• Hex.RCF.Certificate.replay? (Hex.RCF.Sentence.existsIoc a b φ) Hex.RCF.Certificate.emptyIoc = if a < b then none else some false
• Hex.RCF.Certificate.replay? s Hex.RCF.Certificate.emptyIoc = none
• Hex.RCF.Certificate.replay? s Hex.RCF.Certificate.constants = s.replayConstants?
• Hex.RCF.Certificate.replay? s (Hex.RCF.Certificate.noRoots data) = s.replayNoRoots? data
• Hex.RCF.Certificate.replay? s (Hex.RCF.Certificate.cells data) = s.replayCells? data

def Hex.RCF.Certificate.check (s : Sentence) (cert : Certificate) : Bool

The kernel boundary accepts only a fully replayed true verdict.

Equations

• Hex.RCF.Certificate.check s cert = (Hex.RCF.Certificate.replay? s cert == some true)