InformationTheory.Shannon.EPI.Stam.SupplyTwoTime

Density facts from a withDensity law (probability-density normalization): if P.map W = volume.withDensity (ofReal ∘ p) with P a probability measure and p ≥ 0 measurable, then p is volume-integrable with mass 1. @audit:ok

The independent-sum input identity, the seam of the argument: for X ⊥ Y with Lebesgue densities pX, pY and X+Y with Lebesgue density pXY (all from probability-measure withDensity laws), the sum density equals the convolution of the addend densities a.e.: pXY =ᵐ[volume] convDensityAdd pX pY.

Both pXY and convDensityAdd pX pY are densities of P.map (X+Y) = (P.map X) ∗ (P.map Y) (independence), and withDensity densities are a.e.-unique. This is an a.e. identity at the un-smoothed input level; the consumed density_t is pinned pointwise to the smooth convolution. @audit:ok

The asymmetric IsBlachmanConvReady producer (independent times σ ≠ τ): IsBlachmanConvReady (convDensityAdd pX g_σ) (convDensityAdd pY g_τ). Faithful generalization of EPIBlachmanGeneralDensity.isBlachmanConvReady_convDensityAdd_gaussian (which hardcodes the same t for both arms) — every field's construction uses only the public per-arm conv-Gaussian lemmas (convDensityAdd_gaussian_integrable / _bdd / _deriv_bdd / convDensityAdd_fisher_integrand_integrable / convDensityAdd_pos_of_pos_cont / isRegularDensityV2_convDensityAdd_gaussian), each at its own arm's time, so the same-t restriction was incidental. The only structural change is int_fisherZ: the conv-of-conv conv(pX∗g_σ)(pY∗g_τ) is identified with conv(pX∗pY) g_{σ+τ} via the asymmetric interchange bridge convDensityAdd_convGaussian_interchange_asym (variance σ+τ, not 2t).

All hypotheses are regularity preconditions; the conclusion (19-field integrability / boundedness / positivity bundle) is derived from them. @audit:ok

The two-time harmonic-Stam supply producer.

For X Y Z_X Z_Y Z : Ω → ℝ (all unit noises, sum perturbed by separate Z), independent appropriately, with Lebesgue densities and finite second moments, and de Bruijn regularity h_reg_X/h_reg_Y/h_reg_sum, the h_stam_supply clause of entropyPower_add_ge_case1_of_regular_twotime holds: at every matched pair σ, τ > 0, the three smoothed Fisher informations are positive and 1/J_S ≥ 1/J_X + 1/J_Y with J_S the single-noise sum heat flow at σ + τ.

The conv-pin seam indepSum_density_ae (pXY =ᵐ convDensityAdd pX pY) is proved via IndepFun.map_add_eq_map_conv_map + conv_withDensity_eq_lconvolution

• withDensity a.e.-uniqueness + the lconvolution-Bochner a.e. bridge (Tonelli finiteness + a.e.-z ofReal_integral_eq_lintegral_ofReal).

@audit:ok. The honesty of the signature rests on: (1) Core genuinely produced, not assumed: the inverse-Stam 1/J_S ≥ 1/J_X+1/J_Y is CONSTRUCTED by isStamInequalityHyp_of_indepFun P A B (a regularity-only construction via stamCauchySchwarzOptimal_of_indepFun, @audit:ok) then APPLIED at density_t. The three IsDeBruijnRegularityHyp inputs are consumed only as regularity (.pX/.pX_law/.pX_nn/.pX_meas density witnesses + .density_t_eq pointwise pins), never as a bundled inequality core. No := h circularity, no :True, no degenerate exploitation, no *Hypothesis-core bundling, no name laundering. (2) a.e.→pointwise wash: the object IsStamInequalityHyp consumes is the POINTWISE-pinned smooth density_t (density_t_eq pins to the explicit smooth convDensityAdd pX g_t, not an a.e. rnDeriv class); the a.e. seam sits only at the un-smoothed input (pXY =ᵐ convDensityAdd pX pY) and is washed through convDensityAdd · g by integral_congr_ae. A skeptic cannot pick a bad pointwise representative. (3) indepSum_density_ae sound + non-vacuous (see its tag). (4) isBlachmanConvReady_convDensityAdd_gaussian_asym = pure 19-field regularity (see its tag). (5) Unused hyps (hZ/hXZX/hYZY/hZX_law/hZY_law/hZ_law/hX_ac/hY_ac/hmomX/hmomY) are OVER-hypothesized-harmless: kept to match the uniform shape EPIDensityForm passes to entropyPower_add_ge_case1_of_regular_twotime; the de Bruijn regularity hyps already carry the needed density data (no gap masked, proof closes without them = NOT under-hypothesized). hpair_indep is a genuine necessary precondition (pairwise indep insufficient for A=X+√σ·Z_X ⊥ B=Y+√τ·Z_Y; derived via .comp). sorryAx-free.