ZfromScaleLaw
plain-language theorem explainer
Cosmic-Z history generated from a scale-affine ledger law: today's Z times the law's normalized fraction at the scale factor a(z)=1/(1+z). Cited by anyone forcing the dark-energy shape δw(z)=δw₀/(1+z) from scale-affinity. Pure definition: one product, no proof content.
Claim. Given today's cosmic-$Z$ value $Z_t\in\mathbb{R}$, a scale-affine law with normalized fraction $Z_{\mathrm{frac}}:\mathbb{R}\to\mathbb{R}$, and redshift $z$, define the generated history by $Z(z)=Z_t\cdot Z_{\mathrm{frac}}\bigl(1/(1+z)\bigr)$.
background
The module closes the last shape residue in the dark-energy plan. Under the BIT kernel, CosmicZHistory already gives $\delta w(z)=\delta w_0\cdot Z(z)/Z_{\mathrm{today}}$, so the dark-energy shape is exactly the normalized cosmic-$Z$ history. The open question is why that history should be the scale factor $a(z)=1/(1+z)$.
A scale-affine law packages a normalized fraction $Z_{\mathrm{frac}}$ with endpoints $Z_{\mathrm{frac}}(0)=0$, $Z_{\mathrm{frac}}(1)=1$, and the ledger-uniform interpolation condition: equal scale-factor fractions carry equal recognition-ledger fractions between the early zero-complexity endpoint and today. The cosmological scale factor is the usual $a(z)=1/(1+z)$.
This definition simply composes those pieces: evaluate the law's fraction at $a(z)$ and rescale by today's $Z$.
proof idea
Definition, not a theorem. Body is the single product $Z_t\cdot\mathrm{law}.Z_{\mathrm{frac}}(\mathrm{scaleFactor},z)$, with $\mathrm{scaleFactor},z=1/(1+z)$. No lemmas, no tactics.
why it matters
Bridge from abstract scale-affine laws to concrete redshift histories. Downstream, scaleAffine_forces_linearZ unfolds this definition and the identity $Z_{\mathrm{frac}}(a)=a$ to obtain $Z(z)=Z_t/(1+z)$. That feeds scaleAffine_forces_canonical_deviation and scaleAffine_forces_canonical_kernel, which force $\delta w(z)=\delta w_0/(1+z)$ and $w(z)=-1+\delta w_0/(1+z)$.
CosmicZScaleLawCert packages the whole chain: identity forced, and this history equals the linear-in-scale-factor history. DarkEnergyScaleAffinityDerivation reuses it under the no-hidden-scale-coordinate hypothesis, so the same object sits in both the conditional scale-law certificate and the no-hidden-coordinate derivation of the canonical dark-energy kernel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.