theorem
Hex.GraphIso.Nauty.Generation.frame_fixes
{n : Nat}
{base : List (Fin n)}
{level : Nat}
{st : SearchSt n}
{γ : Array Nat}
(hfixed : FixedCells level st)
(hsize : st.lab.size = n)
(hbase : ∀ (b : Fin n), b ∈ base → st.fixedpts.mem ↑b = true)
(hstab : CellStab st.ptn level st.lab γ)
(b : Fin n)
:
Stabilizing a reached frame fixes the individualized base because those vertices are singleton cells in that frame.
theorem
Hex.GraphIso.Nauty.Generation.return_fixes
{n : Nat}
{base : List (Fin n)}
{level : Nat}
{st out : SearchSt n}
{trail : FrameTrail}
{entry : TrailEntry}
{r : Int}
(hreturn : ReturnStab trail r out)
(hlevel : Int.ofNat level ≤ r)
(hentry : trail level = some entry)
(hlab : entry.frame.rsLab = st.lab)
(hptn : entry.frame.rsPtn = st.ptn)
(hfixed : FixedCells level st)
(hsize : st.lab.size = n)
(hbase : ∀ (b : Fin n), b ∈ base → st.fixedpts.mem ↑b = true)
(γ : Array Nat)
:
The return-level stabilization invariant supplies exactly the fixed base condition needed when a first-path sweep resumes.
theorem
Hex.GraphIso.Nauty.Generation.Cover.window
{n k : Nat}
{G : Colored n k}
{base : List (Fin n)}
{st : SearchSt n}
{level tc len : Nat}
{guide : Fin n}
(hpath : PathStab { g := rowsOf G } (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst level st)
(hlab : LabOk st.lab n)
(hcell : IsCell st.ptn level tc len)
(hrange : tc + len ≤ st.lab.size)
(hbase : ∀ (b : Fin n), st.fixedpts.mem ↑b = true → b ∈ base)
(hguide : (windowSet n st.lab tc len).mem ↑guide = true)
:
The path stabilization invariant places every possible image of the first child in the initial target window of its sweep.
theorem
Hex.GraphIso.Nauty.Generation.Cover.frameSkip
{n k : Nat}
{G : Colored n k}
{base : List (Fin n)}
{st : SearchSt n}
{level : Nat}
{guide tv : Fin n}
{tcell : VSet n}
{cursor : Option Nat}
(h : Cover G base guide tcell cursor)
(hnext : tcell.nextElem cursor = some ↑tv)
(horbits : OrbSound (OrbConn st.genTrace.toList n) st.orbits n)
(htrace : ∀ (γ : Array Nat), γ ∈ st.genTrace → γ ∈ Aut.trace G)
(hstab : ∀ (γ : Array Nat), γ ∈ st.genTrace.toList → CellStab st.ptn level st.lab γ)
(hfixed : FixedCells level st)
(hsize : st.lab.size = n)
(hbase : ∀ (b : Fin n), b ∈ base → st.fixedpts.mem ↑b = true)
(hne : st.orbits[↑tv]! ≠ ↑tv)
:
A skipped first-path child uses the live frame's stabilization proof and the final trace inclusion; no certificate is constructed by search.