PathSystem.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Expanded path systems on a clique

Each nontrivial chain is stored as its actual simple vertex list. Distinct chains are disjoint, both endpoints belong to the clique, and successive clique vertices on a chain are separated by nonempty outside interiors. Thus the assigned paths are recovered by splitting at clique vertices.

structure OAI.CycleClique.Construction.ExpandedPathSystem line 18
Source documentation
The nontrivial chains of a path system, after expanding assigned paths.
```
structure ExpandedPathSystem (G : SimpleGraph V) (Q : Finset V) where
…
```
def OAI.CycleClique.Construction.ExpandedPathSystem.empty line 32
def OAI.CycleClique.Construction.ExpandedPathSystem.vertices line 40
def OAI.CycleClique.Construction.ExpandedPathSystem.amount line 45
Source documentation
Total number of interior vertices outside the clique.
```
noncomputable def amount (S : ExpandedPathSystem G Q) : ℕ := by
…
```
Mentions: OAI.CycleClique.Construction.ExpandedPathSystem
def OAI.CycleClique.Construction.ExpandedPathSystem.incident line 50
Source documentation
Clique vertices incident with at least one assigned path.
```
noncomputable def incident (S : ExpandedPathSystem G Q) : ℕ := by
…
```
Mentions: OAI.CycleClique.Construction.ExpandedPathSystem
def OAI.CycleClique.Construction.ExpandedPathSystem.assignedCount line 55
Source documentation
Each nontrivial chain with c clique vertices represents c-1 paths.
```
noncomputable def assignedCount (S : ExpandedPathSystem G Q) : ℕ :=
…
```
Mentions: OAI.CycleClique.Construction.ExpandedPathSystem
theorem OAI.CycleClique.Construction.ExpandedPathSystem.flatten_nodup line 58
theorem OAI.CycleClique.Construction.ExpandedPathSystem.vertices_card line 61
theorem OAI.CycleClique.Construction.ExpandedPathSystem.length_eq_amount_add_incident line 66
theorem OAI.CycleClique.Construction.ExpandedPathSystem.empty_amount line 72
theorem OAI.CycleClique.Construction.ExpandedPathSystem.empty_assignedCount line 77
theorem OAI.CycleClique.Construction.ExpandedPathSystem.forbidden_interval line 84
Source documentation
Closing the system after adjoining exactly the necessary unused clique vertices: manuscript Lemma path:interval.
```
theorem forbidden_interval {k : ℕ} (hk : 3 ≤ k) (hQ : G.IsClique (Q : Set V))
    (hcycle : ¬ HasCycle G (k + 1)) (S : ExpandedPathSystem G Q)
    (hlow : k + 1 - Q.card ≤ S.amount)
    (hhigh : S.amount + S.incident ≤ k + 1) : False := by
…
```
Mentions: OAI.CycleClique.Construction.HasCycle, OAI.CycleClique.Construction.ExpandedPathSystem