theorem
Hex.GraphIso.Nauty.Sparse.Max.Remaining.none
{n : Nat}
{cell : VSet n}
{v : Nat}
:
¬Remaining Option.none cell v
theorem
Hex.GraphIso.Nauty.Sparse.Max.Cell.Cover.live
{n : Nat}
{G : SparseGraph n}
{tcLevel : Nat}
{c : Cell n}
{before after : Nat → Prop}
{best : Option (Key n)}
(h : Cover G tcLevel c before best)
(he : ∀ (v : Nat), before v ↔ after v)
:
Cover G tcLevel c after best
Changing only the description of live vertices preserves frozen coverage.
theorem
Hex.GraphIso.Nauty.Sparse.Max.Cell.Cover.received
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel : Nat}
{c : Cell n}
{st out : State n}
{cell : VSet n}
{tv : Nat}
{bs : List Nat}
{first short : Bool}
{witness : Nat → Option (Key n) → Prop}
(h : Cover G.graph tcLevel c (Remaining (some tv) cell) (State.key G.graph bs st))
(hc : Valid G c)
(he : FrameOut G c.level c.level c.entry st)
(hs : Ready G c.level c.numcells st)
(hv : c.vertices.mem tv = true)
(hr :
MaxResult (Frame.key G.graph tcLevel (c.child first st tv)) (State.key G.graph bs (c.child first st tv).entry)
(State.best G.graph out) c.level witness (Generic.Exit.unwind c.level short))
:
A received child result covers exactly that child's original vertex key. The native frame theorem accounts for the parent's current label order.
theorem
Hex.GraphIso.Nauty.Sparse.Max.Cell.Cover.skipped
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel : Nat}
{c : Cell n}
{st : State n}
{cell : VSet n}
{tv : Nat}
{best : Option (Key n)}
{first : Bool}
(h : Cover G.graph tcLevel c (Remaining (some tv) cell) best)
(hc : Valid G c)
(hf : TraceFrame G c.level c.entry st)
(ho : OrbitTrace G st)
(ht : TraceOk G st)
(hv : c.vertices.mem tv = true)
(hskip : (!first || st.orbits[tv]! == tv) = false)
:
Skipping the actual nonrepresentative advances coverage with the same
cursor used by the native sweep. Stabilization comes from TraceFrame.
theorem
Hex.GraphIso.Nauty.Sparse.Max.Cell.Cover.filtered
{n : Nat}
{G : SparseGraph n}
{tcLevel : Nat}
{c : Cell n}
{cell filtered : VSet n}
{tv : Nat}
{best : Option (Key n)}
(h : Cover G tcLevel c (fun (v : Nat) => Remaining (cell.nextElem (some tv)) cell v ∧ filtered.mem v = true) best)
(hs : ∀ (v : Nat), filtered.mem v = true → cell.mem v = true)
:
Sequential filters retain precisely their larger survivors at the next cursor, even when an earlier filter has already removed a representative.