theorem Hex.RCF.OptionFold.all_eq_none_iff {α : Type u_1} {f : α → Option Bool} {xs : List α} : all f xs = none ↔ ∃ x ∈ xs, f x = none

A strict universal fold returns none exactly when an input evaluates to none.

theorem Hex.RCF.OptionFold.any_eq_none_iff {α : Type u_1} {f : α → Option Bool} {xs : List α} : any f xs = none ↔ ∃ x ∈ xs, f x = none

A strict existential fold returns none exactly when an input evaluates to none.

theorem Hex.RCF.OptionFold.all_spec {α : Type u_1} {f : α → Option Bool} {xs : List α} (htotal : ∀ x ∈ xs, ∃ (value : Bool), f x = some value) : ∃ (value : Bool), all f xs = some value ∧ (value = true ↔ ∀ x ∈ xs, f x = some true)

A total strict universal fold is true exactly when every input is true.

theorem Hex.RCF.OptionFold.any_spec {α : Type u_1} {f : α → Option Bool} {xs : List α} (htotal : ∀ x ∈ xs, ∃ (value : Bool), f x = some value) : ∃ (value : Bool), any f xs = some value ∧ (value = true ↔ ∃ x ∈ xs, f x = some true)

A total strict existential fold is true exactly when some input is true.

theorem Hex.RCF.OptionFold.allArray_none {α : Type u_1} {xs : Array α} {f : α → Option Bool} : allArray xs f = none ↔ ∃ x ∈ xs, f x = none

A strict universal array fold returns none exactly when an entry evaluates to none.

theorem Hex.RCF.OptionFold.anyArray_none {α : Type u_1} {xs : Array α} {f : α → Option Bool} : anyArray xs f = none ↔ ∃ x ∈ xs, f x = none

A strict existential array fold returns none exactly when an entry evaluates to none.

theorem Hex.RCF.OptionFold.allWhereArray_none {α : Type u_1} {xs : Array α} {relevant : α → Bool} {f : α → Option Bool} : allWhereArray xs relevant f = none ↔ ∃ x ∈ xs, relevant x = true ∧ f x = none

A filtered universal array fold returns none exactly at a relevant undefined entry.

theorem Hex.RCF.OptionFold.anyWhereArray_none {α : Type u_1} {xs : Array α} {relevant : α → Bool} {f : α → Option Bool} : anyWhereArray xs relevant f = none ↔ ∃ x ∈ xs, relevant x = true ∧ f x = none

A filtered existential array fold returns none exactly at a relevant undefined entry.

theorem Hex.RCF.OptionFold.allArray_spec {α : Type u_1} {xs : Array α} {f : α → Option Bool} (htotal : ∀ x ∈ xs, ∃ (value : Bool), f x = some value) : ∃ (value : Bool), allArray xs f = some value ∧ (value = true ↔ ∀ x ∈ xs, f x = some true)

A total strict universal array fold is true exactly when every entry is true.

theorem Hex.RCF.OptionFold.anyArray_spec {α : Type u_1} {xs : Array α} {f : α → Option Bool} (htotal : ∀ x ∈ xs, ∃ (value : Bool), f x = some value) : ∃ (value : Bool), anyArray xs f = some value ∧ (value = true ↔ ∃ x ∈ xs, f x = some true)

A total strict existential array fold is true exactly when some entry is true.

theorem Hex.RCF.OptionFold.allWhereArray_spec {α : Type u_1} {xs : Array α} {relevant : α → Bool} {f : α → Option Bool} (htotal : ∀ x ∈ xs, relevant x = true → ∃ (value : Bool), f x = some value) : ∃ (value : Bool), allWhereArray xs relevant f = some value ∧ (value = true ↔ ∀ x ∈ xs, relevant x = true → f x = some true)

A total filtered universal fold is true exactly when every relevant entry is true.

theorem Hex.RCF.OptionFold.anyWhereArray_spec {α : Type u_1} {xs : Array α} {relevant : α → Bool} {f : α → Option Bool} (htotal : ∀ x ∈ xs, relevant x = true → ∃ (value : Bool), f x = some value) : ∃ (value : Bool), anyWhereArray xs relevant f = some value ∧ (value = true ↔ ∃ x ∈ xs, relevant x = true ∧ f x = some true)

A total filtered existential fold is true exactly when some relevant entry is true.

theorem Hex.RCF.CellFold.forall_spec {carrier : ZPoly} {cert : IsolationCert} (M : RootModel carrier cert) (eval : Cell cert.intervals.size → Option Bool) (P : ℝ → Prop) (hcell : ∀ (c : Cell cert.intervals.size), ∃ (value : Bool), eval c = some value ∧ ∀ (x : ℝ), Cell.Sem M c x → (value = true ↔ P x)) : ∃ (value : Bool), OptionFold.allArray (Cell.all cert.intervals.size) eval = some value ∧ (value = true ↔ ∀ (x : ℝ), P x)

Universal folding over all cells is equivalent to universal quantification over the real line.

theorem Hex.RCF.CellFold.exists_spec {carrier : ZPoly} {cert : IsolationCert} (M : RootModel carrier cert) (eval : Cell cert.intervals.size → Option Bool) (P : ℝ → Prop) (hcell : ∀ (c : Cell cert.intervals.size), ∃ (value : Bool), eval c = some value ∧ ∀ (x : ℝ), Cell.Sem M c x → (value = true ↔ P x)) : ∃ (value : Bool), OptionFold.anyArray (Cell.all cert.intervals.size) eval = some value ∧ (value = true ↔ ∃ (x : ℝ), P x)

Existential folding over all cells is equivalent to existential quantification over the real line.

theorem Hex.RCF.CellFold.forallWhere_spec {carrier : ZPoly} {cert : IsolationCert} (M : RootModel carrier cert) (eval : Cell cert.intervals.size → Option Bool) (relevant : Cell cert.intervals.size → Bool) (D P : ℝ → Prop) (hcell : ∀ (c : Cell cert.intervals.size), ∃ (value : Bool), eval c = some value ∧ ∀ (x : ℝ), Cell.Sem M c x → (value = true ↔ P x)) (hrelevant : ∀ (c : Cell cert.intervals.size), relevant c = true ↔ ∃ (x : ℝ), Cell.Sem M c x ∧ D x) : ∃ (value : Bool), OptionFold.allWhereArray (Cell.all cert.intervals.size) relevant eval = some value ∧ (value = true ↔ ∀ (x : ℝ), D x → P x)

Universal folding over relevant cells is equivalent to quantification over the specified domain.

theorem Hex.RCF.CellFold.existsWhere_spec {carrier : ZPoly} {cert : IsolationCert} (M : RootModel carrier cert) (eval : Cell cert.intervals.size → Option Bool) (relevant : Cell cert.intervals.size → Bool) (D P : ℝ → Prop) (hcell : ∀ (c : Cell cert.intervals.size), ∃ (value : Bool), eval c = some value ∧ ∀ (x : ℝ), Cell.Sem M c x → (value = true ↔ P x)) (hrelevant : ∀ (c : Cell cert.intervals.size), relevant c = true ↔ ∃ (x : ℝ), Cell.Sem M c x ∧ D x) : ∃ (value : Bool), OptionFold.anyWhereArray (Cell.all cert.intervals.size) relevant eval = some value ∧ (value = true ↔ ∃ (x : ℝ), D x ∧ P x)

Existential folding over relevant cells is equivalent to quantification over the specified domain.

theorem Hex.RCF.CellFold.forallIoc_spec {carrier : ZPoly} {replay : SturmReplay} (hreplay : SturmReplay.check carrier replay = true) {cert : IsolationCert} (hstrict : IsolationCert.checkStrict replay cert = true) (a b : Dyadic) (cmps : IocCmps cert.intervals.size) (hcmps : IocCmps.check carrier replay cert a b cmps = true) (eval : Cell cert.intervals.size → Option Bool) (P : ℝ → Prop) (hcell : ∀ (c : Cell cert.intervals.size), ∃ (value : Bool), eval c = some value ∧ ∀ (x : ℝ), Cell.Sem (cert.rootModel hreplay hstrict) c x → (value = true ↔ P x)) : ∃ (value : Bool), OptionFold.allWhereArray (Cell.all cert.intervals.size) (Cell.meetsIocOn a b cmps) eval = some value ∧ (value = true ↔ ∀ x ∈ Set.Ioc (HexRealRootsMathlib.Dyadic.toReal a) (HexRealRootsMathlib.Dyadic.toReal b), P x)

Universal folding over cells that meet (a, b] computes the bounded universal proposition.

theorem Hex.RCF.CellFold.existsIoc_spec {carrier : ZPoly} {replay : SturmReplay} (hreplay : SturmReplay.check carrier replay = true) {cert : IsolationCert} (hstrict : IsolationCert.checkStrict replay cert = true) (a b : Dyadic) (cmps : IocCmps cert.intervals.size) (hcmps : IocCmps.check carrier replay cert a b cmps = true) (eval : Cell cert.intervals.size → Option Bool) (P : ℝ → Prop) (hcell : ∀ (c : Cell cert.intervals.size), ∃ (value : Bool), eval c = some value ∧ ∀ (x : ℝ), Cell.Sem (cert.rootModel hreplay hstrict) c x → (value = true ↔ P x)) : ∃ (value : Bool), OptionFold.anyWhereArray (Cell.all cert.intervals.size) (Cell.meetsIocOn a b cmps) eval = some value ∧ (value = true ↔ ∃ x ∈ Set.Ioc (HexRealRootsMathlib.Dyadic.toReal a) (HexRealRootsMathlib.Dyadic.toReal b), P x)

Existential folding over cells that meet (a, b] computes the bounded existential proposition.

theorem Hex.RCF.Certificate.replay_true {s : Sentence} {cert : Certificate} (h : check s cert = true) : replay? s cert = some true

An accepted certificate has three-valued replay result some true.

theorem Hex.RCF.Sentence.evalConstants_of_empty {s : Sentence} (hempty : s.polys.isEmpty = true) (x : ℝ) : s.formula.evalConstants? = some true ↔ s.formula.toProp x

Constant-only sentence replay is exact at every real point.

theorem Hex.RCF.Certificate.emptyIoc_sound {s : Sentence} (h : replay? s emptyIoc = some true) : s.toProp

The empty bounded-domain branch is sound independently of its body.

theorem Hex.RCF.Certificate.constants_sound {s : Sentence} (h : replay? s constants = some true) : s.toProp

A successfully replayed constants-only branch proves the sentence.

theorem Hex.RCF.Sentence.evalOpen_eq_true_iff {s : Sentence} {carrier : CarrierCert} (hcarrier : CarrierCert.check s carrier = true) {isolations : IsolationCert} (hstrict : IsolationCert.checkStrict carrier.replay isolations = true) (cut : Fin (isolations.intervals.size + 1)) {x : ℝ} (hx : Cell.Sem (isolations.rootModel ⋯ hstrict) (Cell.open cut) x) : s.evalOpen? isolations cut = some true ↔ s.formula.toProp x

The matrix-free open-cell evaluator is exact under the carrier and strict isolation checks.

theorem Hex.RCF.Certificate.noRoots_sound {s : Sentence} {data : DecompCert} (h : replay? s (noRoots data) = some true) : s.toProp

A checked empty isolation set gives the single-cell decomposition.

theorem Hex.RCF.Certificate.cells_sound {s : Sentence} {data : CellsCert} (h : replay? s (cells data) = some true) : s.toProp

A checked positive-root decomposition proves the quantified sentence.

theorem Hex.RCF.check_sound (s : Sentence) (cert : Certificate) : Certificate.check s cert = true → s.toProp

The public Boolean certificate checker is sound.