bitDeviation_eq
plain-language theorem explainer
Under the BIT dark-energy kernel, the equation-of-state deviation equals the amplitude times the normalized cosmic-Z history: δw(z) = δw₀ · Z(z)/Z_today. Cosmologists citing the U5 shape reduction use this identity as the algebraic bridge from w(z) to Z-history. The proof unfolds the two definitions and cancels by ring.
Claim. For real parameters $\delta w_0$, $Z_{\mathrm{today}}$, a cosmic-Z history $Z:\mathbb{R}\to\mathbb{R}$, and redshift $z$, the BIT equation-of-state deviation satisfies $\delta w(z)=\delta w_0\cdot Z(z)/Z_{\mathrm{today}}$.
background
This module treats the dark-energy shape problem (U5) under the BIT mechanism: the equation of state is written $w(z)=-1+\delta w_0\cdot Z(z)/Z_{\mathrm{today}}$, where $Z(z)$ is integrated cosmic Z-complexity at redshift $z$ and $Z_{\mathrm{today}}=Z(0)$.
Two local definitions fix the notation. The BIT kernel is $w(z)=-1+\delta w_0\cdot Z(z)/Z_{\mathrm{today}}$. The deviation is $\delta w(z):=w(z)+1$, so it is the excess of $w$ above $-1$. The present lemma simply evaluates that excess.
The module's larger claim is that, once the kernel is fixed, deriving the dark-energy shape is exactly deriving the normalized Z-history; boundary conditions then force $\delta w(0)=\delta w_0$ today and $\delta w\to 0$ in the early universe (ΛCDM recovery).
proof idea
Term-mode one-liner. Unfold the deviation as kernel plus one, unfold the kernel as $-1+\delta w_0\cdot Z(z)/Z_{\mathrm{today}}$, then ring cancels the $\pm 1$ and leaves the product. No external lemmas.
why it matters
This is the algebraic engine of the honest U5 reduction. Downstream, bitDeviation_today specializes to $z=0$ to get $\delta w(0)=\delta w_0$; shape_reduction normalizes both sides so the normalized deviation equals the normalized Z-history; linear_accumulation_forces_canonical_kernel and reciprocal_history_kernel rewrite the same identity under linear-in-$a$ or general reciprocal histories $Z(z)=Z_{\mathrm{today}}/g(z)$. The certificate bundle cosmicZShapeCert records it as the deviation formula.
Framework role: it converts the BIT kernel into a pure shape statement, isolating the remaining freedom as the accumulation law for $Z(z)$ (linear in scale factor versus other monotone histories). That single premise is the stated residue of U5; the identity itself is unconditional and proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.