The truncated W-marginal density converges a.e. (volume) to the full W-marginal density: (((truncW P W n).map W).rnDeriv volume x).toReal → ((P.map W).rnDeriv volume x).toReal as n → ∞. Uses (truncW P W n).map W = cond (P.map W) Sn with Sn n = {r | |r| ≤ n}, the conditioned density formula rnDeriv_cond_eq, and the pointwise limit (no weak convergence).

@audit:ok

h(μ) = ⊤ ⟹ A(μ) = ⊤: the positive-part lintegral diverges when the a.c.-branch differential entropy is ⊤. Since h μ = (A : EReal) - (B : EReal) = ⊤ is impossible for finite A, we get A = ⊤; no hypothesis on B(μ) is needed.

@audit:ok

h(μ) = ⊤ ⟹ B(μ) ≠ ⊤: the negative-part lintegral is finite when the a.c.-branch differential entropy is ⊤ (the symmetric counterpart of posPart_lintegral_eq_top_of_diffEntExt_top). If B = ⊤, then (A : EReal) - ⊤ = ⊥ ≠ ⊤. This lets the assembly derive B(P.map W) ≠ ⊤ from h(W) = ⊤ without adding a hypothesis to the signature.

@audit:ok

Explicit upper bound on the negative-part lintegral of the truncated W-marginal: when c_n ≠ 0, B(W_n) ≤ ofReal |cbar_n · log cbar_n| + ofReal cbar_n · B(W), where cbar_n := ((P.map W) (Sn n))⁻¹ and Sn n = {r | |r| ≤ n}. Obtained from the negMulLog-product decomposition of the truncated density fn = cbar_n · 1_{Sn n} · fW and the probability normalization ∫⁻ ofReal fW = 1.

@audit:ok

⊤-divergence of the W-marginal entropy: if h(W) = ⊤, then h(W_n) → ⊤ along the truncations W_n := truncW P W n. The argument has three steps: a.e. convergence of the truncated densities (truncW_map_density_tendsto_ae), A(P.map W) = ⊤ (posPart_lintegral_eq_top_of_diffEntExt_top) combined via Fatou (differentialEntropyExt_posPart_le_liminf_of_ae_tendsto) to force A(W_n) → ⊤, and a uniform bound on B(W_n) (truncW_map_negPart_lintegral_le), so that h(W_n) = A - B → ⊤. Closes by a.e. convergence of densities alone, with no weak-convergence portmanteau.

@audit:ok

Unconditional ⊤-branch of gateway monotonicity: h(W) = ⊤ ⟹ h(W+V) = ⊤. Combines per-n monotonicity h(W_n) ≤ h(W_n + V) (differentialEntropyExt_mono_add_truncW) with the divergence h(W_n) → ⊤ (differentialEntropyExt_truncW_tendsto_top) to squeeze h(W_n + V) → ⊤, then derives A(ν) = ⊤ via per-n Gibbs and measure domination. The only hypotheses are the regularity preconditions hW/hV/hWV/hW_ac together with the case condition hW_top.

@audit:ok

Finite differential entropy implies integrability of negMulLog ∘ density (the converse of differentialEntropyExt_of_ac_integrable): from μ ≪ volume, h(μ) ≠ ⊤, and h(μ) ≠ ⊥, the function negMulLog ((μ.rnDeriv volume ·).toReal) is volume-integrable. Both A and B (the positive- and negative-part lintegrals) are then finite, giving HasFiniteIntegral.

@audit:ok

Unconditional gateway monotonicity: W a.c. and W ⊥ V ⟹ h(W) ≤ h(W+V). The proof splits into the ⊥ branch (bot_le), the finite branch (differentialEntropyExt_mono_add_of_integrable via the finiteness-to-integrability bridge), and the ⊤ branch (differentialEntropyExt_top_of_indep_add).

@audit:ok

Unconditional gateway atom: W a.c. and W ⊥ V ⟹ N(W+V) ≥ N(W). Lifts differentialEntropyExt_mono_add along EReal.exp_monotone to entropyPowerExt.

@audit:ok