inductive Hex.RCF.Cell (n : Nat) : Type

A root cell or one of the open cuts around n ordered roots.

• open {n : Nat} (cut : Fin (n + 1)) : Cell n

  Open cell at a cut between roots, including both tails.

• root {n : Nat} (i : Fin n) : Cell n

  Singleton cell at an isolated root.

def Hex.RCF.instDecidableEqCell.decEq {n✝ : Nat} (x✝ x✝¹ : Cell n✝) : Decidable (x✝ = x✝¹)

Equations

• Hex.RCF.instDecidableEqCell.decEq (Hex.RCF.Cell.open a) (Hex.RCF.Cell.open b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Hex.RCF.instDecidableEqCell.decEq (Hex.RCF.Cell.open cut) (Hex.RCF.Cell.root i) = isFalse ⋯
• Hex.RCF.instDecidableEqCell.decEq (Hex.RCF.Cell.root i) (Hex.RCF.Cell.open cut) = isFalse ⋯
• Hex.RCF.instDecidableEqCell.decEq (Hex.RCF.Cell.root a) (Hex.RCF.Cell.root b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Hex.RCF.instDecidableEqCell {n✝ : Nat} : DecidableEq (Cell n✝)

Equations

• Hex.RCF.instDecidableEqCell = Hex.RCF.instDecidableEqCell.decEq

@[instance_reducible]

instance Hex.RCF.instReprCell {n✝ : Nat} : Repr (Cell n✝)

Equations

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

def Hex.RCF.instReprCell.repr {n✝ : Nat} : Cell n✝ → Nat → Std.Format

Equations

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

def Hex.RCF.Cell.rank {n : Nat} : Cell n → Nat

Alternating position of a cell in the left-to-right decomposition.

Equations

• (Hex.RCF.Cell.open cut).rank = 2 * ↑cut
• (Hex.RCF.Cell.root i).rank = 2 * ↑i + 1

theorem Hex.RCF.Cell.rank_lt {n : Nat} (c : Cell n) : c.rank < 2 * n + 1

Every rank is a valid index into a 2 * n + 1 cell vector.

def Hex.RCF.Cell.all (n : Nat) : Array (Cell n)

Deterministic left-to-right enumeration of all 2 * n + 1 cells.

Equations

• Hex.RCF.Cell.all n = (List.flatMap (fun (i : Fin n) => [Hex.RCF.Cell.open i.castSucc, Hex.RCF.Cell.root i]) (List.finRange n) ++ [Hex.RCF.Cell.open (Fin.last n)]).toArray

@[simp]

theorem Hex.RCF.Cell.size_all (n : Nat) : (all n).size = 2 * n + 1

The enumeration for n roots contains 2 * n + 1 cells.

theorem Hex.RCF.Cell.mem_all {n : Nat} (c : Cell n) : c ∈ all n

Every size-correct cell occurs in the executable enumeration.

def Hex.RCF.IsolationCert.openPoint (cert : IsolationCert) : Fin (cert.intervals.size + 1) → Dyadic

Exact dyadic sample for an open cut.

Equations

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

structure Hex.RCF.IocCmps (n : Nat) : Type

Claimed carrier-root comparisons against the lower and upper endpoints of a bounded domain.

• lower : Vector Separation.RootCmp n

  Each root's order relative to the excluded lower endpoint.

• upper : Vector Separation.RootCmp n

  Each root's order relative to the included upper endpoint.

def Hex.RCF.instReprIocCmps.repr {n✝ : Nat} : IocCmps n✝ → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Hex.RCF.instReprIocCmps {n✝ : Nat} : Repr (IocCmps n✝)

Equations

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

def Hex.RCF.IocCmps.check (f : ZPoly) (replay : SturmReplay) (cert : IsolationCert) (a b : Dyadic) (cmps : IocCmps cert.intervals.size) : Bool

Recompute every claimed endpoint comparison. This validates comparison data only. The bounded-domain layer separately checks a < b.

Equations

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

def Hex.RCF.Cell.meetsIoc {n : Nat} (cmps : IocCmps n) : Cell n → Bool

Executable bounded-domain relevance test for a cell. The surrounding certificate first checks a < b. This definition assumes that the domain is nonempty.

Equations

• One or more equations did not get rendered due to their size.
• Hex.RCF.Cell.meetsIoc cmps (Hex.RCF.Cell.root i) = (cmps.lower[i] == Hex.RCF.Separation.RootCmp.gt && cmps.upper[i] != Hex.RCF.Separation.RootCmp.gt)

def Hex.RCF.Cell.meetsIocOn {n : Nat} (a b : Dyadic) (cmps : IocCmps n) (c : Cell n) : Bool

Guard the nonempty-domain relevance table against equal or reversed endpoints.

Equations

• Hex.RCF.Cell.meetsIocOn a b cmps c = (decide (a < b) && Hex.RCF.Cell.meetsIoc cmps c)