PlanarGroundUniqueness.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Uniqueness and the actual manufactured planar ground gap, proved on the full closed Sobolev graph without the published spectral hypothesis.

theorem OAI.ContinuumCoulomb.PlanarSobolev.zero_ground_form_multiple line 18
theorem OAI.ContinuumCoulomb.PlanarSobolev.zero_ground_form_orthogonal line 40
theorem OAI.ContinuumCoulomb.PlanarSobolev.manufacturedPlanarWell_gap_proved line 59
Source documentation
Positive gap above the actual manufactured well's attained ground mode.
```
theorem manufacturedPlanarWell_gap_proved :
    ∃ γ : ℝ, 0 < γ ∧ ∀ u : Sobolev,
      inner ℝ u.val.1 normalizedMode.val.1 = 0 →
      ((-1/2:ℝ)+γ)*‖u.val.1‖^2 ≤ form u.val :=
…
```
Mentions: OAI.ContinuumCoulomb.PlanarSobolev.Sobolev, OAI.ContinuumCoulomb.PlanarSobolev.form