def Hex.GraphIso.Nauty.Sparse.Compact.produceNode? {n : Nat} (G : SparseGraph n) (tcLevel : Nat) (gens : List (Perm n)) : Nat → Nat → Array Nat → Array Nat → VSet n → Nat → Key n → Nat → Option (CertNode × Nat)

The compact proof walk with a shared record quota. Admission precedes refinement or witness proposals, and each sibling receives only unused quota. The native splitter, target, witness checks and lazy fallback are unchanged.

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.Sparse.Compact.produceNode? G tcLevel gens 0 x✝⁶ x✝⁵ x✝⁴ x✝³ x✝² x✝¹ x✝ = if x✝ = 0 then none else some (Hex.GraphIso.Nauty.Sparse.CertNode.leaf, x✝ - 1)

theorem Hex.GraphIso.Nauty.Sparse.Compact.produceNode?_budget {n : Nat} {G : SparseGraph n} {tcLevel : Nat} {gens : List (Perm n)} (fuel : Nat) {level : Nat} {lab ptn : Array Nat} {active : VSet n} {nc : Nat} {B : Key n} {remaining final : Nat} {c : CertNode} (h : produceNode? G tcLevel gens fuel level lab ptn active nc B remaining = some (c, final)) : c.stats.records + final = remaining

The bounded producer's counter is exactly the size of its emitted certificate, including all compact references.

theorem Hex.GraphIso.Nauty.Sparse.Compact.produceNode?_eq {n : Nat} {G : SparseGraph n} {tcLevel : Nat} {gens : List (Perm n)} (fuel : Nat) {level : Nat} {lab ptn : Array Nat} {active : VSet n} {nc : Nat} {B : Key n} {remaining final : Nat} {c : CertNode} (h : produceNode? G tcLevel gens fuel level lab ptn active nc B remaining = some (c, final)) : c = produceNode G tcLevel gens fuel level lab ptn active nc B

Successful quota-limited production retains the unlimited compact producer's exact tree, including its literal automorphism references.

def Hex.GraphIso.Nauty.Sparse.Compact.produceRoot? {n k : Nat} (maxRecords : Nat) (G : Sparse.Colored n k) (gens : List (Perm n)) (B : Key n) : Option (CertNode × Nat)

Initialize the bounded proof walk with the native stable colour cells. The empty graph has one leaf record.

Equations

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

theorem Hex.GraphIso.Nauty.Sparse.Compact.produceRoot?_budget {n k maxRecords : Nat} {G : Sparse.Colored n k} {gens : List (Perm n)} {B : Key n} {c : CertNode} {rest : Nat} (h : produceRoot? maxRecords G gens B = some (c, rest)) : c.stats.records + rest = maxRecords

theorem Hex.GraphIso.Nauty.Sparse.Compact.produceRoot?_records {n k maxRecords : Nat} {G : Sparse.Colored n k} {gens : List (Perm n)} {B : Key n} {c : CertNode} {rest : Nat} (h : produceRoot? maxRecords G gens B = some (c, rest)) : c.stats.records ≤ maxRecords

theorem Hex.GraphIso.Nauty.Sparse.Compact.produceRoot?_eq {n k maxRecords : Nat} {G : Sparse.Colored n k} {gens : List (Perm n)} {B : Key n} {c : CertNode} {rest : Nat} (h : produceRoot? maxRecords G gens B = some (c, rest)) : c = produceRoot G gens B

theorem Hex.GraphIso.Nauty.Sparse.Compact.produceRoot?_replays {n k maxRecords : Nat} {G : Sparse.Colored n k} {gens : List (Perm n)} {c : CertNode} {rest : Nat} (h : produceRoot? maxRecords G gens (canonSpecKey G) = some (c, rest)) : checkKey G c (canonSpecKey G) = true

def Hex.GraphIso.Nauty.Sparse.Compact.candidate? {n k : Nat} (maxRecords : Nat) (G : Sparse.Colored n k) (s : State n) : Option (CertCandidate n × Nat)

Retain a supplied native search's key, label and generators while bounding certificate construction. The caller can share a search quota across graphs without repeating either optimized search.

Equations

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

theorem Hex.GraphIso.Nauty.Sparse.Compact.candidate?_budget {n k maxRecords : Nat} {G : Sparse.Colored n k} {s : State n} {c : CertCandidate n} {rest : Nat} (h : candidate? maxRecords G s = some (c, rest)) : c.tree.stats.records + rest = maxRecords

theorem Hex.GraphIso.Nauty.Sparse.Compact.candidate?_label {n k maxRecords : Nat} {G : Sparse.Colored n k} {s : State n} {c : CertCandidate n} {rest : Nat} (h : candidate? maxRecords G s = some (c, rest)) : c.lab = s.canonlab