ConnectedMinima.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Lowering paths across tied heights

This is the finite-path argument of §6.5 of paper 082-03. The local hypotheses are precisely the connected descending neighborhoods and the compatibility across tied adjacent vertices. They are not installed as published assumptions; their verification for the relative harmonic height is a separate part of that paper's proof.

def OAI.HarmonicArtin.ParabolicIntersections.PathWithin line 24
Source documentation
Paths all of whose edges and vertices lie in a specified region. For the reflexive path the endpoint condition is supplied separately.
```
def PathWithin (p : V → Prop) (a b : V) : Prop :=
…
```
theorem OAI.HarmonicArtin.ParabolicIntersections.path_mono line 27
structure OAI.HarmonicArtin.ParabolicIntersections.LocalDescent line 36
Source documentation
Descending neighbors at one vertex lie in one strict-sublevel component; a tied edge carries that component to the other vertex.
```
structure LocalDescent : Prop where
…
```
theorem OAI.HarmonicArtin.ParabolicIntersections.lower_path line 48
Source documentation
Remove all occurrences of one maximal height in a finite path. The invariant also covers a whole segment of tied vertices.
```
theorem lower_path (D : LocalDescent adj height) (h : H)
    {a b : V} (ha : height a < h) (hb : height b < h)
    (p : PathWithin adj (fun v => height v ≤ h) a b) :
    PathWithin adj (fun v => height v < h) a b := by
…
```
Mentions: OAI.HarmonicArtin.ParabolicIntersections.LocalDescent, OAI.HarmonicArtin.ParabolicIntersections.PathWithin
theorem OAI.HarmonicArtin.ParabolicIntersections.bounded_path line 82
theorem OAI.HarmonicArtin.ParabolicIntersections.strictly_bounded_path line 96
theorem OAI.HarmonicArtin.ParabolicIntersections.sublevel_path line 115
Source documentation
Every sublevel of a well-founded height with the two local descent properties contains a path between any of its vertices that were connected in the original graph.
```
theorem sublevel_path (D : LocalDescent adj height)
    (wf : WellFounded ((· < ·) : H → H → Prop)) (c : H)
    {a b : V} (ha : height a ≤ c) (hb : height b ≤ c)
    (p : Relation.ReflTransGen adj a b) :
    PathWithin adj (fun v => height v ≤ c) a b := by
…
```
Mentions: OAI.HarmonicArtin.ParabolicIntersections.LocalDescent, OAI.HarmonicArtin.ParabolicIntersections.PathWithin
theorem OAI.HarmonicArtin.ParabolicIntersections.minimum_path line 133
Source documentation
The minimum-height vertices in a connected graph form a connected subgraph. This is the path-lowering conclusion used in §6.5.
```
theorem minimum_path (D : LocalDescent adj height)
    (wf : WellFounded ((· < ·) : H → H → Prop))
    {a b : V} (ha : ∀ v, height a ≤ height v) (hb : ∀ v, height b ≤ height v)
    (p : Relation.ReflTransGen adj a b) :
    PathWithin adj (fun v => ∀ w, height v ≤ height w) a b := by
…
```
Mentions: OAI.HarmonicArtin.ParabolicIntersections.LocalDescent, OAI.HarmonicArtin.ParabolicIntersections.PathWithin