Entropy-power chain-rule helper: if f has derivative d at t, then the entropy-power composition s ↦ Real.exp (2 · f s) has derivative Real.exp (2 · f t) · (2 · d) at t. Used to lift the V2 de Bruijn identity to entropy-power form. @audit:ok

Ratio-gap derivative core (pure arithmetic): from the harmonic Stam inequality 1 / J_sum ≥ 1 / J_X + 1 / J_Y and positivity of the entropy powers N_X, N_Y, the log-ratio gap derivative J_sum − (N_X · J_X + N_Y · J_Y) / (N_X + N_Y) is ≤ 0, equivalently J_sum · (N_X + N_Y) ≤ N_X · J_X + N_Y · J_Y.

This is the factor-1 inequality (coefficient 1 on J_sum), a true real-arithmetic inequality over the free variables. The analogous factor-2 statement is false from harmonic Stam and positivity alone; the factor mismatch for the 𝒩(0, 2) sum coupling lives in the de Bruijn lift, not in this lemma. @audit:ok

The log-ratio gap derivative: csiszarLogRatioGap X Y Z_X Z_Y P has derivative J_sum − (N_X · J_X + N_Y · J_Y) / (N_X + N_Y) at any t > 0, where N_i = entropyPower (P.map path_i t) and J_i = fisherInfoOfDensityReal ((h_reg_i.reg_at t ht).density_t). Built from the three per-term entropy-power derivatives (via the de Bruijn V2 identity and the chain-rule helper), HasDerivAt.log for the two log terms, composed by HasDerivAt.sub. The h_reg_* are regularity preconditions.

The conclusion is the factor-1 derivative, correct under the stated hypotheses: h_reg_sum's Z_law field asserts P.map (Z_X + Z_Y) = gaussianReal 0 1. For the sum coupling with independent unit-variance noises the sum law is gaussianReal 0 2, so h_reg_sum is then uninhabitable; the sum line is instead closed by the two-time route, where X and Y are perturbed with separate unit-variance noises and the variance-2 view never arises. @audit:ok

The log-ratio gap derivative is ≤ 0 from the 1-source Stam inequality: the value J_sum − (N_X · J_X + N_Y · J_Y) / (N_X + N_Y) ≤ 0 follows from the harmonic Stam inequality 1 / J_sum ≥ 1 / J_X + 1 / J_Y (extracted from h_stam) plus positivity, via the arithmetic core csiszar_ratio_deriv_le_zero_arith. Unlike the difference-gap form, the ratio form is closable from harmonic Stam (weights α = N_X / (N_X + N_Y), β = N_Y / (N_X + N_Y), with α² ≤ α).

The harmonic Stam inequality is extracted by applying the producer h_stam at the three path densities, using the Fisher identifications J_i = (fisherInfoOfMeasureV2 (P.map _) f_i).toReal (rfl, since fisherInfoOfMeasureV2 ignores its measure argument) together with the caller-supplied regularity preconditions (IsRegularDensityV2, the normalizations, the pointwise convolution identification, and the IsBlachmanConvReady bundle). The inequality core is supplied by the producer h_stam, not by those preconditions. @audit:ok

Entropy power inequality recovery from nonnegativity of the gap at t = 0. The log-ratio gap at t = 0 is log (eP(X + Y)) − log (eP X + eP Y); since both arguments are strictly positive, 0 ≤ r(0) is equivalent to eP X + eP Y ≤ eP(X + Y) by Real.log_le_log_iff.

csiszarLogRatioGap X Y Z_X Z_Y P is differentiable on the interior Set.Ioi 0 = interior (Set.Ici 0), via csiszarLogRatioGap_hasDerivAt and HasDerivAt.differentiableAt. @audit:ok

Endpoint continuity ContinuousWithinAt (Set.Ioi 0) 0 of csiszarLogRatioGap X Y Z_X Z_Y P, by composing the endpoint continuity of the three heat-flow entropy powers (heatFlowEntropyPower_continuousWithinAt_zero) through ContinuousWithinAt.log / .add / .sub (with entropyPower_pos / add_pos discharging the ≠ 0 premises). The interior t > 0 continuity is supplied separately by csiszarLogRatioGap_differentiableOn_interior.

The log-ratio gap csiszarLogRatioGap X Y Z_X Z_Y P is antitone on the heat-flow ray Set.Ici 0. Applies antitoneOn_of_deriv_nonpos on the convex domain, with interior differentiability (csiszarLogRatioGap_differentiableOn_interior), endpoint continuity (csiszarLogRatioGap_continuousWithinAt_zero), and the per-t deriv ≤ 0 from csiszarLogRatioGap_hasDerivAt and csiszarLogRatioGap_deriv_le_zero.