Fast validation of certificates against packed incidence tables

def Erdos97Octagon.RawIncidence.packedExtendsTreeB (code : UInt64) (reached : Finset Vertex) : List Vertex → Bool

Validate the tail of a mutual-edge tree directly against a packed table.

Equations

• One or more equations did not get rendered due to their size.
• Erdos97Octagon.RawIncidence.packedExtendsTreeB code reached [] = true

def Erdos97Octagon.RawIncidence.packedComponentTreeB (code : UInt64) (root : Vertex) : List Vertex → Bool

Validate a mutual-edge spanning tree directly against a packed table.

Equations

• Erdos97Octagon.RawIncidence.packedComponentTreeB code root [] = false
• Erdos97Octagon.RawIncidence.packedComponentTreeB code root (vertex :: remaining) = (decide (vertex = root) && Erdos97Octagon.RawIncidence.packedExtendsTreeB code {root} remaining)

def Erdos97Octagon.RawIncidence.Certificate.validPackedB (code : UInt64) : Certificate → Bool

Kernel-check a certificate without first materializing eight finite sets.

Equations

• One or more equations did not get rendered due to their size.
• Erdos97Octagon.RawIncidence.Certificate.validPackedB code (Erdos97Octagon.RawIncidence.Certificate.residual payload) = Erdos97Octagon.RawIncidence.packedResidualValidB✝ code payload

theorem Erdos97Octagon.RawIncidence.Certificate.valid_of_validPackedB {code : UInt64} {certificate : Certificate} (hvalid : validPackedB code certificate = true) : Valid (packedIncidence code) certificate

Packed validation supplies the mathematical certificate predicate.