theorem
Hex.GraphIso.Nauty.Sparse.SpecNode.target_child
{n : Nat}
{G : SparseGraph n}
{tcLevel level numcells : Nat}
{lab ptn : Array Nat}
{active : VSet n}
(h : SpecNode G level lab ptn active numcells)
:
have r := refine (Graph.ofGraph G) level lab ptn active numcells;
have target := maketargetcell (Graph.ofGraph G) r.lab r.ptn level tcLevel (-1);
discreteAt r.ptn level n = false →
∀ (o : Nat),
o < target.snd.snd →
have child := breakout n r.lab r.ptn (level + 1) target.fst r.lab[target.fst + o]!;
SpecNode G (level + 1) child.fst child.snd.fst child.snd.snd (r.numcells + 1)
Every child selected by the unpruned node's native target dispatch has the full entry invariant, including its inherited refinement certificate.
theorem
Hex.GraphIso.Nauty.Sparse.subtreeKey_discrete
{n : Nat}
{G : SparseGraph n}
{tcLevel fuel level numcells : Nat}
{lab ptn : Array Nat}
{active : VSet n}
{label : Label n}
:
have r := refine (Graph.ofGraph G) level lab ptn active numcells;
discreteAt r.ptn level n = true →
Label.ofArray? n r.lab = some label →
subtreeKey G tcLevel (fuel + 1) level lab ptn active numcells = { codes := [r.longcode, codeSentinel], graph := G.relabel label.perm }
The discrete unpruned node has exactly the key read from its executed refinement and parsed leaf label.
theorem
Hex.GraphIso.Nauty.Sparse.SpecNode.child_le
{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 + 1 + numcells)
:
have r := refine (Graph.ofGraph G) level lab ptn active numcells;
have target := maketargetcell (Graph.ofGraph G) r.lab r.ptn level tcLevel (-1);
discreteAt r.ptn level n = false →
∀ (o : Nat),
o < target.snd.snd →
(prefixKey [r.longcode]
(vertexKey G tcLevel fuel level r.lab r.ptn target.fst r.numcells r.lab[target.fst + o]!)).Le
(subtreeKey G tcLevel (fuel + 1) level lab ptn active numcells)
A child's entire maximum, prefixed by this node's code, lies below the node maximum. Sufficient fuel supplies its literal attaining leaf.
theorem
Hex.GraphIso.Nauty.Sparse.SpecNode.key_le
{n : Nat}
{G : SparseGraph n}
{tcLevel fuel level numcells : Nat}
{lab ptn : Array Nat}
{active : VSet n}
{bound : Key n}
(h : SpecNode G level lab ptn active numcells)
(hf : n < fuel + 1 + numcells)
:
have r := refine (Graph.ofGraph G) level lab ptn active numcells;
have target := maketargetcell (Graph.ofGraph G) r.lab r.ptn level tcLevel (-1);
discreteAt r.ptn level n = false →
(∀ (o : Nat),
o < target.snd.snd →
(prefixKey [r.longcode]
(vertexKey G tcLevel fuel level r.lab r.ptn target.fst r.numcells r.lab[target.fst + o]!)).Le
bound) →
(subtreeKey G tcLevel (fuel + 1) level lab ptn active numcells).Le bound
Bounding every complete child bounds the complete parent. The proof decomposes an actual attaining leaf of the existing unpruned enumeration.
theorem
Hex.GraphIso.Nauty.Sparse.SpecNode.child_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 + 1 + numcells)
:
have r := refine (Graph.ofGraph G) level lab ptn active numcells;
have target := maketargetcell (Graph.ofGraph G) r.lab r.ptn level tcLevel (-1);
discreteAt r.ptn level n = false →
∃ (o : Nat), o < target.snd.snd ∧ prefixKey [r.longcode] (vertexKey G tcLevel fuel level r.lab r.ptn target.fst r.numcells r.lab[target.fst + o]!) = subtreeKey G tcLevel (fuel + 1) level lab ptn active numcells
An internal node's maximum is attained by one of its complete child maxima. The child is obtained from a literal attaining specification leaf.
theorem
Hex.GraphIso.Nauty.Sparse.SpecNode.key_prefix
{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 + 1 + numcells)
:
Every sufficiently fueled node maximum begins with that node's literal refinement code, irrespective of the chosen descendant.