sub_gaussian_in_J
plain-language theorem explainer
For any rate λ ≥ 0 and log-deviation t, the forced recognition measure exp(−λ J(eᵗ)) is pointwise dominated by the Gaussian exp(−λ t²/2). Anyone citing continuum Gibbs weights or L² concentration on the recognition ledger needs this bound. The proof rewrites J(eᵗ) as cosh t − 1 and applies the elementary inequality cosh t − 1 ≥ t²/2.
Claim. For all real $\lambda \ge 0$ and all real $t$, $\exp(-\lambda \, J(e^{t})) \le \exp(-\lambda \, t^{2}/2)$, where $J(x) = (x + x^{-1})/2 - 1$ is the recognition cost.
background
Module T9 (MeasureForcing) closes the weighting gap left by the T0–T8 forcing chain: once J, φ, the eight-tick period, and D = 3 are fixed, one still needs the rule that assigns mass to recognition states. The continuum layer takes an additive real cost and forces a Gibbs weight proportional to exp(−λ · cost), with λ pinned by self-similarity.
The recognition cost is $J(x) = (x + x^{-1})/2 - 1$. On the log-deviation coordinate $x = e^{t}$ one has the identity $J(e^{t}) = \cosh t - 1$ (lemma Jcost_exp_eq_cosh_sub_one). The elementary comparison $\cosh t - 1 \ge t^{2}/2$ for all real $t$ (lemma half_sq_le_cosh_sub_one) is the analytic seed of Gaussian domination.
Together these place the forced continuum measure in the sub-Gaussian regime of variance $1/\lambda$ in log-deviation, which is the L² control needed before identifying the measure with existing RS constants.
proof idea
Rewrite the left-hand cost via Jcost_exp_eq_cosh_sub_one, so the claim becomes $\exp(-\lambda(\cosh t - 1)) \le \exp(-\lambda t^{2}/2)$. Monotonicity of exp reduces this to $-\lambda(\cosh t - 1) \le -\lambda t^{2}/2$. Invoke half_sq_le_cosh_sub_one to get $t^{2}/2 \le \cosh t - 1$, multiply by $\lambda \ge 0$, and finish by nlinarith.
why it matters
This is the L² seed of the continuum half of T9. It feeds the master certificate measureForcingCert, which packages lattice forcing, continuum forcing, nonvacuity, and the Gibbs form of the weight. Without sub-Gaussian domination one cannot pass from the abstract Gibbs rule to concrete concentration, Born-type projections, or the identification of existing constants (θ = φ⁻⁴, rung dilution) with the forced measure.
In the broader chain it sits after T5 (J-uniqueness) and T6 (φ fixed point): the cost shape is already forced, and this lemma extracts the quadratic lower bound that makes the continuum weight Gaussian-dominated. Downstream instance-selection problems listed in the module doc (Born weights, chirality, δw₀, η_B, rung occupancy) all inherit L² control from this inequality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.