contWeight_eq_phi_rpow_neg
plain-language theorem explainer
The forced continuum recognition weight at real cost t equals φ to the power −t. Anyone working with the T9 geometric measure cites this to pass between the ρ-power definition and the inverse-φ form used in Gibbs statements. The argument is a short unfold-and-rewrite on real powers, using positivity of φ.
Claim. For every real number $t$, the forced continuum weight satisfies $w(t)=\varphi^{-t}$, where $w(t):=\rho^{t}$ and $\rho:=\varphi^{-1}$.
background
Module T9 closes the missing weighting rule after the T0–T8 chain fixed the shape of the law (unique J-cost, φ-scale, eight-tick period, D=3). The problem is which measure sits on allowed recognition states; Born weights, chirality selection, and rung occupancy are projections of that single gap.
On the lattice, admissible weights factorize over independent composition and obey per-step self-similar balance ρ=1/(1+ρ). That fixed point forces ρ=φ⁻¹, hence discrete weights w(n)=φ⁻ⁿ, identical in form to BIT-kernel rung dilution.
The continuum layer treats weight as a function of a real additive cost. The local definition is the power w(t)=ρ^t with ρ:=1/φ. The present identity rewrites that power in inverse-φ form, matching the module claim that probability is proportional to exp(−(ln φ)·cost).
proof idea
Unfold the continuum weight to ρ^t and ρ to 1/φ, obtaining (1/φ)^t. Rewrite the reciprocal via one_div and Real.inv_rpow (using φ>0), then apply the negation identity Real.rpow_neg to reach φ^(−t). No Recognition-specific lemmas beyond positivity of φ; pure real-power algebra.
why it matters
T9 asserts that any admissible weighting is the geometric φ-measure. This theorem is the continuum identity that puts the forced weight in inverse-φ-power form, the presentation used next to the Gibbs statement w(t)=exp(−(ln φ)·t) with rate pinned by the self-similar ledger rather than fitted.
It sits downstream of the forced per-step ratio ρ=φ⁻¹ (from self-similar attenuation and T6 uniqueness of φ) and of the continuum weight definition itself. The lattice side is already identified with rung dilution via toRungDilution; this line is the matching continuum rewrite. No further used-by edges are recorded yet, so it is presently a presentation lemma inside MeasureForcing rather than a widely imported API fact.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.