Connectivity of positive subdivisions

The explicit-potential checker works with a finite ordered core and then replaces every edge slot by a path of positive integral length. This file keeps the connectivity trust boundary finite: ExplicitPotential.Core.Connected is a cut certificate on the ordered core slots, and SubdivisionGraph.Spec.graph_connected_of_coreConnected proves that every positive subdivision of such a core is connected.

The proof uses only the cut definition of graphConnected. If no subdivided unit edge crosses a cut, membership is constant along each subdivided path. It is therefore constant on the core by core connectedness, and then constant on every interior vertex as well.

def Utilities.Certificate.ExplicitPotential.Core.Connected {n p : ℕ} (core : Core n p) : Prop

Cut connectedness for an ordered loopless core. Edge slots, rather than endpoint pairs, are quantified so parallel edges are retained exactly.

Equations

• core.Connected = ∀ (S : Finset (Fin n)), (∃ (v : Fin n) (w : Fin n), v ∈ S ∧ w ∉ S) → ∃ (edge : Fin p), core.tail edge ∈ S ∧ core.head edge ∉ S ∨ core.head edge ∈ S ∧ core.tail edge ∉ S

def Utilities.Certificate.ExplicitPotential.Core.connectedCheck {n p : ℕ} (core : Core n p) : Bool

Exact finite Boolean checker for core connectedness.

Equations

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

@[simp]

theorem Utilities.Certificate.ExplicitPotential.Core.connectedCheck_eq_true_iff {n p : ℕ} (core : Core n p) : core.connectedCheck = true ↔ core.Connected

theorem Utilities.Certificate.SubdivisionGraph.Spec.coreEndpoints_mem_iff_of_noCrossing {n p : ℕ} (spec : Spec n p) (A : Finset spec.graph.V) (hNoCrossing : ∀ x ∈ A, ∀ y ∉ A, numEdges spec.graph x y = 0) (edge : Fin p) : spec.coreVertex (spec.core.tail edge) ∈ A ↔ spec.coreVertex (spec.core.head edge) ∈ A

If no edge crosses a vertex cut, membership is constant along every subdivided core edge.

theorem Utilities.Certificate.SubdivisionGraph.Spec.coreTail_mem_iff_interior_mem_of_noCrossing {n p : ℕ} (spec : Spec n p) (A : Finset spec.graph.V) (hNoCrossing : ∀ x ∈ A, ∀ y ∉ A, numEdges spec.graph x y = 0) (edge : Fin p) (offset : Fin (spec.length edge - 1)) : spec.coreVertex (spec.core.tail edge) ∈ A ↔ spec.interiorVertex edge offset ∈ A

If no edge crosses a vertex cut, an interior vertex lies on the same side as the tail of its core edge.

theorem Utilities.Certificate.SubdivisionGraph.Spec.graph_connected_of_coreConnected {n p : ℕ} (spec : Spec n p) (hCoreConnected : spec.core.Connected) : graphConnected spec.graph

Positive subdivision preserves connectedness of the ordered core.