theorem
Hex.GraphIso.Nauty.Sparse.checkNode_valid
{n : Nat}
{G : SparseGraph n}
{tcLevel fuel level numcells : Nat}
{lab ptn : Array Nat}
{active : VSet n}
{cert : CertNode}
{B : Key n}
{a : Bool}
(h : checkNode G tcLevel fuel level lab ptn active numcells cert B = some a)
:
Replay.Valid G B (specLeaves G tcLevel fuel level lab ptn active numcells) a
Accepted sparse proof records bound every leaf of the literal native tree and identify attainment. No correctness assumption about a producer, cached code, target size, or proposed label enters the theorem.
theorem
Hex.GraphIso.Nauty.Sparse.checkKey_sound
{n k : Nat}
{G : Sparse.Colored n k}
{cert : CertNode}
{B : Key n}
(h : checkKey G cert B = true)
:
A checked attaining upper bound is the sparse declarative maximum.