The centered Gaussian 𝒩(0, v) (with v ≠ 0) assigns mass exactly 1/2 to the half-line {x | 0 ≤ x}.

@audit:ok (symmetry-by-map).

The Gaussian self-law witness: the identity map on ℝ has law gaussianReal 0 w under gaussianReal 0 w.

The half-line mass tends to the Gaussian median. The tilted-ambient mass (ℝ≥0∞-valued) of the half-line {ω | m·n ≤ ∑_{i<n} Y(ω i)} (at the tilted mean m = ∫ Y ∂tilted) converges to the Gaussian mass gaussianReal 0 v.toNNReal (Ici 0).

@audit:ok (CLT + portmanteau + scaling assembly).

The half-line mass tends to 1/2: the tilted-ambient .real-mass of {ω | m·n ≤ ∑_{i<n} Y(ω i)} tends to 1/2.

Boundary window largeness. At the boundary a = m (= tilted mean), the tilted infinite-product window mass {ω | m·n ≤ ∑Y < (m+ε)·n} is eventually ≥ 1/4.

@audit:ok (CLT + LLN assembly; hVar : 0 < Var is the non-degeneracy precondition required by the Gaussian median gaussianReal_Ici_eq_half (v=0 degeneracy is correctly excluded by spec).

A per-instance change-of-measure half-line lower bound. At a single threshold a and ε > 0, eventual largeness C ≤ tilted-window mass lifts to the un-tilted half-line lower bound C·exp(-n(λa - Λ + λε)) ≤ P{a·n ≤ ∑Y}.

@audit:ok (change-of-measure lift via change_of_measure_lower_bound_pi (real density bound, not vacuous) + cylinder lift; no C=0/exp=0 vacuity — at the call site C = 1/4 > 0, exp(...) > 0 always).

A per-ε boundary liminf lower bound. At the boundary a = m (= tilted mean ∫ Y ∂tilted), for each ε > 0, -(λm - Λ + λε) ≤ liminf (1/n)·log P{m·n ≤ ∑Y}.

@audit:ok (no degenerate-log exploit — hP_pos : 0 < P{...} is derived from the window lower bound (1/4)·exp(...) ≤ P{...}, so log is taken of a strictly positive real; h_coboundedBelow is the genuine liminf_le_liminf side-condition, not load-bearing).

Cramér's theorem (lower bound, boundary closure). At the interior optimal tilt a = m = ∫ Y ∂tilted (= deriv (cgf Y μ₀) lam, the boundary of the residual window), the asymptotic upper-tail rate is bounded below by the per-lam Chernoff exponent -(λm - Λ). The residual largeness hypothesis is removed — the boundary window mass is supplied internally by the CLT. Only the regularity preconditions remain: boundedness, non-degeneracy 0 < Var, and the cobounded hypothesis on the rate sequence (a precondition shared with cramer_lower).

@audit:ok (ε→0⁺ collapse via le_of_forall_sub_le; the CLT supplies the boundary window mass internally — no residual largeness hypothesis).

Cramér's theorem (lower bound, boundary closure, consumer form). The infinitePi-side restatement of cramer_lower_boundary_at_tilted_mean with the cgf written on the coordinate-eval family Y ∘ eval 0 under the un-tilted product, at the optimal tilt a = deriv (cgf (Y∘eval 0) (infinitePi μ₀)) lam. The optimal-tilt hypothesis h_deriv pins a = m = ∫ Y ∂tilted, so the residual largeness hypothesis is removed: the boundary window mass is supplied internally by the CLT.

See also cramer_lower_boundary_at_tilted_mean.

@audit:ok (h_deriv/hVar/h_coboundedBelow are all preconditions, not load-bearing — h_deriv pins a = m (the true-as-framed constraint), hVar is the non-degeneracy precondition, h_coboundedBelow is the standard liminf_le_liminf side-condition (satisfiable: rate terms ≤ 0 since P ≤ 1, not vacuous); matches consumer root cramer_lower_infinitePi signature verbatim).