structure Hex.RCF.RootModel (f : ZPoly) (cert : IsolationCert) : Type

The semantic roots named by a checked isolation array.

• root : Fin cert.intervals.size → ℝ

  Root in each certified interval.

• isRoot (i : Fin cert.intervals.size) : (HexRealRootsMathlib.toPolyℝ f).IsRoot (self.root i)

  Every named point is a carrier root.

• inInterval (i : Fin cert.intervals.size) : HexRealRootsMathlib.Literal.InInterval cert.intervals[i] (self.root i)

  Every named point lies in its certified half-open interval.

• strictMono : StrictMono self.root

  Array order is strict real-root order.

• complete (x : ℝ) : (HexRealRootsMathlib.toPolyℝ f).IsRoot x → ∃! i : Fin cert.intervals.size, self.root i = x

  Every carrier root occurs at exactly one named index.

noncomputable def Hex.RCF.IsolationCert.rootAt {f : ZPoly} {replay : SturmReplay} (cert : IsolationCert) (hreplay : SturmReplay.check f replay = true) (hcert : check replay cert = true) (i : Fin cert.intervals.size) : ℝ

The chosen unique root in one accepted generalized isolation.

Equations

• cert.rootAt hreplay hcert i = Classical.choose ⋯

theorem Hex.RCF.IsolationCert.rootAt_spec {f : ZPoly} {replay : SturmReplay} (cert : IsolationCert) (hreplay : SturmReplay.check f replay = true) (hcert : check replay cert = true) (i : Fin cert.intervals.size) : (HexRealRootsMathlib.toPolyℝ f).IsRoot (cert.rootAt hreplay hcert i) ∧ HexRealRootsMathlib.Literal.InInterval cert.intervals[i] (cert.rootAt hreplay hcert i)

The chosen point is a root of the polynomial in the specified interval.

theorem Hex.RCF.IsolationCert.rootAt_unique {f : ZPoly} {replay : SturmReplay} (cert : IsolationCert) (hreplay : SturmReplay.check f replay = true) (hcert : check replay cert = true) (i : Fin cert.intervals.size) {x : ℝ} (hx : (HexRealRootsMathlib.toPolyℝ f).IsRoot x) (hmem : HexRealRootsMathlib.Literal.InInterval cert.intervals[i] x) : x = cert.rootAt hreplay hcert i

Every root in the specified interval equals the chosen root.

noncomputable def Hex.RCF.IsolationCert.rootModel {f : ZPoly} {replay : SturmReplay} (cert : IsolationCert) (hreplay : SturmReplay.check f replay = true) (hstrict : checkStrict replay cert = true) : RootModel f cert

Package all semantic consequences of an accepted strict isolation array.

Equations

• cert.rootModel hreplay hstrict = { root := cert.rootAt hreplay ⋯, isRoot := ⋯, inInterval := ⋯, strictMono := ⋯, complete := ⋯ }

def Hex.RCF.Cell.Sem {f : ZPoly} {cert : IsolationCert} (M : RootModel f cert) : Cell cert.intervals.size → ℝ → Prop

Semantic membership in a cell of a checked root model.

Equations

• One or more equations did not get rendered due to their size.
• Hex.RCF.Cell.Sem M (Hex.RCF.Cell.root i) x✝ = (x✝ = M.root i)

theorem Hex.RCF.Cell.openPoint_mem {f : ZPoly} {replay : SturmReplay} (cert : IsolationCert) (hreplay : SturmReplay.check f replay = true) (hstrict : IsolationCert.checkStrict replay cert = true) (cut : Fin (cert.intervals.size + 1)) : Sem (cert.rootModel hreplay hstrict) («open» cut) (HexRealRootsMathlib.Dyadic.toReal (cert.openPoint cut))

Every checked open-cell sample lies in its advertised semantic cell.

theorem Hex.RCF.Cell.exists_mem {f : ZPoly} {cert : IsolationCert} (M : RootModel f cert) (x : ℝ) : ∃ (c : Cell cert.intervals.size), Sem M c x

Every real point belongs to at least one semantic cell.

theorem Hex.RCF.Cell.rank_injective {n : ℕ} : Function.Injective rank

rank is an injective encoding of the alternating cell order.

theorem Hex.RCF.Cell.lt_of_rank_lt {f : ZPoly} {cert : IsolationCert} (M : RootModel f cert) {c d : Cell cert.intervals.size} {x y : ℝ} (hcd : c.rank < d.rank) (hx : Sem M c x) (hy : Sem M d y) : x < y

Cells earlier in the alternating enumeration lie strictly to the left.

theorem Hex.RCF.Cell.unique_mem {f : ZPoly} {cert : IsolationCert} (M : RootModel f cert) (x : ℝ) {c d : Cell cert.intervals.size} (hc : Sem M c x) (hd : Sem M d x) : c = d

Semantic cell membership is unique.

theorem Hex.RCF.Cell.existsUnique_mem {f : ZPoly} {cert : IsolationCert} (M : RootModel f cert) (x : ℝ) : ∃! c : Cell cert.intervals.size, Sem M c x

The semantic cells form a genuine partition of the real line.

theorem Hex.RCF.Cell.exists_point {f : ZPoly} {cert : IsolationCert} (M : RootModel f cert) (c : Cell cert.intervals.size) : ∃ (x : ℝ), Sem M c x

Every semantic cell contains a real point.

theorem Hex.RCF.Cell.isPreconnected_open {f : ZPoly} {cert : IsolationCert} (M : RootModel f cert) (cut : Fin (cert.intervals.size + 1)) : IsPreconnected {x : ℝ | Sem M («open» cut) x}

Every open semantic cell is an interval, hence preconnected.

theorem Hex.RCF.Cell.open_not_root {f : ZPoly} {cert : IsolationCert} (M : RootModel f cert) {cut : Fin (cert.intervals.size + 1)} {x : ℝ} (hx : Sem M («open» cut) x) : ¬(HexRealRootsMathlib.toPolyℝ f).IsRoot x

An open carrier cell contains no carrier root.

def Hex.RCF.RootModel.leftSpan {carrier : ZPoly} {cert : IsolationCert} (M : RootModel carrier cert) (i : Fin cert.intervals.size) : Set ℝ

The closed-on-the-right span from the open cell immediately left of root i to that root.

Equations

• M.leftSpan i = if hi : ↑i = 0 then Set.Iic (M.root i) else Set.Ioc (M.root ⟨↑i - 1, ⋯⟩) (M.root i)

theorem Hex.RCF.RootModel.isPreconnected_leftSpan {carrier : ZPoly} {cert : IsolationCert} (M : RootModel carrier cert) (i : Fin cert.intervals.size) : IsPreconnected (M.leftSpan i)

A root and the open cell immediately to its left form an interval.

theorem Hex.RCF.RootModel.leftOpen_mem_leftSpan {carrier : ZPoly} {cert : IsolationCert} (M : RootModel carrier cert) (i : Fin cert.intervals.size) {x : ℝ} (hx : Cell.Sem M (Cell.open i.castSucc) x) : x ∈ M.leftSpan i

The open cell immediately left of root i lies in its left span.

theorem Hex.RCF.RootModel.root_mem_leftSpan {carrier : ZPoly} {cert : IsolationCert} (M : RootModel carrier cert) (i : Fin cert.intervals.size) : M.root i ∈ M.leftSpan i

Root i is the right endpoint of its left span.

theorem Hex.RCF.RootModel.root_unique_leftSpan {carrier : ZPoly} {cert : IsolationCert} (M : RootModel carrier cert) (i : Fin cert.intervals.size) {x : ℝ} (hxroot : (HexRealRootsMathlib.toPolyℝ carrier).IsRoot x) (hx : x ∈ M.leftSpan i) : x = M.root i

A carrier root in the left span of root i is root i itself.

theorem Hex.RCF.IocCmps.holds_of_check {f : ZPoly} {replay : SturmReplay} {cert : IsolationCert} (cmps : IocCmps cert.intervals.size) (a b : Dyadic) (hreplay : SturmReplay.check f replay = true) (hstrict : IsolationCert.checkStrict replay cert = true) (hcmps : check f replay cert a b cmps = true) (i : Fin cert.intervals.size) : cmps.lower[i].Holds ((cert.rootModel hreplay hstrict).root i) (HexRealRootsMathlib.Dyadic.toReal a) ∧ cmps.upper[i].Holds ((cert.rootModel hreplay hstrict).root i) (HexRealRootsMathlib.Dyadic.toReal b)

A checked comparison vector has its claimed meaning against the chosen semantic roots.

theorem Hex.RCF.Cell.meetsIoc_iff {f : ZPoly} {cert : IsolationCert} (M : RootModel f cert) (cmps : IocCmps cert.intervals.size) (a b : Dyadic) (hab : HexRealRootsMathlib.Dyadic.toReal a < HexRealRootsMathlib.Dyadic.toReal b) (hlower : ∀ (i : Fin cert.intervals.size), cmps.lower[i].Holds (M.root i) (HexRealRootsMathlib.Dyadic.toReal a)) (hupper : ∀ (i : Fin cert.intervals.size), cmps.upper[i].Holds (M.root i) (HexRealRootsMathlib.Dyadic.toReal b)) (c : Cell cert.intervals.size) : meetsIoc cmps c = true ↔ ∃ (x : ℝ), Sem M c x ∧ x ∈ Set.Ioc (HexRealRootsMathlib.Dyadic.toReal a) (HexRealRootsMathlib.Dyadic.toReal b)

The executable relevance table is exactly semantic intersection with a nonempty half-open interval.

theorem Hex.RCF.Cell.meetsIoc_iff_of_check {f : ZPoly} {replay : SturmReplay} {cert : IsolationCert} (cmps : IocCmps cert.intervals.size) (a b : Dyadic) (hreplay : SturmReplay.check f replay = true) (hstrict : IsolationCert.checkStrict replay cert = true) (hcmps : IocCmps.check f replay cert a b cmps = true) (hab : HexRealRootsMathlib.Dyadic.toReal a < HexRealRootsMathlib.Dyadic.toReal b) (c : Cell cert.intervals.size) : meetsIoc cmps c = true ↔ ∃ (x : ℝ), Sem (cert.rootModel hreplay hstrict) c x ∧ x ∈ Set.Ioc (HexRealRootsMathlib.Dyadic.toReal a) (HexRealRootsMathlib.Dyadic.toReal b)

Checked comparison vectors decide bounded-domain cell relevance exactly.

theorem Hex.RCF.Cell.meetsIocOn_iff_of_check {f : ZPoly} {replay : SturmReplay} {cert : IsolationCert} (cmps : IocCmps cert.intervals.size) (a b : Dyadic) (hreplay : SturmReplay.check f replay = true) (hstrict : IsolationCert.checkStrict replay cert = true) (hcmps : IocCmps.check f replay cert a b cmps = true) (c : Cell cert.intervals.size) : meetsIocOn a b cmps c = true ↔ ∃ (x : ℝ), Sem (cert.rootModel hreplay hstrict) c x ∧ x ∈ Set.Ioc (HexRealRootsMathlib.Dyadic.toReal a) (HexRealRootsMathlib.Dyadic.toReal b)

The guarded relevance test is exact for all endpoint orders.