Checked core bridge cuts and subdivision lifts

A separating edge of a finite core remains a separating unit edge after arbitrary positive subdivision. This file makes that elementary fact occurrence-safe: the selected ordered core slot is cut at its first unit step, and all of its interior vertices are put on the head side. Thus no choice of an interior point, and no assumption that a bridge has length one, is hidden in a generated core row.

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

Proof-free data for an oriented separating core slot. left is the tail side; the head side is its complement.

• left : Finset (Fin n)

  The chosen tail-side core vertices; validity requires the distinguished bridge to leave this set.

• bridge : Fin p

  The candidate separating slot, oriented from the chosen left side to its complement.

def MarkedGraphs.Certificate.CoreBridgeCut.Data.toCoreVertexCut {n p : ℕ} {core : Utilities.Certificate.ExplicitPotential.Core n p} (c : Data core) : Utilities.Certificate.CoreVertexCut.Data core

Forgetting that the distinguished core edge is a bridge gives an articulation cut at its tail. This is useful because the existing CoreVertexCut genus calculator can then be reused verbatim.

Equations

• c.toCoreVertexCut = { glue := core.tail c.bridge, left := c.left }

def MarkedGraphs.Certificate.CoreBridgeCut.Data.Valid {n p : ℕ} {core : Utilities.Certificate.ExplicitPotential.Core n p} (c : Data core) : Prop

Exact validity of an oriented core bridge cut. The selected slot goes from left to its complement; every other slot stays entirely on one side.

Equations

• c.Valid = (core.tail c.bridge ∈ c.left ∧ core.head c.bridge ∉ c.left ∧ ∀ (edge : Fin p), edge ≠ c.bridge → (core.tail edge ∈ c.left ↔ core.head edge ∈ c.left))

def MarkedGraphs.Certificate.CoreBridgeCut.Data.check {n p : ℕ} {core : Utilities.Certificate.ExplicitPotential.Core n p} (c : Data core) : Bool

Transparent executable replay of bridge-cut data.

Equations

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

@[simp]

theorem MarkedGraphs.Certificate.CoreBridgeCut.Data.check_eq_true_iff {n p : ℕ} {core : Utilities.Certificate.ExplicitPotential.Core n p} (c : Data core) : c.check = true ↔ c.Valid

theorem MarkedGraphs.Certificate.CoreBridgeCut.Data.toCoreVertexCut_valid {n p : ℕ} {core : Utilities.Certificate.ExplicitPotential.Core n p} (c : Data core) (h : c.Valid) : c.toCoreVertexCut.Valid

Valid bridge data gives a valid articulation cut at the bridge tail.

noncomputable def MarkedGraphs.Certificate.CoreBridgeCut.Data.leftVertices {n p : ℕ} (spec : Utilities.Certificate.SubdivisionGraph.Spec n p) (c : Data spec.core) : Finset spec.Vertex

The tail-side vertices after subdivision. An interior vertex is on the tail side exactly when both endpoints of its original core slot are there.

Equations

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

noncomputable def MarkedGraphs.Certificate.CoreBridgeCut.Data.rightVertices {n p : ℕ} (spec : Utilities.Certificate.SubdivisionGraph.Spec n p) (c : Data spec.core) : Finset spec.Vertex

The head-side vertices are the literal complement.

Equations

• MarkedGraphs.Certificate.CoreBridgeCut.Data.rightVertices spec c = Finset.univ \ MarkedGraphs.Certificate.CoreBridgeCut.Data.leftVertices spec c

@[simp]

theorem MarkedGraphs.Certificate.CoreBridgeCut.Data.mem_leftVertices_core {n p : ℕ} (spec : Utilities.Certificate.SubdivisionGraph.Spec n p) (c : Data spec.core) (vertex : Fin n) : spec.coreVertex vertex ∈ leftVertices spec c ↔ vertex ∈ c.left

@[simp]

theorem MarkedGraphs.Certificate.CoreBridgeCut.Data.mem_leftVertices_interior {n p : ℕ} (spec : Utilities.Certificate.SubdivisionGraph.Spec n p) (c : Data spec.core) (edge : Fin p) (offset : Fin (spec.length edge - 1)) : spec.interiorVertex edge offset ∈ leftVertices spec c ↔ spec.core.tail edge ∈ c.left ∧ spec.core.head edge ∈ c.left

@[simp]

theorem MarkedGraphs.Certificate.CoreBridgeCut.Data.mem_rightVertices_iff {n p : ℕ} (spec : Utilities.Certificate.SubdivisionGraph.Spec n p) (c : Data spec.core) (vertex : spec.Vertex) : vertex ∈ rightVertices spec c ↔ vertex ∉ leftVertices spec c

theorem MarkedGraphs.Certificate.CoreBridgeCut.Data.leftVertices_eq_coreVertexCut_leftVertices {n p : ℕ} (spec : Utilities.Certificate.SubdivisionGraph.Spec n p) (c : Data spec.core) : leftVertices spec c = Utilities.Certificate.CoreVertexCut.Data.leftVertices spec c.toCoreVertexCut

Both the bridge lift and the articulation lift put exactly the same vertices on the tail side.

theorem MarkedGraphs.Certificate.CoreBridgeCut.Data.leftVertices_nonempty {n p : ℕ} (spec : Utilities.Certificate.SubdivisionGraph.Spec n p) (c : Data spec.core) (h : c.Valid) : (leftVertices spec c).Nonempty

A valid cut has a nonempty left factor.

theorem MarkedGraphs.Certificate.CoreBridgeCut.Data.tailNeighbor_mem_rightVertices {n p : ℕ} (spec : Utilities.Certificate.SubdivisionGraph.Spec n p) (c : Data spec.core) (h : c.Valid) : spec.tailNeighbor c.bridge ∈ rightVertices spec c

The selected first-step neighbour belongs to the complementary factor.

theorem MarkedGraphs.Certificate.CoreBridgeCut.Data.tail_mem_leftVertices {n p : ℕ} (spec : Utilities.Certificate.SubdivisionGraph.Spec n p) (c : Data spec.core) (h : c.Valid) : spec.coreVertex (spec.core.tail c.bridge) ∈ leftVertices spec c

The tail endpoint of the selected bridge is on the left.

theorem MarkedGraphs.Certificate.CoreBridgeCut.Data.step_eq_bridge_zero_of_left_right {n p : ℕ} (spec : Utilities.Certificate.SubdivisionGraph.Spec n p) (c : Data spec.core) (h : c.Valid) (edge : Fin p) (offset : Fin (spec.length edge)) (hLeft : spec.stepLeft edge offset ∈ leftVertices spec c) (hRight : spec.stepRight edge offset ∈ rightVertices spec c) : edge = c.bridge ∧ ↑offset = 0

A subdivision unit step directed from the left side to the right side is necessarily the selected slot's first unit step.

theorem MarkedGraphs.Certificate.CoreBridgeCut.Data.not_step_right_left {n p : ℕ} (spec : Utilities.Certificate.SubdivisionGraph.Spec n p) (c : Data spec.core) (h : c.Valid) (edge : Fin p) (offset : Fin (spec.length edge)) : ¬(spec.stepLeft edge offset ∈ rightVertices spec c ∧ spec.stepRight edge offset ∈ leftVertices spec c)

No unit step can be directed from the complementary side back into the left side.

noncomputable def MarkedGraphs.Certificate.CoreBridgeCut.Data.toOneBridgeCut {n p : ℕ} (spec : Utilities.Certificate.SubdivisionGraph.Spec n p) (c : Data spec.core) (h : c.Valid) : OneBridgeCut spec.graph

Lift valid core bridge data to an occurrence-safe separating bridge cut of every positive subdivision.

Equations

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

theorem MarkedGraphs.Certificate.CoreBridgeCut.Data.leftGraph_genus {n p : ℕ} (spec : Utilities.Certificate.SubdivisionGraph.Spec n p) (c : Data spec.core) (h : c.Valid) : (toOneBridgeCut spec c h).leftGraph.genus = c.toCoreVertexCut.leftGenus

The left bridge factor has the genus computed from the finite tail-side core data. In particular this number is independent of all edge lengths.

theorem MarkedGraphs.Certificate.CoreBridgeCut.Data.rightGraph_genus_eq {n p : ℕ} (spec : Utilities.Certificate.SubdivisionGraph.Spec n p) (c : Data spec.core) (h : c.Valid) : (toOneBridgeCut spec c h).rightGraph.genus = spec.graph.genus - c.toCoreVertexCut.leftGenus

The complementary bridge factor genus is forced by additive genus across the separating unit edge.

@[simp]

theorem MarkedGraphs.Certificate.CoreBridgeCut.Data.toOneBridgeCut_left {n p : ℕ} (spec : Utilities.Certificate.SubdivisionGraph.Spec n p) (c : Data spec.core) (h : c.Valid) : (toOneBridgeCut spec c h).left = leftVertices spec c

@[simp]

theorem MarkedGraphs.Certificate.CoreBridgeCut.Data.toOneBridgeCut_right {n p : ℕ} (spec : Utilities.Certificate.SubdivisionGraph.Spec n p) (c : Data spec.core) (h : c.Valid) : (toOneBridgeCut spec c h).right = rightVertices spec c

@[simp]

theorem MarkedGraphs.Certificate.CoreBridgeCut.Data.toOneBridgeCut_leftAttach {n p : ℕ} (spec : Utilities.Certificate.SubdivisionGraph.Spec n p) (c : Data spec.core) (h : c.Valid) : (toOneBridgeCut spec c h).leftAttach = spec.coreVertex (spec.core.tail c.bridge)

@[simp]

theorem MarkedGraphs.Certificate.CoreBridgeCut.Data.toOneBridgeCut_rightAttach {n p : ℕ} (spec : Utilities.Certificate.SubdivisionGraph.Spec n p) (c : Data spec.core) (h : c.Valid) : (toOneBridgeCut spec c h).rightAttach = spec.tailNeighbor c.bridge