Cut counting and bridgelessness for contractions and subdivisions

This module proves a double-sum normal form for cutMultiplicity, develops two-edge connectivity for an ordered core, counts crossing steps in a subdivision, and proves bridgelessness of positive subdivisions (twoEdgeCutCondition_graph_of_coreTwoEdgeConnected).

A double-sum normal form for cutMultiplicity

theorem Utilities.Certificate.cutMultiplicity_eq_double_sum (K : CFGraph) (S : Finset K.V) : cutMultiplicity K S = ∑ v : K.V, ∑ w : K.V, if v ∈ S ∧ w ∉ S then ↑(numEdges K v w) else 0

cutMultiplicity written as an unrestricted double sum with an indicator. This is the form in which the quotient equation of a contraction certificate can be substituted.

def Utilities.Certificate.GraphContractionCertificate.preimageFinset {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) (S : Finset H.V) : Finset G.V

The full preimage of a target vertex set.

Equations

• c.preimageFinset S = {x : G.V | c.vertexMap x ∈ S}

@[simp]

theorem Utilities.Certificate.GraphContractionCertificate.mem_preimageFinset {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) (S : Finset H.V) (x : G.V) : x ∈ c.preimageFinset S ↔ c.vertexMap x ∈ S

theorem Utilities.Certificate.GraphContractionCertificate.preimageFinset_nonempty {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) (hValid : c.Valid) {S : Finset H.V} (hS : S.Nonempty) : (c.preimageFinset S).Nonempty

A nonempty target cut has a nonempty preimage.

theorem Utilities.Certificate.GraphContractionCertificate.preimageFinset_ne_univ {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) (hValid : c.Valid) {S : Finset H.V} (hS : S ≠ Finset.univ) : c.preimageFinset S ≠ Finset.univ

A proper target cut has a proper preimage.

theorem Utilities.Certificate.GraphContractionCertificate.cutMultiplicity_preimageFinset {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) (hValid : c.Valid) (S : Finset H.V) : cutMultiplicity G (c.preimageFinset S) = cutMultiplicity H S

Cuts pull back exactly. The crossing multiplicity of a target cut equals the crossing multiplicity of its full preimage. Only the quotient equation is used: the edges of the target are, with multiplicity, exactly the edges of the source running between distinct fibres.

theorem Utilities.Certificate.GraphContractionCertificate.twoEdgeCutCondition_of_valid {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) (hValid : c.Valid) (hSource : TwoEdgeCutCondition G) : TwoEdgeCutCondition H

Two-edge connectivity descends to contractions. A small cut of the target pulls back to an equally small cut of the source.

theorem Utilities.Certificate.GraphContractionCertificate.twoEdgeCutCondition_of_topologicalValid {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) (hTopological : c.TopologicalValid) (hSource : TwoEdgeCutCondition G) : TwoEdgeCutCondition H

The topological form of the previous theorem, matching the shape in which contraction certificates are consumed downstream.

Two-edge connectivity of an ordered core

def Utilities.Certificate.ExplicitPotential.Core.TwoEdgeConnected {n p : ℕ} (core : Core n p) : Prop

Two-edge connectedness for an ordered loopless core: every nonempty proper vertex set is crossed by at least two edge slots. Parallel slots are counted separately, exactly as they are in the subdivision.

Equations

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

def Utilities.Certificate.ExplicitPotential.Core.twoEdgeConnectedCheck {n p : ℕ} (core : Core n p) : Bool

Exact finite Boolean checker for core two-edge connectedness.

Equations

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

@[simp]

theorem Utilities.Certificate.ExplicitPotential.Core.twoEdgeConnectedCheck_eq_true_iff {n p : ℕ} (core : Core n p) : core.twoEdgeConnectedCheck = true ↔ core.TwoEdgeConnected

theorem Utilities.Certificate.ExplicitPotential.Core.connected_of_twoEdgeConnected {n p : ℕ} {core : Core n p} (hTwo : core.TwoEdgeConnected) : core.Connected

A two-edge connected core is connected.

Cuts of a subdivision are counted by crossing unit steps

def Utilities.Certificate.SubdivisionGraph.Spec.crossingSteps {n p : ℕ} (spec : Spec n p) (A : Finset spec.Vertex) : Finset spec.Step

The unit steps of the subdivision whose two endpoints lie on opposite sides of a vertex cut.

Equations

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

@[simp]

theorem Utilities.Certificate.SubdivisionGraph.Spec.mem_crossingSteps {n p : ℕ} (spec : Spec n p) (A : Finset spec.Vertex) (step : spec.Step) : step ∈ spec.crossingSteps A ↔ spec.stepLeft step.fst step.snd ∈ A ∧ spec.stepRight step.fst step.snd ∉ A ∨ spec.stepRight step.fst step.snd ∈ A ∧ spec.stepLeft step.fst step.snd ∉ A

theorem Utilities.Certificate.SubdivisionGraph.Spec.cutMultiplicity_eq_card_crossingSteps {n p : ℕ} (spec : Spec n p) (A : Finset spec.Vertex) : cutMultiplicity spec.graph A = ↑(spec.crossingSteps A).card

Exact cut count. The crossing multiplicity of a vertex cut of a subdivision is the number of emitted unit steps which cross it.

Crossing steps along one subdivided slot

theorem Utilities.Certificate.SubdivisionGraph.Spec.exists_crossing_step_between {n p : ℕ} (spec : Spec n p) (A : Finset spec.Vertex) (edge : Fin p) (lo hi : spec.PathPosition edge) (hlt : ↑lo < ↑hi) (hIn : spec.pathVertex edge lo ∈ A) (hOut : spec.pathVertex edge hi ∉ A) : ∃ (offset : Fin (spec.length edge)), ↑lo ≤ ↑offset ∧ ↑offset < ↑hi ∧ spec.stepLeft edge offset ∈ A ∧ spec.stepRight edge offset ∉ A

Membership in a finite set must change across some unit step between two path positions whose endpoints disagree.

theorem Utilities.Certificate.SubdivisionGraph.Spec.exists_crossingStep_between {n p : ℕ} (spec : Spec n p) (A : Finset spec.Vertex) (edge : Fin p) (lo hi : spec.PathPosition edge) (hlt : ↑lo < ↑hi) (hDiff : spec.pathVertex edge lo ∈ A ∧ spec.pathVertex edge hi ∉ A ∨ spec.pathVertex edge lo ∉ A ∧ spec.pathVertex edge hi ∈ A) : ∃ (offset : Fin (spec.length edge)), ↑lo ≤ ↑offset ∧ ↑offset < ↑hi ∧ ⟨edge, offset⟩ ∈ spec.crossingSteps A

The same statement with the disagreement in either direction, phrased directly in terms of crossingSteps.

Bridgelessness of positive subdivisions

theorem Utilities.Certificate.SubdivisionGraph.Spec.twoEdgeCutCondition_graph_of_coreTwoEdgeConnected {n p : ℕ} (spec : Spec n p) (hCore : spec.core.TwoEdgeConnected) : TwoEdgeCutCondition spec.graph

Positive subdivisions of two-edge connected cores are bridgeless. Every nonempty proper vertex cut of the subdivision is crossed by at least two unit steps. No further hypothesis is needed: a cut which separates a slot interior from both of its core endpoints is crossed twice inside that slot, and any other cut induces a nontrivial core cut, which is crossed by two distinct core slots.