OAI/MathematicalPhysics/DefocusingNLS/Certificates/FreeSymmetryNoChain.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual free H columns at each symmetry root admit no differentiated matching chain. This applies the simple-zero calculation without introducing an additional spectral assumption.

  1. theorem OAI.DefocusingNLS.radialFree_symmetry_no_chain line 13