def Hex.GraphIso.Nauty.Generation.referenceCodes {n : Nat} (ctx : Ctx n) (level : Nat) (st : RefineSt n) : List (Nat × Nat) → List Nat

Refinement codes along an individualization path, including the code at its final refined state. This is proof-side reference data.

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.Generation.referenceCodes ctx level st [] = [st.longcode]

def Hex.GraphIso.Nauty.Generation.referenceTargets {n : Nat} (ctx : Ctx n) (tcLevel level : Nat) (st : RefineSt n) : List (Nat × Nat) → Prop

Every step uses the specification's target-cell rule.

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.Generation.referenceTargets ctx tcLevel level st [] = True

theorem Hex.GraphIso.Nauty.Generation.reference_target {n : Nat} {ctx : Ctx n} {σ : Renaming n} (hg : RowsMap σ ctx.g ctx.g) {level tcLevel : Nat} {U V : RefineSt n} (hU : IterOk ctx level U) (hsp : StPerm level V (mapSt σ U)) : specTargetcell ctx V.lab V.ptn level tcLevel = specTargetcell ctx U.lab U.ptn level tcLevel

Isomorphic cell-equivalent states choose the same target position.

theorem Hex.GraphIso.Nauty.Generation.reference_transport {n : Nat} {ctx : Ctx n} {tcLevel : Nat} {σ : Renaming n} (hg : RowsMap σ ctx.g ctx.g) {level level' : Nat} {p : List (Nat × Nat)} {U U' V : RefineSt n} : DescPath ctx level U p level' U' → referenceTargets ctx tcLevel level U p → IterOk ctx level U → StPerm level V (mapSt σ U) → ∃ (V' : RefineSt n), ∃ (q : List (Nat × Nat)), DescPath ctx level V q level' V' ∧ referenceTargets ctx tcLevel level V q ∧ List.map Prod.fst q = List.map Prod.fst p ∧ referenceCodes ctx level V q = referenceCodes ctx level U p ∧ StPerm level' V' (mapSt σ U')

Transporting a reference descent preserves both the target cells and every refinement code. Unlike equality of maximal keys, this retains the specific reference path needed by the first-reference comparison.

theorem Hex.GraphIso.Nauty.Generation.reference_leaf {n : Nat} {ctx : Ctx n} {tcLevel : Nat} {σ : Renaming n} (hg : RowsMap σ ctx.g ctx.g) {level level' : Nat} {path : List (Nat × Nat)} {U U' V : RefineSt n} (h : DescPath ctx level U path level' U') (htargets : referenceTargets ctx tcLevel level U path) (hU : IterOk ctx level U) (hsp : StPerm level V (mapSt σ U)) (hdisc : ∀ (q : Nat), q < n → U'.ptn[q]! ≤ level') : ∃ (V' : RefineSt n), ∃ (q : List (Nat × Nat)), DescPath ctx level V q level' V' ∧ referenceTargets ctx tcLevel level V q ∧ List.map Prod.fst q = List.map Prod.fst path ∧ referenceCodes ctx level V q = referenceCodes ctx level U path ∧ V'.lab = Array.map σ.toFun U'.lab ∧ V'.ptn = U'.ptn

At a discrete reference leaf, transport gives the exact renamed labelling, as well as every refinement code and target-cell position. Keeping the labelling is essential for identifying the automorphism.