Genus of factors cut from a subdivided core

The finite core-cut checker already lifts articulation data uniformly over all positive integral edge lengths. This file computes the genera of the two induced factors from the same finite data. Counts are made on ordered core slots, not endpoint pairs, so parallel occurrences remain distinct.

Every slot wholly contained in one core side contributes its entire subdivided path to that factor. Its L unit edges and L - 1 new vertices cancel in Euler characteristic, leaving one edge-slot contribution. Hence the answer is independent of every subdivision length.

def Utilities.Certificate.CoreVertexCut.Data.LeftSlot {n p : ℕ} {core : ExplicitPotential.Core n p} (c : Data core) (edge : Fin p) : Prop

A core edge occurrence lies wholly in the named side.

Equations

• c.LeftSlot edge = (core.tail edge ∈ c.left ∧ core.head edge ∈ c.left)

@[instance_reducible]

instance Utilities.Certificate.CoreVertexCut.Data.leftSlotDecidable {n p : ℕ} {core : ExplicitPotential.Core n p} (c : Data core) (edge : Fin p) : Decidable (c.LeftSlot edge)

Equations

• c.leftSlotDecidable edge = id inferInstance

def Utilities.Certificate.CoreVertexCut.Data.RightSlot {n p : ℕ} {core : ExplicitPotential.Core n p} (c : Data core) (edge : Fin p) : Prop

A core edge occurrence lies wholly in the derived complementary side.

Equations

• c.RightSlot edge = (core.tail edge ∈ c.right ∧ core.head edge ∈ c.right)

@[instance_reducible]

instance Utilities.Certificate.CoreVertexCut.Data.rightSlotDecidable {n p : ℕ} {core : ExplicitPotential.Core n p} (c : Data core) (edge : Fin p) : Decidable (c.RightSlot edge)

Equations

• c.rightSlotDecidable edge = id inferInstance

def Utilities.Certificate.CoreVertexCut.Data.leftSlots {n p : ℕ} {core : ExplicitPotential.Core n p} (c : Data core) : Finset (Fin p)

Ordered core slots wholly contained in the named side.

Equations

• c.leftSlots = Finset.filter c.LeftSlot Finset.univ

def Utilities.Certificate.CoreVertexCut.Data.rightSlots {n p : ℕ} {core : ExplicitPotential.Core n p} (c : Data core) : Finset (Fin p)

Ordered core slots wholly contained in the complementary side.

Equations

• c.rightSlots = Finset.filter c.RightSlot Finset.univ

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

Executable number of ordered core slots in the named side.

Equations

• c.leftSlotCount = c.leftSlots.card

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

Executable number of ordered core slots in the complementary side.

Equations

• c.rightSlotCount = c.rightSlots.card

def Utilities.Certificate.CoreVertexCut.Data.leftGenus {n p : ℕ} {core : ExplicitPotential.Core n p} (c : Data core) : ℤ

Cyclomatic genus predicted from the named core side.

Equations

• c.leftGenus = ↑c.leftSlotCount - ↑c.left.card + 1

def Utilities.Certificate.CoreVertexCut.Data.rightGenus {n p : ℕ} {core : ExplicitPotential.Core n p} (c : Data core) : ℤ

Cyclomatic genus predicted from the complementary core side.

Equations

• c.rightGenus = ↑c.rightSlotCount - ↑c.right.card + 1

@[simp]

theorem Utilities.Certificate.CoreVertexCut.Data.leftSlotCount_eq_card {n p : ℕ} {core : ExplicitPotential.Core n p} (c : Data core) : c.leftSlotCount = c.leftSlots.card

@[simp]

theorem Utilities.Certificate.CoreVertexCut.Data.rightSlotCount_eq_card {n p : ℕ} {core : ExplicitPotential.Core n p} (c : Data core) : c.rightSlotCount = c.rightSlots.card

@[simp]

theorem Utilities.Certificate.CoreVertexCut.Data.mem_leftSlots {n p : ℕ} {core : ExplicitPotential.Core n p} (c : Data core) (edge : Fin p) : edge ∈ c.leftSlots ↔ c.LeftSlot edge

@[simp]

theorem Utilities.Certificate.CoreVertexCut.Data.mem_rightSlots {n p : ℕ} {core : ExplicitPotential.Core n p} (c : Data core) (edge : Fin p) : edge ∈ c.rightSlots ↔ c.RightSlot edge

@[simp]

theorem Utilities.Certificate.CoreVertexCut.Data.mem_right_iff {n p : ℕ} {core : ExplicitPotential.Core n p} (c : Data core) (vertex : Fin n) : vertex ∈ c.right ↔ vertex = c.glue ∨ vertex ∉ c.left

theorem Utilities.Certificate.CoreVertexCut.Data.right_card_add_left_card {n p : ℕ} {core : ExplicitPotential.Core n p} (c : Data core) (h : c.Valid) : c.right.card + c.left.card = n + 1

The two core vertex sides overlap only in the retained articulation, so their cardinalities add to one more than the ambient core cardinality.

theorem Utilities.Certificate.CoreVertexCut.Data.leftSlot_or_rightSlot {n p : ℕ} {core : ExplicitPotential.Core n p} (c : Data core) (h : c.Valid) (edge : Fin p) : c.LeftSlot edge ∨ c.RightSlot edge

Valid cut data assigns every core slot wholly to at least one side.

theorem Utilities.Certificate.CoreVertexCut.Data.not_leftSlot_and_rightSlot {n p : ℕ} {core : ExplicitPotential.Core n p} (c : Data core) (hLoopless : ∀ (edge : Fin p), core.tail edge ≠ core.head edge) (edge : Fin p) : ¬(c.LeftSlot edge ∧ c.RightSlot edge)

On a loopless core, no slot lies in both core sides: that would force both endpoints to equal the unique common articulation.

theorem Utilities.Certificate.CoreVertexCut.Data.leftSlots_disjoint_rightSlots {n p : ℕ} {core : ExplicitPotential.Core n p} (c : Data core) (hLoopless : ∀ (edge : Fin p), core.tail edge ≠ core.head edge) : Disjoint c.leftSlots c.rightSlots

The named and complementary slot sets are disjoint.

theorem Utilities.Certificate.CoreVertexCut.Data.leftSlots_card_add_rightSlots_card {n p : ℕ} {core : ExplicitPotential.Core n p} (c : Data core) (h : c.Valid) (hLoopless : ∀ (edge : Fin p), core.tail edge ≠ core.head edge) : c.leftSlots.card + c.rightSlots.card = p

The two side slot counts add to the number of ambient core occurrences.

theorem Utilities.Certificate.CoreVertexCut.Data.leftGenus_add_rightGenus {n p : ℕ} {core : ExplicitPotential.Core n p} (c : Data core) (h : c.Valid) (hLoopless : ∀ (edge : Fin p), core.tail edge ≠ core.head edge) : c.leftGenus + c.rightGenus = ↑p - ↑n + 1

Core-computed factor genera add to the cyclomatic genus of the ambient loopless core.

theorem Utilities.Certificate.CoreVertexCut.Data.step_mem_leftVertices_iff {n p : ℕ} (spec : SubdivisionGraph.Spec n p) (c : Data spec.core) (edge : Fin p) (offset : Fin (spec.length edge)) : spec.stepLeft edge offset ∈ leftVertices spec c ∧ spec.stepRight edge offset ∈ leftVertices spec c ↔ c.LeftSlot edge

Both endpoints of a subdivision unit step lie in the named factor exactly when the parent core slot lies wholly in the named core side.

theorem Utilities.Certificate.CoreVertexCut.Data.leftGraph_edge_card {n p : ℕ} (spec : SubdivisionGraph.Spec n p) (c : Data spec.core) (h : c.Valid) : (toOneVertexCut spec c h).leftGraph.edges.card = ∑ edge ∈ c.leftSlots, spec.length edge

Exact edge-occurrence count of the named induced factor.

theorem Utilities.Certificate.CoreVertexCut.Data.leftVertices_card {n p : ℕ} (spec : SubdivisionGraph.Spec n p) (c : Data spec.core) : (leftVertices spec c).card = c.left.card + ∑ edge ∈ c.leftSlots, (spec.length edge - 1)

Exact vertex count of the named subdivision side: its named core vertices, plus the interiors of precisely its wholly contained slots.

theorem Utilities.Certificate.CoreVertexCut.Data.leftGraph_vertex_card {n p : ℕ} (spec : SubdivisionGraph.Spec n p) (c : Data spec.core) (h : c.Valid) : Fintype.card (toOneVertexCut spec c h).leftGraph.V = c.left.card + ∑ edge ∈ c.leftSlots, (spec.length edge - 1)

Exact vertex count of the named induced factor.

@[simp]

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

The named induced factor has the core-computed genus, independently of all positive subdivision lengths.

@[simp]

theorem Utilities.Certificate.CoreVertexCut.Data.rightGraph_genus {n p : ℕ} (spec : SubdivisionGraph.Spec n p) (c : Data spec.core) (h : c.Valid) : (toOneVertexCut spec c h).rightGraph.genus = c.rightGenus

The complementary induced factor has its core-computed genus, independently of all positive subdivision lengths.

theorem Utilities.Certificate.CoreVertexCut.Data.leftGenus_add_rightGenus_eq_graph_genus {n p : ℕ} (spec : SubdivisionGraph.Spec n p) (c : Data spec.core) (h : c.Valid) : c.leftGenus + c.rightGenus = spec.graph.genus

Both computed factor genera sum to the genus of every positive subdivision of the core.

@[simp]

theorem Utilities.Certificate.CoreVertexCut.Data.leftGraph_genus_of_check {n p : ℕ} (spec : SubdivisionGraph.Spec n p) (c : Data spec.core) (hCheck : c.check = true) : (cutOfCheck spec c hCheck).leftGraph.genus = c.leftGenus

Checker-facing form of the named factor genus calculation.

@[simp]

theorem Utilities.Certificate.CoreVertexCut.Data.rightGraph_genus_of_check {n p : ℕ} (spec : SubdivisionGraph.Spec n p) (c : Data spec.core) (hCheck : c.check = true) : (cutOfCheck spec c hCheck).rightGraph.genus = c.rightGenus

Checker-facing form of the complementary factor genus calculation.

Closed non-unit, parallel-slot regression

The core below is two pairs of parallel slots meeting at the articulation. All four subdivision lengths exceed one and are unequal. Each induced factor is therefore a subdivided cycle, and its checked core genus is one.