def
Hex.GraphIso.Nauty.sweepFrame
(specFuel : Nat)
(codes : List Nat)
(rsLab rsPtn : Array Nat)
(tc numcells : Nat)
:
Package the immutable parameters of a concrete child-loop call.
Equations
- Hex.GraphIso.Nauty.sweepFrame specFuel codes rsLab rsPtn tc numcells = { specFuel := specFuel, codes := codes, rsLab := rsLab, rsPtn := rsPtn, tc := tc, numcells := numcells }
Instances For
One active ancestor frame together with the child offset followed by the current descent.
- frame : SweepFrame
- offset : Nat
Instances For
@[reducible, inline]
Active ancestor children, keyed by their parent search level.
Equations
Instances For
The empty active-frame trail.
Equations
Instances For
structure
Hex.GraphIso.Nauty.TrailOk
{n : Nat}
(ctx : Ctx n)
(level : Nat)
(st : SearchSt n)
(trail : FrameTrail)
:
Every active ancestor frame reaches the current labelling, and its closed boundaries remain frozen in the current partition.
- picked (target : Nat) (entry : TrailEntry) : target < level → trail target = some entry → ∃ (len : Nat), IsCell entry.frame.rsPtn target entry.frame.tc len ∧ entry.offset < len ∧ st.ptn[entry.frame.tc]! = target + 1 ∧ IsCell st.ptn level entry.frame.tc 1 ∧ st.lab[entry.frame.tc]! = entry.frame.rsLab[entry.frame.tc + entry.offset]!
Instances For
theorem
Hex.GraphIso.Nauty.TrailOk.empty
{n : Nat}
(ctx : Ctx n)
(level : Nat)
(st : SearchSt n)
:
TrailOk ctx level st FrameTrail.empty
No ancestor frame is present in the empty trail.
Record the active child of one parent level.
Instances For
@[simp]
theorem
Hex.GraphIso.Nauty.FrameTrail.push_self
(trail : FrameTrail)
(level : Nat)
(entry : TrailEntry)
:
theorem
Hex.GraphIso.Nauty.FrameTrail.push_of_ne
(trail : FrameTrail)
{level q : Nat}
(entry : TrailEntry)
(hne : q ≠ level)
:
def
Hex.GraphIso.Nauty.Anchor.Located
{n : Nat}
{ctx : Ctx n}
{tcLevel level : Nat}
{best : Option (Key n)}
(trail : FrameTrail)
(a : Anchor ctx tcLevel level best)
:
A direct anchor was created from the active frame at its target.
Equations
Instances For
def
Hex.GraphIso.Nauty.Guide.Located
{n : Nat}
{ctx : Ctx n}
{tcLevel level : Nat}
{best : Option (Key n)}
(trail : FrameTrail)
(g : Guide ctx tcLevel level best)
:
A guide names the active frame at its target.
Equations
Instances For
theorem
Hex.GraphIso.Nauty.Anchor.Located.push
{n : Nat}
{ctx : Ctx n}
{tcLevel target level : Nat}
{best : Option (Key n)}
{trail : FrameTrail}
{a : Anchor ctx tcLevel target best}
{entry : TrailEntry}
(h : Located trail a)
(hne : target ≠ level)
:
Adding a different, deeper active child preserves an older anchor's location.
theorem
Hex.GraphIso.Nauty.Guide.Located.push
{n : Nat}
{ctx : Ctx n}
{tcLevel target level : Nat}
{best : Option (Key n)}
{trail : FrameTrail}
{g : Guide ctx tcLevel target best}
{entry : TrailEntry}
(h : Located trail g)
(hne : target ≠ level)
:
Adding a different, deeper active child preserves a guide's frame location.
theorem
Hex.GraphIso.Nauty.Guide.Located.pushSelf
{n : Nat}
{ctx : Ctx n}
{tcLevel level : Nat}
{best : Option (Key n)}
(trail : FrameTrail)
(g : Guide ctx tcLevel level best)
(offset : Nat)
:
A guide for the newly pushed frame is located there immediately. The active descent offset need not be the guide's own explored offset.
theorem
Hex.GraphIso.Nauty.Guide.reachAt
{n : Nat}
{ctx : Ctx n}
{tcLevel target level : Nat}
{st : SearchSt n}
{best : Option (Key n)}
{trail : FrameTrail}
(g : Guide ctx tcLevel target best)
(hloc : Located trail g)
(hok : TrailOk ctx level st trail)
(hlt : target < level)
:
A located guide's ancestor frame reaches the current labelling.
theorem
Hex.GraphIso.Nauty.Guide.active
{n : Nat}
{ctx : Ctx n}
{tcLevel target level : Nat}
{st : SearchSt n}
{best : Option (Key n)}
{trail : FrameTrail}
(g : Guide ctx tcLevel target best)
(hloc : Located trail g)
(hok : TrailOk ctx level st trail)
(hlt : target < level)
:
A located guide identifies the exact active ancestor child followed by the current descent.
theorem
Hex.GraphIso.Nauty.Guide.locateAnchor
{n : Nat}
{ctx : Ctx n}
{tcLevel level : Nat}
{before best : Option (Key n)}
(trail : FrameTrail)
(g : Guide ctx tcLevel level before)
{oCur : Nat}
(hentry : trail level = some { frame := g.frame, offset := oCur })
(hgsz : ctx.g.size = n)
(hinc : IncGrows before best)
{cur : Array Nat}
{store : Array (Array Nat)}
(hcarrier : LabelCarrier ctx g.ref cur store)
(hstab : ∀ (γ : Array Nat), γ ∈ store → CellStab g.rsPtn level g.rsLab γ)
(hcur : oCur < g.len)
(hatCur : cur[g.tc]! = g.rsLab[g.tc + oCur]!)
:
Anchor.Located trail (g.anchor hgsz hinc hcarrier hstab hcur hatCur)
Location evidence follows a guide when a checked carrier turns it into an unwind anchor.
theorem
Hex.GraphIso.Nauty.Guide.locateAnchorCell
{n : Nat}
{ctx : Ctx n}
{tcLevel level : Nat}
{before best : Option (Key n)}
(trail : FrameTrail)
(g : Guide ctx tcLevel level before)
{oCur : Nat}
(hentry : trail level = some { frame := g.frame, offset := oCur })
(hgsz : ctx.g.size = n)
(hinc : IncGrows before best)
{cur : Array Nat}
{store : Array (Array Nat)}
(hcarrier : CellCarrier ctx g.rsPtn level g.rsLab g.ref cur store)
(hcur : oCur < g.len)
(hatCur : cur[g.tc]! = g.rsLab[g.tc + oCur]!)
:
Anchor.Located trail (g.anchorCell hgsz hinc hcarrier hcur hatCur)
Location evidence follows a witness-local carrier into its direct unwind anchor.
inductive
Hex.GraphIso.Nauty.Unwind.Located
{n : Nat}
(trail : FrameTrail)
{ctx : Ctx n}
{tcLevel target : Nat}
{out : SearchSt n}
{best : Option (Key n)}
:
Location evidence attached to each direct unwind constructor. Orbit unwinds use only the target loop's own frame and need no stored frame.
- first {n : Nat} {trail : FrameTrail} {ctx : Ctx n} {tcLevel target : Nat} {out : SearchSt n} {best : Option (Key n)} (anchor : Anchor ctx tcLevel target best) (carrier : LabelCarrier ctx out.firstlab out.lab out.genTrace) (atFirst : target ≤ out.gcaFirst) (located : Anchor.Located trail anchor) : Located trail (Unwind.first anchor carrier atFirst)
- canon {n : Nat} {trail : FrameTrail} {ctx : Ctx n} {tcLevel target : Nat} {out : SearchSt n} {best : Option (Key n)} (anchor : Anchor ctx tcLevel target best) (carrier : LabelCarrier ctx out.canonlab out.lab out.genTrace) (atCanon : target = out.gcaCanon) (located : Anchor.Located trail anchor) : Located trail (Unwind.canon anchor carrier atCanon)
- orbit {n : Nat} {trail : FrameTrail} {ctx : Ctx n} {tcLevel target : Nat} {out : SearchSt n} {best : Option (Key n)} (payload : OrbitUnwind ctx target out) : Located trail (Unwind.orbit payload)
Instances For
inductive
Hex.GraphIso.Nauty.Unwind.FrameStable
{n : Nat}
{ctx : Ctx n}
{tcLevel target : Nat}
{out : SearchSt n}
{best : Option (Key n)}
(rsPtn : Array Nat)
(level : Nat)
(rsLab : Array Nat)
:
The frame-local condition needed to consume an unwind. Direct unwinds already carry a checked cell carrier in their anchor, while the orbit-pointer arm relies on every admitted generator stabilizing the receiving cell.
- first {n : Nat} {ctx : Ctx n} {tcLevel target : Nat} {out : SearchSt n} {best : Option (Key n)} {rsPtn : Array Nat} {level : Nat} {rsLab : Array Nat} (anchor : Anchor ctx tcLevel target best) (carrier : LabelCarrier ctx out.firstlab out.lab out.genTrace) (atFirst : target ≤ out.gcaFirst) : FrameStable rsPtn level rsLab (Unwind.first anchor carrier atFirst)
- canon {n : Nat} {ctx : Ctx n} {tcLevel target : Nat} {out : SearchSt n} {best : Option (Key n)} {rsPtn : Array Nat} {level : Nat} {rsLab : Array Nat} (anchor : Anchor ctx tcLevel target best) (carrier : LabelCarrier ctx out.canonlab out.lab out.genTrace) (atCanon : target = out.gcaCanon) : FrameStable rsPtn level rsLab (Unwind.canon anchor carrier atCanon)
- orbit {n : Nat} {ctx : Ctx n} {tcLevel target : Nat} {out : SearchSt n} {best : Option (Key n)} {rsPtn : Array Nat} {level : Nat} {rsLab : Array Nat} (payload : OrbitUnwind ctx target out) (stable : ∀ (γ : Array Nat), γ ∈ out.genTrace.toList → CellStab rsPtn level rsLab γ) : FrameStable rsPtn level rsLab (Unwind.orbit payload)
Instances For
theorem
Hex.GraphIso.Nauty.Unwind.Located.push
{n : Nat}
{ctx : Ctx n}
{tcLevel target level : Nat}
{out : SearchSt n}
{best : Option (Key n)}
{trail : FrameTrail}
{payload : Unwind ctx tcLevel target out best}
{entry : TrailEntry}
(h : Located trail payload)
(hne : target ≠ level)
:
Extending the trail at a different, deeper level preserves the source location of a transported unwind.
structure
Hex.GraphIso.Nauty.Anchor.At
{n : Nat}
{ctx : Ctx n}
{tcLevel level : Nat}
{best : Option (Key n)}
(a : Anchor ctx tcLevel level best)
(specFuel : Nat)
(codes : List Nat)
(rsLab rsPtn : Array Nat)
(tc numcells : Nat)
:
An unwind anchor belongs to the indicated frozen child-loop frame.
Instances For
theorem
Hex.GraphIso.Nauty.Anchor.at_of_loc
{n : Nat}
{ctx : Ctx n}
{tcLevel level specFuel tc numcells : Nat}
{codes : List Nat}
{rsLab rsPtn : Array Nat}
{best : Option (Key n)}
{trail : FrameTrail}
{offset : Nat}
(a : Anchor ctx tcLevel level best)
(hloc : Located trail a)
(hframe : trail level = some { frame := sweepFrame specFuel codes rsLab rsPtn tc numcells, offset := offset })
:
a.At specFuel codes rsLab rsPtn tc numcells
Looking up the same active frame as a located anchor identifies all of the frozen loop parameters required to consume it.
theorem
Hex.GraphIso.Nauty.Anchor.offset_of_loc
{n : Nat}
{ctx : Ctx n}
{tcLevel level : Nat}
{best : Option (Key n)}
{trail : FrameTrail}
{frame : SweepFrame}
{offset : Nat}
(a : Anchor ctx tcLevel level best)
(hloc : Located trail a)
(hframe : trail level = some { frame := frame, offset := offset })
:
A located anchor follows the child offset recorded by the active descent at its target.
theorem
Hex.GraphIso.Nauty.Anchor.doneAt
{n : Nat}
{ctx : Ctx n}
{tcLevel level specFuel tc numcells : Nat}
{codes : List Nat}
{rsLab rsPtn : Array Nat}
{best : Option (Key n)}
(a : Anchor ctx tcLevel level best)
(h : a.At specFuel codes rsLab rsPtn tc numcells)
:
A located anchor supplies coverage of its stored child offset in the receiving loop's frame.
theorem
Hex.GraphIso.Nauty.SweepCover.anchor
{n : Nat}
{ctx : Ctx n}
{tcLevel specFuel level tc len numcells : Nat}
{tcell : VSet n}
{tv : Nat}
{codes : List Nat}
{rsLab rsPtn : Array Nat}
{cursor : Option Nat}
{before best : Option (Key n)}
(h : SweepCover ctx tcLevel specFuel level codes rsLab rsPtn tc len numcells tcell cursor before)
(hinc : IncGrows before best)
(hnext : tcell.nextElem cursor = some tv)
(a : Anchor ctx tcLevel level best)
(hat : a.At specFuel codes rsLab rsPtn tc numcells)
(htv : rsLab[tc + a.offset]! = tv)
(hinj : LabInj rsLab rsLab.size)
(hrange : tc + len ≤ rsLab.size)
(hoff : tc + a.offset < rsLab.size)
:
SweepCover ctx tcLevel specFuel level codes rsLab rsPtn tc len numcells tcell (some tv) best
A direct generator anchor addressed to this loop advances coverage past the current child.
theorem
Hex.GraphIso.Nauty.SweepCover.locatedAnchor
{n : Nat}
{ctx : Ctx n}
{tcLevel specFuel level tc len numcells : Nat}
{tcell : VSet n}
{tv offset : Nat}
{codes : List Nat}
{rsLab rsPtn : Array Nat}
{cursor : Option Nat}
{before best : Option (Key n)}
{trail : FrameTrail}
(h : SweepCover ctx tcLevel specFuel level codes rsLab rsPtn tc len numcells tcell cursor before)
(hinc : IncGrows before best)
(hnext : tcell.nextElem cursor = some tv)
(a : Anchor ctx tcLevel level best)
(hloc : Anchor.Located trail a)
(hframe : trail level = some { frame := sweepFrame specFuel codes rsLab rsPtn tc numcells, offset := offset })
(htv : rsLab[tc + offset]! = tv)
(hinj : LabInj rsLab rsLab.size)
(hrange : tc + len ≤ rsLab.size)
(hoff : tc + offset < rsLab.size)
:
SweepCover ctx tcLevel specFuel level codes rsLab rsPtn tc len numcells tcell (some tv) best
A located direct anchor consumes the active child named by the target trail entry.
theorem
Hex.GraphIso.Nauty.SweepCover.orbitUnwind
{n : Nat}
{ctx : Ctx n}
{tcLevel specFuel level tc len numcells : Nat}
{tcell : VSet n}
{tv o : Nat}
{codes : List Nat}
{rsLab rsPtn : Array Nat}
{cursor : Option Nat}
{before best : Option (Key n)}
{out : SearchSt n}
(h : SweepCover ctx tcLevel specFuel level codes rsLab rsPtn tc len numcells tcell cursor before)
(hinc : IncGrows before best)
(hnext : tcell.nextElem cursor = some tv)
(ho : o < len)
(htv : rsLab[tc + o]! = tv)
(payload : OrbitUnwind ctx level out)
(hcoset : out.cosetindex = tv)
(hgsz : ctx.g.size = n)
(hv : ∀ (γ : Array Nat), γ ∈ out.genTrace.toList → checkAutom ctx.g γ = true)
(hstab : ∀ (γ : Array Nat), γ ∈ out.genTrace.toList → CellStab rsPtn level rsLab γ)
(hs : rsLab.size = n)
(hinj : LabInj rsLab rsLab.size)
(hok : LabOk rsLab n)
(hsp : rsPtn.size = n)
(hend : rsPtn[rsPtn.size - 1]! ≤ level)
(hvals : ∀ (q : Nat), rsPtn[q]! ≤ level ∨ rsPtn[q]! = n + 2)
(hic : IsCell rsPtn level tc len)
(hrange : tc + len ≤ n)
(hlf : level + 1 + specFuel ≤ n + 1)
:
SweepCover ctx tcLevel specFuel level codes rsLab rsPtn tc len numcells tcell (some tv) best
An orbit unwind addressed to this loop advances coverage through its strictly smaller, sound pointer.
theorem
Hex.GraphIso.Nauty.SweepCover.unwind
{n : Nat}
{ctx : Ctx n}
{tcLevel specFuel level tc len numcells : Nat}
{tcell : VSet n}
{tv offset : Nat}
{codes : List Nat}
{rsLab rsPtn : Array Nat}
{cursor : Option Nat}
{before best : Option (Key n)}
{out : SearchSt n}
{trail : FrameTrail}
{payload : Unwind ctx tcLevel level out best}
(h : SweepCover ctx tcLevel specFuel level codes rsLab rsPtn tc len numcells tcell cursor before)
(hinc : IncGrows before best)
(hnext : tcell.nextElem cursor = some tv)
(hloc : Unwind.Located trail payload)
(hframe : trail level = some { frame := sweepFrame specFuel codes rsLab rsPtn tc numcells, offset := offset })
(ho : offset < len)
(htv : rsLab[tc + offset]! = tv)
(hcoset : out.cosetindex = tv)
(hgsz : ctx.g.size = n)
(hv : ∀ (γ : Array Nat), γ ∈ out.genTrace.toList → checkAutom ctx.g γ = true)
(hstab : Unwind.FrameStable rsPtn level rsLab payload)
(hs : rsLab.size = n)
(hinj : LabInj rsLab rsLab.size)
(hok : LabOk rsLab n)
(hsp : rsPtn.size = n)
(hend : rsPtn[rsPtn.size - 1]! ≤ level)
(hvals : ∀ (q : Nat), rsPtn[q]! ≤ level ∨ rsPtn[q]! = n + 2)
(hic : IsCell rsPtn level tc len)
(hrange : tc + len ≤ n)
(hlf : level + 1 + specFuel ≤ n + 1)
:
SweepCover ctx tcLevel specFuel level codes rsLab rsPtn tc len numcells tcell (some tv) best
Every located generator unwind addressed to this loop consumes the active child. Direct carriers use their stored frame and offset. The special code-two arm uses its sound orbit pointer.
Every recorded generator stabilizes each active frame that the return level permits the caller to resume.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Hex.GraphIso.Nauty.ReturnStab.lower
{n : Nat}
{trail : FrameTrail}
{r r' : Int}
{st : SearchSt n}
(h : ReturnStab trail r st)
(hle : r' ≤ r)
:
ReturnStab trail r' st
Lowering the advertised return level requires stabilization of fewer frames.
theorem
Hex.GraphIso.Nauty.ReturnStab.empty
{n : Nat}
{trail : FrameTrail}
{r : Int}
{st : SearchSt n}
(h : st.genTrace = #[])
:
ReturnStab trail r st
A state with no recorded generators satisfies every return frame.
theorem
Hex.GraphIso.Nauty.ReturnStab.ofGenTraceEq
{n : Nat}
{trail : FrameTrail}
{r : Int}
{st out : SearchSt n}
(h : ReturnStab trail r st)
(heq : out.genTrace = st.genTrace)
:
ReturnStab trail r out
Return stabilization depends only on the recorded-generator store.
theorem
Hex.GraphIso.Nauty.ReturnStab.setFixed
{n : Nat}
{trail : FrameTrail}
{r : Int}
{st : SearchSt n}
(h : ReturnStab trail r st)
(fixedpts : VSet n)
:
ReturnStab trail r
{ lab := st.lab, ptn := st.ptn, active := st.active, orbits := st.orbits, fixedpts := fixedpts, autos := st.autos,
wsCap := st.wsCap, firstcode := st.firstcode, canoncode := st.canoncode, firsttc := st.firsttc,
firstlab := st.firstlab, canonlab := st.canonlab, canong := st.canong, samerows := st.samerows,
compCanon := st.compCanon, eqlevFirst := st.eqlevFirst, eqlevCanon := st.eqlevCanon, gcaFirst := st.gcaFirst,
gcaCanon := st.gcaCanon, canonlevel := st.canonlevel, noncheaplevel := st.noncheaplevel,
allsamelevel := st.allsamelevel, cosetindex := st.cosetindex, stabvertex := st.stabvertex,
needshortprune := st.needshortprune, numnodes := st.numnodes, tctotal := st.tctotal, canupdates := st.canupdates,
numorbits := st.numorbits, numgenerators := st.numgenerators, numbadleaves := st.numbadleaves,
maxlevel := st.maxlevel, genTrace := st.genTrace }
Fixed-point bookkeeping does not affect return stabilization.
theorem
Hex.GraphIso.Nauty.ReturnStab.setFirst
{n : Nat}
{trail : FrameTrail}
{r : Int}
{st : SearchSt n}
(h : ReturnStab trail r st)
(gcaFirst stabvertex : Nat)
:
ReturnStab trail r
{ lab := st.lab, ptn := st.ptn, active := st.active, orbits := st.orbits, fixedpts := st.fixedpts, autos := st.autos,
wsCap := st.wsCap, firstcode := st.firstcode, canoncode := st.canoncode, firsttc := st.firsttc,
firstlab := st.firstlab, canonlab := st.canonlab, canong := st.canong, samerows := st.samerows,
compCanon := st.compCanon, eqlevFirst := st.eqlevFirst, eqlevCanon := st.eqlevCanon, gcaFirst := gcaFirst,
gcaCanon := st.gcaCanon, canonlevel := st.canonlevel, noncheaplevel := st.noncheaplevel,
allsamelevel := st.allsamelevel, cosetindex := st.cosetindex, stabvertex := stabvertex,
needshortprune := st.needshortprune, numnodes := st.numnodes, tctotal := st.tctotal, canupdates := st.canupdates,
numorbits := st.numorbits, numgenerators := st.numgenerators, numbadleaves := st.numbadleaves,
maxlevel := st.maxlevel, genTrace := st.genTrace }
First-path return bookkeeping does not affect the generator store or the ancestor frames it stabilizes.
theorem
Hex.GraphIso.Nauty.ReturnStab.clearShort
{n : Nat}
{trail : FrameTrail}
{r : Int}
{st : SearchSt n}
(h : ReturnStab trail r st)
:
ReturnStab trail r
{ lab := st.lab, ptn := st.ptn, active := st.active, orbits := st.orbits, fixedpts := st.fixedpts, autos := st.autos,
wsCap := st.wsCap, firstcode := st.firstcode, canoncode := st.canoncode, firsttc := st.firsttc,
firstlab := st.firstlab, canonlab := st.canonlab, canong := st.canong, samerows := st.samerows,
compCanon := st.compCanon, eqlevFirst := st.eqlevFirst, eqlevCanon := st.eqlevCanon, gcaFirst := st.gcaFirst,
gcaCanon := st.gcaCanon, canonlevel := st.canonlevel, noncheaplevel := st.noncheaplevel,
allsamelevel := st.allsamelevel, cosetindex := st.cosetindex, stabvertex := st.stabvertex, numnodes := st.numnodes,
tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits, numgenerators := st.numgenerators,
numbadleaves := st.numbadleaves, maxlevel := st.maxlevel, genTrace := st.genTrace }
Clearing the one-shot short-prune flag does not affect stabilization.
theorem
Hex.GraphIso.Nauty.ReturnStab.setAllsame
{n : Nat}
{trail : FrameTrail}
{r : Int}
{st : SearchSt n}
(h : ReturnStab trail r st)
(allsamelevel : Nat)
:
ReturnStab trail r
{ lab := st.lab, ptn := st.ptn, active := st.active, orbits := st.orbits, fixedpts := st.fixedpts, autos := st.autos,
wsCap := st.wsCap, firstcode := st.firstcode, canoncode := st.canoncode, firsttc := st.firsttc,
firstlab := st.firstlab, canonlab := st.canonlab, canong := st.canong, samerows := st.samerows,
compCanon := st.compCanon, eqlevFirst := st.eqlevFirst, eqlevCanon := st.eqlevCanon, gcaFirst := st.gcaFirst,
gcaCanon := st.gcaCanon, canonlevel := st.canonlevel, noncheaplevel := st.noncheaplevel,
allsamelevel := allsamelevel, cosetindex := st.cosetindex, stabvertex := st.stabvertex,
needshortprune := st.needshortprune, numnodes := st.numnodes, tctotal := st.tctotal, canupdates := st.canupdates,
numorbits := st.numorbits, numgenerators := st.numgenerators, numbadleaves := st.numbadleaves,
maxlevel := st.maxlevel, genTrace := st.genTrace }
Updating the first-path agreement counter does not affect generator stabilization.
theorem
Hex.GraphIso.Nauty.ReturnStab.recover
{n : Nat}
{trail : FrameTrail}
{r : Int}
{st : SearchSt n}
(h : ReturnStab trail r st)
(inf level : Nat)
:
ReturnStab trail r (Nauty.recover n inf level st)
Recovering a parent changes no recorded generator, so it preserves return stabilization at every level.
theorem
Hex.GraphIso.Nauty.ReturnStab.pushGen
{n : Nat}
{trail : FrameTrail}
{r : Int}
{st out : SearchSt n}
{gamma : Array Nat}
(h : ReturnStab trail r st)
(hpush : out.genTrace = st.genTrace.push gamma)
(hnew :
∀ (level : Nat) (entry : TrailEntry),
Int.ofNat level ≤ r → trail level = some entry → CellStab entry.frame.rsPtn level entry.frame.rsLab gamma)
:
ReturnStab trail r out
Appending one generator preserves return stabilization when the existing store already satisfies it and the new generator stabilizes every resumable frame.
theorem
Hex.GraphIso.Nauty.ReturnStab.push
{n : Nat}
{trail : FrameTrail}
{r : Int}
{st : SearchSt n}
{level : Nat}
{entry : TrailEntry}
(h : ReturnStab trail r st)
(hnew :
Int.ofNat level ≤ r →
∀ (γ : Array Nat), γ ∈ st.genTrace.toList → CellStab entry.frame.rsPtn level entry.frame.rsLab γ)
:
ReturnStab (trail.push level entry) r st
Pushing a child frame preserves return stabilization at every shallower frame. The new frame is required only when the return reaches it.
theorem
Hex.GraphIso.Nauty.ReturnStab.frameStable
{n : Nat}
{trail : FrameTrail}
{ctx : Ctx n}
{tcLevel target : Nat}
{out : SearchSt n}
{best : Option (Key n)}
{payload : Unwind ctx tcLevel target out best}
{entry : TrailEntry}
(hret : ReturnStab trail (min (Int.ofNat target) (Int.ofNat out.gcaFirst)) out)
(hentry : trail target = some entry)
:
Unwind.FrameStable entry.frame.rsPtn target entry.frame.rsLab payload
At the exact target of a located unwind, return stabilization supplies the store-wide premise needed by the orbit constructor. Direct carrier unwinds are frame-stable without a store-wide premise.