ScaleFree
plain-language theorem explainer
Scale-free is the multiplicative Cauchy property for redshift kernels: composing scale factors multiplies attenuations. Cosmologists deriving the BIT dark-energy kernel cite it as the functional class that rung factorization forces. It is a pure Prop definition, not a proved statement.
Claim. A real function $f$ is scale-free when, for all redshifts $z,w \ge 0$, $$f\bigl((1+z)(1+w)-1\bigr) = f(z)\,f(w).$$ Equivalently, $f$ turns multiplication of cosmic scale factors into multiplication of attenuations.
background
The module forces the shape of the BIT dark-energy deviation kernel $K(z)$ in $w(z)=-1+\delta w_0\cdot K(z)$. Two premises drive the derivation: rung factorization (attenuation across $m+n$ $\varphi$-rungs is the product of the sub-attenuations) and single-rung balance (one rung attenuates by the unique positive fixed point of $\rho=1/(1+\rho)$, namely $\varphi^{-1}$).
Scale composition on the redshift line is the map $(z,w)\mapsto(1+z)(1+w)-1$. A kernel that respects independent composition of aging charges must convert that product of scale factors into a product of attenuations. That is exactly the scale-free property.
Related objects in the same file include the power family $K_s(z)=(1+z)^{-s}$ and the canonical kernel pinned by the rung law $\mathrm{occ},n=\varphi^{-n}$. Upstream kernel families (constant, $1/(1+z)$, exponential) supply the comparison class against which the forced shape is selected.
proof idea
No proof: this is a definition of a Prop. The body is the universal quantification over nonnegative $z,w$ of the multiplicative identity under redshift composition. Downstream theorems (e.g. every power kernel is scale-free) unfold this definition and discharge the equality by elementary algebra on $(1+z)^{-s}$.
why it matters
Scale-free is the functional class in which the rung condition pins the exponent. The immediate consumer is powerKernel_scaleFree, which places every power kernel $K_s(z)=(1+z)^{-s}$ inside this class. Combined with the forced single-rung value $\varphi^{-1}$, the module obtains $s=1$ exactly, excluding volume dilution ($s=3$) and spacetime dilution ($s=4$).
That selection yields the canonical kernel $K(z)=1/(1+z)$, which is CPL on the thawing line $w_a=-(1+w_0)$ with sum rule $w_0+w_a=-1$ and the band $w_0\in(-1,-0.88)$. The same class underwrites the no-phantom bound $w(z)\ge-1$ and the retirement of the "BIT explains the Planck–RS $\Omega_\Lambda$ gap" hypothesis. Open remain the BIT aging mechanism itself, the single-channel ($d=1$) selection, and the today-amplitude $\delta w_0\in(0,J(\varphi)]$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.