A kernel interface for the strong-separator rank-one lemma

Van Dobben de Bruyn--Gijswijt, Lemma 2.6, says that a divisor which reaches every vertex of a strong separator has rank at least one. The usual graph theoretic definition asks that every component of the complement be a tree and that a separator vertex have at most one edge into each component.

This file isolates the proof from a missing connected-component/path API for CFGraph. StrongSeparatorCertificate is a transparent, slightly stronger finite certificate. For every proper enlargement R of the separator it provides one complementary cell C, an anchor on its boundary, the one-edge-per-boundary-vertex condition, and the sole cut consequence of the paths through the tree C used in the paper proof. No rank or winnability claim occurs in the certificate.

For an ordinary strong separator, choose a component of the complement of R. It is a subtree of an original complementary tree. Its unique paths give pathCut, while acyclicity gives oneEdge. Formalizing that standard component-to-certificate construction, in particular for subdivided cores, is deliberately left as future graph-plumbing work; the soundness theorem below is complete and uses only the public qReduced API.

def Utilities.Certificate.StrongSeparator.Reaches (G : CFGraph) (D : CFDiv G) (v : G.V) : Prop

The divisor class of D reaches v after one chip is removed.

Equations

• Utilities.Certificate.StrongSeparator.Reaches G D v = winnable G (D - oneChip v)

def Utilities.Certificate.StrongSeparator.intoMultiplicity (G : CFGraph) (C : Finset G.V) (v : G.V) : ℤ

Total edge multiplicity from v into C, as an integer.

Equations

• Utilities.Certificate.StrongSeparator.intoMultiplicity G C v = ∑ x ∈ C, ↑(numEdges G v x)

def Utilities.Certificate.StrongSeparator.IsBoundary (G : CFGraph) (C : Finset G.V) (v : G.V) : Prop

A vertex outside C is on its boundary when it has a positive-multiplicity edge into C.

Equations

• Utilities.Certificate.StrongSeparator.IsBoundary G C v = ∃ x ∈ C, 0 < numEdges G v x

def Utilities.Certificate.StrongSeparator.borrowScript {G : CFGraph} (C : Finset G.V) : firingScript G

Borrow once on every vertex of C.

Equations

• Utilities.Certificate.StrongSeparator.borrowScript C v = if v ∈ C then -1 else 0

theorem Utilities.Certificate.StrongSeparator.intoMultiplicity_nonneg {G : CFGraph} (C : Finset G.V) (v : G.V) : 0 ≤ intoMultiplicity G C v

theorem Utilities.Certificate.StrongSeparator.edge_le_intoMultiplicity {G : CFGraph} {C : Finset G.V} {v x : G.V} (hx : x ∈ C) : ↑(numEdges G v x) ≤ intoMultiplicity G C v

theorem Utilities.Certificate.StrongSeparator.edge_le_outdeg_S {G : CFGraph} {A : Finset G.V} {v x : G.V} (hx : x ∉ A) : ↑(numEdges G v x) ≤ outdegreeSet G A v

theorem Utilities.Certificate.StrongSeparator.intoMultiplicity_eq_zero_of_not_boundary {G : CFGraph} {C : Finset G.V} {v : G.V} (h : ¬IsBoundary G C v) : intoMultiplicity G C v = 0

theorem Utilities.Certificate.StrongSeparator.prin_indicator_script_of_mem {G : CFGraph} {A : Finset G.V} {v : G.V} (hv : v ∈ A) : (prin G) (indicatorScript G A) v = -outdegreeSet G A v

theorem Utilities.Certificate.StrongSeparator.prin_indicator_script_of_not_mem {G : CFGraph} {A : Finset G.V} {v : G.V} (hv : v ∉ A) : (prin G) (indicatorScript G A) v = intoMultiplicity G A v

theorem Utilities.Certificate.StrongSeparator.borrowScript_eq_neg_indicator_script {G : CFGraph} (C : Finset G.V) : borrowScript C = -indicatorScript G C

theorem Utilities.Certificate.StrongSeparator.prin_borrowScript_of_mem {G : CFGraph} {C : Finset G.V} {v : G.V} (hv : v ∈ C) : (prin G) (borrowScript C) v = outdegreeSet G C v

theorem Utilities.Certificate.StrongSeparator.prin_borrowScript_of_not_mem {G : CFGraph} {C : Finset G.V} {v : G.V} (hv : v ∉ C) : (prin G) (borrowScript C) v = -intoMultiplicity G C v

theorem Utilities.Certificate.StrongSeparator.qReduced_sub_one_chip {G : CFGraph} {q : G.V} {D : CFDiv G} (hReduced : qReduced G q D) : qReduced G q (D - oneChip q)

Removing a chip at the reduction vertex preserves reducedness.

theorem Utilities.Certificate.StrongSeparator.linearEquiv_sub_one_chip {G : CFGraph} {D E : CFDiv G} (hEquiv : linearEquiv G D E) (v : G.V) : linearEquiv G (D - oneChip v) (E - oneChip v)

Subtracting the same chip from linearly equivalent divisors preserves linear equivalence.

theorem Utilities.Certificate.StrongSeparator.reaches_of_effective_representative {G : CFGraph} {D E : CFDiv G} {v : G.V} (hEquiv : linearEquiv G D E) (hEffective : effective E) (hChip : 1 ≤ E v) : Reaches G D v

An effective representative carrying a chip at v proves that the original divisor reaches v.

structure Utilities.Certificate.StrongSeparator.ExpansionCell (G : CFGraph) (R : Finset G.V) : Type u_1

The finite complementary cell used by the strong-separator argument.

• carrier : Finset G.V

  The nonempty finite complementary cell, disjoint from the reached set R.

• nonempty : self.carrier.Nonempty
• disjoint : Disjoint self.carrier R
• anchor : G.V

  A reached boundary vertex in R used as the anchor for expanding into the complementary cell.

• anchor_mem : self.anchor ∈ R
• anchor_boundary : IsBoundary G self.carrier self.anchor
• closed {x y : G.V} : x ∈ self.carrier → y ∉ self.carrier → 0 < numEdges G x y → y ∈ R

  Every edge leaving the cell lands in the reached enlargement.

• oneEdge {y : G.V} : y ∈ R → intoMultiplicity G self.carrier y ≤ 1

  A reached vertex has at most one edge, counted with multiplicity, into this complementary cell.

• pathCut {t : G.V} : t ∈ R → IsBoundary G self.carrier t → ∀ (A : Finset G.V), self.anchor ∈ A → t ∉ A → (∃ x ∈ self.carrier, x ∉ A ∧ ∃ y ∈ A, 0 < numEdges G x y) ∨ ∃ x ∈ self.carrier, x ∈ A ∧ ∃ y ∉ A, 0 < numEdges G x y

  The cut consequence of the path from the anchor to any other boundary vertex through the complementary tree.

def Utilities.Certificate.StrongSeparator.StrongSeparatorCertificate (G : CFGraph) (S : Finset G.V) : Prop

A transparent strong-separator certificate: every proper enlargement of S has a complementary cell with the exact tree/path cut data above.

Equations

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

theorem Utilities.Certificate.StrongSeparator.linearEquiv_add_prin {G : CFGraph} (D : CFDiv G) (script : firingScript G) : linearEquiv G D (D + (prin G) script)

Adding an explicit principal divisor does not change a divisor class.

theorem Utilities.Certificate.StrongSeparator.rank_ge_one_of_strongSeparatorCertificate {G : CFGraph} (hConnected : graphConnected G) {S : Finset G.V} (hSNonempty : S.Nonempty) (hSeparator : StrongSeparatorCertificate G S) {D : CFDiv G} (hReaches : ∀ s ∈ S, Reaches G D s) : rank G D ≥ 1

Kernel-checked strong-separator lemma (discrete form of van Dobben de Bruyn--Gijswijt, Lemma 2.6).

The proof enlarges S to the finite set of all vertices reached by D. A certificate cell for a hypothetical proper enlargement then supplies a new reached vertex, a contradiction.