ExtremalRootFlow.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

A neutral flow for the shortest remaining positive root

For type A roots in a fixed positive chamber, choose a root of shortest index distance. Moving its two diagonal weights to their midpoint makes that root neutral and keeps every other remaining root strictly contracting. This is the root-removal step in EK2003 Proposition 8.3.

def OAI.DukePrimeDegree.midpointRootRaw line 22
Source documentation
Equalize the selected two coordinates while keeping all other coordinates at their original ordered values.
```
def midpointRootRaw {n : ℕ} (a b r : Fin n) : ℝ :=
…
```
lemma OAI.DukePrimeDegree.midpointRootRaw_equal line 25
lemma OAI.DukePrimeDegree.midpointRootRaw_strict line 29

theorem OAI.DukePrimeDegree.exists_extremal_root_flow line 64

Source documentation

A nonempty collection of positive type-A roots has a root which can be made neutral while every other root remains strictly contracting.

theorem exists_extremal_root_flow (d : ℕ)
    (S : Finset (Fin (d + 1) × Fin (d + 1))) (hS : S.Nonempty)
    (hpos : ∀ p ∈ S, p.1 < p.2) :
    ∃ p ∈ S, ∃ ell : Fin (d + 1) → ℝ, (∑ r, ell r) = 0 ∧
      ell p.1 = ell p.2 ∧ ∀ q ∈ S, q ≠ p → ell q.1 < ell q.2 := by
…

theorem OAI.DukePrimeDegree.erase_shortest_root_closed line 90

Source documentation

Removing a shortest positive root leaves a collection closed under root addition. This is the ideal needed for the product induction.

theorem erase_shortest_root_closed (n : ℕ)
    (S : Finset (Fin n × Fin n))
    (hpos : ∀ p ∈ S, p.1 < p.2)
    (hcomp : ∀ a b c : Fin n, (a, b) ∈ S → (b, c) ∈ S → (a, c) ∈ S)
    (p : Fin n × Fin n)
    (hmin : ∀ q ∈ S, p.2.val - p.1.val ≤ q.2.val - q.1.val) :
    ∀ a b c : Fin n, (a, b) ∈ S.erase p → (b, c) ∈ S.erase p → (a, c) ∈ S.erase p := by
…