Uniform sup bound gaussianPDFReal μ v x ≤ (√(2πv))⁻¹ (attained at x = μ), from exp(-(x-μ)²/(2v)) ≤ 1. @audit:ok

Boundedness of gaussianPDFReal μ v. @audit:ok

Elementary bound s * exp(-s²/(2v)) ≤ √v for s ≥ 0, v > 0. Proof: with u = s/√v ≥ 0, the claim is u ≤ exp(u²/2), which follows from u ≤ 1 + u²/2 ≤ exp(u²/2). @audit:ok

Continuity of deriv (gaussianPDFReal m v) via its closed form -(x-m)/v · gaussianPDFReal m v x. @audit:ok

Boundedness of deriv (gaussianPDFReal m v). deriv f w = -(w-m)/v · f w, and |w-m| · exp(-(w-m)²/(2v)) ≤ √v (by mul_exp_neg_sq_le), so the derivative is uniformly bounded. @audit:ok

Integrable (fun x => logDeriv (gaussianPDFReal m v) x * gaussianPDFReal m v x). Since logDeriv f · f = -(x-m)/v · f, this is -(1/v) times integrable_sub_mul_gaussianPDFReal. @audit:ok

The pointwise density convolution closed form for Gaussians.

convDensityAdd (gaussianPDFReal mX vX) (gaussianPDFReal mY vY) z = gaussianPDFReal (mX+mY) (vX+vY) z for every z.

Built via the measure-level route gaussianReal_conv_gaussianReal + gaussianReal_of_var_ne_zero

• mconv_withDensity_eq_mlconvolution₀, then ENNReal↔Real bridge and an a.e.→pointwise upgrade using continuity of both sides. @audit:ok

IsRegularDensityV2 (gaussianPDFReal m v) — all six fields discharged from the existing Gaussian regularity lemmas in FisherInfoGaussian. @audit:ok

A Gaussian witness for IsBlachmanConvReady, establishing density-route non-vacuousness.

The structure literal supplies each of the 19 fields from the existing Gaussian lemmas (and the linchpin for int_fisherZ). All 19 fields are now genuine (0 sorry). The previously-residual 5 — int_Wsq, int_inner (quadratic-score integrability) and int_prod1/2/3 (non-separable 2D Tonelli terms) — are closed WITHOUT a Mathlib wall: int_Wsq by the 3-term (a+b)² expansion (each term integrable × bounded, then /pZ); int_prod1/2/3 by the shear change of variables measurePreserving_prod_sub_swap ((z,x) ↦ (x, z-x)) turning the non-separable fY(z-x) into a separable g(x)·h(z-x) to which Integrable.mul_prod applies; int_inner by reducing to those product-measure integrabilities via the Tonelli marginal Integrable.integral_prod_left plus the condDensityX · pZ = fX·fY(z-·) cancellation.

The witness is a plain structure literal {mX mY vX vY} (hvX hvY); IsBlachmanConvReady carries only Integrable/boundedness/positivity fields (no inequality/equality/value core), so this is not a load-bearing bundle. It is a proven inhabitant of IsBlachmanConvReady (gaussianPDFReal mX vX) (gaussianPDFReal mY vY), establishing non-vacuousness for the density route. @audit:ok

The density-route convex Fisher bound for Gaussians.

The density-route convex Fisher bound convex_fisher_bound_of_ready fires end-to-end on Gaussian densities: feeding the proven IsBlachmanConvReady witness + IsRegularDensityV2 instances + Gaussian normalization. The only hypotheses are regularity (vX,vY ≠ 0, 0 ≤ lam ≤ 1); none carries the inequality core. @audit:ok

The density-route Gaussian Fisher bound in closed form.

Specializing convex_fisher_bound_gaussian_via_density_route via the Gaussian Fisher closed form J(𝒩(m,v)) = 1/v (fisherInfoOfDensity_gaussianPDFReal) and the convolution closed form convDensityAdd (gaussian)(gaussian) = gaussian(sum), the density route yields the same 1/(vX+vY) ≤ λ²/vX + (1-λ)²/vY arithmetic content as the measure-level closed-form route stam_convex_fisher_bound_gaussian. This is the same arithmetic content, not a definitional identity of fisherInfoOfDensity vs fisherInfoOfMeasureV2. @audit:ok