scaleAffine_forces_identity
plain-language theorem explainer
Under the scale-affine ledger law, the normalized cosmic-Z fraction equals the scale factor itself at every real a. Cosmologists closing the dark-energy shape residue cite this uniqueness. The argument is a one-line simplification of the affine interpolation identity at the early-zero and today-one endpoints.
Claim. Let $Z_{\mathrm{frac}}$ be any normalized cosmic-$Z$ history that is scale-affine between the early endpoint $a=0$ and today $a=1$ (so $Z_{\mathrm{frac}}(0)=0$, $Z_{\mathrm{frac}}(1)=1$, and $Z_{\mathrm{frac}}$ preserves convex interpolation along that interval). Then $Z_{\mathrm{frac}}(a)=a$ for every real scale factor $a$.
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 normalized history should be the cosmological scale factor $a(z)=1/(1+z)$.
A scale-affine $Z$-law is a normalized history $Z_{\mathrm{frac}}:\mathbb{R}\to\mathbb{R}$ with early endpoint $Z_{\mathrm{frac}}(0)=0$, today endpoint $Z_{\mathrm{frac}}(1)=1$, and the ledger-uniform interpolation rule: equal scale-factor fractions carry equal recognition-ledger fractions between those endpoints. That rule is the no-extra-coordinate condition: the ledger does not select an intermediate scale-factor coordinate until a further physical input is supplied.
The present theorem is the uniqueness half of that admissibility package: scale-affinity alone forces $Z_{\mathrm{frac}}$ to be the identity on scale factor.
proof idea
Term-mode, essentially a one-line wrapper. Instantiate the structure field scale_affine_from_early_to_today at the given $a$. The left-hand side collapses because $(1-a)\cdot 0+a\cdot 1=a$, so one obtains $Z_{\mathrm{frac}}(a)$ on the left. The right-hand side is $(1-a),Z_{\mathrm{frac}}(0)+a,Z_{\mathrm{frac}}(1)$. Rewrite with the endpoint fields $Z_{\mathrm{frac}}(0)=0$ and $Z_{\mathrm{frac}}(1)=1$; simpa finishes $Z_{\mathrm{frac}}(a)=a$.
why it matters
This is the uniqueness engine for the cosmic-$Z$ scale law. Downstream, scaleAffine_forces_linearZ rewrites the redshift history as the linear-in-scale form $Z(z)=Z_{\mathrm{today}}/(1+z)$, and the certificate cosmicZScaleLawCert packages identity, linear redshift, canonical deviation, and canonical kernel as an inhabited witness. DarkEnergyScaleAffinityDerivation also routes its no-hidden-scale-coordinate condition through this theorem via a structure coercion.
In the module narrative, once identity is forced, the BIT kernel yields $\delta w(z)=\delta w_0/(1+z)$ with no curve fit: the shape is the statement that the ledger is uniform in the scale-factor coordinate. That tightens the last free shape residue in the dark-energy plan under the named admissibility law, with zero sorry and no new axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.