linearZ_today

This module treats the cosmic Z-complexity history $Z(z)$ that enters the BIT dark-energy equation of state $w(z)=-1+\delta w\cdot Z(z)/Z_{\mathrm{today}}$. Under the BIT kernel the normalized equation-of-state deviation equals the normalized Z-history, so deriving the dark-energy shape reduces exactly to deriving $Z(z)$.

The linear-in-scale-factor candidate is defined by $Z_{\mathrm{lin}}(Z_t,z)=Z_t/(1+z)$, i.e. $Z(z)=Z_{\mathrm{today}}\cdot a(z)$. It is the unique monotone positive history that, under the linear-accumulation hypothesis, forces the canonical kernel $\delta w(z)=\delta w_0/(1+z)$. Boundary values at $z=0$ and in the deep past are forced by the shape-reduction theorem.

One-line tactic proof: unfold the definition $Z_{\mathrm{lin}}(Z_t,z)=Z_t/(1+z)$, specialize to $z=0$, and apply norm_num to obtain $Z_t/(1+0)=Z_t$. No external lemmas are required beyond the definition itself.

The present-day boundary $\delta w(0)=\delta w_0$ in the module's shape-reduction story requires $Z(0)=Z_{\mathrm{today}}$. This lemma discharges that identity for the linear-in-$a$ history, so the conditional derivation of the canonical kernel can quote a clean normalization rather than re-expanding the definition inline.

It sits inside the honest residue of U5: shape reduction is proved outright; the canonical $1/(1+z)$ form is proved only conditional on linear scale-factor accumulation. The lemma does not close that hypothesis; it only pins the $z=0$ endpoint once the hypothesis is assumed. No downstream theorems currently depend on it in the graph, but sibling positivity and antitonicity facts for the same history use the same normalization.