The integrated pipeline predicate.

Carries the Stam inequality (Cover–Thomas signature) as its single field. The Stam-to-EPI bridge (Cover–Thomas coupling) is deliberately not a field: consumers that need the entropy power inequality supply IsStamToEPIBridgeHyp separately (epi_via_stam) rather than threading a bridge : IsStamToEPIBridgeHyp predicate hypothesis through the pipeline.

A Gaussian pipeline witness from a Stam hypothesis.

For independent Gaussians X, Y with non-zero variance, the Stam field is supplied as an IsStamInequalityHyp X Y P argument, not discharged. The hypothesis-free Gaussian EPI (no Stam claim at all) is entropy_power_inequality_gaussian.

IsEPIL3IntegratedPipeline X Y P implies IsEPIL3IntegratedPipeline Y X P.

A pipeline built directly from a Stam hypothesis.

The Stam inequality is the pipeline's only field; the Stam-to-EPI bridge is not part of it and is supplied separately by consumers (epi_via_stam).

The Gaussian entropy power inequality, combining the Gaussian saturation case directly (no Stam predicate needed for the inequality itself; the predicate is only needed for the integrated pipeline form).

Building a pipeline from the Stam hypothesis and then extracting it yields the original.

The de Bruijn tail-analysis hypothesis IsDeBruijnTailHyp X Z P.

Externalizes the T → ∞ tail-analysis of the heat-flow differential entropy T ↦ h(P.map (X + √T · Z)) as a load-bearing hypothesis with EReal lift h_inf : EReal (Gaussian case h_inf = ⊤) and a Z_law field structurally closing the Z := 0 vacuous-bypass channel.

Each field is a regularity precondition: Z_law rules out the vacuous Z := 0 bypass, h_inf : EReal lifts the divergent Gaussian case, and tail_limit carries the Tendsto content. The Gaussian instance constructor isDeBruijnTailHyp_of_gaussian exhibits a substantive multi-step Tendsto discharge via Real.tendsto_log_atTop + EReal.tendsto_coe_nhds_top_iff. @audit:ok

gaussianConvolution X Z 0 = X pointwise (uses Real.sqrt 0 = 0).

P.map (gaussianConvolution X Z 0) = P.map X.

differentialEntropy (P.map (gaussianConvolution X Z 0)) = differentialEntropy (P.map X).

The Gaussian per-time-point V2 family lift (Gaussian restricted, hypothesis-free).

For independent Gaussian X ∼ 𝒩(m, v) (with v ≠ 0) and standard normal Z ∼ 𝒩(0, 1), the V2 de Bruijn regularity IsRegularDeBruijnHypV2 X Z P t holds for every t > 0, with explicit density witness gaussianPDFReal m (v + ⟨t, ht.le⟩).

The witness is constructed by routing FisherInfo.deBruijn_identity_v2_gaussian (which gives the HasDerivAt directly) into the structure constructor.

(Returns Type, not Prop, because IsRegularDeBruijnHypV2 carries a density witness as data; declared noncomputable def accordingly.) @audit:ok

The Gaussian heat-flow entropy boundary value at T, for T ≥ 0.

The Gaussian instance of IsDeBruijnTailHyp.

When P.map X = gaussianReal m v with v ≠ 0, P.map Z = gaussianReal 0 1, and X ⊥ Z, the heat-flow entropy diverges to +∞ (Gaussian sub-entropy lower bound (1/2) log (2π e (v + T)) → +∞), so h_inf := ⊤.

Discharge route (differentialEntropy_gaussianConvolution_of_gaussian above already gives the closed form (1/2) log (2π e (v + T))):

• shift T ↦ (v : ℝ) + T via tendsto_atTop_add_const_left;
• scale by 2 π e > 0 via Tendsto.const_mul_atTop;
• apply Real.tendsto_log_atTop;
• scale by (1/2) > 0 via Tendsto.const_mul_atTop;
• congr with the closed-form identity on [0, ∞) via Tendsto.congr';
• lift to EReal via EReal.tendsto_coe_nhds_top_iff.mpr.

The heat-flow entropy derivative (Gaussian, on an s > 0 neighborhood).

For Gaussian X and s > 0, the derivative of s' ↦ differentialEntropy(P.map (X + √s' · Z)) at s equals 1/(2(v+s)). This is the per-point statement from deBruijn_identity_v2_gaussian rewritten with the Gaussian closed-form Fisher information value 1/(v+t).

Continuity of 1/(2(v+t)) on [0, T], for v > 0, T ≥ 0.

For Gaussian X ∼ 𝒩(m, v) with v ≠ 0 and standard normal Z independent of X, the heat-flow entropy s' ↦ differentialEntropy (P.map (X + √s' · Z)) is continuous on [0, T], since it agrees there with the closed form (1/2)·log (2π e (v + s')).

The bounded-T FTC application (Gaussian case).

For Gaussian X ∼ 𝒩(m, v) with v ≠ 0, the heat-flow entropy gap over the bounded interval (0, T) equals the path integral of 1/(2(v+t)):

h(N(m, v+T)) - h(N(m, v)) = ∫_(0, T) 1/(2(v+t)) dt,

stated as a direct equality (bypassing the IsDeBruijnIntegrationHyp X Z P T predicate). The integration uses Mathlib intervalIntegral and is converted to Set.Ioo-form for downstream consumption. @audit:ok

The 1-source Csiszár log-ratio gap (a monotone object).

r(t) = log (N_sum t) − log (N_X t + N_Y t) where N_sum = entropyPower (P.map (X+Y+√t·(Z_X+Z_Y))), N_X = entropyPower (P.map (X+√t·Z_X)), N_Y = entropyPower (P.map (Y+√t·Z_Y)).

The log-ratio derivative r'(t) = J_sum − (N_X·J_X + N_Y·J_Y)/(N_X+N_Y) ≤ 0 is closable from plain harmonic Stam. Both log arguments are strictly positive (entropyPower_pos, add_pos), so the gap is well-defined.

At the endpoint t = 0 the log-ratio gap reduces to log (eP(X+Y)) − log (eP X + eP Y), the form bridging to EPI (r(0) ≥ 0 ⟺ entropyPower (X+Y) ≥ entropyPower X + entropyPower Y).

At the endpoint t = 1 the log-ratio gap is zero (Gaussian saturation).

At t = 1 the 1-source heat-flow paths are X + Z_X, Y + Z_Y, and their sum X + Y + (Z_X + Z_Y) = (X + Z_X) + (Y + Z_Y). When the convolved endpoints X + Z_X and Y + Z_Y are independent Gaussians of nonzero variance, EPI saturates: N_sum(1) = N_X(1) + N_Y(1) by entropyPower_gaussian_additivity. Hence r(1) = log N_sum(1) − log (N_X(1) + N_Y(1)) = log A − log A = 0 (sub_self).

This is the endpoint of the monotone log-ratio object: together with r'(t) ≤ 0 on [0, ∞) and r(1) = 0, monotonicity gives r(0) ≥ 0, i.e. EPI. The Gaussian-pair hypotheses are preconditions (laws + independence of the convolved endpoints), not load-bearing bundling.