ProfileCertificateComparisons.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Exact rational comparisons for Lemma free:profile-degree. The state is obtained by nine checked blocks of the K=34 recurrence.

def OAI.DefocusingNLS.ProfileCertificate.CentralBounds line 12
Source documentation
All entrywise comparisons in free:profile-enclosures, before taking roots.
```
def CentralBounds (s : State) : Prop :=
…
```
Mentions: OAI.DefocusingNLS.ProfileCertificate.State
theorem OAI.DefocusingNLS.ProfileCertificate.central_bounds line 30
def OAI.DefocusingNLS.ProfileCertificate.LinearBounds line 36
Source documentation
Sylvester's strict inequalities and the denominator/linear-size comparisons.
```
def LinearBounds (s : State) : Prop :=
…
```
Mentions: OAI.DefocusingNLS.ProfileCertificate.State
theorem OAI.DefocusingNLS.ProfileCertificate.linear_bounds line 49
def OAI.DefocusingNLS.ProfileCertificate.determinantSqBound line 55
Source documentation
Factorwise rational upper bound for the determinant on the parameter disk.
```
def determinantSqBound : ℚ :=
…
```
theorem OAI.DefocusingNLS.ProfileCertificate.determinant_bound line 60
theorem OAI.DefocusingNLS.ProfileCertificate.propagation_comparisons line 65