OutsidePathRules.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Required-path constraints and inheritance, including the parameter-zero edge case, from manuscript Lemmas finite:required-path-rule and finite:inheritance.

def OAI.CycleClique.Construction.OutsidePath line 15
Source documentation
A simple outside path with d internal vertices. Parameter zero is the joining edge; positive parameters agree with the boundary-graph version.
```
def OutsidePath (G : SimpleGraph V) (X : Set V) (x y : V) (d : ℕ) : Prop :=
…
```
theorem OAI.CycleClique.Construction.outsidePath_zero line 19
theorem OAI.CycleClique.Construction.outsidePath_one_of_common_neighbor line 29
def OAI.CycleClique.Construction.boundaryHom line 48
theorem OAI.CycleClique.Construction.PositiveOutsidePath.toOutside line 52
theorem OAI.CycleClique.Construction.OutsidePath.of_enlargement line 62
theorem OAI.CycleClique.Construction.OutsidePath.reverse line 67
theorem OAI.CycleClique.Construction.outsidePath_forbidden_enlargement line 74
theorem OAI.CycleClique.Construction.OutsidePath.interior line 80
Source documentation
Extract the actual internal vertex list. Its vertices avoid X, and its length is exactly the outside parameter.
```
theorem OutsidePath.interior {X : Set V} {x y : V} {d : ℕ}
    (h : OutsidePath G X x y d) :
    ∃ J : List V, J.Nodup ∧ J.length = d ∧ (∀ z ∈ J, z ∉ X) ∧
      (x :: (J ++ [y])).IsChain G.Adj := by
…
```
Mentions: OAI.CycleClique.Construction.OutsidePath
theorem OAI.CycleClique.Construction.start_not_mem_support_tail line 112
theorem OAI.CycleClique.Construction.hasCycle_of_required_outside_path line 120
Source documentation
A required path lies in X, while the internal vertices of the outside path avoid X; joining the two gives the exact cycle length.
```
theorem hasCycle_of_required_outside_path {X : Set V} {x y : V}
    (p : G.Walk x y) (hp : p.IsPath) (hpX : ∀ v ∈ p.support, v ∈ X)
    {d : ℕ} (houtside : OutsidePath G X x y d)
    (hlen : 2 ≤ p.length ∨ 1 ≤ d) : HasCycle G (p.length + (d + 1)) := by
…
```
Mentions: OAI.CycleClique.Construction.OutsidePath, OAI.CycleClique.Construction.HasCycle
theorem OAI.CycleClique.Construction.required_path_forbids line 145
Source documentation
Every simple required path of length ℓ≤k excludes exactly the outside parameter k-ℓ. This also covers a required path of length k and a hypothetical joining edge.
```
theorem required_path_forbids {X : Set V} {x y : V} {k : ℕ}
    (hk : 3 ≤ k) (hcycle : ¬ HasCycle G (k + 1))
    (p : G.Walk x y) (hp : p.IsPath) (hpX : ∀ v ∈ p.support, v ∈ X)
    (hpos : 1 ≤ p.length) (hbound : p.length ≤ k) :
    ¬ OutsidePath G X x y (k - p.length) := by
…
```
Mentions: OAI.CycleClique.Construction.HasCycle, OAI.CycleClique.Construction.OutsidePath