OAI/MathematicalPhysics/DefocusingNLS/Certificates/ZeroTailDeterminantPolynomial.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exact polynomial identity for the zero-tail determinant

  1. theorem OAI.DefocusingNLS.SeparatorArithmetic.map_gaussian_conjugate line 13
  2. theorem OAI.DefocusingNLS.SeparatorArithmetic.windingPolynomial_eval_zeroTailDeterminant line 22

    Source documentation

    The central certificate polynomial is exactly the entire zero-tail matching determinant, with its documented spectral translation and integer scaling.

    theorem windingPolynomial_eval_zeroTailDeterminant (ell : ℕ) (z : ℂ) :
    (2 * Complex.I) * ((windingPolynomial ell).map (Int.castRingHom ℂ)).eval z =
      (100000000 : ℂ) ^ 16 * spectralHomotopyDeterminant ell
        (33477607 / 100000000) (270506819 / 100000000) 0 (z - 1 / 32) := by
…

    Mentions: OAI.DefocusingNLS.SeparatorArithmetic.windingPolynomial, OAI.DefocusingNLS.spectralHomotopyDeterminant