Individualised vertices stay where they were put

Refinement rearranges vertices inside cells and never across them. A vertex that has been individualised sits alone in a cell, so from that moment on it never moves again: this file follows a singleton cell through splitCell, splitCellsFrom, refineStep, refineLoop, refine, individualize and child, exactly as Progress.lean follows cell starts.

The payoff is Node.pin. Write pinPos n f (path.take j) for the start of the target cell of the depth-j ancestor of a node — a position that depends on the first j individualised vertices but not on the j-th. Then at every descendant, position pinPos n f (path.take j) holds the vertex individualised at depth j. So two leaves whose paths agree up to depth j park their depth-j choices at the same position, which is what makes the permutation relating two equal-certificate leaves visibly map one branch onto the other.

Along the way nodePath makes a node an honest function of its path (Node.det).

structure IsoGraph.Canon.Pinned (n : ℕ) (p : Part) (c v : ℕ) : Prop

Position c is a singleton cell of p, and the vertex sitting there is v.

• lt : c < n

  The position is in range.

• cst : p.cst[c]! = c

  The cell starts here.

• cen : p.cen[c]! = c + 1

  …and ends immediately after.

• lab : p.lab[c]! = v

  The vertex parked here.

theorem IsoGraph.Canon.splitCell_pinned {n : ℕ} {cnt : Array ℕ} {c0 c v : ℕ} {st : SplitState} (hinv : SplitInv n cnt st) (hc0 : c0 < n) (hcst0 : st.cst[c0]! = c0) (hpin : Pinned n st.part c v) : Pinned n (splitCell cnt c0 st).part c v

theorem IsoGraph.Canon.splitCellsFrom_pinned {n : ℕ} {cnt cells : Array ℕ} {c v : ℕ} (hnd : cells.toList.Nodup) (fuel j : ℕ) (st : SplitState) : SplitInv n cnt st → (∀ (j' : ℕ), j ≤ j' → j' < cells.size → cells[j']! < n ∧ st.cst[cells[j']!]! = cells[j']!) → Pinned n st.part c v → Pinned n (splitCellsFrom cnt cells fuel j st).part c v

theorem IsoGraph.Canon.refineStep_pinned {n : ℕ} {f : ℕ → ℕ → Bool} {p : Part} {c v : ℕ} (hp : Part.WF n p) {s : ℕ} (hs : s < n) (hcst : p.cst[s]! = s) (inW : Array Bool) (tr : UInt64) (hpin : Pinned n p c v) : Pinned n (refineStep (Graph.ofOracle n f) p inW s tr (Scratch.empty n)).1 c v

theorem IsoGraph.Canon.refineLoop_pinned {n : ℕ} {f : ℕ → ℕ → Bool} {c v : ℕ} (fuel : ℕ) (p : Part) (inW : Array Bool) (tr : UInt64) : Part.WF n p → Pinned n p c v → Pinned n (refineLoop (Graph.ofOracle n f) fuel p inW tr (Scratch.empty n)).1 c v

theorem IsoGraph.Canon.refine_pinned {n : ℕ} {f : ℕ → ℕ → Bool} {p : Part} {c v : ℕ} (hp : Part.WF n p) (inW : Array Bool) (tr : UInt64) (hpin : Pinned n p c v) : Pinned n (refine (Graph.ofOracle n f) p inW tr).1 c v

Individualisation pins the vertex it splits off

theorem IsoGraph.Canon.individualize_pinned_new {n : ℕ} {p : Part} {v : ℕ} (hp : Part.WF n p) (hv : v < n) : Pinned n (individualize p v).1 (individualize p v).2 v

theorem IsoGraph.Canon.individualize_pinned {n : ℕ} {p : Part} {v c v' : ℕ} (hp : Part.WF n p) (hv : v < n) (hpin : Pinned n p c v') : Pinned n (individualize p v).1 c v'

theorem IsoGraph.Canon.child_pinned {n : ℕ} {f : ℕ → ℕ → Bool} {p : Part} {v c v' : ℕ} (hp : Part.WF n p) (hv : v < n) (hpin : Pinned n p c v') : Pinned n (child (Graph.ofOracle n f) p v).1 c v'

theorem IsoGraph.Canon.child_pinned_new {n : ℕ} {f : ℕ → ℕ → Bool} {p : Part} {v : ℕ} (hp : Part.WF n p) (hv : v < n) : Pinned n (child (Graph.ofOracle n f) p v).1 p.cst[p.pos[v]!]! v

Individualising v pins it at the start of its cell, for good. Refinement never moves a vertex out of its cell, and {v} is a cell, so every descendant of this child has v sitting at position cst[pos[v]].

A node is a function of its path

def IsoGraph.Canon.nodePath (n : ℕ) (f : ℕ → ℕ → Bool) (path : List ℕ) : Array UInt64 × Part

The node reached by individualising path, in order, from the root. Node is the graph of this function (Node.nodePath_eq); having it as an actual function is what lets two branches of the search that share a path prefix be identified.

Equations

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

theorem IsoGraph.Canon.nodePath_append (n : ℕ) (f : ℕ → ℕ → Bool) (path : List ℕ) (v : ℕ) : nodePath n f (path ++ [v]) = (childInv (Graph.ofOracle n f) (nodePath n f path).1 (nodePath n f path).2 v, (child (Graph.ofOracle n f) (nodePath n f path).2 v).1)

theorem IsoGraph.Canon.Node.nodePath_eq {n : ℕ} {f : ℕ → ℕ → Bool} {path : Array ℕ} {invPath : Array UInt64} {p : Part} (h : Node n f path invPath p) : nodePath n f path.toList = (invPath, p)

theorem IsoGraph.Canon.Node.det {n : ℕ} {f : ℕ → ℕ → Bool} {path : Array ℕ} {invPath invPath' : Array UInt64} {p p' : Part} (h : Node n f path invPath p) (h' : Node n f path invPath' p') : invPath = invPath' ∧ p = p'

Determinism. Two runs that individualise the same vertices in the same order sit at the same node.

Every individualised vertex is pinned at a position fixed by the path prefix

def IsoGraph.Canon.pinPos (n : ℕ) (f : ℕ → ℕ → Bool) (path : List ℕ) : ℕ

The position at which the depth-j individualisation is parked: the start of the target cell of the depth-j ancestor. It depends only on the first j entries of the path.

Equations

• IsoGraph.Canon.pinPos n f path = ((IsoGraph.Canon.nodePath n f path).2.targetCell n).getD 0

theorem IsoGraph.Canon.Node.pin {n : ℕ} {f : ℕ → ℕ → Bool} {path : Array ℕ} {invPath : Array UInt64} {p : Part} (h : Node n f path invPath p) (j : ℕ) : j < path.size → Pinned n p (pinPos n f (List.take j path.toList)) path[j]!

Individualised vertices stay put. At any node, the vertex individualised at depth j sits at position pinPos n f (path.take j) — a position determined by the path prefix, not by the vertex. This is what makes two leaves comparable position by position.