deltaW0_tendsto_ceiling
plain-language theorem explainer
The deep-occupancy limit of the equilibrium BIT today-amplitude δw₀(N) is exactly the recognition cost J(φ). Foundation and cosmology workers tracking δw₀ saturation cite this to pin the ceiling once occupancy depth diverges. The argument is a constant-multiple transfer of the already-proved saturation→1 limit after unfolding the product definition.
Claim. As occupancy depth $N\to\infty$, the equilibrium BIT today-amplitude satisfies $\delta w_0(N)\to J(\varphi)$, where $J(x)=(x+x^{-1})/2-1$ is the recognition cost and $\varphi$ is the golden-ratio fixed point.
background
Module T9 forces the weighting on recognition states after T0–T8 fixed the law's shape. Any admissible weight factorizes over independent steps and obeys per-step self-similar balance ρ=1/(1+ρ), which pins ρ=φ⁻¹ and yields geometric weights w(n)=φ⁻ⁿ.
The equilibrium BIT today-amplitude is the product δw₀(N)=J(φ)·saturation(N), reducing a free real parameter to one integer occupancy depth. J is the unique RS cost J(x)=(x+x⁻¹)/2−1 (T5); φ is the self-similar scale (T6).
Upstream, saturation_tendsto_one already records that deep occupancy exhausts the measure: saturation(N)→1, via the closed form 1−ρ^{N+1} with 0<ρ<1.
proof idea
Unfold δw₀ to the product J(φ)·saturation(N). Invoke Filter.Tendsto.const_mul on the constant J(φ) together with saturation_tendsto_one. A short simplification closes the neighborhood limit at J(φ). No fresh analysis: pure constant-multiple transfer of the saturation limit.
why it matters
Pins the deep-occupancy ceiling of δw₀ inside the T9 measure-forcing program. The module lists δw₀ saturation among the recurring instance-selection gaps (Born weights, chirality, η_B prefactor, rung occupancy) that all project onto the missing weighting primitive. With the geometric φ-measure forced, the asymptotic amplitude equals the cost of φ itself, consistent with T5 J-uniqueness and T6 φ-forcing. No recorded downstream users yet; it is a terminal saturation fact for BIT/cosmology interfaces that import MeasureForcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.