ScaleAffinityDerivationCert
plain-language theorem explainer
Certificate type packaging the derivation from the no-hidden-scale-coordinate gate to the scale-affine cosmic-Z law and the canonical dark-energy equation of state. Cosmologists citing the RS dark-energy shape (δw ∝ 1/(1+z)) use this bundle. It is a pure structure definition; the inhabited instance wires five already-proved forcing lemmas.
Claim. A derivation certificate consists of: (i) a map sending any no-hidden-scale-coordinate datum (normalized $Z$-fraction with endpoints $Z(0)=0$, $Z(1)=1$ and convex interpolation) to a scale-affine $Z$-law; (ii) the identity $Z_{\mathrm{frac}}(a)=a$; (iii) equality of the induced redshift history with the linear history $Z(z)=Z_{\mathrm{today}}/(1+z)$; (iv) the forced deviation $\delta w(z)=\delta w_0/(1+z)$; (v) the forced BIT kernel $w(z)=-1+\delta w_0/(1+z)$, under the usual nondegeneracy $Z_{\mathrm{today}}\neq 0$ and $1+z\neq 0$.
background
The module closes the remaining U5 residue in RS cosmology. Upstream, CosmicZScaleLaw already showed that a scale-affine normalized $Z$-history forces $Z(z)/Z_{\mathrm{today}}=a(z)$ and therefore $\delta w(z)=\delta w_0/(1+z)$. The open question was the origin of scale-affinity itself.
The lower gate is NoHiddenScaleCoordinate: once the early endpoint $a=0$ and today $a=1$ are fixed, the recognition ledger may not insert an extra preferred coordinate on the scale interval. Concretely, the normalized fraction $Z_{\mathrm{frac}}$ obeys endpoint convex interpolation, $Z_{\mathrm{frac}}((1-a)\cdot 0+a\cdot 1)=(1-a)Z_{\mathrm{frac}}(0)+a Z_{\mathrm{frac}}(1)$, together with $Z_{\mathrm{frac}}(0)=0$ and $Z_{\mathrm{frac}}(1)=1$.
BIT dark energy is written via the kernel $w(z)=-1+\delta w_0, Z(z)/Z_{\mathrm{today}}$ and deviation $\delta w=w+1$. The linear history is $Z(z)=Z_{\mathrm{today}}/(1+z)$. The shifted cost $H=J+1$ appears only as ambient algebra and is not used in the certificate fields.
proof idea
No proof body: this is a structure (certificate type) with five fields. Inhabitation is deferred to the sibling definition that fills each field by an already-proved lemma: conversion of the no-hidden gate into a scale-affine law; identity forcing $Z_{\mathrm{frac}}(a)=a$; equality of the induced history with the linear-$a$ history; and the two canonical BIT shapes for deviation and kernel. Each field is therefore a one-line wiring of a named forcing lemma rather than a fresh argument.
why it matters
This certificate is the honest theorem-layer closure of the dark-energy scale-affinity story. The module doc states the status explicitly: conditional on the named no-hidden-scale-coordinate admissibility gate, zero sorry, zero new axiom. The single downstream consumer is the inhabited instance that packages the five forcing maps into one object a parent development can cite.
In the RS chain this sits below the universal forcing layer (T0–T8, RCL, $\phi$). The remaining deeper problem, flagged in the module, is to derive the no-hidden-scale gate itself from that universal layer rather than postulating it as a cosmic-$Z$ admissibility condition. Until then, the certificate records the strongest available reduction: canonical $\delta w\propto 1/(1+z)$ is forced once no extra scale coordinate is allowed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.