OptimalPathSystem.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Existence and the exact optimality criterion for manuscript Section 6.

structure OAI.CycleClique.Construction.ExpandedPathSystem.IsOptimal line 13
Source documentation
Maximize the total amount below k+1-|Q|, then minimize the number of assigned paths. Both optimization orders are on natural numbers.
```
structure IsOptimal (S : ExpandedPathSystem G Q) (k : ℕ) : Prop where
…
```
Mentions: OAI.CycleClique.Construction.ExpandedPathSystem
theorem OAI.CycleClique.Construction.ExpandedPathSystem.exists_optimal line 20
Source documentation
The empty system ensures existence, even when the amount budget is zero.
```
theorem exists_optimal (G : SimpleGraph V) (Q : Finset V) (k : ℕ) :
    ∃ S : ExpandedPathSystem G Q, S.IsOptimal k := by
…
```
Mentions: OAI.CycleClique.Construction.ExpandedPathSystem
theorem OAI.CycleClique.Construction.ExpandedPathSystem.incident_le line 45

theorem OAI.CycleClique.Construction.ExpandedPathSystem.IsOptimal.criterion line 51

Source documentation

Manuscript Lemma path:optimality, retaining its exact indicator and the secondary minimization of the number of assigned paths.

theorem IsOptimal.criterion {S : ExpandedPathSystem G Q} {k : ℕ}
    (hopt : S.IsOptimal k) (hk : 3 ≤ k) (hQk : Q.card ≤ k)
    (hQ : G.IsClique (Q : Set V)) (hcycle : ¬ HasCycle G (k + 1))
    (T : ExpandedPathSystem G Q)
    (hlow : S.amount + (if S.assignedCount ≤ T.assignedCount then 1 else 0) ≤ T.amount)
    (hhigh : T.amount + T.incident ≤ k + 1) : False := by
…

Mentions: OAI.CycleClique.Construction.ExpandedPathSystem, OAI.CycleClique.Construction.HasCycle

theorem OAI.CycleClique.Construction.ExpandedPathSystem.IsOptimal.no_one_vertex_increase line 70
Source documentation
A valid improvement by one outside vertex is impossible, regardless of how the number of represented paths changes.
```
theorem IsOptimal.no_one_vertex_increase {S : ExpandedPathSystem G Q} {k : ℕ}
    (hopt : S.IsOptimal k) (hk : 3 ≤ k) (hQk : Q.card ≤ k)
    (hQ : G.IsClique (Q : Set V)) (hcycle : ¬ HasCycle G (k + 1))
    (T : ExpandedPathSystem G Q) (hinc : T.amount = S.amount + 1) : False := by
…
```
Mentions: OAI.CycleClique.Construction.ExpandedPathSystem, OAI.CycleClique.Construction.HasCycle