module module moderate

`IndisputableMonolith.Cosmology.BITKernelShapeForcing`

Cosmology module that forces the BIT occupancy kernel from self-similar attenuation: the unique positive fixed point of ρ = 1/(1+ρ) is φ⁻¹, and occupancy along the rung ladder is thereby fixed as 1/(1+z) (equivalently φ-power dilution). Anyone deriving the forced measure on recognition states or a scale-free cosmological kernel cites it. The argument is algebraic uniqueness plus inductive rung conditions, not a single wrapper.

claimThe unique positive solution of $\rho = 1/(1+\rho)$ is $\rho = \varphi^{-1}$. Under self-similar rung dilution, occupancy satisfies $\mathrm{occ}(0)=1$ and the forced recurrence, hence $\mathrm{occ} = 1/(1+z)$ on the cosmological ladder; the canonical and power kernels are scale-free with that shape.

background

Recognition Science fixes the cost $J$ and the golden scale $\varphi$ in the T0–T8 forcing chain; cosmology still needs a weighting rule for how much recognition mass sits at each rung or redshift. This module works in RS-native units from Constants and the cost calculus from Cost, and treats occupancy as a positive real assigned to ladder steps.

The fixed-point equation $\rho = 1/(1+\rho)$ is the self-similar attenuation law: each step keeps a fraction equal to the residual after one unit of dilution. Its unique positive root is $\varphi^{-1}$ (the Berry threshold scale). Sibling structure introduces rung dilution, occupancy at zero and one, the forced occupancy map, the identity $\mathrm{occ}=1/(1+z)$, and both canonical and power kernels with a scale-free predicate and a rung condition.

proof idea

The module is theorem-bearing, not a pure definitions file. Uniqueness of the positive root of $\rho(1+\rho)=1$ is elementary algebra and pins $\varphi^{-1}$. Occupancy is then forced by a rung condition: base value at the zero rung, one-step attenuation by the fixed point, and inductive extension along the ladder. Equality with $1/(1+z)$ is the closed form of that recurrence. Canonical and power kernels are defined from that occupancy; scale-freeness is checked by homogeneity under rung rescaling. Downstream measure work only needs the forced kernel shape, not a fresh derivation of $\varphi$.

why it matters in Recognition Science

T0–T8 force the shape of the law ($J$, $\varphi$, eight-tick period, $D=3$) but not the weighting over allowed recognition states. This module supplies the cosmological BIT kernel shape that MeasureForcing imports when it closes T9: the forced measure on recognition states. Downstream doc-comment: the earlier chain "did not force the weighting: given the allowed recognition states, which rule says how much of reality sits in each one?"

By tying occupancy to $\varphi^{-1}$ self-similar attenuation and to $1/(1+z)$, the module connects the golden ladder (mass/rung structure, Berry threshold $\varphi^{-1}$) to a concrete scale-free cosmological kernel. Without it, T9 would lack a forced radial or redshift weight and would remain an open interface rather than a forced measure.

scope and limits

Does not derive $J$-uniqueness, $\varphi$, eight-tick structure, or $D=3$; those stay in the T0–T8 chain.
Does not construct the full T9 measure; only the BIT/occupancy kernel shape used by MeasureForcing.
Does not fit observational $H(z)$ or $\Lambda$CDM parameters; the kernel is RS-native and scale-free.
Does not claim empirical uniqueness beyond the algebraic fixed point and rung recurrence stated in-module.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Foundation.MeasureForcing module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (34)

theorem self_similar_attenuation_forced L54
structure RungDilution L74
theorem occ_zero L89
theorem occ_one_forced L99
theorem occ_forced L103
theorem occ_eq_inv_one_plus_z L113
def canonicalKernel L124
theorem canonicalKernel_today L126
def powerKernel L130
def ScaleFree L134
theorem powerKernel_scaleFree L138
def RungCondition L148
theorem powerKernel_rung_condition_iff L154
theorem powerKernel_one_eq_canonical L176
def RungScalingLaw L185
theorem canonicalKernel_rungScaling L189
theorem rungScaling_forces_lattice L201
def w_CPL L219
def w_RS L222
theorem w_RS_is_CPL L225
def OnThawingLine L233
theorem rs_on_thawing_line L236
theorem cpl_sum_rule L242
lemma jcost_phi_closed L244
theorem jcost_phi_lt_012 L253
theorem w0_band L260
theorem no_phantom L267
theorem deviation_ceiling L276
def omega_lambda_bare L295
def omega_lambda_corrected_max_amplitude L298
def planck_central L301
def planck_sigma L304
theorem omega_gap_explanation_retired L311
theorem bit_kernel_shape_one_statement L326