CosmicZScaleLawCert
plain-language theorem explainer
Certificate bundling four consequences of the scale-affine ledger law: the normalized cosmic-Z fraction equals the scale factor, the redshift history is linear in a, and the BIT dark-energy deviation and kernel take the canonical forms δw₀/(1+z) and −1+δw₀/(1+z). Cosmologists tracking the RS dark-energy shape cite this package. It is a pure structure; inhabitance is discharged by four named forcing lemmas.
Claim. A certificate asserting that every scale-affine normalized cosmic-$Z$ law $Z_{\mathrm{frac}}$ satisfies $Z_{\mathrm{frac}}(a)=a$ for all scale factors $a$; that the induced history equals the linear history $Z(z)=Z_{\mathrm{today}}/(1+z)$; and that, whenever $Z_{\mathrm{today}}\neq 0$ and $1+z\neq 0$, the BIT deviation and kernel are $\delta w(z)=\delta w_0/(1+z)$ and $w(z)=-1+\delta w_0/(1+z)$.
background
The module closes the last shape residue in the RS dark-energy plan. Under the BIT kernel, the equation-of-state deviation is $\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 normalized history should be the scale factor $a(z)=1/(1+z)$.
A scale-affine law is a normalized $Z$-fraction $Z_{\mathrm{frac}}$ with endpoints $Z_{\mathrm{frac}}(0)=0$ and $Z_{\mathrm{frac}}(1)=1$ that preserves convex interpolation along the cosmic interval from early zero-complexity ($a=0$) to today ($a=1$). That is the no-extra-coordinate condition: equal scale-factor fractions carry equal ledger fractions until a new physical input is supplied.
Upstream, bitKernel is $w(z)=-1+\delta w_0\cdot Z(z)/Z_t$ and bitDeviation is $\delta w=w+1$; linearZ is the reference history $Z_t/(1+z)$. The induced history from a scale-affine law is $Z_t\cdot Z_{\mathrm{frac}}(a(z))$.
proof idea
No proof body: this is a structure definition packaging four propositions as fields. Inhabitance is separate. The four fields are exactly the statements of the sibling forcing lemmas (identity of $Z_{\mathrm{frac}}$, equality of the induced history with linear-$a$ history, and the two canonical BIT shapes). Downstream, the inhabited certificate fills each field by applying the corresponding lemma.
why it matters
This certificate is the named packaging of the module's main claim: under the scale-affine ledger admissibility law, the normalized cosmic-$Z$ history is forced to be the scale factor, and the BIT kernel therefore forces the canonical dark-energy shape $\delta w(z)=\delta w_0/(1+z)$. The sole downstream consumer is the inhabited instance, which wires the four forcing lemmas into the four fields and records that the certificate is realized with zero sorry and zero new axiom.
In the broader RS cosmology stack this is the sharp admissibility cut that removes curve-fitting freedom from the dark-energy equation of state once the BIT kernel and the early-to-today ledger endpoints are fixed. It does not itself derive $\delta w_0$ or the BIT kernel; it only forces the $z$-shape once those are given.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.