structure Hex.GraphIso.Nauty.Generation.Matches {n : Nat} (ctx : Ctx n) (level : Nat) (st : SearchSt n) (targets : List Nat) (key : Key n) : Prop

A reference occurrence agrees with the stored first-leaf comparison at this level, including every target hint and the terminal row array.

• codes (i : Nat) : i < key.codes.length → key.codes[i]! = st.firstcode[level + i]!
• targets (i : Nat) : i < targets.length → Int.ofNat targets[i]! = st.firsttc[level + i]!
• rows : key.rows = leafRows ctx st.firstlab

theorem Hex.GraphIso.Nauty.Generation.Matches.stateEq {n : Nat} {ctx : Ctx n} {level : Nat} {st : SearchSt n} {targets : List Nat} {key : Key n} (h : Matches ctx level st targets key) {out : SearchSt n} (hcode : out.firstcode = st.firstcode) (htc : out.firsttc = st.firsttc) (hlab : out.firstlab = st.firstlab) : Matches ctx level out targets key

The comparison witness depends only on the stored first reference.

theorem Hex.GraphIso.Nauty.Generation.Matches.tail {n : Nat} {ctx : Ctx n} {level : Nat} {st : SearchSt n} {targets : List Nat} {key : Key n} {tc code : Nat} (h : Matches ctx level st (tc :: targets) { codes := code :: key.codes, rows := key.rows }) : Matches ctx (level + 1) st targets key

Descending one target consumes one code and one target hint.

theorem Hex.GraphIso.Nauty.Generation.Matches.cons {n : Nat} {ctx : Ctx n} {level : Nat} {st : SearchSt n} {targets : List Nat} {key : Key n} {tc code : Nat} (h : Matches ctx (level + 1) st targets key) (hcode : code = st.firstcode[level]!) (htc : Int.ofNat tc = st.firsttc[level]!) : Matches ctx level st (tc :: targets) { codes := code :: key.codes, rows := key.rows }

Returning from a reference child restores the enclosing code and hint once the recursive call's unchanged prefix supplies those entries.

theorem Hex.GraphIso.Nauty.Generation.Matches.prep {n : Nat} {ctx : Ctx n} {level : Nat} {st : SearchSt n} {targets : List Nat} {key : Key n} {tcLevel : Nat} {rs : RefineSt n} (h : Matches ctx level st targets key) (hleaf : HasLeaf ctx tcLevel level rs targets key) (hlevel : st.eqlevFirst = level - 1) : (otherNodePrep level rs.longcode st).eqlevFirst = level

The head of the occurrence justifies advancing the first-reference comparison in the executable preparation step.

theorem Hex.GraphIso.Nauty.Generation.Matches.target {n : Nat} {ctx : Ctx n} {level : Nat} {st : SearchSt n} {key : Key n} {tcLevel tc : Nat} {rest : List Nat} {rs : RefineSt n} (h : Matches ctx level st (tc :: rest) key) (hleaf : HasLeaf ctx tcLevel level rs (tc :: rest) key) (hok : IterOk ctx level rs) (heq : Equitable ctx level rs.lab rs.ptn) : Int.ofNat (maketargetcell ctx rs.lab rs.ptn level tcLevel st.firsttc[level]!).fst = st.firsttc[level]!

The first target of a nonterminal occurrence justifies the stored hint, not merely the equality of refinement codes.

theorem Hex.GraphIso.Nauty.Generation.Matches.target_spec {n : Nat} {ctx : Ctx n} {level : Nat} {st : SearchSt n} {key : Key n} {tcLevel tc : Nat} {rest : List Nat} {rs : RefineSt n} (h : Matches ctx level st (tc :: rest) key) (hleaf : HasLeaf ctx tcLevel level rs (tc :: rest) key) (hok : IterOk ctx level rs) (heq : Equitable ctx level rs.lab rs.ptn) : maketargetcell ctx rs.lab rs.ptn level tcLevel st.firsttc[level]! = specMaketargetcell ctx rs.lab rs.ptn level tcLevel

A matching reference's complete hinted target record agrees with the specification, including the vertex set and its size.

theorem Hex.GraphIso.Nauty.Generation.Matches.discrete {n : Nat} {ctx : Ctx n} {level : Nat} {st : SearchSt n} {targets : List Nat} {key : Key n} {tcLevel : Nat} {rs : RefineSt n} (h : Matches ctx level st targets key) (hleaf : HasLeaf ctx tcLevel level rs targets key) (hok : IterOk ctx level rs) (hdisc : ∀ (q : Nat), q < n → rs.ptn[q]! ≤ level) : st.firstcode[level + 1]! = codeSentinel ∧ leafRows ctx st.firstlab = leafRows ctx rs.lab

At a discrete matching occurrence the terminal sentinel and row comparison are both exact, even if the canonical incumbent is larger.

theorem Hex.GraphIso.Nauty.Generation.rows_emit {n : Nat} {ctx : Ctx n} {level : Nat} {st : SearchSt n} (hgsz : ctx.g.size = n) (hfirstSize : st.firstlab.size = n) (hfirst : st.firstlab.toList.Perm (List.range n)) (hsize : st.lab.size = n) (hperm : st.lab.toList.Perm (List.range n)) (hrows : leafRows ctx st.firstlab = leafRows ctx st.lab) (hlevel : st.eqlevFirst = level) (hsent : st.firstcode[level + 1]! = codeSentinel) : (processnode ctx level n st).snd.genTrace = st.genTrace.push (firstScatter n st.firstlab st.lab) ∧ LabelCarrier ctx st.firstlab st.lab (processnode ctx level n st).snd.genTrace ∧ (processnode ctx level n st).fst = Int.ofNat st.gcaFirst

Equal first-reference rows at a matching discrete leaf force a code-one emission. The argument does not need an a priori choice of automorphism between the two leaf labellings.