linear_accumulation_kernel
plain-language theorem explainer
Under linear-in-scale-factor cosmic-Z accumulation, the BIT dark-energy equation of state is exactly w(z) = -1 + δw₀/(1+z). Cosmologists tracking the U5 shape reduction cite this as the w-form of the canonical kernel. The proof is a one-step rewrite of the companion δw identity via the definition δw = w + 1 and linear arithmetic.
Claim. For real parameters $\delta w_0$, $Z_{\mathrm{today}}\neq 0$, and redshift $z$ with $1+z\neq 0$, if the cosmic-$Z$ history is the linear-in-scale-factor law $Z(z)=Z_{\mathrm{today}}/(1+z)$, then the BIT equation of state evaluates to $w(z)=-1+\delta w_0/(1+z)$.
background
The module CosmicZHistory reduces the dark-energy shape problem (U5) under the BIT mechanism. The BIT kernel writes the equation of state as $w(z)=-1+\delta w_0\cdot Z(z)/Z_{\mathrm{today}}$, where $Z(z)$ is the integrated cosmic $Z$-complexity and $Z_{\mathrm{today}}=Z(0)$. The companion deviation is $\delta w(z):=w(z)+1$.
Shape reduction shows that the normalized deviation equals the normalized $Z$-history, so deriving $w(z)$ is exactly deriving $Z(z)$. The linear history $Z(z)=Z_{\mathrm{today}}/(1+z)$ (equivalently linear in the scale factor $a=1/(1+z)$) is the stated accumulation premise.
The upstream theorem linear_accumulation_forces_canonical_kernel already proves $\delta w(z)=\delta w_0/(1+z)$ under that premise. The present result is the same identity rewritten for $w$ itself.
proof idea
Invoke the companion theorem linear_accumulation_forces_canonical_kernel, which yields bitDeviation dw0 Zt (linearZ Zt) z = dw0 / (1+z). Unfold the definition bitDeviation := bitKernel + 1 in that equality, then finish by linarith: subtracting 1 from both sides gives bitKernel = -1 + dw0/(1+z). No further unfolding of linearZ or division algebra is needed here; that work lives in the companion.
why it matters
This is the equation-of-state form of the conditional canonical-kernel derivation that closes the second result of the CosmicZHistory module. The module doc states that if $Z$ accumulates linearly in $a$, then BIT produces exactly the canonical $\delta w(z)=\delta w_0/(1+z)$; the present theorem packages that conclusion as $w(z)=-1+\delta w_0/(1+z)$, matching the classical phenomenological kernel used in dark-energy reconstructions.
Together with shape reduction, it localizes the entire U5 residue to a single physical premise: why cosmic $Z$ accumulates linearly in the scale factor rather than in cosmic time or as a power $a^p$. The following module comment on general reciprocal histories makes the same point: the accumulation law chooses $g$, and every downstream observable is then fixed. No downstream Lean consumers are wired yet; the declaration stands as the $w$-side export of the conditional derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.