bitKernel_early
plain-language theorem explainer
When cosmic Z-complexity vanishes at redshift z, the BIT dark-energy equation of state equals −1 for any amplitude and any present-day normalizer. Cosmologists reducing U5 (dark-energy shape) cite this as the early-universe boundary that recovers ΛCDM. The proof is a three-step unfold–rewrite–simp from the kernel definition.
Claim. For any amplitude $\delta w_0$, any present-day normalizer $Z_{\mathrm{today}}$, and any cosmic Z-history $Z_{\mathrm{hist}}$, if $Z_{\mathrm{hist}}(z)=0$ then the BIT equation of state satisfies $w(z)=-1$.
background
The module treats the BIT dark-energy equation of state
$$w(z)=-1+\delta w_0\cdot Z(z)/Z_{\mathrm{today}},$$
where $Z(z)$ is the integrated cosmic Z-complexity at redshift $z$ and $Z_{\mathrm{today}}=Z(0)$. The kernel is the real-valued map
$$\mathrm{bitKernel}(\delta w_0,Z_t,Z_{\mathrm{hist}},z)=-1+\delta w_0\cdot(Z_{\mathrm{hist}}(z)/Z_t).$$
Under the BIT mechanism the normalized equation-of-state deviation equals the normalized cosmic-Z history, so deriving the dark-energy shape is exactly deriving $Z(z)$. Boundary conditions are forced: today $\delta w(0)=\delta w_0$, and in the deep past $\delta w\to 0$ as $Z\to 0$, recovering pure $\Lambda$CDM.
proof idea
One-line algebraic evaluation. Unfold the kernel definition to $-1+\delta w_0\cdot(Z_{\mathrm{hist}}(z)/Z_t)$, substitute the hypothesis $Z_{\mathrm{hist}}(z)=0$, and simplify the product to zero. No external lemmas are required.
why it matters
This is the early-universe half of the forced boundary pair for the U5 shape reduction: $\delta w\to 0$ whenever $Z\to 0$, so $w\to-1$ and $\Lambda$CDM is recovered at high redshift. Together with the today evaluation it pins the endpoints of the normalized deviation curve that shape_reduction identifies with the normalized Z-history. The remaining open residue of U5 is not this boundary but why $Z$ accumulates linearly in the scale factor (the LinearScaleFactorAccumulation hypothesis that yields the canonical $1/(1+z)$ kernel). No downstream consumers are wired yet; the lemma stands as a local boundary fact inside CosmicZHistory.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.