RungCondition
plain-language theorem explainer
The φ-rung condition on a real kernel f asserts that at redshift z = φ−1 (one cosmic rung: 1+z = φ) the value equals the forced single-rung attenuation φ⁻¹. Cosmologists pinning the BIT dark-energy kernel cite it as the balance constraint that selects the scale-free exponent. It is a pure Prop definition encoding that single evaluation, not a proved claim.
Claim. A real function $f$ satisfies the rung condition when $f(\varphi-1)=\varphi^{-1}$. Equivalently, at the redshift of one $\varphi$-rung ($1+z=\varphi$) the kernel equals the forced single-rung attenuation $\varphi^{-1}$.
background
This module forces the shape of the BIT dark-energy kernel $K(z)$ appearing in $w(z)=-1+\delta w_0\cdot K(z)$. Two premises drive the derivation: rung factorization (attenuation across $m+n$ φ-rungs multiplies) and single-rung balance (one rung attenuates by the unique positive fixed point of $\rho=1/(1+\rho)$, which is $\varphi^{-1}$).
The golden ratio $\varphi$ is the self-similar fixed point of Recognition Science (forcing chain T6). On the cosmic lattice $1+z=\varphi^n$, the forced occupation is $\mathrm{occ},n=\varphi^{-n}$. The present definition packages the $n=1$ instance as a predicate on an arbitrary real function $f$, so later theorems can ask which candidate kernels obey it.
Sibling objects include the scale-free family $\mathrm{powerKernel},s=(1+z)^{-s}$ and the canonical kernel $1/(1+z)$. The condition is the bridge from the single-rung fixed-point premise to exponent selection inside that family.
proof idea
Definition only: the body is the equality $f(\varphi-1)=1/\varphi$. No tactics, no lemmas. Downstream proofs unfold this Prop and simplify the argument $1+(\varphi-1)=\varphi$ by ring before comparing exponents.
why it matters
This predicate is the pinning interface for the forced-redshift-kernel paper. The theorem powerKernel_rung_condition_iff uses it to prove that among scale-free kernels $K_s(z)=(1+z)^{-s}$ the rung condition holds if and only if $s=1$, excluding volume dilution ($s=3$) and spacetime dilution ($s=4$).
The one-statement summary bit_kernel_shape_one_statement packages that biconditional with the forced occupation law $\mathrm{occ},n=\varphi^{-n}$, agreement of the $s=1$ power kernel with the canonical kernel, the CPL thawing line $w_a=-(1+w_0)$, and the no-phantom bound $w(z)\ge-1$.
Framework landmarks: φ from T6, single-rung balance $\varphi^{-1}$ as the reciprocal fixed point, and the multiplicative shadow of cost additivity. Open items remain the BIT aging mechanism itself, the single-channel ($d=1$) selection behind the rung condition, and the today-amplitude band $\delta w_0\in(0,J(\varphi)]$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.