def Hex.GraphIso.Nauty.Sparse.incMax {n : Nat} (before : Option (Key n)) (bound : Key n) : Key n

The native maximum of a subtree bound and an optional incoming key.

Equations

• Hex.GraphIso.Nauty.Sparse.incMax none bound = bound
• Hex.GraphIso.Nauty.Sparse.incMax (some key) bound = key.max bound

theorem Hex.GraphIso.Nauty.Sparse.le_incMax {n : Nat} (before : Option (Key n)) (bound : Key n) : bound.Le (incMax before bound)

theorem Hex.GraphIso.Nauty.Sparse.incMax_mono {n : Nat} (before : Option (Key n)) {a b : Key n} (h : a.Le b) : (incMax before a).Le (incMax before b)

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

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

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

A fragment preserves its incoming key and only installs native keys bounded by the incoming incumbent and the frozen complete subtree.

• upper (key : Key n) : after = some key → key.Le (incMax before bound)
• grows : Grows before after

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

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

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

theorem Hex.GraphIso.Nauty.Sparse.Bounded.absorb {n : Nat} {child parent : Key n} {before after : Option (Key n)} (h : Bounded child before after) (hc : child.Le (incMax before parent)) : Bounded parent before after

A child may be bounded by the incoming incumbent as well as the parent subtree. This is needed for dominated, hinted target choices.

theorem Hex.GraphIso.Nauty.Sparse.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

theorem Hex.GraphIso.Nauty.Sparse.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 of the frozen bound and the upper invariant determine the exact native maximum, including calls made before the first incumbent.

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

A completed exit covers its frozen subtree. A return to an earlier ancestor carries the witness for that ancestor; fuel exhaustion asserts neither kind of coverage and is excluded by production totality.

Equations

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

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

Native upper bounds and the coverage appropriate to the actual exit.

• bounded : Bounded bound before after
• coverage : ExitCover bound after stop witness exit

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

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

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

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

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

At the root, production's no-exhaustion theorem rules out the only exit without coverage; there is no earlier ancestor witness to discharge.