def Hex.GraphIso.Nauty.Sparse.SpecLeaf.maximum {n : Nat} (G : SparseGraph n) : List (SpecLeaf n) → Key n

The scalar maximum of an existing unpruned leaf list. The empty case only totalizes this specification helper; sufficient-fuel theorems prove that every valid subtree used in the production proof has an attaining leaf.

Equations

• Hex.GraphIso.Nauty.Sparse.SpecLeaf.maximum G [] = { codes := [], graph := G }
• Hex.GraphIso.Nauty.Sparse.SpecLeaf.maximum G (first :: rest) = Hex.GraphIso.Nauty.Sparse.SpecLeaf.key G (Hex.GraphIso.Nauty.Sparse.SpecLeaf.best G first rest)

theorem Hex.GraphIso.Nauty.Sparse.SpecLeaf.maximum_attains {n : Nat} (G : SparseGraph n) {leaves : List (SpecLeaf n)} (hne : leaves ≠ []) : ∃ (leaf : SpecLeaf n), leaf ∈ leaves ∧ key G leaf = maximum G leaves

theorem Hex.GraphIso.Nauty.Sparse.SpecLeaf.maximum_bound {n : Nat} (G : SparseGraph n) {leaves : List (SpecLeaf n)} {leaf : SpecLeaf n} (hm : leaf ∈ leaves) : (key G leaf).Le (maximum G leaves)

theorem Hex.GraphIso.Nauty.Sparse.SpecLeaf.maximum_le {n : Nat} {G H : SparseGraph n} {left right : List (SpecLeaf n)} (hne : left ≠ []) (hm : ∀ (leaf : SpecLeaf n), leaf ∈ left → ∃ (other : SpecLeaf n), other ∈ right ∧ key H other = key G leaf) : (maximum G left).Le (maximum H right)

Leaf transport gives an inequality between subtree maxima, without requiring that the two enumerations use the same order or have unique keys.

def Hex.GraphIso.Nauty.Sparse.subtreeKey {n : Nat} (G : SparseGraph n) (tcLevel fuel level : Nat) (lab ptn : Array Nat) (active : VSet n) (numcells : Nat) : Key n

The native unpruned subtree's maximum. This aggregates specLeaves and introduces no alternate refinement or production search.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.GraphIso.Nauty.Sparse.SpecNode.key_attains {n : Nat} {G : SparseGraph n} {tcLevel fuel level numcells : Nat} {lab ptn : Array Nat} {active : VSet n} (h : SpecNode G level lab ptn active numcells) (hf : n < fuel + numcells) : ∃ (leaf : SpecLeaf n), leaf ∈ specLeaves G tcLevel fuel level lab ptn active numcells ∧ SpecLeaf.key G leaf = subtreeKey G tcLevel fuel level lab ptn active numcells

Every sufficiently fueled valid subtree has a literal attaining leaf.

theorem Hex.GraphIso.Nauty.Sparse.subtreeKey_bound {n : Nat} {G : SparseGraph n} {tcLevel fuel level numcells : Nat} {lab ptn : Array Nat} {active : VSet n} {leaf : SpecLeaf n} (hm : leaf ∈ specLeaves G tcLevel fuel level lab ptn active numcells) : (SpecLeaf.key G leaf).Le (subtreeKey G tcLevel fuel level lab ptn active numcells)

theorem Hex.GraphIso.Nauty.Sparse.root_maximum {n k : Nat} (G : Sparse.Colored n k) : SpecLeaf.maximum G.graph (rootLeaves G) = canonSpecKey G

The scalar maximum agrees with the existing root declaration and its attaining-label definition, including the special empty graph leaf.