Two-regular genus-one factors cut from a subdivided core

The genus checker records the Euler characteristic of each core side. This module supplies the complementary local check needed to recognize a cycle: every retained core vertex has two incident retained slot occurrences. The count is made on Fin p, so parallel slots are never collapsed.

The checked condition lifts uniformly through arbitrary positive subdivision lengths. Core vertices retain the checked incident-slot degree, while every interior path vertex has degree two. Together with core connectedness and a checked side genus of one, this constructs a PointedGenusOneRigid witness.

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

Number of incidences of retained ordered slots at a named-side core vertex. A parallel slot contributes separately; each endpoint contributes one incidence.

Equations

• c.leftIncidentDegree vertex = ∑ edge ∈ c.leftSlots, ((if core.tail edge = vertex then 1 else 0) + if core.head edge = vertex then 1 else 0)

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

Number of incidences of retained ordered slots at a complementary-side core vertex.

Equations

• c.rightIncidentDegree vertex = ∑ edge ∈ c.rightSlots, ((if core.tail edge = vertex then 1 else 0) + if core.head edge = vertex then 1 else 0)

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

Every core vertex retained by the named side has retained degree two.

Equations

• c.LeftTwoRegular = ∀ vertex ∈ c.left, c.leftIncidentDegree vertex = 2

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

Every core vertex retained by the complementary side has retained degree two.

Equations

• c.RightTwoRegular = ∀ vertex ∈ c.right, c.rightIncidentDegree vertex = 2

@[instance_reducible]

instance Utilities.Certificate.CoreVertexCut.Data.leftTwoRegularDecidable {n p : ℕ} {core : ExplicitPotential.Core n p} (c : Data core) : Decidable c.LeftTwoRegular

Equations

• c.leftTwoRegularDecidable = id inferInstance

@[instance_reducible]

instance Utilities.Certificate.CoreVertexCut.Data.rightTwoRegularDecidable {n p : ℕ} {core : ExplicitPotential.Core n p} (c : Data core) : Decidable c.RightTwoRegular

Equations

• c.rightTwoRegularDecidable = id inferInstance

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

Transparent finite replay of LeftTwoRegular.

Equations

• c.leftTwoRegularCheck = Utilities.Certificate.ExplicitPotential.allFin fun (vertex : Fin n) => decide (vertex ∈ c.left → c.leftIncidentDegree vertex = 2)

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

Transparent finite replay of RightTwoRegular.

Equations

• c.rightTwoRegularCheck = Utilities.Certificate.ExplicitPotential.allFin fun (vertex : Fin n) => decide (vertex ∈ c.right → c.rightIncidentDegree vertex = 2)

@[simp]

theorem Utilities.Certificate.CoreVertexCut.Data.leftTwoRegularCheck_eq_true_iff {n p : ℕ} {core : ExplicitPotential.Core n p} (c : Data core) : c.leftTwoRegularCheck = true ↔ c.LeftTwoRegular

@[simp]

theorem Utilities.Certificate.CoreVertexCut.Data.rightTwoRegularCheck_eq_true_iff {n p : ℕ} {core : ExplicitPotential.Core n p} (c : Data core) : c.rightTwoRegularCheck = true ↔ c.RightTwoRegular

Induced-factor degree calculations

theorem Utilities.Certificate.CoreVertexCut.Data.mem_rightVertices_core {n p : ℕ} (spec : SubdivisionGraph.Spec n p) (c : Data spec.core) (vertex : Fin n) : spec.coreVertex vertex ∈ rightVertices spec c ↔ vertex ∈ c.right

The core vertices in the derived subdivision side are exactly the core vertices in right.

theorem Utilities.Certificate.CoreVertexCut.Data.mem_rightVertices_interior_iff {n p : ℕ} (spec : SubdivisionGraph.Spec n p) (c : Data spec.core) (h : c.Valid) (edge : Fin p) (offset : Fin (spec.length edge - 1)) : spec.interiorVertex edge offset ∈ rightVertices spec c ↔ c.RightSlot edge

Under valid cut data, an interior belongs to the derived subdivision side exactly when its parent slot lies wholly in the derived core side.

theorem Utilities.Certificate.CoreVertexCut.Data.step_mem_rightVertices_iff {n p : ℕ} (spec : 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 ∈ rightVertices spec c ↔ c.RightSlot edge

A unit step lies wholly in the derived subdivision side exactly when its parent slot lies wholly in the derived core side.

theorem Utilities.Certificate.CoreVertexCut.Data.leftGraph_vertex_degree_coreVertex {n p : ℕ} (spec : SubdivisionGraph.Spec n p) (c : Data spec.core) (h : c.Valid) (vertex : Fin n) (hVertex : vertex ∈ c.left) : vertexDegree (toOneVertexCut spec c h).leftGraph ⟨spec.coreVertex vertex, ⋯⟩ = ↑(c.leftIncidentDegree vertex)

Named-factor core vertices have exactly the finite retained incidence count, independently of subdivision lengths.

theorem Utilities.Certificate.CoreVertexCut.Data.rightGraph_vertex_degree_coreVertex {n p : ℕ} (spec : SubdivisionGraph.Spec n p) (c : Data spec.core) (h : c.Valid) (vertex : Fin n) (hVertex : vertex ∈ c.right) : vertexDegree (toOneVertexCut spec c h).rightGraph ⟨spec.coreVertex vertex, ⋯⟩ = ↑(c.rightIncidentDegree vertex)

Complementary-factor core vertices have exactly the finite retained incidence count, independently of subdivision lengths.

theorem Utilities.Certificate.CoreVertexCut.Data.leftGraph_vertex_degree_two {n p : ℕ} (spec : SubdivisionGraph.Spec n p) (c : Data spec.core) (h : c.Valid) (hRegular : c.LeftTwoRegular) (vertex : (toOneVertexCut spec c h).leftGraph.V) : vertexDegree (toOneVertexCut spec c h).leftGraph vertex = 2

A checked two-regular named core side remains two-regular after every positive subdivision.

theorem Utilities.Certificate.CoreVertexCut.Data.rightGraph_vertex_degree_two {n p : ℕ} (spec : SubdivisionGraph.Spec n p) (c : Data spec.core) (h : c.Valid) (hRegular : c.RightTwoRegular) (vertex : (toOneVertexCut spec c h).rightGraph.V) : vertexDegree (toOneVertexCut spec c h).rightGraph vertex = 2

A checked two-regular complementary core side remains two-regular after every positive subdivision.

theorem Utilities.Certificate.exists_vertex_ne_of_vertexDegree_two (H : CFGraph) (marked : H.V) (hDegree : ∀ (vertex : H.V), vertexDegree H vertex = 2) : ∃ (other : H.V), other ≠ marked

A loopless graph in which every vertex has degree two has a vertex other than any prescribed mark.

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

Exact finite conditions which make the named factor a pointed rigid genus-one graph.

Equations

• c.LeftRigidConditions = (c.Valid ∧ core.Connected ∧ c.LeftTwoRegular ∧ c.leftGenus = 1)

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

Exact finite conditions which make the complementary factor a pointed rigid genus-one graph.

Equations

• c.RightRigidConditions = (c.Valid ∧ core.Connected ∧ c.RightTwoRegular ∧ c.rightGenus = 1)

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

Single executable check for a named pointed rigid genus-one factor.

Equations

• c.leftRigidCheck = (c.check && core.connectedCheck && c.leftTwoRegularCheck && decide (c.leftGenus = 1))

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

Single executable check for a complementary pointed rigid genus-one factor.

Equations

• c.rightRigidCheck = (c.check && core.connectedCheck && c.rightTwoRegularCheck && decide (c.rightGenus = 1))

@[simp]

theorem Utilities.Certificate.CoreVertexCut.Data.leftRigidCheck_eq_true_iff {n p : ℕ} {core : ExplicitPotential.Core n p} (c : Data core) : c.leftRigidCheck = true ↔ c.LeftRigidConditions

@[simp]

theorem Utilities.Certificate.CoreVertexCut.Data.rightRigidCheck_eq_true_iff {n p : ℕ} {core : ExplicitPotential.Core n p} (c : Data core) : c.rightRigidCheck = true ↔ c.RightRigidConditions

theorem Utilities.Certificate.CoreVertexCut.Data.leftPointedGenusOneRigid {n p : ℕ} (spec : SubdivisionGraph.Spec n p) (c : Data spec.core) (h : c.LeftRigidConditions) : PointedGenusOneRigid (toOneVertexCut spec c ⋯).leftGraph (toOneVertexCut spec c ⋯).leftGlue

Finite core conditions construct pointed genus-one rigidity on the named factor, uniformly in all positive subdivision lengths.

theorem Utilities.Certificate.CoreVertexCut.Data.rightPointedGenusOneRigid {n p : ℕ} (spec : SubdivisionGraph.Spec n p) (c : Data spec.core) (h : c.RightRigidConditions) : PointedGenusOneRigid (toOneVertexCut spec c ⋯).rightGraph (toOneVertexCut spec c ⋯).rightGlue

Finite core conditions construct pointed genus-one rigidity on the complementary factor, uniformly in all positive subdivision lengths.

theorem Utilities.Certificate.CoreVertexCut.Data.leftPointedGenusOneRigid_of_check {n p : ℕ} (spec : SubdivisionGraph.Spec n p) (c : Data spec.core) (hCheck : c.leftRigidCheck = true) : PointedGenusOneRigid (cutOfCheck spec c ⋯).leftGraph (cutOfCheck spec c ⋯).leftGlue

Checker-facing named-factor rigidity constructor.

theorem Utilities.Certificate.CoreVertexCut.Data.rightPointedGenusOneRigid_of_check {n p : ℕ} (spec : SubdivisionGraph.Spec n p) (c : Data spec.core) (hCheck : c.rightRigidCheck = true) : PointedGenusOneRigid (cutOfCheck spec c ⋯).rightGraph (cutOfCheck spec c ⋯).rightGlue

Checker-facing complementary-factor rigidity constructor.

Closed non-unit parallel-slot regression