bitDeviation_today
plain-language theorem explainer
At redshift zero, when the cosmic Z-history equals today's value $Z_{\mathrm{today}}\neq 0$, the BIT equation-of-state deviation equals the amplitude $\delta w_0$. Anyone citing the U5 dark-energy shape reduction or the cosmic-Z certificate needs this boundary condition. The proof is a three-step rewrite through the closed form $\delta w=\delta w_0\cdot Z/Z_{\mathrm{today}}$.
Claim. Let $\delta w_0,Z_t\in\mathbb{R}$ and let $Z:\mathbb{R}\to\mathbb{R}$ be a cosmic Z-history. If $Z(0)=Z_t$ and $Z_t\neq 0$, then the BIT equation-of-state deviation satisfies $\delta w(0)=\delta w_0$, where $\delta w(z):=w(z)+1$ is given by the BIT kernel.
background
The module reduces the dark-energy shape problem (U5) under the BIT mechanism: $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 is defined as the BIT kernel plus one, and bitDeviation_eq proves the closed form $\delta w(z)=\delta w_0\cdot Z(z)/Z_t$. The present result is the $z=0$ boundary of that identity: today the normalized ratio is one, so the deviation collapses to the free amplitude $\delta w_0$. The companion early-universe boundary ($Z\to 0$) recovers $w=-1$ (standard $\Lambda$CDM).
proof idea
One-line rewrite proof. Apply bitDeviation_eq to replace the deviation by $\delta w_0\cdot Z(z)/Z_t$ at $z=0$. Substitute the hypothesis $Z(0)=Z_t$, cancel the ratio by div_self (using $Z_t\neq 0$), and finish with mul_one.
why it matters
This is the forced today-boundary of the shape reduction: $\delta w(0)=\delta w_0$. It is recorded as the today_value field of cosmicZShapeCert, the module's certificate packaging the exact shape reduction and the conditional canonical-kernel derivation.
Together with the early-universe vanishing of the deviation, it localizes U5 to a single remaining premise: whether cosmic Z accumulates linearly in the scale factor. The shape reduction itself is unconditional; the canonical $1/(1+z)$ kernel is theorem only under that linear-accumulation hypothesis. No new axiom is introduced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.