structure Hex.GraphIso.Nauty.FirstPre {n k : Nat} (G : Colored n k) (ctx : Ctx n) (level numcells : Nat) (st : Search n) : Prop

The first descent begins before a reference leaf is installed. A previously passed cheap guard supplies the small-cell invariant at its current node.

• positive : 1 ≤ level
• partition : SearchOk G level numcells st
• equitable : Equitable ctx level (SearchState.refined ctx level numcells st).lab (SearchState.refined ctx level numcells st).ptn
• codes : st.firstcode.size = n + 2
• targets : n < st.firsttc.size
• cache : st.canong.size = n
• scratch : st.workperm.size = n
• trace : TraceOk ctx st
• orbits : OrbitsOk st

  Every orbit pointer is connected by recorded generators.

• colors : TraceStab G st

  Recorded generators stabilize the initial colour partition.

• small : st.noncheaplevel < level → SubtreeOk ctx level (SearchState.refined ctx level numcells st)
• boundary : Boundary G ctx level st
• cheapBound : st.noncheaplevel ≤ level
• pairs : PairsOk G ctx st
• workspace : WorkspaceOk st
• path : PathInv G ctx level st
• starts (v : Nat) : st.active.mem v = true → v = 0 ∨ st.ptn[v - 1]! ≤ level

theorem Hex.GraphIso.Nauty.firstChild_offset {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel level numcells tv : Nat} {st : Search n} (hn0 : 0 < n) (hlevel : 1 ≤ level) (hok : SearchOk G level numcells st) (htv : (Generic.prepareFirst ctx tcLevel level numcells st).snd.snd.fst.nextElem none = some tv) : have r := Generic.prepareFirst ctx tcLevel level numcells st; have R := SearchState.refined ctx level numcells st; ∃ (e : Nat), ∃ (o : Nat), level < n ∧ (r.snd.fst.toNat, e) ∈ cells R.ptn level n ∧ r.snd.fst.toNat < e ∧ o ≤ e - r.snd.fst.toNat ∧ R.lab[r.snd.fst.toNat + o]! = tv

The chosen first child is a valid mathematical individualization step.

theorem Hex.GraphIso.Nauty.prepareFirst_stores {n : Nat} (ctx : Ctx n) (tcLevel level numcells : Nat) (st : Search n) : have out := (Generic.prepareFirst ctx tcLevel level numcells st).snd.snd.snd.snd; out.firstcode.size = st.firstcode.size ∧ out.firsttc.size = st.firsttc.size ∧ out.canong = st.canong ∧ out.workperm.size = st.workperm.size ∧ out.genTrace = st.genTrace

First-path preparation preserves allocation sizes and the existing generator trace.

theorem Hex.GraphIso.Nauty.prepareFirst_autos {n : Nat} (ctx : Ctx n) (tcLevel level numcells : Nat) (st : Search n) : (Generic.prepareFirst ctx tcLevel level numcells st).snd.snd.snd.snd.autos = st.autos

First-path preparation preserves the workspace before the first admission.

theorem Hex.GraphIso.Nauty.prepareFirst_capacity {n : Nat} (ctx : Ctx n) (tcLevel level numcells : Nat) (st : Search n) : (Generic.prepareFirst ctx tcLevel level numcells st).snd.snd.snd.snd.wsCap = st.wsCap

First-path preparation keeps the configured workspace capacity.

theorem Hex.GraphIso.Nauty.FirstPre.prepare_boundary {n k : Nat} {G : Colored n k} {ctx : Ctx n} {level numcells : Nat} {st : Search n} (h : FirstPre G ctx level numcells st) (tcLevel : Nat) : Boundary G ctx level (Generic.prepareFirst ctx tcLevel level numcells st).snd.snd.snd.snd

First-path preparation preserves every previously frozen implicit pair.

theorem Hex.GraphIso.Nauty.FirstPre.prepare_path {n k : Nat} {G : Colored n k} {ctx : Ctx n} {level numcells : Nat} {st : Search n} (h : FirstPre G ctx level numcells st) (hn0 : 0 < n) (hgsz : ctx.g.size = n) (tcLevel : Nat) : PathInv G ctx level (Generic.prepareFirst ctx tcLevel level numcells st).snd.snd.snd.snd

First-path preparation refines the path and preserves it while recording codes and targets.

theorem Hex.GraphIso.Nauty.FirstPre.cheap_boundary {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel level numcells : Nat} {st : Search n} (h : FirstPre G ctx level numcells st) (hn0 : 0 < n) (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) : Boundary G ctx (level + 1) (cheapCheck true level (Generic.prepareFirst ctx tcLevel level numcells st).snd.snd.snd.snd)

The first-path guard validates the pair needed at the next child.

theorem Hex.GraphIso.Nauty.FirstPre.child {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel level numcells tv : Nat} {st : Search n} (h : FirstPre G ctx level numcells st) (hn0 : 0 < n) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) (htv : (Generic.prepareFirst ctx tcLevel level numcells st).snd.snd.fst.nextElem none = some tv) (hgsz : ctx.g.size = n) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) : have r := Generic.prepareFirst ctx tcLevel level numcells st; FirstPre G ctx (level + 1) (r.fst + 1) (Nauty.child true level r.snd.fst.toNat tv (cheapCheck true level r.snd.snd.snd.snd))

A first-path child inherits the entry conditions, including the exact cheap boundary.