The embedded core is a strong separator of a subdivision

This module supplies the graph-theoretic part of an explicit-potential rank certificate. Every component left after removing an enlargement of the embedded core is a contiguous interval in the interior of one subdivided edge. Such an interval has two boundary vertices, at most one boundary edge at each reached vertex, and the elementary path-cut property required by StrongSeparator.ExpansionCell.

Vertices along one subdivided edge

@[reducible, inline]

abbrev Utilities.Certificate.SubdivisionGraph.Spec.PathPosition {n p : ℕ} (spec : Spec n p) (edge : Fin p) : Type

Positions from the tail (0) through the head (length).

Equations

• spec.PathPosition edge = Fin (spec.length edge + 1)

def Utilities.Certificate.SubdivisionGraph.Spec.pathVertex {n p : ℕ} (spec : Spec n p) (edge : Fin p) (position : spec.PathPosition edge) : spec.Vertex

The vertex at a path position.

Equations

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

def Utilities.Certificate.SubdivisionGraph.Spec.stepLeftPosition {n p : ℕ} (spec : Spec n p) (edge : Fin p) (offset : Fin (spec.length edge)) : spec.PathPosition edge

Position of the left endpoint of a unit step.

Equations

• spec.stepLeftPosition edge offset = ⟨↑offset, ⋯⟩

def Utilities.Certificate.SubdivisionGraph.Spec.stepRightPosition {n p : ℕ} (spec : Spec n p) (edge : Fin p) (offset : Fin (spec.length edge)) : spec.PathPosition edge

Position of the right endpoint of a unit step.

Equations

• spec.stepRightPosition edge offset = ⟨↑offset + 1, ⋯⟩

theorem Utilities.Certificate.SubdivisionGraph.Spec.pathVertex_zero {n p : ℕ} (spec : Spec n p) (edge : Fin p) : spec.pathVertex edge ⟨0, ⋯⟩ = spec.coreVertex (spec.core.tail edge)

@[simp]

theorem Utilities.Certificate.SubdivisionGraph.Spec.pathVertex_length {n p : ℕ} (spec : Spec n p) (edge : Fin p) : spec.pathVertex edge ⟨spec.length edge, ⋯⟩ = spec.coreVertex (spec.core.head edge)

@[simp]

theorem Utilities.Certificate.SubdivisionGraph.Spec.pathVertex_stepLeftPosition {n p : ℕ} (spec : Spec n p) (edge : Fin p) (offset : Fin (spec.length edge)) : spec.pathVertex edge (spec.stepLeftPosition edge offset) = spec.stepLeft edge offset

@[simp]

theorem Utilities.Certificate.SubdivisionGraph.Spec.pathVertex_stepRightPosition {n p : ℕ} (spec : Spec n p) (edge : Fin p) (offset : Fin (spec.length edge)) : spec.pathVertex edge (spec.stepRightPosition edge offset) = spec.stepRight edge offset

theorem Utilities.Certificate.SubdivisionGraph.Spec.pathVertex_injective {n p : ℕ} (spec : Spec n p) (edge : Fin p) : Function.Injective (spec.pathVertex edge)

Distinct positions on one loopless core slot give distinct subdivision vertices, including its two core endpoints.

theorem Utilities.Certificate.SubdivisionGraph.Spec.consecutive_num_edges_pos {n p : ℕ} (spec : Spec n p) (edge : Fin p) (offset : Fin (spec.length edge)) : 0 < numEdges spec.graph (spec.pathVertex edge (spec.stepLeftPosition edge offset)) (spec.pathVertex edge (spec.stepRightPosition edge offset))

Consecutive positions are joined by the corresponding unit step.

def Utilities.Certificate.SubdivisionGraph.Spec.IsInteriorPosition {n p : ℕ} (spec : Spec n p) (edge : Fin p) (position : spec.PathPosition edge) : Prop

A numerical path position is strictly internal to its edge.

Equations

• spec.IsInteriorPosition edge position = (0 < ↑position ∧ ↑position < spec.length edge)

def Utilities.Certificate.SubdivisionGraph.Spec.interiorOffsetOfPosition {n p : ℕ} (spec : Spec n p) (edge : Fin p) (position : spec.PathPosition edge) (hInterior : spec.IsInteriorPosition edge position) : Fin (spec.length edge - 1)

Interior-vertex coordinate represented by an internal path position.

Equations

• spec.interiorOffsetOfPosition edge position hInterior = ⟨↑position - 1, ⋯⟩

def Utilities.Certificate.SubdivisionGraph.Spec.previousPathPosition {n p : ℕ} (spec : Spec n p) (edge : Fin p) (position : spec.PathPosition edge) (hPositive : 0 < ↑position) : spec.PathPosition edge

Predecessor of a positive path position.

Equations

• spec.previousPathPosition edge position hPositive = ⟨↑position - 1, ⋯⟩

def Utilities.Certificate.SubdivisionGraph.Spec.nextPathPosition {n p : ℕ} (spec : Spec n p) (edge : Fin p) (position : spec.PathPosition edge) (hBeforeHead : ↑position < spec.length edge) : spec.PathPosition edge

Successor of a position strictly before the head.

Equations

• spec.nextPathPosition edge position hBeforeHead = ⟨↑position + 1, ⋯⟩

theorem Utilities.Certificate.SubdivisionGraph.Spec.pathVertex_eq_interiorVertex {n p : ℕ} (spec : Spec n p) (edge : Fin p) (position : spec.PathPosition edge) (hInterior : spec.IsInteriorPosition edge position) : spec.pathVertex edge position = spec.interiorVertex edge (spec.interiorOffsetOfPosition edge position hInterior)

theorem Utilities.Certificate.SubdivisionGraph.Spec.previousVertex_eq_pathVertex {n p : ℕ} (spec : Spec n p) (edge : Fin p) (position : spec.PathPosition edge) (hInterior : spec.IsInteriorPosition edge position) : spec.previousVertex edge (spec.interiorOffsetOfPosition edge position hInterior) = spec.pathVertex edge (spec.previousPathPosition edge position ⋯)

theorem Utilities.Certificate.SubdivisionGraph.Spec.nextVertex_eq_pathVertex {n p : ℕ} (spec : Spec n p) (edge : Fin p) (position : spec.PathPosition edge) (hInterior : spec.IsInteriorPosition edge position) : spec.nextVertex edge (spec.interiorOffsetOfPosition edge position hInterior) = spec.pathVertex edge (spec.nextPathPosition edge position ⋯)

theorem Utilities.Certificate.SubdivisionGraph.Spec.pathVertex_num_edges_pos_iff {n p : ℕ} (spec : Spec n p) (edge : Fin p) (position : spec.PathPosition edge) (hInterior : spec.IsInteriorPosition edge position) (vertex : spec.Vertex) : 0 < numEdges spec.graph (spec.pathVertex edge position) vertex ↔ vertex = spec.pathVertex edge (spec.previousPathPosition edge position ⋯) ∨ vertex = spec.pathVertex edge (spec.nextPathPosition edge position ⋯)

At an internal path position, positivity of an edge multiplicity is equivalent to being the immediately preceding or following path vertex.

theorem Utilities.Certificate.SubdivisionGraph.Spec.previousVertex_ne_nextVertex {n p : ℕ} (spec : Spec n p) (edge : Fin p) (offset : Fin (spec.length edge - 1)) : spec.previousVertex edge offset ≠ spec.nextVertex edge offset

The two path neighbors of an interior subdivision vertex are distinct.

theorem Utilities.Certificate.SubdivisionGraph.Spec.unitEdge_incident_interior_iff {n p : ℕ} (spec : Spec n p) (edge : Fin p) (offset : Fin (spec.length edge - 1)) (vertex : spec.Vertex) (step : spec.Step) : spec.unitEdge step = (spec.interiorVertex edge offset, vertex) ∨ spec.unitEdge step = (vertex, spec.interiorVertex edge offset) ↔ step = ⟨edge, spec.nextStep edge offset⟩ ∧ vertex = spec.nextVertex edge offset ∨ step = ⟨edge, spec.previousStep edge offset⟩ ∧ vertex = spec.previousVertex edge offset

Exact classification of unit steps incident to one interior vertex.

theorem Utilities.Certificate.SubdivisionGraph.Spec.num_edges_interior_le_one {n p : ℕ} (spec : Spec n p) (edge : Fin p) (offset : Fin (spec.length edge - 1)) (vertex : spec.Vertex) : numEdges spec.graph (spec.interiorVertex edge offset) vertex ≤ 1

Every edge incident to an interior subdivision vertex has multiplicity at most one. Parallel core slots cannot create parallel edges here because the interior vertex remembers its own slot.

Complement intervals

structure Utilities.Certificate.SubdivisionGraph.Spec.ComplementInterval {n p : ℕ} (spec : Spec n p) (R : Finset spec.Vertex) : Type

A nonempty open path interval whose endpoints lie in R and whose interior is disjoint from R.

• edge : Fin p

  The slot containing this interval of the complement of R.

• left : spec.PathPosition self.edge

  The left path endpoint, whose corresponding subdivision vertex belongs to R.

• right : spec.PathPosition self.edge

  The right path endpoint, also in R, with all strictly intermediate path vertices outside R.

• center : spec.PathPosition self.edge

  A path position strictly between the interval endpoints, hence representing a vertex outside R.

• left_lt_center : ↑self.left < ↑self.center
• center_lt_right : ↑self.center < ↑self.right
• left_mem : spec.pathVertex self.edge self.left ∈ R
• right_mem : spec.pathVertex self.edge self.right ∈ R
• interior_not_mem (position : spec.PathPosition self.edge) : ↑self.left < ↑position → ↑position < ↑self.right → spec.pathVertex self.edge position ∉ R

def Utilities.Certificate.SubdivisionGraph.Spec.ComplementInterval.positions {n p : ℕ} {spec : Spec n p} {R : Finset spec.Vertex} (interval : spec.ComplementInterval R) : Finset (spec.PathPosition interval.edge)

Positions in the open interval.

Equations

• interval.positions = {position : spec.PathPosition interval.edge | ↑interval.left < ↑position ∧ ↑position < ↑interval.right}

def Utilities.Certificate.SubdivisionGraph.Spec.ComplementInterval.carrier {n p : ℕ} {spec : Spec n p} {R : Finset spec.Vertex} (interval : spec.ComplementInterval R) : Finset spec.Vertex

Vertices in the complementary path interval.

Equations

• interval.carrier = Finset.image (spec.pathVertex interval.edge) interval.positions

@[simp]

theorem Utilities.Certificate.SubdivisionGraph.Spec.ComplementInterval.mem_positions_iff {n p : ℕ} {spec : Spec n p} {R : Finset spec.Vertex} (interval : spec.ComplementInterval R) (position : spec.PathPosition interval.edge) : position ∈ interval.positions ↔ ↑interval.left < ↑position ∧ ↑position < ↑interval.right

theorem Utilities.Certificate.SubdivisionGraph.Spec.ComplementInterval.mem_carrier_iff {n p : ℕ} {spec : Spec n p} {R : Finset spec.Vertex} (interval : spec.ComplementInterval R) (vertex : spec.Vertex) : vertex ∈ interval.carrier ↔ ∃ (position : spec.PathPosition interval.edge), ↑interval.left < ↑position ∧ ↑position < ↑interval.right ∧ spec.pathVertex interval.edge position = vertex

theorem Utilities.Certificate.SubdivisionGraph.Spec.ComplementInterval.position_isInterior {n p : ℕ} {spec : Spec n p} {R : Finset spec.Vertex} (interval : spec.ComplementInterval R) {position : spec.PathPosition interval.edge} (hLeft : ↑interval.left < ↑position) (hRight : ↑position < ↑interval.right) : spec.IsInteriorPosition interval.edge position

theorem Utilities.Certificate.SubdivisionGraph.Spec.ComplementInterval.carrier_nonempty {n p : ℕ} {spec : Spec n p} {R : Finset spec.Vertex} (interval : spec.ComplementInterval R) : interval.carrier.Nonempty

theorem Utilities.Certificate.SubdivisionGraph.Spec.ComplementInterval.carrier_disjoint {n p : ℕ} {spec : Spec n p} {R : Finset spec.Vertex} (interval : spec.ComplementInterval R) : Disjoint interval.carrier R

def Utilities.Certificate.SubdivisionGraph.Spec.ComplementInterval.firstPosition {n p : ℕ} {spec : Spec n p} {R : Finset spec.Vertex} (interval : spec.ComplementInterval R) : spec.PathPosition interval.edge

First vertex of the open interval.

Equations

• interval.firstPosition = ⟨↑interval.left + 1, ⋯⟩

def Utilities.Certificate.SubdivisionGraph.Spec.ComplementInterval.lastPosition {n p : ℕ} {spec : Spec n p} {R : Finset spec.Vertex} (interval : spec.ComplementInterval R) : spec.PathPosition interval.edge

Final vertex of the open interval.

Equations

• interval.lastPosition = ⟨↑interval.right - 1, ⋯⟩

theorem Utilities.Certificate.SubdivisionGraph.Spec.ComplementInterval.firstPosition_mem {n p : ℕ} {spec : Spec n p} {R : Finset spec.Vertex} (interval : spec.ComplementInterval R) : interval.firstPosition ∈ interval.positions

theorem Utilities.Certificate.SubdivisionGraph.Spec.ComplementInterval.lastPosition_mem {n p : ℕ} {spec : Spec n p} {R : Finset spec.Vertex} (interval : spec.ComplementInterval R) : interval.lastPosition ∈ interval.positions

theorem Utilities.Certificate.SubdivisionGraph.Spec.ComplementInterval.firstVertex_mem {n p : ℕ} {spec : Spec n p} {R : Finset spec.Vertex} (interval : spec.ComplementInterval R) : spec.pathVertex interval.edge interval.firstPosition ∈ interval.carrier

theorem Utilities.Certificate.SubdivisionGraph.Spec.ComplementInterval.lastVertex_mem {n p : ℕ} {spec : Spec n p} {R : Finset spec.Vertex} (interval : spec.ComplementInterval R) : spec.pathVertex interval.edge interval.lastPosition ∈ interval.carrier

theorem Utilities.Certificate.SubdivisionGraph.Spec.ComplementInterval.left_boundary {n p : ℕ} {spec : Spec n p} {R : Finset spec.Vertex} (interval : spec.ComplementInterval R) : StrongSeparator.IsBoundary spec.graph interval.carrier (spec.pathVertex interval.edge interval.left)

The left endpoint is a boundary vertex of the interval carrier.

theorem Utilities.Certificate.SubdivisionGraph.Spec.ComplementInterval.closed {n p : ℕ} {spec : Spec n p} {R : Finset spec.Vertex} (interval : spec.ComplementInterval R) {x y : spec.Vertex} (hx : x ∈ interval.carrier) (hy : y ∉ interval.carrier) (hxy : 0 < numEdges spec.graph x y) : y ∈ R

Every edge leaving an open complement interval lands in R.

theorem Utilities.Certificate.SubdivisionGraph.Spec.ComplementInterval.reached_neighbor_classification {n p : ℕ} {spec : Spec n p} {R : Finset spec.Vertex} (interval : spec.ComplementInterval R) {x y : spec.Vertex} (hx : x ∈ interval.carrier) (hy : y ∈ R) (hyx : 0 < numEdges spec.graph y x) : x = spec.pathVertex interval.edge interval.firstPosition ∧ y = spec.pathVertex interval.edge interval.left ∨ x = spec.pathVertex interval.edge interval.lastPosition ∧ y = spec.pathVertex interval.edge interval.right

A reached vertex adjacent to the carrier is one of its two boundary vertices, and the adjacent carrier vertex is the corresponding endpoint.

theorem Utilities.Certificate.SubdivisionGraph.Spec.ComplementInterval.reached_carrier_neighbor_unique {n p : ℕ} {spec : Spec n p} {R : Finset spec.Vertex} (interval : spec.ComplementInterval R) {y x z : spec.Vertex} (hy : y ∈ R) (hx : x ∈ interval.carrier) (hz : z ∈ interval.carrier) (hyx : 0 < numEdges spec.graph y x) (hyz : 0 < numEdges spec.graph y z) : x = z

A vertex of R has at most one neighboring vertex in this carrier.

theorem Utilities.Certificate.SubdivisionGraph.Spec.ComplementInterval.oneEdge {n p : ℕ} {spec : Spec n p} {R : Finset spec.Vertex} (interval : spec.ComplementInterval R) {y : spec.Vertex} (hy : y ∈ R) : StrongSeparator.intoMultiplicity spec.graph interval.carrier y ≤ 1

Exact multiplicities and uniqueness of the boundary neighbor give the one-edge condition required by a strong-separator expansion cell.

theorem Utilities.Certificate.SubdivisionGraph.Spec.ComplementInterval.exists_crossing_step {n p : ℕ} {spec : Spec n p} {R : Finset spec.Vertex} (interval : spec.ComplementInterval R) (A : Finset spec.Vertex) (hLeftA : spec.pathVertex interval.edge interval.left ∈ A) (hRightNotA : spec.pathVertex interval.edge interval.right ∉ A) : ∃ (offset : Fin (spec.length interval.edge)), ↑interval.left ≤ ↑offset ∧ ↑offset < ↑interval.right ∧ spec.pathVertex interval.edge (spec.stepLeftPosition interval.edge offset) ∈ A ∧ spec.pathVertex interval.edge (spec.stepRightPosition interval.edge offset) ∉ A

Along the path from the left endpoint to the right endpoint, membership in any finite set must change across some unit step when the left endpoint is inside and the right endpoint is outside.

theorem Utilities.Certificate.SubdivisionGraph.Spec.ComplementInterval.pathCut {n p : ℕ} {spec : Spec n p} {R : Finset spec.Vertex} (interval : spec.ComplementInterval R) {t : spec.Vertex} (htR : t ∈ R) (htBoundary : StrongSeparator.IsBoundary spec.graph interval.carrier t) (A : Finset spec.Vertex) (hLeftA : spec.pathVertex interval.edge interval.left ∈ A) (htNotA : t ∉ A) : (∃ x ∈ interval.carrier, x ∉ A ∧ ∃ y ∈ A, 0 < numEdges spec.graph x y) ∨ ∃ x ∈ interval.carrier, x ∈ A ∧ ∃ y ∉ A, 0 < numEdges spec.graph x y

The open interval has the path-cut property required by StrongSeparator.ExpansionCell.

def Utilities.Certificate.SubdivisionGraph.Spec.ComplementInterval.expansionCell {n p : ℕ} {spec : Spec n p} {R : Finset spec.Vertex} (interval : spec.ComplementInterval R) : StrongSeparator.ExpansionCell spec.graph R

Every complement interval supplies exactly the transparent cell consumed by the strong-separator rank theorem.

Equations

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

Selecting a maximal complement interval

theorem Utilities.Certificate.SubdivisionGraph.Spec.exists_complementInterval {n p : ℕ} (spec : Spec n p) (R : Finset spec.Vertex) (hCore : ExplicitPotential.CertificateData.coreVertices spec ⊆ R) (hProper : R ≠ Finset.univ) : Nonempty (spec.ComplementInterval R)

Every proper enlargement of the embedded core omits a nonempty open interval on some edge slot. The endpoints are chosen by finite max/min, so the construction is valid for arbitrary (not necessarily connected) R.

theorem Utilities.Certificate.SubdivisionGraph.Spec.coreVertices_strongSeparatorCertificate {n p : ℕ} (spec : Spec n p) : StrongSeparator.StrongSeparatorCertificate spec.graph (ExplicitPotential.CertificateData.coreVertices spec)

The embedded core vertices form a strong separator in every subdivision graph. No connectedness hypothesis is needed for this local statement; graph connectedness enters only when the strong-separator rank theorem is applied.

theorem Utilities.Certificate.ExplicitPotential.CertificateData.bnExists_on_subdivision_of_valid {m n p : ℕ} (certificate : CertificateData m n p) (point : Fin m → ℤ) (core_nonempty : 0 < n) (degree : ℤ) (hValid : certificate.Valid degree) (hCone : FormsHold certificate.cone point) (hConnected : graphConnected (certificate.subdivisionSpec point core_nonempty hValid hCone).graph) : BNExists (certificate.subdivisionSpec point core_nonempty hValid hCone).graph 1 degree

A checked explicit-potential record now proves rank-one existence on its connected subdivision with no separately supplied separator hypothesis.