MatchingColumns.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Division-free backward matching

The tail recurrences imply the matrix identity in Lemma free:columns of Stable self-similar blowup for a supercritical defocusing Schrödinger equation on the torus (September 2026), including at zeros of the Pochhammer factor.

def OAI.DefocusingNLS.backwardMatrix line 20
Source documentation
One backward step, with t = q + n and d = t - M.
```
noncomputable def backwardMatrix (M s t : ℂ) : Matrix (Fin 2) (Fin 2) ℂ :=
…
```

def OAI.DefocusingNLS.backwardProduct line 24

Source documentation

The ordered product F₀ ⋯ Fₖ₋₁.

noncomputable def backwardProduct (M s q : ℂ) : ℕ → Matrix (Fin 2) (Fin 2) ℂ
  | 0 => 1
  | k + 1 => backwardProduct M s q k * backwardMatrix M s (q + k)

/-- The backward recurrence requires no division by `t` or `t - M`. -/

Mentions: OAI.DefocusingNLS.backwardMatrix

theorem OAI.DefocusingNLS.backwardMatrix_step line 29

Source documentation

The backward recurrence requires no division by t or t - M.

theorem backwardMatrix_step (M s t B C B' C' : ℂ)
    (hB : (t - M) * B' = t * B + s * C)
    (hC : C' = C - B') :
    backwardMatrix M s t *ᵥ ![B', C'] = t • ![B, C] := by
…

Mentions: OAI.DefocusingNLS.backwardMatrix

theorem OAI.DefocusingNLS.backwardProduct_apply line 42

Source documentation

Multiplication of the division-free recurrences gives precisely the Pochhammer factor, including at its zeros.

theorem backwardProduct_apply (M s q : ℂ) (B C : ℕ → ℂ)
    (hB : ∀ n, (q + n - M) * B (n + 1) = (q + n) * B n + s * C n)
    (hC : ∀ n, C (n + 1) = C n - B (n + 1)) (k : ℕ) :
    backwardProduct M s q k *ᵥ ![B k, C k] =
      (ascPochhammer ℂ k).eval q • ![B 0, C 0] := by
…

Mentions: OAI.DefocusingNLS.backwardProduct

theorem OAI.DefocusingNLS.pochhammer_zero_iff line 56

Source documentation

In the relevant half-plane the only Pochhammer zero is q = 0.

theorem pochhammer_zero_iff (q : ℂ) (k : ℕ) (hk : 0 < k)
    (hq : -1 < q.re) : (ascPochhammer ℂ k).eval q = 0 ↔ q = 0 := by
…