linear_accumulation_forces_canonical_kernel
plain-language theorem explainer
Under linear-in-scale-factor cosmic-Z accumulation Z(z)=Z_today/(1+z), the BIT equation-of-state deviation collapses exactly to δw(z)=δw₀/(1+z). Cosmologists working the U5 dark-energy shape reduction cite this as the conditional derivation of the canonical kernel. The proof is a short algebraic rewrite: apply the BIT deviation identity, unfold the linear history, and cancel Z_today.
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 deviation equals $\delta w(z)=\delta w_0/(1+z)$.
background
The module treats the dark-energy shape problem (U5) under the BIT mechanism: the equation of state is $w(z)=-1+\delta w\cdot Z(z)/Z_{\mathrm{today}}$, with $Z(z)$ the integrated cosmic $Z$-complexity and $Z_{\mathrm{today}}=Z(0)$. The deviation is $\delta w(z):=w(z)+1$.
Upstream, bitDeviation_eq states that under the BIT kernel the deviation is exactly $\delta w(z)=\delta w_0\cdot Z(z)/Z_{\mathrm{today}}$. Thus the normalized dark-energy shape is identical to the normalized $Z$-history (shape reduction). The linear history is defined by $Z(z)=Z_{\mathrm{today}}/(1+z)$, i.e. accumulation linear in the scale factor $a=1/(1+z)$.
The BIT kernel family also names the target shape inv_one_plus_z as $1/(1+z)$. The present result shows that this canonical kernel is forced once the linear-$a$ premise is adopted, rather than inserted by hand.
proof idea
One short algebraic chain. Rewrite the left-hand side by bitDeviation_eq, which replaces the BIT deviation by $\delta w_0\cdot Z(z)/Z_{\mathrm{today}}$. Unfold linearZ to substitute $Z(z)=Z_{\mathrm{today}}/(1+z)$. The quotient becomes $\delta w_0\cdot(Z_{\mathrm{today}}/(1+z))/Z_{\mathrm{today}}$. Cancel $Z_{\mathrm{today}}$ via div_self (using $Z_{\mathrm{today}}\neq 0$) and rearrange with div_div, mul_comm, and mul_one_div to obtain $\delta w_0/(1+z)$.
why it matters
This is the second main result of the Cosmic Z-History module: the conditional derivation of the canonical dark-energy shape from linear-$a$ accumulation. Downstream, linear_accumulation_kernel lifts the deviation identity to the full equation of state $w(z)=-1+\delta w_0/(1+z)$. The certificate cosmicZShapeCert packages this theorem as linear_forces_canonical. In CosmicZScaleLaw, scaleAffine_forces_canonical_deviation reduces scale-affine $Z$-laws to the same linear history and reuses this identity.
Within Recognition Science this localizes U5 honestly: shape reduction is unconditional under BIT; the $1/(1+z)$ form is theorem conditional on linear accumulation. The remaining open question is why $Z$ accumulates linearly in $a$ rather than in cosmic time or $a^p$. No new axioms or sorrys are introduced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.