contWeight
plain-language theorem explainer
Defines the continuum recognition weight w(t)=ρ^t=φ^{-t} on real additive cost t. Anyone deriving α^{-1}, self-similar dressings, or Gibbs-style occupancy from the T9 measure cites this as the forced continuum form. The body is a one-line abbreviation of the already-forced per-step factor ρ=φ^{-1}.
Claim. The continuum weight on a real load $t$ is $w(t)=\rho^{t}$, where $\rho=\varphi^{-1}$ is the forced per-step weight, equivalently $w(t)=\varphi^{-t}$.
background
Module T9 closes the missing weighting rule after the T0–T8 shape chain (unique J-cost, φ scale, eight-tick period, D=3). Lattice weights factorize over independent steps and obey the self-similar balance ρ=1/(1+ρ), which forces ρ=φ^{-1}. The continuum layer lifts that discrete geometric measure to a real additive cost.
Here rho is defined as 1/φ. The continuum object is the exponential of that same factor: weight decays by one power of φ per unit of additive load. Downstream AlphaGenesis work treats this as the unique self-similar dressing on nonnegative loads, so α-channel attenuation is literally this function evaluated at spectral load.
proof idea
Pure definition: contWeight t is rho ^ t. No tactics. The mathematical content sits in the surrounding theorems that prove this function is the unique continuum weight satisfying factorization, antitonicity, and step self-similarity, and that it equals the Gibbs form exp(-(ln φ)·t).
why it matters
This is the T9 continuum primitive that AlphaGenesis plugs into every forward α construction. canonical exhibits it as a self-similar dressing; response_forced says every such dressing equals this weight on t≥0; alphaInvGenesis and correctedAlphaInv multiply channel budget by contWeight at spectral (plus residual) load; alphaInv_eq_seed_mul_forced_weight unifies the certified α^{-1} with seed times contWeight(w₈/seed).
Framework landmark: the geometric φ-measure (weight φ^{-1} per recognition step), equivalently Gibbs with rate fixed by the self-similar ledger rather than calibrated. It turns the open instance-selection problems listed in the module doc (Born weights, rung occupancy, η_B prefactor) into evaluations of one forced function.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.