reciprocal_history_kernel
plain-language theorem explainer
For any reciprocal cosmic-Z history Z(z) = Z_today / g(z), the BIT equation-of-state deviation collapses to δw(z) = δw₀ / g(z). Cosmologists reconstructing dark-energy shape from the BIT kernel cite this to read the accumulation law g directly off w(z). The proof is a short algebraic reduction from the general deviation identity after substituting the reciprocal form.
Claim. For all real $\delta w_0$, $Z_t$, $z$ and any $g:\mathbb{R}\to\mathbb{R}$, if $Z_t\neq 0$, then the BIT deviation of the reciprocal history $Z(z)=Z_t/g(z)$ equals $\delta w_0/g(z)$. In symbols: $\delta w(z)=\delta w_0/g(z)$.
background
Under the BIT mechanism the dark-energy equation of state is $w(z)=-1+\delta w\cdot Z(z)/Z_{\mathrm{today}}$, with $Z(z)$ the integrated cosmic Z-complexity. The module defines the deviation $\delta w(z)=w(z)+1$ via bitDeviation, and the identity bitDeviation_eq states that this equals $\delta w_0\cdot Z(z)/Z_t$ for an arbitrary history.
Shape reduction then says deriving the dark-energy shape is exactly deriving the normalized Z-history: no more, no less. Reciprocal histories are those written $Z(z)=Z_t/g(z)$. The canonical kernel takes $g(z)=1+z$ (linear in scale factor $a$); a power law $g(z)=(1+z)^p$ yields $\delta w(z)=\delta w_0/(1+z)^p$, so the shape index $p$ is read straight off a $w(z)$ reconstruction.
The local setting is the honest reduction of U5: shape reduction is unconditional; the canonical $1/(1+z)$ form is conditional on linear-in-$a$ accumulation.
proof idea
Rewrite with bitDeviation_eq, which expands the left-hand side to $\delta w_0\cdot(Z_{\mathrm{hist}}(z)/Z_t)$. Substitute the reciprocal history $Z_{\mathrm{hist}}=\lambda z.,Z_t/g(z)$ to obtain $\delta w_0\cdot(Z_t/g(z)/Z_t)$. Nested-division and commutativity rewrites, followed by div_self on the hypothesis $Z_t\neq 0$ and mul_one_div, cancel $Z_t$ and leave $\delta w_0/g(z)$. Pure real-field algebra; no cosmology-specific lemmas beyond the deviation identity.
why it matters
The theorem is the precise statement that U5's residue is exactly the choice of accumulation law $g$: once $g$ is fixed, every downstream dark-energy observable is fixed. The module certificate records that the dark-energy shape is the cosmic-Z history and that the canonical $1/(1+z)$ is forced by linear-in-$a$ accumulation; the only residual freedom is that law itself.
Sibling results specialize the picture: shape_reduction equates normalized deviation to normalized Z-history; linear_accumulation_forces_canonical_kernel recovers $\delta w(z)=\delta w_0/(1+z)$ under the linear-scale-factor hypothesis. No downstream uses are wired yet, but the result sits at the hinge between the unconditional shape reduction and the still-open question why accumulation is linear in $a$ rather than in cosmic time or $a^p$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.