Source Jensen Integral Extension

Abstract

Adjacent source Jensen polynomials differ by one exact integration constant.

Theorem 1.1 (The primitive and its constant).

$$\begin{array}{c}\forall d\ge 2,{q_d}_{\mathbb{C}}={\mathrm{reflect}}_d(P_d(-X)),\forall x\in \mathbb{R},q_d^{\prime }(x)=d{\alpha }_d^{d-1}{q}_{d-1}(\frac{x}{{\alpha }_d}),\\ q_d(0)={\beta }_d,\forall x\in \mathbb{R},q_d(x)=R_d(x)+{\beta }_d,\\ \forall b,x\in \mathbb{R},q_{d,b}=q_d+b-{\beta }_d,q_{d,b}^{\prime }=q_d^{\prime },q_{d,b}(x)=R_d(x)+b,\\ (q_{d,b}(x)=0⟺R_d(x)=-b),\forall x\in \mathbb{R},\exists b_0,b_1\in \mathbb{R},q_{d,b_0}(x)=0\wedge q_{d,b_1}(x)\ne 0\end{array}$$

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

Source. Repository-derived.

Commentary.

For every natural d at least two, P is the real finite source polynomial with coefficients (d)_k a_k/d^k, where a_k is the frozen sourceThetaCoefficient k. Q is Polynomial.reflect d applied to P(-X). The theorem identifies its complexification with the reflection of the actual sourceJensenPolynomial, so Q is defined at zero as a polynomial.

${\alpha }_d=\frac{d-1}{d},{\beta }_d=(-1{)}^d\frac{d!}{d^d}{a}_d,R_d(x)={\int }_0^{x}d{\alpha }_d^{d-1}{q}_{d-1}(\frac{u}{{\alpha }_d})du$

Every x and every replacement constant b in the formulas is real. The integral is oriented from zero to x; negative x and zero are included. Write Q_b = Q + b - beta. Its derivative is unchanged, its value is R(x)+b, and its roots satisfy R(x)=-b. The two symbolic constants -R(x) and 1-R(x) respectively include and exclude the chosen x from the real zero set. This concerns the family obtained by replacing the constant; the actual theta constant remains fixed. No assertion of computational ease or of a real-rooted theta tower follows.

The proof binds the frozen Jensen degree-lowering identity through Polynomial.coeff_reflect and applies Mathlib’s fundamental theorem of calculus. The remaining equalities are coefficient, field, and ring normalization; there is no finite enumeration or new analytic estimate.

References

• Truth anchor: D5/S3/Zeros/Jensen/SourceJensenIntegralExtension.source_jensen_integral_extension
• Dependency: D5/S3/Zeros/Jensen/NormalizedJensenDegreeLowering