FiniteGraph.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

Finite uniform sparsest cut

The rational-capacity objective and its unit-demand denominator follow the introduction of Constant-factor hardness of uniform sparsest cut by OpenAI.

structure OAI.UniformSparsestCut.Graph line 23
Source documentation
An undirected rational-capacity graph. Zero capacities encode absent edges. There are no input demand weights: all distinct pairs have demand one.
```
structure Graph where
…
```
def OAI.UniformSparsestCut.Graph.demand line 32
Source documentation
Demand is fixed, not chosen by the reduction.
```
def Graph.demand (G : Graph) (i j : Fin G.n) : ℕ := if i = j then 0 else 1
```
Mentions: OAI.UniformSparsestCut.Graph
theorem OAI.UniformSparsestCut.Graph.demand_self line 34
theorem OAI.UniformSparsestCut.Graph.demand_of_ne line 37
def OAI.UniformSparsestCut.IsCut line 42
Source documentation
A nonempty proper subset of the vertices.
```
def IsCut {n : ℕ} (S : Finset (Fin n)) : Prop := 0 < S.card ∧ S.card < n
```
instance OAI.UniformSparsestCut.(instance at line 44) line 44
def OAI.UniformSparsestCut.cuts line 47
theorem OAI.UniformSparsestCut.mem_cuts line 49
theorem OAI.UniformSparsestCut.cuts_nonempty line 52
def OAI.UniformSparsestCut.Graph.cutCapacity line 58
Source documentation
Each unordered separated pair occurs once, with its endpoint in S first.
```
def Graph.cutCapacity (G : Graph) (S : Finset (Fin G.n)) : ℚ :=
…
```
Mentions: OAI.UniformSparsestCut.Graph
def OAI.UniformSparsestCut.Graph.cutRatio line 61
def OAI.UniformSparsestCut.Graph.phi line 65
Source documentation
The actual minimum over all nonempty proper cuts, not a relaxation.
```
def Graph.phi (G : Graph) : ℚ :=
…
```
Mentions: OAI.UniformSparsestCut.Graph
theorem OAI.UniformSparsestCut.cut_card_le line 68
theorem OAI.UniformSparsestCut.cut_denominator_pos line 71
theorem OAI.UniformSparsestCut.Graph.cutCapacity_nonneg line 75
theorem OAI.UniformSparsestCut.Graph.cutRatio_nonneg line 79
theorem OAI.UniformSparsestCut.Graph.phi_le_cutRatio line 83
theorem OAI.UniformSparsestCut.Graph.exists_minimizing_cut line 87
theorem OAI.UniformSparsestCut.Graph.phi_nonneg line 93
theorem OAI.UniformSparsestCut.Graph.lt_phi_iff line 99
Source documentation
In particular, strict soundness for every cut implies strict soundness for the minimum.
```
theorem Graph.lt_phi_iff (G : Graph) (r : ℚ) :
    r < G.phi ↔ ∀ S : Finset (Fin G.n), IsCut S → r < G.cutRatio S := by
…
```
Mentions: OAI.UniformSparsestCut.Graph, OAI.UniformSparsestCut.IsCut
theorem OAI.UniformSparsestCut.Graph.separated_demand line 109
Source documentation
Summing the exactly-unit demands gives precisely the denominator in the source.
```
theorem Graph.separated_demand (G : Graph) (S : Finset (Fin G.n)) :
    (∑ i ∈ S, ∑ j ∈ Finset.univ \ S, G.demand i j) = S.card * (G.n - S.card) := by
…
```
Mentions: OAI.UniformSparsestCut.Graph