DecompositionCuts.lean`

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

structure OAI.ParityWL.RootedCuts line 15
Source documentation
A finite rooted tree is indexed in parent-before-child order. The cuts below are the vertex sides of its edges. Validity is recorded separately.
```
structure RootedCuts (W : Type) where
…
```
def OAI.ParityWL.RootedCuts.separator line 25
def OAI.ParityWL.RootedCuts.reverseSide line 28
def OAI.ParityWL.RootedCuts.branch line 33
Source documentation
At node i, region i is the parent branch; a child is indexed by itself. All other regions are empty.
```
noncomputable def RootedCuts.branch (D : RootedCuts W) (i j : Fin D.nodes) : Finset W :=
…
```
Mentions: OAI.ParityWL.RootedCuts
def OAI.ParityWL.RootedCuts.branchSeparator line 37
structure OAI.ParityWL.ReducedCutDecomposition line 46
Source documentation
Standard finite tree-decomposition cuts: the incident outer sides and the bag partition the graph, and each cut is separated by the intersection of the incident bags. The strict intersection bound is the reduced form. No parity or graph-homomorphism property is part of this definition.
```
structure ReducedCutDecomposition (F : SimpleGraph W) (t : ℕ) extends RootedCuts W where
…
```
Mentions: OAI.ParityWL.RootedCuts
lemma OAI.ParityWL.ReducedCutDecomposition.reverse_boundary line 59
lemma OAI.ParityWL.ReducedCutDecomposition.branchSeparator_sub line 74
lemma OAI.ParityWL.ReducedCutDecomposition.branchSeparator_small line 84
lemma OAI.ParityWL.ReducedCutDecomposition.branch_boundary line 93
def OAI.ParityWL.ReducedCutDecomposition.region line 103
lemma OAI.ParityWL.ReducedCutDecomposition.region_none line 108
lemma OAI.ParityWL.ReducedCutDecomposition.region_some line 113
lemma OAI.ParityWL.ReducedCutDecomposition.main_side_equal line 135
lemma OAI.ParityWL.ReducedCutDecomposition.main_sides_sum line 146
theorem OAI.ParityWL.ReducedCutDecomposition.balancedStar line 166
Source documentation
The sink is obtained constructively from a largest inward-pointing edge in parent-before-child order. Empty branch indices contribute zero, as required.
```
theorem ReducedCutDecomposition.balancedStar (D : ReducedCutDecomposition F t)
    (w : WeightedWitness (template t) F a (starParity t)) (ht : 0 < t) :
    Nonempty (BalancedStar w) := by
…
```
Mentions: OAI.ParityWL.ReducedCutDecomposition, OAI.ParityWL.WeightedWitness, OAI.ParityWL.template, OAI.ParityWL.starParity, OAI.ParityWL.BalancedStar
theorem OAI.ParityWL.choice_of_reducedCutDecomposition line 224
Source documentation
The helper boundary argument in reduced decomposition-cut form.
```
theorem choice_of_reducedCutDecomposition {C : ChoiceSystem t}
    (φ : F →g baseGraph C)
    (w : WeightedWitness (template t) F ((baseProjection C).comp φ) (starParity t))
    (D : ReducedCutDecomposition F t) (ht : 0 < t) : C.Successful := by
…
```
Mentions: OAI.ParityWL.ChoiceSystem, OAI.ParityWL.baseGraph, OAI.ParityWL.WeightedWitness, OAI.ParityWL.template, OAI.ParityWL.baseProjection, OAI.ParityWL.starParity, OAI.ParityWL.ReducedCutDecomposition