contWeight_gibbs
plain-language theorem explainer
The forced continuum recognition weight equals the Gibbs exponential exp(−(ln φ)·t) for every real cost t. Anyone citing T9 measure forcing, α resummation, or dressing responses needs this identity. The proof rewrites ρ^t via the positive real power-to-exp definition and substitutes ρ = φ⁻¹.
Claim. For every real $t$, the forced continuum weight $w(t)=\rho^{t}$ with $\rho=\varphi^{-1}$ equals the Gibbs form $w(t)=\exp\bigl(-(\ln\varphi)\cdot t\bigr)$.
background
Module T9 closes the missing weighting rule after the T0–T8 forcing chain has fixed the shape of the law (unique J-cost, φ-scale, eight-tick period, D=3). Admissible weights on recognition states are forced to the geometric φ-measure: weight φ⁻¹ per recognition step, equivalently probability ∝ exp(−(ln φ)·cost).
The per-step factor is rho := 1/φ, forced by reciprocal self-similarity (the same fixed-point balance that pins φ under T6). The continuum weight is the real power contWeight t := rho^t, the continuous extension of the lattice rule w(n)=φ⁻ⁿ obtained from factorization plus step self-similarity.
Upstream positivity rho_pos supplies the hypothesis needed to convert real powers into exponentials. The Gibbs rewriting is the continuum face of the same geometric measure that the lattice layer already forces.
proof idea
Short tactic proof. Unfold contWeight to rho^t. Rewrite the real power by Real.rpow_def_of_pos using rho_pos, obtaining an exponential whose rate is log rho. Congruence on the exponent, unfold rho = 1/φ, then one_div and Real.log_inv turn log(φ⁻¹) into −log φ, which is the claimed Gibbs rate.
why it matters
This is the explicit Gibbs form of the T9 forced measure: probability ∝ exp(−cost) with rate locked at ln φ by the self-similar ledger, nothing fitted. It is recorded as the gibbs_form field of the master certificate measureForcingCert.
Downstream, alphaInv_eq_seed_mul_forced_weight rewrites the certified fine-structure inverse as the channel seed times this continuum weight at the eight-tick spectral load, so α dressing is identified with the unique recognition measure rather than α-specific structure. Likewise response_is_forced_measure shows every dressing response g satisfies g((ln φ)·t) = contWeight t by routing through this identity.
Framework landmark: closes the continuum half of T9 after lattice forcing w(n)=φ⁻ⁿ, linking measure selection (Born weights, rung occupancy, η_B prefactors) to the same φ fixed by T6.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.