FreeMatching.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Algebra in the free exterior matching problem

The finite-dimensional cone identity in Stable self-similar blowup for a supercritical defocusing Schrödinger equation on the torus (September 2026), Lemma free:laguerre, follows algebraically from the Laguerre recurrence.

def OAI.DefocusingNLS.coneForm line 21
Source documentation
The real cone form in equation free:cone-form.
```
noncomputable def coneForm (M : ℝ) (s B C : ℂ) : ℝ :=
…
```

theorem OAI.DefocusingNLS.coneForm_increment line 25

Source documentation

The Laguerre recurrence implies its exact cone increment.

theorem coneForm_increment (M : ℝ) (s t B C g : ℂ)
    (hs : s.re = 0)
    (hrec : t * g = -(M : ℂ) * (B - g) - s * C) :
    coneForm M s (B - g) (C - (B - g)) - coneForm M s B C =
      (t.re - M / 2) * Complex.normSq g := by
…

Mentions: OAI.DefocusingNLS.coneForm

theorem OAI.DefocusingNLS.mode_coneForm_increment line 41

Source documentation

With the paper's mode parameters, the angular degree cancels from the increment.

theorem mode_coneForm_increment (σ : ℝ) (ℓ n : ℕ) (s t B C g : ℂ)
    (hs : s.re = 0) (ht : t.re = σ + (ℓ : ℝ) / 2 + n)
    (hrec : t * g = -((ℓ : ℝ) + 5 : ℂ) * (B - g) - s * C) :
    coneForm ((ℓ : ℝ) + 5) s (B - g) (C - (B - g)) -
      coneForm ((ℓ : ℝ) + 5) s B C =
        (σ + n - 5 / 2) * Complex.normSq g := by
…

Mentions: OAI.DefocusingNLS.coneForm

theorem OAI.DefocusingNLS.mode_increment_nonneg line 53

Source documentation

The cone increments past index three are nonnegative in the counting half-plane.

theorem mode_increment_nonneg (σ : ℝ) (n : ℕ) (g : ℂ)
    (hσ : -(1 / 32 : ℝ) ≤ σ) (hn : 3 ≤ n) :
    0 ≤ (σ + n - 5 / 2) * Complex.normSq g := by
…

theorem OAI.DefocusingNLS.coneForm_square_identity line 61
Source documentation
Completing the square identifies the cone with the tail disk.
```
theorem coneForm_square_identity (M : ℝ) (s B C : ℂ) :
    Complex.normSq ((M : ℂ) * B + s * C) - Complex.normSq (s * C) =
      2 * M * coneForm M s B C := by
…
```
Mentions: OAI.DefocusingNLS.coneForm
theorem OAI.DefocusingNLS.tail_disk_of_negative_cone line 72
Source documentation
A strictly negative cone form implies both a nonzero denominator and the strict disk bound used in Lemma free:cone. The purely imaginary specialization s = h * I * Z has disk center -s / M and radius Z / M.
```
theorem tail_disk_of_negative_cone (M : ℝ) (s B C : ℂ)
    (hM : 0 < M) (hcone : coneForm M s B C < 0) :
    C ≠ 0 ∧ Complex.normSq (B / C + s / (M : ℂ)) <
      Complex.normSq (s / (M : ℂ)) := by
…
```
Mentions: OAI.DefocusingNLS.coneForm

theorem OAI.DefocusingNLS.negative_of_increasing_tail line 97

Source documentation

Increasing cone forms that tend to zero are nonpositive; one nonzero positive-weight increment makes the initial cone strictly negative.

theorem negative_of_increasing_tail {p : ℕ → ℝ} (K : ℕ)
    (hlimit : Tendsto p atTop (𝓝 0))
    (hinc : ∀ n, K ≤ n → p n ≤ p (n + 1))
    (hstrict : ∃ n, K ≤ n ∧ p n < p (n + 1)) : p K < 0 := by
…