Pith. sign in
def

powerKernel

definition
show as:
module
IndisputableMonolith.Cosmology.BITKernelShapeForcing
domain
Cosmology
line
130 · github
papers citing
none yet

plain-language theorem explainer

Defines the one-parameter scale-free redshift kernel family K_s(z)=(1+z)^{-s}. Cosmologists and RS auditors cite it as the multiplicative-Cauchy class in which the BIT rung condition is tested. The body is a direct real-power abbreviation; no proof content.

Claim. For real parameters $s$ and redshift $z$, the power kernel is $K_s(z) = (1+z)^{-s}$.

background

The module forces the shape of the BIT dark-energy kernel in $w(z)=-1+\delta w_0\cdot K(z)$. Two premises drive the argument: rung factorization (attenuation across $m+n$ $\varphi$-rungs multiplies) and single-rung balance (one rung attenuates by the unique positive fixed point of $\rho=1/(1+\rho)$, namely $\varphi^{-1}$).

Among candidate families, the scale-free class converts multiplication of scale factors into multiplication of attenuations. That class is exactly the real-power family $K_s(z)=(1+z)^{-s}$. Related named kernels elsewhere (constant, $1/(1+z)$, exponential) sit in a discrete family enum; here the continuous exponent $s$ is kept free so the rung condition can pin it.

On the $\varphi$-ladder, cosmic scale factors are $\varphi^k$. The lattice identity $1+z=\varphi^n$ converts rung dilution into a concrete value of $K$ at those points, which is what later theorems compare against $K_s$.

proof idea

Pure definition: the body is the real power $(1+z)^{-s}$. No tactics, no lemmas. Downstream proofs unfold this abbreviation and apply real-power algebra (e.g. $x^{-1}=1/x$, multiplicative Cauchy for scale-freeness).

why it matters

This family is the ambient class for the exponent-pinning theorem: the rung condition holds for $K_s$ if and only if $s=1$, which excludes volume dilution ($s=3$) and spacetime dilution ($s=4$). The same definition feeds the scale-free certificate, the identity $K_1=\mathrm{canonical}$ on $z\ge 0$, and the one-statement BIT kernel summary (forced $K(z)=1/(1+z)$, CPL thawing line $w_a=-(1+w_0)$, $w_0\in(-1,-0.88)$, no phantom).

In the paper companion "The Forced Redshift Kernel," this is the modeling class reduced to a single free exponent before $\varphi$-rung balance kills every option but $s=1$. Open items remain the BIT aging mechanism itself, the single-channel ($d=1$) selection, and the today-amplitude $\delta w_0\in(0,J(\varphi)]$; the kernel shape inside the scale-free class is closed.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.