The 1-dimensional Stam inequality in inverse form (Cover–Thomas; Stam 1959; Blachman 1965): for independent X, Y with finite Fisher information, 1 / J(X + Y) ≥ 1 / J(X) + 1 / J(Y), where J is the (real-valued) Fisher information.

The quantification block carries regularity preconditions (IsRegularDensityV2 fX/fY, the normalizations ∫ fX = 1, ∫ fY = 1, the pointwise convolution identity ∀ x, fXY x = convDensityAdd fX fY x, and the IsBlachmanConvReady fX fY bundle). These are not the inequality core: the bound is produced from regularity alone by stamCauchySchwarzOptimal_of_indepFun via convex_fisher_bound_of_ready. They are jointly satisfiable (a Gaussian witness inhabits the IsBlachmanConvReady bundle), so the predicate is non-vacuous.

@audit:ok

The Stam inequality hypothesis is symmetric in X, Y.

Regularity of the heat-flow path needed for the de Bruijn identity. For each t > 0 it bundles the family-level regularity IsRegularDeBruijnHypV2 X Z P t (which carries genuine HasDerivAt content) with a shared density witness density_path, the pin density_t_eq tying it to the per-t internal density, and bounded-window integrability of the derivative.

The structure carries genuine HasDerivAt content via reg_at and the density_t_eq pin, so its body cannot be reduced to sorry. It is load-bearing rather than a regularity precondition; the tag flags it for eventual decomposition into a regularity precondition plus the genuine de Bruijn lemma.

@audit:retract-candidate(load-bearing-predicate)

The de Bruijn integration identity along the heat-flow path (Cover–Thomas): h(target) - h(X) = ∫₀^T (1/2) · J(X + √t · Z) dt, i.e. the differential entropy gap equals the path integral of half the Fisher information. Stated existentially over the density path fPath.

The predicate carries the integration-identity content, so its def body cannot be reduced to sorry; it is load-bearing. There are no hypothesis-form consumers: the general witness isDeBruijnIntegrationHyp_holds produces it from 0 ≤ T and a path-regularity precondition by delegating to debruijnIntegrationIdentity_holds.

@audit:retract-candidate(load-bearing-predicate)

Trivial degenerate case: when T ≤ 0 the integration interval (0, T) is empty, so the identity is h_target - h_X = 0. This holds whenever h_target = h_X, which is the natural boundary case (T = 0).

IsDeBruijnIntegrationHyp X Z P T holds whenever 0 ≤ T and the heat-flow path is regular (IsDeBruijnPathRegular), by delegation to debruijnIntegrationIdentity_holds. The integration identity reduces to the per-time de Bruijn identity via the fundamental theorem of calculus; the upstream lemma carries only a path-regularity precondition and 0 ≤ T.

The Stam-to-EPI bridge hypothesis: the implication from the Stam inequality to the entropy power inequality hypothesis. Cover–Thomas derives the entropy power inequality from the Stam inequality and the de Bruijn identity by a heat-flow path-concavity argument plus a saturation argument at the endpoint; this predicate bundles that implication.

Trivial discharge: when the EPI hypothesis is already known by some other route (e.g. Gaussian saturation), the bridge holds trivially.

Assembles the Stam inequality and the Stam-to-EPI bridge into the entropy power inequality hypothesis IsEntropyPowerInequalityHypothesis.

@audit:ok

For independent Gaussian X, Y with non-zero variance, IsStamToEPIBridgeHyp X Y P is discharged with no upstream hypothesis (the EPI hypothesis is provable directly via isEntropyPowerInequalityHypothesis_of_gaussian).

For independent Gaussians X, Y, EPI holds with equality via the Gaussian saturation discharge — no upstream hypothesis required. Routes through the §6 wrapper to demonstrate the Stam-bridge pipeline structure.

Symmetric form of epi_via_stam.

@audit:ok

Pass-through bridge: IsStamToEPIBridgeHyp is implied by the conjunction Stam → EPI.

Chains epi_via_stam twice to obtain the 3-argument EPI via the Stam pipeline.

@audit:ok

The Stam predicate is preserved under arithmetic equivalent rephrasings: if two functions X, Y are pointwise equal to X', Y' then their Stam predicates coincide (the predicate depends only on P.map X, P.map Y, P.map (X + Y)).

The Stam predicate is preserved by adding a constant to X and Y when the distributional shape of P.map X, P.map Y, and P.map (X+Y) (and hence Fisher information) is preserved by the translation. This is the predicate- level statement; the corresponding distributional invariance (Fisher info is translation-invariant) is in the downstream discharge plan.

de Bruijn integration T = 0 always holds in the structurally trivial case where X + √0 · Z = X pointwise.

The √0 = 0 specialization: at T = 0, the heat-flow path returns X + 0 · Z = X. Used to discharge isDeBruijnIntegrationHyp_at_zero.

The Stam-to-EPI bridge is not symmetric in the usual sense (Stam is symmetric while the bridge picks up Y + X vs X + Y from the IsEntropyPowerInequalityHypothesis ordering). The symmetric form re-routes through isEntropyPowerInequalityHypothesis_symm.

@audit:ok

The Stam-to-EPI bridge composes through trivial EPI fact: if EPI is already known, the bridge is the constant function.

@audit:ok

Variance-additive form of Gaussian saturation: the entropy power of the Gaussian sum equals 2πe (v₁ + v₂) = 2πe v₁ + 2πe v₂, matching the EPI inequality with equality.

Chains epi_via_stam three times to obtain the 4-argument EPI via the Stam pipeline.

@audit:ok

Any conjunction (Stam X Y P) ∧ (StamToEPIBridge X Y P) yields the EPI hypothesis.

@audit:ok

Given the entropy-power-inequality form already, the Stam pipeline trivially returns the same hypothesis.

@audit:ok

The three-summand entropy power inequality, normalized by gaussianEntropyPowerConst, from Stam inequality and Stam-to-EPI bridge hypotheses on the pairs (X, Y) and (X + Y, Z) rather than from entropy-power-inequality hypotheses directly. It shows that the Stam-pipeline three-summand form composes with entropy_power_inequality_three_arg.

@audit:ok

If we have the Stam-derived EPI, the EntropyPowerInequality predicate is exactly the result of the bridge applied to Stam.

@audit:ok