Checked genus-four rank-one core cuts

A proof-free core articulation is sufficient for the genus-four critical pencil when its factor genera are (2,2), or (3,1) with the genus-one side two-regular. The checker and its soundness theorem are public and apply uniformly to every positive subdivision.

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

The three finite factor alternatives consumed by the genus-four wedge theorems. The two-regular condition is required only on a genus-one side.

Equations

• c.GenusFourRankOneAlternatives = (c.leftGenus = 2 ∧ c.rightGenus = 2 ∨ c.leftGenus = 3 ∧ c.RightTwoRegular ∧ c.rightGenus = 1 ∨ c.LeftTwoRegular ∧ c.leftGenus = 1 ∧ c.rightGenus = 3)

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

Exact mathematical conditions for the genus-four cut argument.

Equations

• c.GenusFourRankOneConditions = (c.Valid ∧ core.Connected ∧ c.GenusFourRankOneAlternatives)

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

Finite checker for the three allowed factor configurations.

Equations

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

def Utilities.Certificate.CoreVertexCut.Data.genusFourRankOneCheck {n p : ℕ} {core : ExplicitPotential.Core n p} (c : Data core) (tree : MarkedGraphs.Certificate.SpanningTreeConnectivity.CertificateData core) : Bool

Kernel-cheap finite checker for the complete genus-four cut condition. Connectivity is supplied by local rooted spanning-tree data rather than the exponential all-cuts checker.

Equations

• c.genusFourRankOneCheck tree = (c.check && tree.check && c.genusFourRankOneAlternativesCheck)

theorem Utilities.Certificate.CoreVertexCut.Data.genusFourRankOneAlternativesCheck_eq_true_iff {n p : ℕ} {core : ExplicitPotential.Core n p} (c : Data core) : c.genusFourRankOneAlternativesCheck = true ↔ c.GenusFourRankOneAlternatives

The finite Boolean alternatives match the three factor configurations.

@[simp]

theorem Utilities.Certificate.CoreVertexCut.Data.genusFourRankOneCheck_eq_true_iff {n p : ℕ} {core : ExplicitPotential.Core n p} (c : Data core) (tree : MarkedGraphs.Certificate.SpanningTreeConnectivity.CertificateData core) : c.genusFourRankOneCheck tree = true ↔ c.Valid ∧ tree.Valid ∧ c.GenusFourRankOneAlternatives

The executable checker implements the cut, spanning-tree, and factor conditions exactly.

theorem Utilities.Certificate.CoreVertexCut.Data.genusFourRankOneConditions_of_check {n p : ℕ} {core : ExplicitPotential.Core n p} (c : Data core) (tree : MarkedGraphs.Certificate.SpanningTreeConnectivity.CertificateData core) (hCheck : c.genusFourRankOneCheck tree = true) : c.GenusFourRankOneConditions

Accepted cheap checker data imply the mathematical conditions used by the subdivision theorem.

theorem Utilities.Certificate.CoreVertexCut.Data.graph_connected_of_genusFourRankOneConditions {n p : ℕ} (spec : SubdivisionGraph.Spec n p) (c : Data spec.core) (h : c.GenusFourRankOneConditions) : graphConnected spec.graph

Accepted genus-four cut data makes every positive subdivision connected.

theorem Utilities.Certificate.CoreVertexCut.Data.graph_genus_eq_four_of_genusFourRankOneConditions {n p : ℕ} (spec : SubdivisionGraph.Spec n p) (c : Data spec.core) (h : c.GenusFourRankOneConditions) : spec.graph.genus = 4

The finite factor alternatives force ambient genus four, independently of the subdivision lengths.

theorem Utilities.Certificate.CoreVertexCut.Data.bnExists_one_three_of_genusFourRankOneConditions {n p : ℕ} (spec : SubdivisionGraph.Spec n p) (c : Data spec.core) (h : c.GenusFourRankOneConditions) : BNExists spec.graph 1 3

A checked (2,2) or rigid (3,1) core cut supplies the critical degree-three rank-one divisor on every positive subdivision.

theorem Utilities.Certificate.CoreVertexCut.Data.bnExists_one_three_of_genusFourRankOneCheck {n p : ℕ} (spec : SubdivisionGraph.Spec n p) (c : Data spec.core) (tree : MarkedGraphs.Certificate.SpanningTreeConnectivity.CertificateData spec.core) (hCheck : c.genusFourRankOneCheck tree = true) : BNExists spec.graph 1 3

Checker-facing form of the critical genus-four conclusion.