bitDeviation
plain-language theorem explainer
Defines the dark-energy equation-of-state deviation δw(z) := w(z) + 1 under the BIT kernel. Anyone working the U5 shape reduction cites it as the object equal to δw₀ · Z(z)/Z_today. The body is a one-line shift of the BIT kernel by +1.
Claim. For parameters $\delta w_0$, $Z_{\mathrm{today}}$, a cosmic-$Z$ history $Z_{\mathrm{hist}}$, and redshift $z$, the equation-of-state deviation is $\delta w(z) := w_{\mathrm{BIT}}(z) + 1$, where $w_{\mathrm{BIT}}(z) = -1 + \delta w_0 \cdot Z_{\mathrm{hist}}(z)/Z_{\mathrm{today}}$.
background
The 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}}$, with $Z(z)$ the integrated cosmic $Z$-complexity at redshift $z$ and $Z_{\mathrm{today}} = Z(0)$.
The BIT kernel is the real-valued map sending $(\delta w_0, Z_t, Z_{\mathrm{hist}}, z)$ to $-1 + \delta w_0 \cdot Z_{\mathrm{hist}}(z)/Z_t$. The deviation is the natural companion quantity $\delta w(z) = w(z) + 1$, so that a pure cosmological-constant phase is exactly $\delta w = 0$.
Local goal of the file: prove that under BIT the normalized deviation equals the normalized cosmic-$Z$ history (shape reduction), and that linear-in-scale-factor accumulation forces the canonical $1/(1+z)$ kernel.
proof idea
Pure definitional wrapper. Unfolds as the BIT kernel plus one: $\mathrm{bitDeviation} = \mathrm{bitKernel} + 1$. No lemmas, no tactics; the algebraic content appears only in the companion equality theorem that simplifies the sum to $\delta w_0 \cdot Z_{\mathrm{hist}}(z)/Z_t$.
why it matters
This is the working object for the entire Cosmic $Z$-History / dark-energy shape certificate. Downstream theorems prove it equals $\delta w_0 \cdot Z(z)/Z_{\mathrm{today}}$, that today it recovers $\delta w_0$, and that under linear-in-$a$ accumulation it becomes exactly $\delta w_0/(1+z)$. The reciprocal-history theorem generalizes: any $Z(z) = Z_{\mathrm{today}}/g(z)$ yields $\delta w(z) = \delta w_0/g(z)$.
In the Recognition framework this localizes U5: deriving the dark-energy shape is exactly deriving the cosmic-$Z$ accumulation law. The residual open question is why accumulation is linear in the scale factor rather than in cosmic time or $a^p$. The definition feeds both the in-module shape certificate and the scale-law certificate in CosmicZScaleLaw.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.