HighAngularCertificate.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The high angular degree polynomial certificate

Exact rational comparisons from Appendix cert:high-angular of Stable self-similar blowup for a supercritical defocusing Schrödinger equation on the torus (September 2026) give positivity of the multiplier polynomial.

def OAI.DefocusingNLS.highAngularPolynomial line 16
Source documentation
The rational lower bound in equation free:high-polynomial.
```
noncomputable def highAngularPolynomial (t : ℝ) : ℝ :=
…
```
def OAI.DefocusingNLS.highAngularComparison line 26
Source documentation
The comparison polynomial in Appendix cert:high-angular.
```
noncomputable def highAngularComparison (t : ℝ) : ℝ :=
…
```

theorem OAI.DefocusingNLS.highAngular_difference line 31

Source documentation

All seven coefficients of the difference, checked as a polynomial identity.

theorem highAngular_difference (t : ℝ) :
    highAngularPolynomial t - highAngularComparison t =
      142518401 / 500000000 + 325932989 / 1000000000 * t +
      15777215591 / 200000000000 * t ^ 2 +
      8728703679 / 200000000000 * t ^ 3 +
      34209914771 / 800000000000 * t ^ 4 +
      16113799 / 3125000000 * t ^ 5 +
      60018849 / 40000000000 * t ^ 6 := by
…

Mentions: OAI.DefocusingNLS.highAngularPolynomial, OAI.DefocusingNLS.highAngularComparison

theorem OAI.DefocusingNLS.highAngular_first_quadratic_pos line 43
Source documentation
The first quadratic is strictly positive, by completing the square.
```
theorem highAngular_first_quadratic_pos (t : ℝ) :
    0 < 33 - 361 / 5 * t + 224 / 5 * t ^ 2 := by
…
```
theorem OAI.DefocusingNLS.highAngular_second_quadratic_pos line 48
Source documentation
The second quadratic is strictly positive, by completing the square.
```
theorem highAngular_second_quadratic_pos (t : ℝ) :
    0 < 179 / 10 - 461 / 100 * t + 27 / 50 * t ^ 2 := by
…
```
theorem OAI.DefocusingNLS.highAngularComparison_ge_two line 53
Source documentation
The comparison polynomial is at least two on the positive half-line.
```
theorem highAngularComparison_ge_two {t : ℝ} (ht : 0 ≤ t) :
    2 ≤ highAngularComparison t := by
…
```
Mentions: OAI.DefocusingNLS.highAngularComparison
theorem OAI.DefocusingNLS.highAngularPolynomial_pos line 61
Source documentation
The manuscript's exact polynomial lower bound is strictly positive.
```
theorem highAngularPolynomial_pos {t : ℝ} (ht : 0 ≤ t) :
    0 < highAngularPolynomial t := by
…
```
Mentions: OAI.DefocusingNLS.highAngularPolynomial