powerKernel_scaleFree
plain-language theorem explainer
Every real power kernel $K_s(z)=(1+z)^{-s}$ is scale-free: it converts multiplication of cosmic scale factors into multiplication of attenuations. Cosmologists forcing the BIT redshift kernel cite this to place the power family inside the multiplicative Cauchy class before the rung condition pins $s=1$. The proof is a short algebraic reduction via the real power product law after simplifying the composed redshift argument.
Claim. For every real exponent $s$, the map $K_s(z)=(1+z)^{-s}$ is scale-free: for all $z,w\ge 0$, $K_s\bigl((1+z)(1+w)-1\bigr)=K_s(z)\,K_s(w)$.
background
The module forces the shape of the dark-energy deviation kernel $K(z)$ in $w(z)=-1+\delta w_0\cdot K(z)$ from two premises: rung factorization (attenuation across $m+n$ $\varphi$-rungs multiplies) and single-rung balance (one rung attenuates by $\varphi^{-1}$, the positive fixed point of $\rho=1/(1+\rho)$).
A kernel is scale-free when it turns multiplication of scale factors into multiplication of attenuations: $f\bigl((1+z)(1+w)-1\bigr)=f(z)f(w)$ for $z,w\ge 0$. The power family is $K_s(z)=(1+z)^{-s}$. Scale-freeness is the continuous multiplicative Cauchy law on the redshift coordinate $1+z$, the natural shadow of cost additivity under independent composition of cosmic scale steps.
This sits inside the BIT kernel shape-forcing development: once power kernels are known to be scale-free, the rung condition (value $\varphi^{-1}$ at $1+z=\varphi$) can pin the exponent.
proof idea
Tactic proof. Introduce $z,w\ge 0$ and unfold the power kernel. Nonnegativity of $1+z$ and $1+w$ is immediate from linarith. A one-line ring identity rewrites the composed argument: $1+\bigl((1+z)(1+w)-1\bigr)=(1+z)(1+w)$. Rewrite with that identity and apply Real.mul_rpow, which gives $\bigl((1+z)(1+w)\bigr)^{-s}=(1+z)^{-s}(1+w)^{-s}$. Done.
why it matters
Places every power kernel inside the scale-free (multiplicative Cauchy) class that the module uses as the ambient family for shape forcing. The module doc records the payoff: powerKernel_rung_condition_iff then pins $s=1$ exactly from the single-rung value $\varphi^{-1}$, excluding volume dilution ($s=3$) and spacetime dilution ($s=4$). That forced $K(z)=1/(1+z)$ feeds the CPL identification on the thawing line $w_a=-(1+w_0)$, the sum rule $w_0+w_a=-1$, the $w_0$ band, and the no-phantom bound $w(z)\ge -1$.
Framework link: the single-rung attenuation $\varphi^{-1}$ is the reciprocal-balance fixed point tied to the golden ratio forced at T6; rung factorization is the multiplicative shadow of cost additivity (RCL / J-cost structure). No used_by edges are recorded on this declaration itself; its role is the class-membership lemma that makes the exponent-pinning step well-typed.
Open items upstream of this lemma remain the BIT aging mechanism hypothesis 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.