Concrete graph data for the NBC layer.

Mathlib has the graph-side notion of a simple cycle, but it does not provide the graphic matroid. This file therefore stops at the interface that can be proved without importing an unproved graphic-matroid construction: cycles are represented by finite edge sets of actual Walk.IsCycle witnesses, and the final bridge is conditional on a matroid's ground, spanning, and circuit presentations.

Finite edge and cycle sets

noncomputable def HsVirial.graphEdgeFinset {V : Type u_1} [Fintype V] (G : SimpleGraph V) : Finset (Sym2 V)

The graph's edge set as a finite set of unordered vertex pairs.

Equations

• HsVirial.graphEdgeFinset G = {e : Sym2 V | e ∈ G.edgeSet}

@[simp]

theorem HsVirial.mem_graphEdgeFinset {V : Type u_1} [Fintype V] {G : SimpleGraph V} {e : Sym2 V} : e ∈ graphEdgeFinset G ↔ e ∈ G.edgeSet

@[simp]

theorem HsVirial.coe_graphEdgeFinset {V : Type u_1} [Fintype V] (G : SimpleGraph V) : ↑(graphEdgeFinset G) = G.edgeSet

def HsVirial.cycleEdgeFinset {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} {v : V} (c : G.Walk v v) : Finset (Sym2 V)

The finite edge set traversed by a closed walk.

Equations

• HsVirial.cycleEdgeFinset c = c.edges.toFinset

@[simp]

theorem HsVirial.mem_cycleEdgeFinset {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} {v : V} {c : G.Walk v v} {e : Sym2 V} : e ∈ cycleEdgeFinset c ↔ e ∈ c.edges

theorem HsVirial.walkEdgeFinset_subset_graphEdgeFinset {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} {v : V} {c : G.Walk v v} : cycleEdgeFinset c ⊆ graphEdgeFinset G

theorem HsVirial.cycleEdgeFinset_card {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} {v : V} {c : G.Walk v v} (hc : c.IsCycle) : (cycleEdgeFinset c).card = c.length

theorem HsVirial.cycleEdgeFinset_nonempty {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} {v : V} {c : G.Walk v v} (hc : c.IsCycle) : (cycleEdgeFinset c).Nonempty

IsGraphCycle is deliberately an edge-set predicate rather than a predicate on a chosen walk. Different orientations or starting points of one cycle consequently describe the same circuit candidate.

def HsVirial.IsGraphCycle {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) (C : Finset (Sym2 V)) : Prop

An edge set realized by a simple graph cycle.

Equations

• HsVirial.IsGraphCycle G C = ∃ (v : V) (c : G.Walk v v), c.IsCycle ∧ C = HsVirial.cycleEdgeFinset c

theorem HsVirial.IsGraphCycle.nonempty {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} {C : Finset (Sym2 V)} (hC : IsGraphCycle G C) : C.Nonempty

theorem HsVirial.IsGraphCycle.subset_ground {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} {C : Finset (Sym2 V)} (hC : IsGraphCycle G C) : C ⊆ graphEdgeFinset G

Broken circuits and graph-side candidates

def HsVirial.graphEdgeLE {V : Type u_1} [LinearOrder (Sym2 V)] (a b : Sym2 V) : Prop

The chosen non-strict comparison of graph edges.

Equations

• HsVirial.graphEdgeLE a b = (a ≤ b)

def HsVirial.graphEdgeLT {V : Type u_1} [LinearOrder (Sym2 V)] (a b : Sym2 V) : Prop

The chosen strict comparison of graph edges.

Equations

• HsVirial.graphEdgeLT a b = (a < b)

theorem HsVirial.graphEdgeLT_iff {V : Type u_1} [LinearOrder (Sym2 V)] {a b : Sym2 V} : graphEdgeLT a b ↔ graphEdgeLE a b ∧ ¬graphEdgeLE b a

theorem HsVirial.graphEdgeLT_not_graphEdgeLE {V : Type u_1} [LinearOrder (Sym2 V)] {a b : Sym2 V} (h : graphEdgeLT a b) : ¬graphEdgeLE b a

def HsVirial.IsGraphBrokenCircuit {V : Type u_1} [DecidableEq V] [LinearOrder (Sym2 V)] (G : SimpleGraph V) (B : Finset (Sym2 V)) : Prop

An edge set obtained by deleting the greatest edge from a cycle.

Equations

• HsVirial.IsGraphBrokenCircuit G B = ∃ (C : Finset (Sym2 V)) (e : Sym2 V), HsVirial.IsGraphCycle G C ∧ e ∈ C ∧ (∀ f ∈ C, HsVirial.graphEdgeLE f e) ∧ B = C.erase e

theorem HsVirial.IsGraphBrokenCircuit.subset_ground {V : Type u_1} [Fintype V] [DecidableEq V] [LinearOrder (Sym2 V)] {G : SimpleGraph V} {B : Finset (Sym2 V)} (hB : IsGraphBrokenCircuit G B) : B ⊆ graphEdgeFinset G

def HsVirial.IsGraphNBCandidate {V : Type u_1} [DecidableEq V] [LinearOrder (Sym2 V)] (G : SimpleGraph V) (A : Finset (Sym2 V)) (e : Sym2 V) : Prop

An edge whose insertion completes a cycle with the remaining edges already present.

Equations

• HsVirial.IsGraphNBCandidate G A e = ∃ (C : Finset (Sym2 V)), HsVirial.IsGraphCycle G C ∧ e ∈ C ∧ (∀ f ∈ C, HsVirial.graphEdgeLE f e) ∧ ↑(C.erase e) ⊆ ↑A

theorem HsVirial.graphNBCandidate_mem_ground {V : Type u_1} [Fintype V] [DecidableEq V] [LinearOrder (Sym2 V)] {G : SimpleGraph V} {A : Finset (Sym2 V)} {e : Sym2 V} (h : IsGraphNBCandidate G A e) : e ∈ graphEdgeFinset G

theorem HsVirial.graphNBCandidate_has_brokenCircuit {V : Type u_1} [DecidableEq V] [LinearOrder (Sym2 V)] {G : SimpleGraph V} {A : Finset (Sym2 V)} {e : Sym2 V} (h : IsGraphNBCandidate G A e) : ∃ (B : Finset (Sym2 V)), IsGraphBrokenCircuit G B ∧ ↑B ⊆ ↑A

theorem HsVirial.graphBrokenCircuit_subset_isGraphNBCandidate {V : Type u_1} [DecidableEq V] [LinearOrder (Sym2 V)] {G : SimpleGraph V} {A B : Finset (Sym2 V)} (hB : IsGraphBrokenCircuit G B) (hBA : ↑B ⊆ ↑A) : ∃ (e : Sym2 V), IsGraphNBCandidate G A e

theorem HsVirial.exists_graphNBCandidate_iff_exists_graphBrokenCircuit {V : Type u_1} [DecidableEq V] [LinearOrder (Sym2 V)] {G : SimpleGraph V} {A : Finset (Sym2 V)} : (∃ (e : Sym2 V), IsGraphNBCandidate G A e) ↔ ∃ (B : Finset (Sym2 V)), IsGraphBrokenCircuit G B ∧ ↑B ⊆ ↑A

theorem HsVirial.graphNBCandidate_toggleEdge {V : Type u_1} [DecidableEq V] [LinearOrder (Sym2 V)] {G : SimpleGraph V} {A : Finset (Sym2 V)} {e : Sym2 V} (h : IsGraphNBCandidate G A e) : IsGraphNBCandidate G (toggleEdge A e) e

theorem HsVirial.graphNBCandidate_smaller_toggle_iff {V : Type u_1} [DecidableEq V] [LinearOrder (Sym2 V)] {G : SimpleGraph V} {A : Finset (Sym2 V)} {e f : Sym2 V} (hfe : graphEdgeLT f e) : IsGraphNBCandidate G (toggleEdge A e) f ↔ IsGraphNBCandidate G A f

These are explicit interface theorems, not a proposed graphic-matroid definition: the graph predicates above remain concrete while the matroid construction is developed separately.

theorem HsVirial.isNBCandidate_iff_graphCycle_circuits {V : Type u_1} [DecidableEq V] [LinearOrder (Sym2 V)] {G : SimpleGraph V} {M : Matroid (Sym2 V)} {A : Finset (Sym2 V)} {e : Sym2 V} (hcircuits : ∀ (C : Finset (Sym2 V)), M.IsCircuit ↑C ↔ IsGraphCycle G C) : IsNBCandidate M A e ↔ IsGraphNBCandidate G A e

theorem HsVirial.mem_nbcCandidates_iff_graphCycle_circuits {V : Type u_1} [Fintype V] [DecidableEq V] [LinearOrder (Sym2 V)] {G : SimpleGraph V} {M : Matroid (Sym2 V)} {A : Finset (Sym2 V)} {e : Sym2 V} (hground : M.E = G.edgeSet) (hcircuits : ∀ (C : Finset (Sym2 V)), M.IsCircuit ↑C ↔ IsGraphCycle G C) : e ∈ nbcCandidates M A ↔ e ∈ graphEdgeFinset G ∧ IsGraphNBCandidate G A e

theorem HsVirial.generic_candidate_toggle_of_graphCycle_circuits {V : Type u_1} [DecidableEq V] [LinearOrder (Sym2 V)] {G : SimpleGraph V} {M : Matroid (Sym2 V)} {A : Finset (Sym2 V)} {e : Sym2 V} (hcircuits : ∀ (C : Finset (Sym2 V)), M.IsCircuit ↑C ↔ IsGraphCycle G C) (h : IsGraphNBCandidate G A e) : IsNBCandidate M (toggleEdge A e) e

theorem HsVirial.graph_nbcBad_iff_generic_nbcBad {V : Type u_1} [Fintype V] [DecidableEq V] [LinearOrder (Sym2 V)] {G : SimpleGraph V} {M : Matroid (Sym2 V)} {A : Finset (Sym2 V)} (hground : M.E = G.edgeSet) (hcircuits : ∀ (C : Finset (Sym2 V)), M.IsCircuit ↑C ↔ IsGraphCycle G C) : IsNBCBad M A ↔ ∃ (e : Sym2 V), IsGraphNBCandidate G A e

theorem HsVirial.graph_candidate_toggle_of_generic {V : Type u_1} [DecidableEq V] [LinearOrder (Sym2 V)] {G : SimpleGraph V} {M : Matroid (Sym2 V)} {A : Finset (Sym2 V)} {e : Sym2 V} (hcircuits : ∀ (C : Finset (Sym2 V)), M.IsCircuit ↑C ↔ IsGraphCycle G C) (h : IsNBCandidate M A e) : IsGraphNBCandidate G (toggleEdge A e) e

Graph-side signed cancellation

def HsVirial.IsGraphSpanning {V : Type u_1} (G : SimpleGraph V) (A : Finset (Sym2 V)) : Prop

The edge set induces the same reachability relation as the ambient graph.

Equations

• HsVirial.IsGraphSpanning G A = ((SimpleGraph.fromEdgeSet ↑A).Reachable = G.Reachable)

def HsVirial.IsGraphNBCBad {V : Type u_1} [DecidableEq V] [LinearOrder (Sym2 V)] (G : SimpleGraph V) (A : Finset (Sym2 V)) : Prop

There exists an edge witnessing a broken circuit in the given edge set.

Equations

• HsVirial.IsGraphNBCBad G A = ∃ (e : Sym2 V), HsVirial.IsGraphNBCandidate G A e

noncomputable def HsVirial.graphSpanningSubsets {V : Type u_1} [Fintype V] (G : SimpleGraph V) : Finset (Finset (Sym2 V))

Enumerate edge subsets preserving the graph's connected components.

Equations

• HsVirial.graphSpanningSubsets G = Finset.filter (HsVirial.IsGraphSpanning G) (HsVirial.graphEdgeFinset G).powerset

noncomputable def HsVirial.graphNBCSpanningSubsets {V : Type u_1} [Fintype V] [DecidableEq V] [LinearOrder (Sym2 V)] (G : SimpleGraph V) : Finset (Finset (Sym2 V))

The spanning edge subsets that contain no broken circuit.

Equations

• HsVirial.graphNBCSpanningSubsets G = {A ∈ HsVirial.graphSpanningSubsets G | ¬HsVirial.IsGraphNBCBad G A}

theorem HsVirial.graph_spanning_finset_eq_matroid_ground {V : Type u_1} [Fintype V] {G : SimpleGraph V} {M : Matroid (Sym2 V)} (hground : M.E = G.edgeSet) : matroidGround M = graphEdgeFinset G

theorem HsVirial.spanningSubsets_eq_graphSpanningSubsets {V : Type u_1} [Fintype V] {G : SimpleGraph V} {M : Matroid (Sym2 V)} (hground : M.E = G.edgeSet) (hspanning : ∀ A ⊆ graphEdgeFinset G, M.Spanning ↑A ↔ IsGraphSpanning G A) : spanningSubsets M = graphSpanningSubsets G

theorem HsVirial.nbcBaseSubsets_eq_graphNBCSpanningSubsets {V : Type u_1} [Fintype V] [DecidableEq V] [LinearOrder (Sym2 V)] {G : SimpleGraph V} {M : Matroid (Sym2 V)} (hground : M.E = G.edgeSet) (hspanning : ∀ A ⊆ graphEdgeFinset G, M.Spanning ↑A ↔ IsGraphSpanning G A) (hcircuits : ∀ (C : Finset (Sym2 V)), M.IsCircuit ↑C ↔ IsGraphCycle G C) : nbcBaseSubsets M = graphNBCSpanningSubsets G

theorem HsVirial.graph_signed_spanning_eq_graph_signed_nbc {V : Type u_1} [Fintype V] [DecidableEq V] [LinearOrder (Sym2 V)] {G : SimpleGraph V} {M : Matroid (Sym2 V)} (hground : M.E = G.edgeSet) (hspanning : ∀ A ⊆ graphEdgeFinset G, M.Spanning ↑A ↔ IsGraphSpanning G A) (hcircuits : ∀ (C : Finset (Sym2 V)), M.IsCircuit ↑C ↔ IsGraphCycle G C) : ∑ A ∈ graphSpanningSubsets G, matroidParitySign A.card = ∑ A ∈ graphNBCSpanningSubsets G, matroidParitySign A.card