BoundaryPolynomialDegree.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

Structural cancellation in the boundary determinant

The proof holds for every coherent choice of constant terms. It never uses cancellation observed at the certificate's central parameter values.

def OAI.DefocusingNLS.boundaryLeadingMatrix line 15
theorem OAI.DefocusingNLS.boundaryForwardProduct_top_matrix line 18
theorem OAI.DefocusingNLS.star_I_pow_mul line 28
theorem OAI.DefocusingNLS.forwardFormEntry_boundaryLeadingMatrix line 32
theorem OAI.DefocusingNLS.boundaryHermitian_top line 56
theorem OAI.DefocusingNLS.boundaryReflected_top line 62
theorem OAI.DefocusingNLS.conjugatePolynomial_add line 73
theorem OAI.DefocusingNLS.conjugatePolynomial_sub line 77
theorem OAI.DefocusingNLS.conjugatePolynomial_mul line 81
theorem OAI.DefocusingNLS.conjugatePolynomial_C line 85
theorem OAI.DefocusingNLS.conjugatePolynomial_conjugate line 88
theorem OAI.DefocusingNLS.hermitianPolynomial_conjugate line 93
theorem OAI.DefocusingNLS.hermitianPolynomial_diagonal_coefficient line 102
theorem OAI.DefocusingNLS.reflectedHermitianPolynomial_diagonal_odd line 110
theorem OAI.DefocusingNLS.boundaryReflected_offDiagonal_degree line 117
theorem OAI.DefocusingNLS.boundaryReflected_secondDiagonal_degree line 129
def OAI.DefocusingNLS.boundaryDeterminantPolynomial line 144
theorem OAI.DefocusingNLS.boundaryDeterminantPolynomial_degree line 150
Source documentation
The cancellation required by the finite certificate is uniform throughout its parameter box: at depth eight the determinant has degree at most thirty.
```
theorem boundaryDeterminantPolynomial_degree (M : ℝ) (s : ℂ) (a : ℕ → ℂ)
    (K : ℕ) (hK : 0 < K) (hs : s.re = 0) :
    (boundaryDeterminantPolynomial M s a K).natDegree ≤ 4 * K - 2 := by
…
```
Mentions: OAI.DefocusingNLS.boundaryDeterminantPolynomial