shape_reduction
plain-language theorem explainer
Under the BIT dark-energy kernel, the normalized equation-of-state deviation δw(z)/δw(0) equals the normalized cosmic-Z history Z(z)/Z(0). Cosmologists deriving the U5 dark-energy shape cite this to collapse that problem onto deriving Z(z) alone. The proof is a two-line rewrite from the closed form δw(z)=δw₀·Z(z)/Z_today, cancelling the nonzero amplitude.
Claim. For nonzero amplitude $\delta w_0\neq 0$, today's cosmic-$Z$ value $Z_t$, any history $Z_{\mathrm{hist}}:\mathbb{R}\to\mathbb{R}$, and any redshift $z$, $$\frac{\delta w(\delta w_0,Z_t,Z_{\mathrm{hist}},z)}{\delta w(\delta w_0,Z_t,Z_{\mathrm{hist}},0)}=\frac{Z_{\mathrm{hist}}(z)/Z_t}{Z_{\mathrm{hist}}(0)/Z_t},$$ where $\delta w$ is the BIT equation-of-state deviation $w(z)+1$.
background
The module treats the honest reduction of U5 (dark-energy shape). The BIT mechanism supplies the equation of state $w(z)=-1+\delta w_0\cdot Z(z)/Z_{\mathrm{today}}$, with $Z(z)$ the integrated cosmic $Z$-complexity and $Z_{\mathrm{today}}=Z(0)$.
Locally, bitKernel is the BIT $w(z)$ and bitDeviation is $\delta w(z):=w(z)+1$. The upstream identity bitDeviation_eq states the closed form
$\delta w(z)=\delta w_0\cdot Z_{\mathrm{hist}}(z)/Z_t$
(proved by unfolding and ring). Boundary conditions forced by that formula: $\delta w(0)=\delta w_0$ today, and $\delta w\to 0$ as $Z\to 0$ (early universe recovers $\Lambda$CDM).
Shape reduction is the exact half of the module program: normalized $\delta w$ is identical to normalized $Z$-history, so deriving the dark-energy shape is exactly deriving $Z(z)$.
proof idea
Term-mode rewrite. Apply bitDeviation_eq at redshift $z$ and at redshift $0$, obtaining
$\delta w(z)=\delta w_0\cdot Z_{\mathrm{hist}}(z)/Z_t$ and $\delta w(0)=\delta w_0\cdot Z_{\mathrm{hist}}(0)/Z_t$.
The ratio is then a pure cancellation of the common nonzero factor $\delta w_0$ via mul_div_mul_left (hypothesis $\delta w_0\neq 0$). No further structure on $Z_{\mathrm{hist}}$ is used.
why it matters
This is result (1) of the Cosmic Z-History module: the exact shape reduction that turns U5 from a posited $1/(1+z)$ into a localized derivation problem. Downstream it is packaged into cosmicZShapeCert as the field shape_is_z_history, alongside the deviation formula, today's value, and the conditional linear-accumulation theorem.
Together with the conditional result that linear-in-scale-factor accumulation $Z(z)=Z_{\mathrm{today}}/(1+z)$ forces the canonical kernel $\delta w(z)=\delta w_0/(1+z)$, it isolates the single remaining freedom of U5: why $Z$ accumulates linearly in the scale factor $a$ rather than in cosmic time or $a^p$. No new axioms; the reduction itself is unconditional under BIT.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.