The score-convolution representation (Blachman 1965 / Cover–Thomas): for independent X, Y with smooth densities, the score of Z := X + Y is the conditional expectation s_Z(z) = E[λ s_X(X) + (1 - λ) s_Y(Y) | X + Y = z] for every λ. This predicate reifies the output of that identity — the existence of the optimal λ-witness λ* = J_Y / (J_X + J_Y) in [0, 1] — rather than its derivation. The witness is unconditionally constructible (isStamScoreConvolution_intro), so the predicate is not load-bearing: the downstream λ-optimization only consumes the witness.

@audit:ok

Unconditional discharge of the score-convolution predicate: the optimal λ-witness λ* = J_Y / (J_X + J_Y) always lies in [0, 1] for positive Fisher infos.

@audit:ok

The Cauchy-Schwarz plus total expectation hypothesis (Stam body).

The Stam-proof body step: given the score-convolution identity, apply Cauchy-Schwarz pointwise to s_Z(z)² = E[λ s_X + (1 - λ) s_Y | sum = z]², then take total expectation against p_Z to obtain

`J(Z) ≤ λ² J(X) + (1 - λ)² J(Y)`.

Phrased here as: there exists λ ∈ [0, 1] with the inequality between real-valued Fisher info projections. The predicate enforces only the existence of the bounding λ-witness; the optimum is selected separately in §3.

The Cauchy-Schwarz predicate is symmetric in X, Y (swap λ ↦ 1 - λ).

The λ-optimization closed form (Stam Step 4).

For positive a, b > 0, the function λ ↦ λ² a + (1 - λ)² b is minimized at λ* = b / (a + b) with minimum value a b / (a + b). Combined with Step 3, this gives J(Z) ≤ J(X) J(Y) / (J(X) + J(Y)), equivalently 1 / J(Z) ≥ 1 / J(X) + 1 / J(Y).

For any λ ∈ ℝ, λ² a + (1-λ)² b ≥ ab / (a+b), the lower bound at the λ optimum. A direct consequence of Cauchy-Schwarz / AM-GM.

The inverse-form Stam algebraic identity: for a, b, c > 0 with c ≤ ab/(a+b), the inverse relation 1/c ≥ 1/a + 1/b holds.

The optimal Cauchy–Schwarz form: IsStamCauchySchwarz strengthened to the optimal witness λ = J_Y / (J_X + J_Y), giving the harmonic-mean bound J_sum ≤ J_X · J_Y / (J_X + J_Y). The quantification block carries regularity preconditions (IsRegularDensityV2 fX/fY, the normalizations, the pointwise convolution identity, and the IsBlachmanConvReady fX fY bundle), not the inequality core; the bound is produced from regularity by stamCauchySchwarzOptimal_of_indepFun via convex_fisher_bound_of_ready. @audit:ok

The analytic core of the Stam inequality's Steps 2-3 (Cover–Thomas / Blachman 1965): for independent X, Y with smooth densities, the conditional Cauchy–Schwarz s_Z(z)² ≤ E[(λ s_X + (1 - λ) s_Y)² | X + Y = z] integrated against p_Z gives the convex Fisher bound J(Z) ≤ λ² J(X) + (1 - λ)² J(Y), whose λ-optimum is the optimal Cauchy–Schwarz form J(Z) ≤ J(X) J(Y) / (J(X) + J(Y)).

The convex Fisher bound is supplied by convex_fisher_bound_of_ready (EPIBlachmanDensity, a condExp-free explicit-density formulation), and the λ-optimization is stam_lambda_min. The pointwise convolution hypothesis collapses fisherInfoOfDensity fXY to fisherInfoOfDensity (convDensityAdd fX fY) by funext; the added hypotheses are regularity preconditions, not the inequality core. @audit:ok

Given the optimal Cauchy–Schwarz predicate, chains through the λ-optimization closed form to obtain the inverse-form Stam inequality 1 / J_sum ≥ 1 / J_X + 1 / J_Y. The body is the algebraic reshaping of J_sum ≤ J_X · J_Y / (J_X + J_Y). @audit:ok

Bridge from the body-level optimal Cauchy–Schwarz predicate to the published Stam signature IsStamInequalityHyp (Cover–Thomas). It introduces the matching hypotheses, applies h_cs_opt to get the harmonic-mean bound J_sum ≤ J_X · J_Y / (J_X + J_Y), and reshapes to the inverse form via stam_inverse_form_of_harmonic_mean. The inequality core lives upstream in stamCauchySchwarzOptimal_of_indepFun; the antecedent's extra hypotheses are regularity preconditions. @audit:ok

The Stam-to-EPI bridge via body discharge (Gaussian case): combine the body-derived Stam inequality with the Stam-to-EPI bridge from StamEPIBridge.isStamToEPIBridgeHyp_of_gaussian.

For Gaussian X, Y with non-zero variance, EPI follows end-to-end through the body discharge and the Gaussian saturation bridge — no upstream hypothesis required.

The optimal CS predicate is strictly stronger than the existential CS predicate IsStamCauchySchwarz.

The score-convolution predicate is symmetric in X, Y — unconditionally provable since the body is a pure existence Prop on the optimal λ witness (which is constructed from J_X, J_Y only, no asymmetry in the predicate body). Provided primarily to absorb IsStamScoreConvolution Y X P slots in upstream pipelines that swap (X, Y) order.

Given a Cauchy-Schwarz witness with λ = J_Y / (J_X + J_Y), the optimal-form predicate is recovered from the λ-witness at the optimum.

@audit:ok

Composes the body-discharged Stam inequality into the EPIL3Integration integrated pipeline, whose single field is the Stam inequality. The Stam-to-EPI bridge is not part of the pipeline; consumers that need the entropy power inequality supply it separately (epi_via_stam). @audit:ok

A sanity check that stam_inverse_form_of_harmonic_mean recovers the standard form 1/c ≥ 1/a + 1/b when c = ab/(a+b) exactly.

A sanity check that at λ = 0, the upper bound is J_Y.

A sanity check that at λ = 1, the upper bound is J_X.