UniformOutgoingCount.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Certified outgoing determinant counts throughout the parameter box

theorem OAI.DefocusingNLS.exists_spectral_rectangle_homotopy_count_above line 16

Source documentation

Tail homotopy transport works in every sufficiently tall counting rectangle, uniformly over the certified real parameter box.

theorem exists_spectral_rectangle_homotopy_count_above (hR : RectangleRouche)
    (ell : Fin 4) :
    ∃ V : ℝ, 0 < V ∧ ∀ W : ℝ, V < W → ∀ b Z : ℝ,
      |100000000 * b - 33477607| ≤ 2 → |100000000 * Z - 270506819| ≤ 2 →
      rectangleZeroCount W (spectralHomotopyDeterminant ell b Z 0) =
        rectangleZeroCount W (spectralHomotopyDeterminant ell b Z 1) := by
…

Mentions: OAI.DefocusingNLS.RectangleRouche, OAI.DefocusingNLS.rectangleZeroCount, OAI.DefocusingNLS.spectralHomotopyDeterminant

theorem OAI.DefocusingNLS.outgoing_halfPlane_count line 47
Source documentation
The full outgoing determinant count is 2, 1, 0, 0 for every parameter pair in the manuscript's certified box. The only hypothesis is the precisely cited rectangle specialization of the published Rouché theorem.
```
theorem outgoing_halfPlane_count (hR : RectangleRouche) (ell : Fin 4)
    (b Z : ℝ) (hb : |100000000 * b - 33477607| ≤ 2)
    (hZ : |100000000 * Z - 270506819| ≤ 2) :
    countingHalfPlaneZeroCount (spectralSlowDeterminant ell b Z) =
      (SeparatorArithmetic.positiveRootCount ell : ℕ∞) := by
…
```
Mentions: OAI.DefocusingNLS.RectangleRouche, OAI.DefocusingNLS.countingHalfPlaneZeroCount, OAI.DefocusingNLS.spectralSlowDeterminant, OAI.DefocusingNLS.SeparatorArithmetic.positiveRootCount