structure Hex.GraphIso.Nauty.Sparse.CertStats : Type

Sizes of the actual certificate, including every reference payload. These counters use unbounded natural numbers and one tree traversal.

• records : Nat
• automorphisms : Nat
• permutationEntries : Nat

def Hex.GraphIso.Nauty.Sparse.instReprCertStats.repr : CertStats → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Hex.GraphIso.Nauty.Sparse.instReprCertStats : Repr CertStats

Equations

• Hex.GraphIso.Nauty.Sparse.instReprCertStats = { reprPrec := Hex.GraphIso.Nauty.Sparse.instReprCertStats.repr }

@[instance_reducible]

instance Hex.GraphIso.Nauty.Sparse.instBEqCertStats : BEq CertStats

Equations

• Hex.GraphIso.Nauty.Sparse.instBEqCertStats = { beq := Hex.GraphIso.Nauty.Sparse.instBEqCertStats.beq }

def Hex.GraphIso.Nauty.Sparse.instBEqCertStats.beq : CertStats → CertStats → Bool

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.Sparse.instBEqCertStats.beq x✝¹ x✝ = false

def Hex.GraphIso.Nauty.Sparse.CertNode.stats : CertNode → CertStats

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.Sparse.CertNode.leaf.stats = { records := 1, automorphisms := 0, permutationEntries := 0 }
• Hex.GraphIso.Nauty.Sparse.CertNode.codePrune.stats = { records := 1, automorphisms := 0, permutationEntries := 0 }
• (Hex.GraphIso.Nauty.Sparse.CertNode.autom earlier raw).stats = { records := 1, automorphisms := 1, permutationEntries := raw.size }

def Hex.GraphIso.Nauty.Sparse.CertNode.statsList : List CertNode → CertStats

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.Sparse.CertNode.statsList [] = { records := 0, automorphisms := 0, permutationEntries := 0 }

theorem Hex.GraphIso.Nauty.Sparse.CertNode.records_pos (c : CertNode) : 0 < c.stats.records

def Hex.GraphIso.Nauty.Sparse.Compact.checkRecords? {n k : Nat} (maxRecords : Nat) (G : Sparse.Colored n k) (cert : CertNode) (B : Key n) : Option Bool

Apply the certificate-record limit before replaying any proof rule. none is exhaustion, some false is a rejected certificate, and only some true supplies an accepted canonical key.

Equations

• Hex.GraphIso.Nauty.Sparse.Compact.checkRecords? maxRecords G cert B = if cert.stats.records ≤ maxRecords then some (Hex.GraphIso.Nauty.Sparse.Compact.checkKey G cert B) else none

theorem Hex.GraphIso.Nauty.Sparse.Compact.checkRecords?_eq_some {n k maxRecords : Nat} {G : Sparse.Colored n k} {cert : CertNode} {B : Key n} {b : Bool} : checkRecords? maxRecords G cert B = some b ↔ cert.stats.records ≤ maxRecords ∧ checkKey G cert B = b

Successful bounded replay has exactly the unlimited checker's verdict, and its complete certificate fits the record limit.

theorem Hex.GraphIso.Nauty.Sparse.Compact.checkRecords?_sound {n k maxRecords : Nat} {G : Sparse.Colored n k} {cert : CertNode} {B : Key n} (h : checkRecords? maxRecords G cert B = some true) : canonSpecKey G = B

theorem Hex.GraphIso.Nauty.Sparse.Compact.checkRecords?_none {n k maxRecords : Nat} {G : Sparse.Colored n k} {cert : CertNode} {B : Key n} : checkRecords? maxRecords G cert B = none ↔ maxRecords < cert.stats.records

theorem Hex.GraphIso.Nauty.Sparse.Compact.checkRecords?_zero {n k : Nat} (G : Sparse.Colored n k) (cert : CertNode) (B : Key n) : checkRecords? 0 G cert B = none

theorem Hex.GraphIso.Nauty.Sparse.Compact.produceRoot_records {n k : Nat} (G : Sparse.Colored n k) (gens : List (Perm n)) (maxRecords : Nat) (h : (produceRoot G gens (canonSpecKey G)).stats.records ≤ maxRecords) : checkRecords? maxRecords G (produceRoot G gens (canonSpecKey G)) (canonSpecKey G) = some true

Every unlimited produced certificate is admitted once the finite record limit covers its actual size. No isomorphism conclusion follows from exhaustion.

def Hex.GraphIso.Nauty.Sparse.Literal.Compact.checkRecords? {n k : Nat} (maxRecords : Nat) (G : Sparse.Colored n k) (cert : CertNode) (B : Key n) : Option Bool

Literal record-limited replay has the native checker's exact verdict.

Equations

• Hex.GraphIso.Nauty.Sparse.Literal.Compact.checkRecords? maxRecords G cert B = if cert.stats.records ≤ maxRecords then some (Hex.GraphIso.Nauty.Sparse.Literal.Compact.checkKey G cert B) else none

theorem Hex.GraphIso.Nauty.Sparse.Literal.Compact.checkRecords?_eq : @checkRecords? = @Sparse.Compact.checkRecords?

theorem Hex.GraphIso.Nauty.Sparse.Literal.Compact.checkRecords?_sound {n k maxRecords : Nat} {G : Sparse.Colored n k} {cert : CertNode} {B : Key n} (h : checkRecords? maxRecords G cert B = some true) : canonSpecKey G = B