OAI/MathematicalPhysics/DefocusingNLS/Certificates/RectangleHomotopyCount.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Root-count transport along the tail homotopy

Only the explicit published Rouché input is conditional. Compactness gives local Rouché comparison and connectedness gives equality of endpoint counts.

  1. theorem OAI.DefocusingNLS.rectangleZeroCount_homotopy line 16