Kernel-cheap spanning-tree connectivity certificates

The cut checker for a finite core enumerates every vertex subset. Generated cores can instead display a root, one parent and incident parent-edge slot for every vertex, and a strictly decreasing rank along parent links. Checking those local facts is linear in the number of vertices.

The parent/rank argument is proved once below: in either side of a nontrivial cut not containing the root, a minimum-rank vertex has its parent outside that side, so its displayed parent edge crosses the cut. The external program which chooses this data is not trusted.

def MarkedGraphs.Certificate.SpanningTreeConnectivity.EdgeJoins {n p : ℕ} (core : Utilities.Certificate.ExplicitPotential.Core n p) (edge : Fin p) (first second : Fin n) : Prop

An unordered edge slot joins the displayed pair of vertices.

Equations

• MarkedGraphs.Certificate.SpanningTreeConnectivity.EdgeJoins core edge first second = (core.tail edge = first ∧ core.head edge = second ∨ core.tail edge = second ∧ core.head edge = first)

structure MarkedGraphs.Certificate.SpanningTreeConnectivity.CertificateData {n p : ℕ} (core : Utilities.Certificate.ExplicitPotential.Core n p) : Type

Proof-free rooted parent data for an ordered finite multigraph core.

• root : Fin n

  The proposed root of the spanning-tree parent certificate.

• parent : Fin n → Fin n

  The proposed parent of each vertex; validity requires every non-root parent link to be an edge and decrease rank.

• parentEdge : Fin n → Fin p

  The core slot proposed to join each non-root vertex to its parent.

• rank : Fin n → ℕ

  The natural rank intended to decrease strictly along every non-root parent link, ruling out cycles.

def MarkedGraphs.Certificate.SpanningTreeConnectivity.CertificateData.Valid {n p : ℕ} {core : Utilities.Certificate.ExplicitPotential.Core n p} (data : CertificateData core) : Prop

Mathematical validity of every non-root parent link.

Equations

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

def MarkedGraphs.Certificate.SpanningTreeConnectivity.CertificateData.check {n p : ℕ} {core : Utilities.Certificate.ExplicitPotential.Core n p} (data : CertificateData core) : Bool

Linear-time exact checker for rooted parent data.

Equations

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

@[simp]

theorem MarkedGraphs.Certificate.SpanningTreeConnectivity.CertificateData.check_eq_true_iff {n p : ℕ} {core : Utilities.Certificate.ExplicitPotential.Core n p} (data : CertificateData core) : data.check = true ↔ data.Valid

theorem MarkedGraphs.Certificate.SpanningTreeConnectivity.CertificateData.coreConnected_of_valid {n p : ℕ} {core : Utilities.Certificate.ExplicitPotential.Core n p} (data : CertificateData core) (hValid : data.Valid) : core.Connected

Valid rooted parent data imply the exact cut-connectedness predicate used by explicit-potential cores.

theorem MarkedGraphs.Certificate.SpanningTreeConnectivity.CertificateData.coreConnected_of_check_eq_true {n p : ℕ} {core : Utilities.Certificate.ExplicitPotential.Core n p} (data : CertificateData core) (hCheck : data.check = true) : core.Connected

Checker acceptance implies exact ordered-core connectedness.

theorem MarkedGraphs.Certificate.SpanningTreeConnectivity.SubdivisionGraph.Spec.graph_connected_of_spanningCheck {n p : ℕ} (spec : Utilities.Certificate.SubdivisionGraph.Spec n p) (data : CertificateData spec.core) (hCheck : data.check = true) : graphConnected spec.graph

A checked parent certificate on the ordered core proves connectivity of every positive subdivision as a chip-firing graph.

Closed ordinary-kernel regressions

def MarkedGraphs.Certificate.SpanningTreeConnectivity.Examples.pathCore : Utilities.Certificate.ExplicitPotential.Core 3 2

The three-vertex path with ordered slots from 0 to 1 and from 1 to 2.

Equations

• MarkedGraphs.Certificate.SpanningTreeConnectivity.Examples.pathCore = { tail := ![0, 1], head := ![1, 2] }

def MarkedGraphs.Certificate.SpanningTreeConnectivity.Examples.pathCertificate : CertificateData pathCore

The valid parent certificate for the three-vertex path, rooted at 0 with ranks 0, 1, and 2.

Equations

• MarkedGraphs.Certificate.SpanningTreeConnectivity.Examples.pathCertificate = { root := 0, parent := ![0, 0, 1], parentEdge := ![0, 0, 1], rank := ![0, 1, 2] }

theorem MarkedGraphs.Certificate.SpanningTreeConnectivity.Examples.pathCore_connected : pathCore.Connected

def MarkedGraphs.Certificate.SpanningTreeConnectivity.Examples.badRankCertificate : CertificateData pathCore

An intentionally invalid path certificate with constant zero rank, rejected because non-root links do not decrease rank.

Equations

• MarkedGraphs.Certificate.SpanningTreeConnectivity.Examples.badRankCertificate = { root := 0, parent := ![0, 0, 1], parentEdge := ![0, 0, 1], rank := ![0, 0, 0] }