theorem
Hex.GraphIso.Nauty.Sparse.Compact.produceNode?_complete
{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 : Nat}
(hq : (produceNode G tcLevel gens fuel level lab ptn active nc B).stats.records ≤ remaining)
:
produceNode? G tcLevel gens fuel level lab ptn active nc B remaining = some
(produceNode G tcLevel gens fuel level lab ptn active nc B, remaining - (produceNode G tcLevel gens fuel level lab ptn active nc B).stats.records)
The exact unlimited certificate size is a sufficient record quota. This follows the executed bounded recursion, including lazy witness reuse.
theorem
Hex.GraphIso.Nauty.Sparse.Compact.produceRoot?_complete
{n k maxRecords : Nat}
{G : Sparse.Colored n k}
{gens : List (Perm n)}
{B : Key n}
(hq : (produceRoot G gens B).stats.records ≤ maxRecords)
:
produceRoot? maxRecords G gens B = some (produceRoot G gens B, maxRecords - (produceRoot G gens B).stats.records)
theorem
Hex.GraphIso.Nauty.Sparse.Compact.produceRoot?_none
{n k maxRecords : Nat}
{G : Sparse.Colored n k}
{gens : List (Perm n)}
{B : Key n}
:
Exhaustion occurs exactly when the unlimited tree exceeds the record cap.
theorem
Hex.GraphIso.Nauty.Sparse.Compact.candidate?_complete
{n k maxRecords : Nat}
{G : Sparse.Colored n k}
{c : CertCandidate n}
(hc : produceCand G = some c)
(hq : c.tree.stats.records ≤ maxRecords)
:
A sufficient record quota packages exactly the unlimited candidate from the optimized native search, retaining its key and literal label.
theorem
Hex.GraphIso.Nauty.Sparse.Compact.candidate?_agrees
{n k maxRecords : Nat}
{G : Sparse.Colored n k}
{c : CertCandidate n}
{rest : Nat}
(h : candidate? maxRecords G (runColored G) = some (c, rest))
:
Every successful bounded candidate from the direct run is exactly the unlimited candidate, without any extra assumption on its proposed key.
theorem
Hex.GraphIso.Nauty.Sparse.Compact.candidate?_from_run
{n k maxNodes maxRecords : Nat}
{G : Sparse.Colored n k}
{s : Limited.State n}
{c : CertCandidate n}
{rest : Nat}
(hs : Limited.runColored? maxNodes G = some s)
(hc : candidate? maxRecords G s.value = some (c, rest))
:
Accepted bounded search and bounded certificate production retain the optimized producer's full candidate. Both limits may be arbitrary.
theorem
Hex.GraphIso.Nauty.Sparse.Compact.candidate?_replays
{n k maxNodes maxRecords : Nat}
{G : Sparse.Colored n k}
{s : Limited.State n}
{c : CertCandidate n}
{rest : Nat}
(hs : Limited.runColored? maxNodes G = some s)
(hc : candidate? maxRecords G s.value = some (c, rest))
: