The NBC cancellation is first proved at the level of a finite matroid. The graphic specialization only needs the standard cycle-matroid interface: spanning edge sets are the connected subgraphs and circuits are graph cycles. Keeping this layer independent makes the cancellation proof auditable and avoids hiding it behind a library theorem.

noncomputable def HsVirial.matroidGround {α : Type u_1} [Fintype α] (M : Matroid α) : Finset α

The ground set of a matroid on a finite ambient type, as a finite set.

Equations

• HsVirial.matroidGround M = {e : α | e ∈ M.E}

theorem HsVirial.mem_matroidGround {α : Type u_1} [Fintype α] (M : Matroid α) (e : α) : e ∈ matroidGround M ↔ e ∈ M.E

def HsVirial.IsNBCandidate {α : Type u_1} [DecidableEq α] [LinearOrder α] (M : Matroid α) (A : Finset α) (e : α) : Prop

An element completing a circuit whose other elements lie in the specified set.

Equations

• HsVirial.IsNBCandidate M A e = ∃ (C : Finset α), M.IsCircuit ↑C ∧ e ∈ C ∧ (∀ f ∈ C, f ≤ e) ∧ ↑(C.erase e) ⊆ ↑A

noncomputable def HsVirial.nbcCandidates {α : Type u_1} [Fintype α] [DecidableEq α] [LinearOrder α] (M : Matroid α) (A : Finset α) : Finset α

The possible circuit-completing elements used by the cancellation involution.

Equations

• HsVirial.nbcCandidates M A = Finset.filter (HsVirial.IsNBCandidate M A) (HsVirial.matroidGround M)

def HsVirial.IsNBCBad {α : Type u_1} [Fintype α] [DecidableEq α] [LinearOrder α] (M : Matroid α) (A : Finset α) : Prop

The set has at least one broken-circuit witness.

Equations

• HsVirial.IsNBCBad M A = (HsVirial.nbcCandidates M A).Nonempty

theorem HsVirial.nbcCandidate_mem_ground {α : Type u_1} [Fintype α] [DecidableEq α] [LinearOrder α] {M : Matroid α} {A : Finset α} {e : α} (h : IsNBCandidate M A e) : e ∈ matroidGround M

theorem HsVirial.mem_nbcCandidates {α : Type u_1} [Fintype α] [DecidableEq α] [LinearOrder α] {M : Matroid α} {A : Finset α} {e : α} : e ∈ nbcCandidates M A ↔ e ∈ matroidGround M ∧ IsNBCandidate M A e

noncomputable def HsVirial.leastNBCandidate {α : Type u_1} [Fintype α] [DecidableEq α] [LinearOrder α] (M : Matroid α) (A : Finset α) (h : IsNBCBad M A) : α

The least circuit-completing element, chosen to define the cancellation pairing.

Equations

• HsVirial.leastNBCandidate M A h = (HsVirial.nbcCandidates M A).min' h

theorem HsVirial.leastNBCandidate_mem {α : Type u_1} [Fintype α] [DecidableEq α] [LinearOrder α] {M : Matroid α} {A : Finset α} (h : IsNBCBad M A) : leastNBCandidate M A h ∈ nbcCandidates M A

theorem HsVirial.leastNBCandidate_isCandidate {α : Type u_1} [Fintype α] [DecidableEq α] [LinearOrder α] {M : Matroid α} {A : Finset α} (h : IsNBCBad M A) : IsNBCandidate M A (leastNBCandidate M A h)

theorem HsVirial.leastNBCandidate_le {α : Type u_1} [Fintype α] [DecidableEq α] [LinearOrder α] {M : Matroid α} {A : Finset α} (h : IsNBCBad M A) {e : α} (he : IsNBCandidate M A e) : leastNBCandidate M A h ≤ e

def HsVirial.toggleEdge {α : Type u_1} [DecidableEq α] (A : Finset α) (e : α) : Finset α

Remove an element if present and insert it otherwise.

Equations

• HsVirial.toggleEdge A e = if e ∈ A then A.erase e else insert e A

theorem HsVirial.toggleEdge_toggleEdge {α : Type u_1} [DecidableEq α] (A : Finset α) (e : α) : toggleEdge (toggleEdge A e) e = A

theorem HsVirial.toggleEdge_ne {α : Type u_1} [DecidableEq α] (A : Finset α) (e : α) : toggleEdge A e ≠ A

theorem HsVirial.card_toggleEdge {α : Type u_1} [DecidableEq α] (A : Finset α) (e : α) : (toggleEdge A e).card = if e ∈ A then A.card - 1 else A.card + 1

theorem HsVirial.candidate_toggleEdge {α : Type u_1} [DecidableEq α] [LinearOrder α] {M : Matroid α} {A : Finset α} {e : α} (h : IsNBCandidate M A e) : IsNBCandidate M (toggleEdge A e) e

theorem HsVirial.candidate_smaller_toggle_iff {α : Type u_1} [DecidableEq α] [LinearOrder α] {M : Matroid α} {A : Finset α} {e f : α} (hfe : f < e) : IsNBCandidate M (toggleEdge A e) f ↔ IsNBCandidate M A f

theorem HsVirial.leastNBCandidate_toggle_eq {α : Type u_1} [Fintype α] [DecidableEq α] [LinearOrder α] {M : Matroid α} {A : Finset α} (h : IsNBCBad M A) : leastNBCandidate M (toggleEdge A (leastNBCandidate M A h)) ⋯ = leastNBCandidate M A h

def HsVirial.matroidParitySign : ℕ → ℤ

The alternating sign determined by a natural-number cardinality.

Equations

• HsVirial.matroidParitySign 0 = 1
• HsVirial.matroidParitySign n.succ = -HsVirial.matroidParitySign n

theorem HsVirial.matroidParitySign_succ (n : ℕ) : matroidParitySign (n + 1) = -matroidParitySign n

theorem HsVirial.toggleEdge_sign {α : Type u_1} [DecidableEq α] {A : Finset α} {e : α} : matroidParitySign (toggleEdge A e).card = -matroidParitySign A.card

noncomputable def HsVirial.spanningSubsets {α : Type u_1} [Fintype α] (M : Matroid α) : Finset (Finset α)

Enumerate the spanning subsets of the matroid ground set.

Equations

• HsVirial.spanningSubsets M = {A ∈ (HsVirial.matroidGround M).powerset | M.Spanning ↑A}

noncomputable def HsVirial.badSpanningSubsets {α : Type u_1} [Fintype α] [DecidableEq α] [LinearOrder α] (M : Matroid α) : Finset (Finset α)

Enumerate spanning subsets with a broken-circuit witness.

Equations

• HsVirial.badSpanningSubsets M = Finset.filter (HsVirial.IsNBCBad M) (HsVirial.spanningSubsets M)

noncomputable def HsVirial.baseSubsets {α : Type u_1} [Fintype α] (M : Matroid α) : Finset (Finset α)

Enumerate the bases of the matroid.

Equations

• HsVirial.baseSubsets M = {A ∈ (HsVirial.matroidGround M).powerset | M.IsBase ↑A}

theorem HsVirial.mem_spanningSubsets {α : Type u_1} [Fintype α] {M : Matroid α} {A : Finset α} (hA : A ∈ spanningSubsets M) : M.Spanning ↑A

theorem HsVirial.mem_badSpanningSubsets {α : Type u_1} [Fintype α] [DecidableEq α] [LinearOrder α] {M : Matroid α} {A : Finset α} (hA : A ∈ badSpanningSubsets M) : M.Spanning ↑A ∧ IsNBCBad M A

theorem HsVirial.spanning_toggleEdge {α : Type u_1} [DecidableEq α] [LinearOrder α] {M : Matroid α} {A : Finset α} {e : α} (hA : M.Spanning ↑A) (he : IsNBCandidate M A e) : M.Spanning ↑(toggleEdge A e)

theorem HsVirial.mem_badSpanningSubsets_iff {α : Type u_1} [Fintype α] [DecidableEq α] [LinearOrder α] {M : Matroid α} {A : Finset α} : A ∈ badSpanningSubsets M ↔ A ∈ spanningSubsets M ∧ IsNBCBad M A

theorem HsVirial.toggle_mem_badSpanningSubsets {α : Type u_1} [Fintype α] [DecidableEq α] [LinearOrder α] {M : Matroid α} {A : Finset α} (hA : A ∈ badSpanningSubsets M) : toggleEdge A (leastNBCandidate M A ⋯) ∈ badSpanningSubsets M

theorem HsVirial.toggle_bad_involutive {α : Type u_1} [Fintype α] [DecidableEq α] [LinearOrder α] {M : Matroid α} {A : Finset α} (hA : A ∈ badSpanningSubsets M) : toggleEdge (toggleEdge A (leastNBCandidate M A ⋯)) (leastNBCandidate M (toggleEdge A (leastNBCandidate M A ⋯)) ⋯) = A

theorem HsVirial.spanning_not_nbcBad_isIndependent {α : Type u_1} [Fintype α] [DecidableEq α] [LinearOrder α] {M : Matroid α} {A : Finset α} (hA : A ∈ spanningSubsets M) (hbad : ¬IsNBCBad M A) : M.Indep ↑A

noncomputable def HsVirial.nbcBaseSubsets {α : Type u_1} [Fintype α] [DecidableEq α] [LinearOrder α] (M : Matroid α) : Finset (Finset α)

Enumerate spanning sets with no broken circuit, which are the surviving bases.

Equations

• HsVirial.nbcBaseSubsets M = {A ∈ HsVirial.spanningSubsets M | ¬HsVirial.IsNBCBad M A}

theorem HsVirial.mem_nbcBaseSubsets {α : Type u_1} [Fintype α] [DecidableEq α] [LinearOrder α] {M : Matroid α} {A : Finset α} (hA : A ∈ nbcBaseSubsets M) : A ∈ spanningSubsets M ∧ ¬IsNBCBad M A

theorem HsVirial.nbcBase_isBase {α : Type u_1} [Fintype α] [DecidableEq α] [LinearOrder α] {M : Matroid α} {A : Finset α} (hA : A ∈ nbcBaseSubsets M) : M.IsBase ↑A

noncomputable def HsVirial.signedSpanningSum {α : Type u_1} [Fintype α] (M : Matroid α) : ℤ

The sum of cardinality-parity signs over all spanning subsets.

Equations

• HsVirial.signedSpanningSum M = ∑ A ∈ HsVirial.spanningSubsets M, HsVirial.matroidParitySign A.card

noncomputable def HsVirial.signedNBCSum {α : Type u_1} [Fintype α] [DecidableEq α] [LinearOrder α] (M : Matroid α) : ℤ

The sum of cardinality-parity signs over the surviving no-broken-circuit sets.

Equations

• HsVirial.signedNBCSum M = ∑ A ∈ HsVirial.nbcBaseSubsets M, HsVirial.matroidParitySign A.card

theorem HsVirial.badSpanningSum_zero {α : Type u_1} [Fintype α] [DecidableEq α] [LinearOrder α] (M : Matroid α) : ∑ A ∈ badSpanningSubsets M, matroidParitySign A.card = 0

theorem HsVirial.signed_spanning_eq_signed_nbc {α : Type u_1} [Fintype α] [DecidableEq α] [LinearOrder α] (M : Matroid α) : signedSpanningSum M = signedNBCSum M