theorem Hex.GraphIso.Nauty.Generation.first_reference {n k : Nat} {G : Colored n k} {ctx : Ctx n} (inf tcLevel : Nat) (hg : ctx.g = rowsOf G) (fuel level numcells : Nat) (codes : List Nat) (st : SearchSt n) (trail : FrameTrail) (hfirst : FirstInv G ctx level codes numcells st trail) (hlevel : 1 ≤ level) (hpath : level = codes.length + 1) (htcsize : st.firsttc.size = n + 2) (hfuel : n < level + fuel) : ∃ (targets : List Nat), ∃ (key : Key n), HasLeaf ctx tcLevel level (refine ctx level st.lab st.ptn st.active numcells) targets key ∧ Matches ctx level (firstPathNode ctx inf tcLevel fuel level numcells st).snd targets key ∧ level ≤ (firstPathNode ctx inf tcLevel fuel level numcells st).snd.allsamelevel

The unique first descent installs a reference that actually occurs below its entry, preserving its codes, target hints and all-same boundary.

theorem Hex.GraphIso.Nauty.Generation.first_agreement {n k : Nat} {G : Colored n k} {ctx : Ctx n} (inf tcLevel : Nat) (hg : ctx.g = rowsOf G) (fuel level numcells : Nat) (codes : List Nat) (st : SearchSt n) (trail : FrameTrail) (hfirst : FirstInv G ctx level codes numcells st trail) (hlevel : 1 ≤ level) (hpath : level = codes.length + 1) (htcsize : st.firsttc.size = n + 2) (hfuel : n < level + fuel) : level ≤ (firstPathNode ctx inf tcLevel fuel level numcells st).snd.eqlevFirst

The first descent establishes agreement through its entry level. This records the actual comparison depth, which cannot be recovered from the weaker prefix invariant alone.