theorem
Hex.GraphIso.Nauty.pairOk_of_reach
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{lab₁ lab₂ γ : Array Nat}
(hn0 : 0 < n)
(hs₁ : lab₁.size = n)
(hr₁ : CellsReach G lab₁)
(hr₂ : CellsReach G lab₂)
(hsc : ∀ (i : Nat), i < n → γ[lab₁[i]!]! = lab₂[i]!)
(hca : checkAutom ctx.g γ = true)
:
A checked scatter between two reached labellings yields a valid explicit autos-ledger entry at the initial coloured partition.
theorem
Hex.GraphIso.Nauty.SubtreeOk.pair_ok
{n k : Nat}
{ctx : Ctx n}
{G : Colored n k}
{level : Nat}
{r : RefineSt n}
(hn0 : 0 < n)
(hlevel : 1 ≤ level)
(hgsz : ctx.g.size = n)
(hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u)
(hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false)
(hS : SubtreeOk ctx level r)
(hreach : CellsReach G r.lab)
(hinit : ∀ (q : Nat), (initPtn n (n + 2) (initialPartition G).snd)[q]! ≤ 1 → r.ptn[q]! ≤ 1)
:
The implicit pair recorded at a small-cell node is valid at the root partition. Its missing vertices are realized by the node's flip automorphisms, while singleton cells supply the fixed set.