Kernel tree walk

Boxes are KBoxes (integers over 2^K); a split halves one radius, doubling the common scale first when that radius is odd. .hole leaves mark subtrees that are checked by separate theorems (see holes).

inductive Cayley.K.KTree : Type

• split (d : Nat) (l r : KTree) : KTree
• dom (code : Nat) : KTree
• gap (s : Nat) (w0 w1 : Int) : KTree
• hole : KTree

def Cayley.K.KBox.split (b : KBox) (d : Nat) : KBox × KBox

Halve the radius in direction d.

Equations

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

def Cayley.K.rootK (i : Nat) : KBox

The 15 root boxes (scale 2^2): u ∈ [0,1], v ∈ [0,1/2], r ∈ [-1,1]³ (charts 1–3), (c, ρ) ∈ [-1,1]² × [0,1] (chart 0, faces 0–5), (c, ρ) ∈ [-1,1]² × [0,2] (chart 4).

Equations

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

def Cayley.K.kCheck (hok : Bool) (b : KBox) : KTree → Bool

Check every leaf; .hole leaves pass exactly when hok (holes are then covered by separate theorems, see holes).

Equations

• Cayley.K.kCheck hok b (Cayley.K.KTree.split d l r) = (Cayley.K.kCheck hok (b.split d).fst l && Cayley.K.kCheck hok (b.split d).snd r)
• Cayley.K.kCheck hok b (Cayley.K.KTree.dom code) = Cayley.K.pDomOK b code
• Cayley.K.kCheck hok b (Cayley.K.KTree.gap s w0 w1) = Cayley.K.pGapOK b s w0 w1
• Cayley.K.kCheck hok b Cayley.K.KTree.hole = hok

def Cayley.K.holes (b : KBox) : KTree → List KBox

The boxes of the holes, left to right.

Equations

• Cayley.K.holes b (Cayley.K.KTree.split d l r) = Cayley.K.holes (b.split d).fst l ++ Cayley.K.holes (b.split d).snd r
• Cayley.K.holes b Cayley.K.KTree.hole = [b]
• Cayley.K.holes b x✝ = []

def Cayley.K.AllOK : List (KBox × KTree) → Prop

Every (box, subtree) pair checks, with no holes.

Equations

• Cayley.K.AllOK [] = True
• Cayley.K.AllOK ((b, t) :: l) = (Cayley.K.kCheck false b t = true ∧ Cayley.K.AllOK l)