Documentation

HexGraphIso.Nauty.Sparse.PairsState

source
structure Hex.GraphIso.Nauty.Sparse.PairsEntry {n k : Nat} (G : Sparse.Colored n k) (tcLevel level numcells : Nat) (st : State n) extends Hex.GraphIso.Nauty.Sparse.TraceEntry G tcLevel level numcells st :
Prop

Off-path entry facts needed to validate every pruning-pair admission.

Instances For
    source
    structure Hex.GraphIso.Nauty.Sparse.PairsReady {n k : Nat} (G : Sparse.Colored n k) (tcLevel level numcells : Nat) (st : State n) extends Hex.GraphIso.Nauty.Sparse.TraceReady G tcLevel level numcells st :
    Prop

    A sweep carries a valid workspace and a boundary advanced through its cheap guard. The path and trace histories justify subsequent child admissions.

    Instances For
      source
      theorem Hex.GraphIso.Nauty.Sparse.cheap_bound {n level : Nat} {st : State n} (first : Bool) (h : st.noncheaplevel ≤ level) :
      (cheapCheck first level st).noncheaplevel ≤ level + 1

      The actual guard parks a failed boundary at the next child's level.

      source
      theorem Hex.GraphIso.Nauty.Sparse.recover_bound {n : Nat} (level : Nat) (st : State n) :
      (Generic.Policy.recover (n + 2) level st).noncheaplevel ≤ level + 1

      Recovery always bounds the revived boundary by the next child's level.

      source
      theorem Hex.GraphIso.Nauty.Sparse.PairsEntry.prepare {n k : Nat} {G : Sparse.Colored n k} {tcLevel level numcells : Nat} {st : State n} (h : PairsEntry G tcLevel level numcells st) (hn : 0 < n) (hl : 1 ≤ level) :
      have r := prepareOther (Graph.ofGraph G.graph) tcLevel level numcells st; TraceReady G tcLevel level r.fst r.snd.snd.snd.snd.snd ∧ PathInv G level r.snd.snd.snd.snd.snd ∧ PairsOk G r.snd.snd.snd.snd.snd ∧ CheapBoundary G level r.snd.snd.snd.snd.snd ∧ r.snd.snd.snd.snd.snd.noncheaplevel ≤ level

      Native off-path preparation preserves the path, root workspace and saved-pair boundary while establishing the admission history.

      source
      theorem Hex.GraphIso.Nauty.Sparse.classified_pairs {n k : Nat} {G : Sparse.Colored n k} {tcLevel level numcells : Nat} {st : State n} (h : TraceReady G tcLevel level numcells st) (hn : 0 < n) (hp : PairsOk G st) (hb : CheapBoundary G level st) (hl : st.noncheaplevel ≤ level) :
      have c := classify (Graph.ofGraph G.graph) level numcells st; PairsOk G (leafExit c.fst level c.snd).snd

      Classifying and acting on a prepared leaf preserves both explicit and implicit pair validity, using the executed classifier's sound workspace.

      source
      theorem Hex.GraphIso.Nauty.Sparse.PairsReady.child {n k : Nat} {G : Sparse.Colored n k} {tcLevel level numcells : Nat} {st : State n} (h : PairsReady G tcLevel level numcells st) (hn : 0 < n) (hl : 1 ≤ level) (first : Bool) {tc tv : Nat} {cell : VSet n} (ht : Generic.Target State.frame level tc cell st) (hv : cell.mem tv = true) (hrecord : CheapRecorded level tc st) :
      PairsEntry G tcLevel (level + 1) (numcells + 1) (Generic.Policy.child first level tc tv st)

      Child entry extends the path and keeps the inherited pair boundary.

      source
      theorem Hex.GraphIso.Nauty.Sparse.PairsReady.child_return {n k : Nat} {G : Sparse.Colored n k} {tcLevel level numcells : Nat} {st : State n} (h : PairsReady G tcLevel level numcells st) (hn : 0 < n) (hl : 1 ≤ level) (first : Bool) (fuel : Nat) {tc tv : Nat} {cell : VSet n} (ht : Generic.Target State.frame level tc cell st) (hv : cell.mem tv = true) (hrecord : CheapRecorded level tc st) (hp : PairsOk G (Generic.node false (Graph.ofGraph G.graph) (n + 2) tcLevel fuel (level + 1) (numcells + 1) (Generic.Policy.child first level tc tv st)).snd) :
      have out := (Generic.node false (Graph.ofGraph G.graph) (n + 2) tcLevel fuel (level + 1) (numcells + 1) (Generic.Policy.child first level tc tv st)).snd; have result := Generic.Policy.recover (n + 2) level (Generic.Policy.leaveChild tv out); PairsReady G tcLevel level numcells result ∧ CheapRecorded level tc result

      A returned workspace combines with independent trace, frame, fixed-set and boundary theorems to establish the next actual sibling state.