Source Jensen Coupling Budget

Abstract

The exact source coupling sum is the fourth cumulant budget.

Theorem 1.1 (The coefficient and cumulant sum).

$$\begin{array}{r}\forall n\in \mathbb{N},\forall \lambda :\mathrm{Fin}(n+1)\to \mathbb{R},\\ a_0=1\wedge \mathrm{Injective}(\lambda )\wedge (\forall i,0<{\lambda }_i\wedge q_{d-1}({\lambda }_i)=0)⟹\\ (\forall i,q_d^{\prime \prime }(t_i)\ne 0)\\ \wedge \sum _i{\mathrm{eta}}_i=\frac{d-1}{d^2}(a_1^2-2a_2)\\ \wedge \sum _i{\mathrm{eta}}_i=-\frac{d-1}{12d^2}{\mathrm{chi}}_4\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Zeros/Jensen/SourceJensenCouplingBudget.source_jensen_coupling_budget (✓ std3). ∎

Source. Repository-derived.

Commentary.

Here d=n+2, a_k=sourceThetaCoefficient k, and q_d is the same real sourceQ as in SourceJensenIntegralExtension. All i range over Fin(n+1), with exactly d-1 terms. The hypotheses are source normalization a_0=1 and the preceding polynomial’s distinct strictly positive real roots lambda_i. Set t_i=((d-1)/d)lambda_i and eta_i=sourceCoupling d t_i, exactly the couplings used in SourceJensenPositiveExtension.

$t_i=\frac{d-1}{d}{\lambda }_i,{\mathrm{eta}}_i=\frac{-d{q}_d(t_i)}{q_d^{\prime \prime }(t_i)},{\mathrm{chi}}_4=m_4-3m_2^2$

The stored sourceThetaMoment k is the moment of order 2k: m_2=sourceThetaMoment 1 and m_4=sourceThetaMoment 2. Thus chi_4 is m_4-3m_2^2. Both displayed equalities are explicit conclusions, as is the nonzero second derivative at every node. This algebraic identity requires no assumption that the couplings are nonnegative.

The proof specializes Lagrange.coeff_eq_sum to R=q-d^(-1)Xq’+(a_1/d^2)q’. Its degree, node values, and coefficient are polynomial normalization; B1.1 supplies the critical nodes. The fourth-cumulant equality uses only a_1=m_2/2, a_2=m_4/24 and ring normalization. No root estimate, induction, or finite instance is added.

References

• Truth anchor: D5/S3/Zeros/Jensen/SourceJensenCouplingBudget.source_jensen_coupling_budget
• Dependency: D5/S3/Zeros/Jensen/SourceJensenPositiveExtension