cosmicZScaleLawCert
plain-language theorem explainer
Any scale-affine ledger law forces the normalized cosmic-Z fraction to equal the scale factor $a$, hence $Z(z)=Z_{\mathrm{today}}/(1+z)$ and the canonical BIT dark-energy shape $\delta w(z)=\delta w_0/(1+z)$. Cosmologists closing the RS dark-energy plan cite this certificate. It is a pure structure inhabitant packing four already-proved forcing lemmas.
Claim. There is an inhabited certificate asserting that every scale-affine Z-law forces four conclusions: the normalized Z-fraction equals the scale factor $a$; the redshift history equals the linear law $Z(z)=Z_{\mathrm{today}}/(1+z)$; the BIT deviation equals $\delta w(z)=\delta w_0/(1+z)$ (when $Z_{\mathrm{today}}\neq 0$ and $1+z\neq 0$); and the equation of state is the canonical kernel $w(z)=-1+\delta w_0/(1+z)$.
background
The module closes the last shape residue in the RS dark-energy plan. Upstream, CosmicZHistory shows that under the BIT kernel the dark-energy deviation tracks the normalized cosmic-Z history: $\delta w(z)=\delta w_0\cdot Z(z)/Z_{\mathrm{today}}$. The open question is why that normalized history should be the FLRW scale factor $a(z)=1/(1+z)$.
The answer is the scale-affine ledger admissibility law: along the cosmic interval from the early zero-complexity endpoint $a=0$ to today $a=1$, equal scale-factor fractions carry equal recognition-ledger fractions. Formally, the normalized Z-fraction preserves convex interpolation between those endpoints, so no intermediate scale coordinate is preferred by the ledger without a new physical input.
A ScaleAffineZLaw packages that convexity condition together with the endpoint normalizations. The certificate structure records the four forced identities that follow from any such law.
proof idea
One-line structure inhabitant. Each field of the certificate is filled by the corresponding forcing theorem already proved in the module: identity of the normalized Z-fraction by scaleAffine_forces_identity (endpoint convexity plus early-zero and today-one); linear redshift history by scaleAffine_forces_linearZ (unfold and rewrite via the identity); canonical BIT deviation by scaleAffine_forces_canonical_deviation (function extensionality to the linear history); and the canonical kernel $w=-1+\delta w$ by scaleAffine_forces_canonical_kernel (linarith on the deviation identity).
why it matters
This certificate is the module's public packing of the scale-law forcing chain. The module doc states the status explicitly: theorem conditional on the named scale-affine ledger admissibility law, zero sorry, zero new axiom. Under that law the BIT kernel yields the unique dark-energy shape $\delta w(z)=\delta w_0/(1+z)$, so the last free shape residue in the dark-energy plan is discharged.
No downstream consumers are wired yet (used_by is empty); the declaration exists as the citable endpoint of the CosmicZScaleLaw development. It sits downstream of CosmicZHistory's BIT tracking result and upstream of any observational comparison that would test $\delta w\propto 1/(1+z)$. Framework-wise it is a cosmology-side uniqueness statement, not a T0–T8 forcing step, but it inherits the same style: an admissibility law with no free intermediate coordinate forces a unique history.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.