def Hex.GraphIso.Nauty.Generic.Grows {n : Nat} (before after : Option (Key n)) : Prop

An installed incumbent can only increase.

Equations

• Hex.GraphIso.Nauty.Generic.Grows before after = ∀ (b : Hex.GraphIso.Nauty.Key n), before = some b → ∃ (a : Hex.GraphIso.Nauty.Key n), after = some a ∧ Hex.GraphIso.Nauty.keyLe b a

def Hex.GraphIso.Nauty.Generic.Covers {n : Nat} (bound : Key n) (best : Option (Key n)) : Prop

A key is bounded by an installed incumbent.

Equations

• Hex.GraphIso.Nauty.Generic.Covers bound best = ∃ (b : Hex.GraphIso.Nauty.Key n), best = some b ∧ Hex.GraphIso.Nauty.keyLe bound b

structure Hex.GraphIso.Nauty.Generic.Bounded {n : Nat} (bound : Key n) (before after : Option (Key n)) : Prop

A fragment only installs keys bounded by its incoming incumbent and its fixed subtree bound, and preserves any incoming incumbent.

• upper (b : Key n) : after = some b → keyLe b (incMax before bound)

  Every installed output has the fixed upper bound.

• grows : Grows before after

  Previously installed keys are retained or improved.

theorem Hex.GraphIso.Nauty.Generic.max_le {n : Nat} {a b c : Key n} (ha : keyLe a c) (hb : keyLe b c) : keyLe (keyMax a b) c

Taking a maximum preserves either upper bound.

theorem Hex.GraphIso.Nauty.Generic.le_incMax {n : Nat} (best : Option (Key n)) (bound : Key n) : keyLe bound (incMax best bound)

Folding a key into an optional incumbent bounds that key.

theorem Hex.GraphIso.Nauty.Generic.incMax_mono {n : Nat} (best : Option (Key n)) {a b : Key n} (h : keyLe a b) : keyLe (incMax best a) (incMax best b)

Increasing the subtree bound increases its incumbent maximum.

theorem Hex.GraphIso.Nauty.Generic.Grows.refl {n : Nat} (best : Option (Key n)) : Grows best best

Leaving the incumbent unchanged preserves it.

theorem Hex.GraphIso.Nauty.Generic.Grows.trans {n : Nat} {a b c : Option (Key n)} (hab : Grows a b) (hbc : Grows b c) : Grows a c

Incumbent growth composes across consecutive fragments.

theorem Hex.GraphIso.Nauty.Generic.Grows.incMax {n : Nat} (best : Option (Key n)) (bound : Key n) : Grows best (some (Nauty.incMax best bound))

Installing an incumbent maximum preserves the old incumbent.

theorem Hex.GraphIso.Nauty.Generic.Covers.grow {n : Nat} {bound : Key n} {before after : Option (Key n)} (h : Covers bound before) (hg : Grows before after) : Covers bound after

Coverage survives subsequent incumbent growth.

theorem Hex.GraphIso.Nauty.Generic.Covers.mono {n : Nat} {a b : Key n} {best : Option (Key n)} (h : Covers b best) (hab : keyLe a b) : Covers a best

A covered upper bound covers any smaller key.

theorem Hex.GraphIso.Nauty.Generic.Covers.incMax {n : Nat} (best : Option (Key n)) (bound : Key n) : Covers bound (some (Nauty.incMax best bound))

An exact incumbent maximum covers the folded subtree.

theorem Hex.GraphIso.Nauty.Generic.Covers.keysMax {n : Nat} {head : Key n} {tail : List (Key n)} {best : Option (Key n)} (hh : Covers head best) (ht : ∀ (key : Key n), key ∈ tail → Covers key best) : Covers (Nauty.keysMax head tail) best

Covering every child covers the maximum of their nonempty key list.

theorem Hex.GraphIso.Nauty.Generic.Bounded.refl {n : Nat} (bound : Key n) (best : Option (Key n)) : Bounded bound best best

A fragment that changes nothing satisfies any fixed bound.

theorem Hex.GraphIso.Nauty.Generic.Bounded.of_eq {n : Nat} {bound : Key n} {before after : Option (Key n)} (h : after = some (incMax before bound)) : Bounded bound before after

An exact maximum satisfies both fragment bounds.

theorem Hex.GraphIso.Nauty.Generic.Bounded.mono {n : Nat} {a b : Key n} {before after : Option (Key n)} (h : Bounded a before after) (hab : keyLe a b) : Bounded b before after

A child fragment also satisfies every larger parent bound.

theorem Hex.GraphIso.Nauty.Generic.Bounded.trans {n : Nat} {bound : Key n} {before middle after : Option (Key n)} (h₁ : Bounded bound before middle) (h₂ : Bounded bound middle after) : Bounded bound before after

Fragments with the same frozen bound compose.

theorem Hex.GraphIso.Nauty.Generic.Bounded.exact {n : Nat} {bound : Key n} {before after : Option (Key n)} (h : Bounded bound before after) (hc : Covers bound after) : after = some (incMax before bound)

Coverage and fragment bounds determine the exact maximum.

theorem Hex.GraphIso.Nauty.Generic.ChildCover.covers {n : Nat} {key : Nat → Key n} {rank : Nat → Nat} {all live : Nat → Prop} {best : Option (Key n)} (h : ChildCover key rank all (fun (x : Nat) => Covers (key x) best) live) (hlive : ∀ (x : Nat), live x → Covers (key x) best) (x : Nat) : all x → Covers (key x) best

Ranked child coverage composes with an installed incumbent.

def Hex.GraphIso.Nauty.Generic.ExitCover {n : Nat} (bound : Key n) (best : Option (Key n)) (stop : Nat) (witness : Nat → Option (Key n) → Prop) : Exit → Prop

Coverage carried by an exit. A smaller target refers to the frozen ancestor child named by witness; the receiving level supplies ordinary coverage. Fuel exhaustion makes no coverage assertion.

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.Generic.ExitCover bound best stop witness Hex.GraphIso.Nauty.Generic.Exit.done = Hex.GraphIso.Nauty.Generic.Covers bound best
• Hex.GraphIso.Nauty.Generic.ExitCover bound best stop witness Hex.GraphIso.Nauty.Generic.Exit.fuel = True

structure Hex.GraphIso.Nauty.Generic.Result {n : Nat} (bound : Key n) (before after : Option (Key n)) (stop : Nat) (witness : Nat → Option (Key n) → Prop) (exit : Exit) : Prop

Bounds and the coverage appropriate to a nonlocal exit.

• bounded : Bounded bound before after

  The incumbent stays within this fragment's bound.

• coverage : ExitCover bound after stop witness exit

  The exit either completes coverage or transports an ancestor witness.

theorem Hex.GraphIso.Nauty.Generic.Result.node {n : Nat} {head : Key n} {tail : List (Key n)} {before after : Option (Key n)} {parent : Nat} {witness : Nat → Option (Key n) → Prop} (hbound : Bounded (keysMax head tail) before after) (hhead : Covers head after) (htail : ∀ (key : Key n), key ∈ tail → Covers key after) : Result (keysMax head tail) before after parent witness (Exit.unwind parent false)

Complete child coverage closes a node once all installed keys have the same parent bound. The children include their common code prefix.

theorem Hex.GraphIso.Nauty.Generic.Result.mapWitness {n : Nat} {bound : Key n} {before after : Option (Key n)} {stop : Nat} {witness other : Nat → Option (Key n) → Prop} {exit : Exit} (h : Result bound before after stop witness exit) (hw : ∀ (target : Nat), target < stop → witness target after → other target after) : Result bound before after stop other exit

Ancestor witnesses may be rewritten without changing a fragment's incumbent bounds or its ordinary completed coverage.

theorem Hex.GraphIso.Nauty.Generic.Result.done {n : Nat} {bound : Key n} {before after : Option (Key n)} {stop : Nat} {witness : Nat → Option (Key n) → Prop} (h : Result bound before after stop witness Exit.done) : after = some (incMax before bound)

A complete sweep computes its fixed incumbent maximum.

theorem Hex.GraphIso.Nauty.Generic.Result.received {n : Nat} {bound : Key n} {before after : Option (Key n)} {stop : Nat} {witness : Nat → Option (Key n) → Prop} {short : Bool} (h : Result bound before after stop witness (Exit.unwind stop short)) : after = some (incMax before bound)

A return to the receiving level computes its fixed incumbent maximum.

theorem Hex.GraphIso.Nauty.Generic.Result.finish {n : Nat} {bound : Key n} {before after : Option (Key n)} {stop parent : Nat} {witness : Nat → Option (Key n) → Prop} (h : Result bound before after stop witness Exit.done) : Result bound before after parent witness (Exit.unwind parent false)

A completed child sweep becomes ordinary node completion at its parent. No ancestor witness is needed for this exit.

theorem Hex.GraphIso.Nauty.Generic.Result.ascend {n : Nat} {bound : Key n} {before after : Option (Key n)} {level target : Nat} {short : Bool} {witness : Nat → Option (Key n) → Prop} (h : Result bound before after level witness (Exit.unwind target short)) (ht : target < level) (hresolve : witness (level - 1) after → Covers bound after) : Result bound before after (level - 1) witness (Exit.unwind target short)

Transport an early sweep return through its node. When the target is the node's parent, its frozen-child witness supplies node coverage.

theorem Hex.GraphIso.Nauty.Generic.Result.root {n : Nat} {bound : Key n} {before after : Option (Key n)} {witness : Nat → Option (Key n) → Prop} {exit : Exit} (h : Result bound before after 0 witness exit) (hfuel : exit ≠ Exit.fuel) : after = some (incMax before bound)

The root has no earlier ancestor, so every non-exhausted return is an exact maximum.