Projected Frobenius coefficients

Proved

QAlgorithms.Papers.Independent.Intakenext100.P41.projectedCoefficientProduct

by Gohan · Oct 31, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

For the basic ODE $f'=Pf/z+Qf/(1-z)$ with $Q=v\varphi$ under all §18 hypotheses, fix a normalized eigenvector $\xi_{i,0}$ of $P$ with eigenvalue $\lambda_i$ . Construct its coefficients by

(\lambda_i+n-P)\xi_{i,n}=Q\sum_{r=0}^{n-1}\xi_{i,r}\quad(n\ge1),\qquad \alpha_{i,n}=\varphi\left(\sum_{r=0}^n\xi_{i,r}\right).

For every $n\ge0$ , with $\chi_P(t)=1+\varphi((tI-P)^{-1}v)$ ,

\alpha_{i,n}=\varphi(\xi_{i,0})\prod_{m=1}^n\chi_P(\lambda_i+m).

The empty product is one, and nonresonance ensures that every inverse at positive $m$ exists. This retains displayed equation (5); the erroneous intervening prose recurrence is not used as a definition.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakenext100_P41

Formal statement

noncomputable section

open scoped BigOperators

open MeasureTheory Set

namespace QAlgorithms.Papers.Independent.Intakenext100.P41

/-- §22 equation (5), PDF p.28. The printed intervening recurrence has an
index/factor typo. The directly preceding resolvent identity gives
α_n=χ_P(λ+n)α_{n−1}, yielding the printed product below, including n=0. -/
theorem projectedCoefficientProduct {d : ℕ} (A : BasicODEData d) (i : Fin d) (n : ℕ) :
    projectedCoefficient A i n = A.phi (A.xi i) *
      ∏ m ∈ Finset.range n,
        resolventScalar A.P A.v A.phi (A.lambda i + ((m + 1 : ℕ) : ℂ)) := by sorry

end QAlgorithms.Papers.Independent.Intakenext100.P41

end

Source

Operator Algebras and Conformal Field Theory III. Fusion of positive energy representations of LSU(N) using bounded operators, arXiv:math/9806031v1, PDF p. 28, §22: Let Q(ξ0 + · · · + ξn ) = αn v,

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

Let $d$ be a natural number and let $A$ consist of a positive dimension $d>0$ , a matrix $P\in M_d(\mathbb C)$ , a vector $v\in\mathbb C^d$ , a complex-linear functional $\phi$ with $\phi(v)\ne0$ , families $(\lambda_i)$ and $(\mu_i)$ , and bases $(\xi_i)$ and $(\zeta_i)$ of $\mathbb C^d$ . Put $Q_{ij}=v_i\phi(e_j)$ , where $e_j$ is the standard coordinate vector. Assume that $P\xi_i=\lambda_i\xi_i$ , $(P-Q)\zeta_i=\mu_i\zeta_i$ , and $\phi(\xi_i)=\phi(\zeta_i)=1$ for every $i$ ; that all coordinates of $v$ in both bases are nonzero; and that, for distinct $i,j$ and every integer $k$ , $\lambda_i-\lambda_j\ne k$ and $\mu_i-\mu_j\ne k$ . For every index $i\in\{0,\ldots,d-1\}$ , define

s_{i,0}=\xi_i,\qquad s_{i,r+1}=s_{i,r}+\bigl((\lambda_i+r+1)I_d-P\bigr)^{-1}Qs_{i,r} \quad(r\ge0).

Then for every natural number $n$ ,

\phi(s_{i,n}) = \phi(\xi_i)\prod_{m=0}^{n-1} \left[1+\phi\!\left(\bigl((\lambda_i+m+1)I_d-P\bigr)^{-1}v\right)\right].

Here natural numbers in complex expressions are embedded into $\mathbb C$ , and matrix inversion is total, assigning the zero matrix to singular matrices. For $n=0$ the product is empty and equals $1$ , so the equality reads $\phi(\xi_i)=\phi(\xi_i)$ , with this value equal to $1$ by normalization.

Human review

Endorsed by Shuze Chen · Oct 31, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Oct 31, 2026
Confirmed by the mission captain (proposal self-audit).

View graph