Checked core vertex cuts and subdivision lifts

The input data name an articulation vertex and one side of the cut on the core vertices. The other side is the complement, with the articulation reinserted. This module checks that finite data occurrence by occurrence, and lifts it uniformly to every positive-length subdivision.

An interior path vertex belongs to the named side exactly when both core endpoints of its slot belong to that side. Thus a path from the articulation to the complementary side is assigned wholly to the complementary factor; there is no length-dependent case split and parallel slots are retained.

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

Proof-free articulation data on an ordered finite core. left contains the articulation; right is derived rather than redundantly emitted.

• glue : Fin n

  The proposed articulation vertex shared by the two sides of the cut.

• left : Finset (Fin n)

  The chosen left vertex set; validity includes the articulation, which is also inserted into the complementary right side.

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

The complementary core side, retaining the articulation in both sides.

Equations

• c.right = insert c.glue (Finset.univ \ c.left)

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

A core slot whose two non-articulation endpoints lie on opposite sides. Both orientations are included, since slots are stored as ordered pairs while the graph is undirected.

Equations

• c.Crosses edge = (core.tail edge ∈ c.left ∧ core.tail edge ≠ c.glue ∧ core.head edge ∉ c.left ∨ core.head edge ∈ c.left ∧ core.head edge ≠ c.glue ∧ core.tail edge ∉ c.left)

@[instance_reducible]

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

Equations

• c.crossesDecidable edge = id inferInstance

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

Exact mathematical validity of passive core-cut data.

Equations

• c.Valid = (c.glue ∈ c.left ∧ ∀ (edge : Fin p), ¬c.Crosses edge)

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

Transparent finite replay of Valid.

Equations

• c.check = (decide (c.glue ∈ c.left) && Utilities.Certificate.ExplicitPotential.allFin fun (edge : Fin p) => decide ¬c.Crosses edge)

@[simp]

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

theorem Utilities.Certificate.CoreVertexCut.Data.mem_right_of_not_mem_left {n p : ℕ} {core : ExplicitPotential.Core n p} (c : Data core) {vertex : Fin n} (hNotLeft : vertex ∉ c.left) : vertex ∈ c.right

A core vertex outside the named side is in the derived complementary side.

theorem Utilities.Certificate.CoreVertexCut.Data.ne_glue_of_not_mem_left {n p : ℕ} {core : ExplicitPotential.Core n p} (c : Data core) (h : c.Valid) {vertex : Fin n} (hNotLeft : vertex ∉ c.left) : vertex ≠ c.glue

The articulation cannot be outside the named side of valid data.

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

The named factor in a subdivision. An interior is admitted precisely when both endpoints of its original slot are admitted by the core cut.

Equations

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

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

The complementary subdivision factor. It is literally the complement of leftVertices, with the embedded articulation reinserted.

Equations

• Utilities.Certificate.CoreVertexCut.Data.rightVertices spec c = insert (spec.coreVertex c.glue) (Finset.univ \ Utilities.Certificate.CoreVertexCut.Data.leftVertices spec c)

@[simp]

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

@[simp]

theorem Utilities.Certificate.CoreVertexCut.Data.mem_leftVertices_interior {n p : ℕ} (spec : 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 Utilities.Certificate.CoreVertexCut.Data.mem_rightVertices_iff {n p : ℕ} (spec : SubdivisionGraph.Spec n p) (c : Data spec.core) (vertex : spec.Vertex) : vertex ∈ rightVertices spec c ↔ vertex = spec.coreVertex c.glue ∨ vertex ∉ leftVertices spec c

theorem Utilities.Certificate.CoreVertexCut.Data.stepLeft_eq_glue_of_mem_not_mem {n p : ℕ} (spec : 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 ∉ leftVertices spec c) : spec.stepLeft edge offset = spec.coreVertex c.glue

A unit step cannot leave the named subdivision side except through the embedded articulation. This is the key length-independent lift lemma.

theorem Utilities.Certificate.CoreVertexCut.Data.stepRight_eq_glue_of_mem_not_mem {n p : ℕ} (spec : SubdivisionGraph.Spec n p) (c : Data spec.core) (h : c.Valid) (edge : Fin p) (offset : Fin (spec.length edge)) (hRight : spec.stepRight edge offset ∈ leftVertices spec c) (hLeft : spec.stepLeft edge offset ∉ leftVertices spec c) : spec.stepRight edge offset = spec.coreVertex c.glue

The symmetric unit-step statement: a step cannot enter the named side except through the embedded articulation.

noncomputable def Utilities.Certificate.CoreVertexCut.Data.toOneVertexCut {n p : ℕ} (spec : SubdivisionGraph.Spec n p) (c : Data spec.core) (h : c.Valid) : OneVertexCut spec.graph

Lift valid finite core data to a literal one-vertex cut of every positive subdivision of that core.

Equations

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

theorem Utilities.Certificate.CoreVertexCut.Data.BNExists_iff {n p : ℕ} (spec : SubdivisionGraph.Spec n p) (c : Data spec.core) (h : c.Valid) (r d : ℤ) : BNExists spec.graph r d ↔ BNExists (vertexWedge (toOneVertexCut spec c h).leftGraph (toOneVertexCut spec c h).rightGraph (toOneVertexCut spec c h).leftGlue (toOneVertexCut spec c h).rightGlue) r d

Brill--Noether existence on a subdivided core is equivalent to existence on the vertex wedge extracted from valid core-cut data.

theorem Utilities.Certificate.CoreVertexCut.Data.BNExists_rank_one_of_factors {n p : ℕ} (spec : SubdivisionGraph.Spec n p) (c : Data spec.core) (h : c.Valid) (dLeft dRight : ℤ) (hLeft : BNExists (toOneVertexCut spec c h).leftGraph 1 dLeft) (hRight : BNExists (toOneVertexCut spec c h).rightGraph 1 dRight) : BNExists spec.graph 1 (dLeft + dRight)

Rank-one pencils on the two factors of a valid core cut glue to a pencil on the full subdivision, with degrees adding.

theorem Utilities.Certificate.CoreVertexCut.Data.transmissionExists_of_profile {n p : ℕ} (spec : SubdivisionGraph.Spec n p) (c : Data spec.core) (h : c.Valid) (u : (toOneVertexCut spec c h).leftGraph.V) (v : (toOneVertexCut spec c h).rightGraph.V) (tau : AspPerm) (D : CFDiv (toOneVertexCut spec c h).leftGraph) (E : CFDiv (toOneVertexCut spec c h).rightGraph) (hProfile : WedgeTransmissionProfile (toOneVertexCut spec c h).leftGraph (toOneVertexCut spec c h).rightGraph (toOneVertexCut spec c h).leftGlue (toOneVertexCut spec c h).rightGlue D E u v tau) : TransmissionExists spec.graph (↑u) (↑v) tau

An arbitrary-ASP transmission profile on the two induced factors of a valid core cut transfers directly to the subdivided graph.

theorem Utilities.Certificate.CoreVertexCut.Data.transmissionExists_sameLeft_of_profile {n p : ℕ} (spec : SubdivisionGraph.Spec n p) (c : Data spec.core) (h : c.Valid) (a b : (toOneVertexCut spec c h).leftGraph.V) (tau : AspPerm) (D : CFDiv (toOneVertexCut spec c h).leftGraph) (E : CFDiv (toOneVertexCut spec c h).rightGraph) (hProfile : WedgeSameLeftTransmissionProfile (toOneVertexCut spec c h).leftGraph (toOneVertexCut spec c h).rightGraph (toOneVertexCut spec c h).leftGlue (toOneVertexCut spec c h).rightGlue D E a b tau) : TransmissionExists spec.graph (↑a) (↑b) tau

A same-left arbitrary-ASP profile on the factors of a valid core cut transfers to the full subdivision.

theorem Utilities.Certificate.CoreVertexCut.Data.satisfiesTransmission_map_wedgeAddDivisor_sameLeft_of_profile {n p : ℕ} (spec : SubdivisionGraph.Spec n p) (c : Data spec.core) (h : c.Valid) (a b : (toOneVertexCut spec c h).leftGraph.V) (tau : AspPerm) (D : CFDiv (toOneVertexCut spec c h).leftGraph) (E : CFDiv (toOneVertexCut spec c h).rightGraph) (hProfile : WedgeSameLeftTransmissionProfile (toOneVertexCut spec c h).leftGraph (toOneVertexCut spec c h).rightGraph (toOneVertexCut spec c h).leftGlue (toOneVertexCut spec c h).rightGlue D E a b tau) : SatisfiesTransmission spec.graph (↑a) (↑b) tau ((toOneVertexCut spec c h).graphIso.mapDiv (wedgeAddDivisor (toOneVertexCut spec c h).leftGraph (toOneVertexCut spec c h).rightGraph (toOneVertexCut spec c h).leftGlue (toOneVertexCut spec c h).rightGlue D E))

Explicit subdivided-core divisor supplied by a same-left profile.

theorem Utilities.Certificate.CoreVertexCut.Data.transmissionExists_sameRight_of_profile {n p : ℕ} (spec : SubdivisionGraph.Spec n p) (c : Data spec.core) (h : c.Valid) (a b : (toOneVertexCut spec c h).rightGraph.V) (tau : AspPerm) (D : CFDiv (toOneVertexCut spec c h).leftGraph) (E : CFDiv (toOneVertexCut spec c h).rightGraph) (hProfile : WedgeSameRightTransmissionProfile (toOneVertexCut spec c h).leftGraph (toOneVertexCut spec c h).rightGraph (toOneVertexCut spec c h).leftGlue (toOneVertexCut spec c h).rightGlue D E a b tau) : TransmissionExists spec.graph (↑a) (↑b) tau

A same-right arbitrary-ASP profile on the factors of a valid core cut transfers to the full subdivision.

theorem Utilities.Certificate.CoreVertexCut.Data.satisfiesTransmission_map_wedgeAddDivisor_sameRight_of_profile {n p : ℕ} (spec : SubdivisionGraph.Spec n p) (c : Data spec.core) (h : c.Valid) (a b : (toOneVertexCut spec c h).rightGraph.V) (tau : AspPerm) (D : CFDiv (toOneVertexCut spec c h).leftGraph) (E : CFDiv (toOneVertexCut spec c h).rightGraph) (hProfile : WedgeSameRightTransmissionProfile (toOneVertexCut spec c h).leftGraph (toOneVertexCut spec c h).rightGraph (toOneVertexCut spec c h).leftGlue (toOneVertexCut spec c h).rightGlue D E a b tau) : SatisfiesTransmission spec.graph (↑a) (↑b) tau ((toOneVertexCut spec c h).graphIso.mapDiv (wedgeAddDivisor (toOneVertexCut spec c h).leftGraph (toOneVertexCut spec c h).rightGraph (toOneVertexCut spec c h).leftGlue (toOneVertexCut spec c h).rightGlue D E))

Explicit subdivided-core divisor supplied by a same-right profile.

noncomputable def Utilities.Certificate.CoreVertexCut.Data.cutOfCheck {n p : ℕ} (spec : SubdivisionGraph.Spec n p) (c : Data spec.core) (h : c.check = true) : OneVertexCut spec.graph

Accepted finite core data immediately yields a checked cut of any positive subdivision.

Equations

• Utilities.Certificate.CoreVertexCut.Data.cutOfCheck spec c h = Utilities.Certificate.CoreVertexCut.Data.toOneVertexCut spec c ⋯

noncomputable def Utilities.Certificate.CoreVertexCut.Data.subdivisionCheckData {n p : ℕ} (spec : SubdivisionGraph.Spec n p) (c : Data spec.core) : OneVertexCutCheck.Data spec.graph

The generic core-cut lift can be fed straight into the existing proof-carrying one-vertex-cut interface.

Equations

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

@[simp]

theorem Utilities.Certificate.CoreVertexCut.Data.subdivisionCheckData_check {n p : ℕ} (spec : SubdivisionGraph.Spec n p) (c : Data spec.core) (h : c.Valid) : (subdivisionCheckData spec c).check = true

Closed regression

The two core slots below meet at vertex 1. Their lengths are deliberately different and greater than one, so the accepted lift exercises the rule that every interior is assigned from both endpoints of its parent slot.