scaleAffine_forces_linearZ
plain-language theorem explainer
Under any scale-affine ledger law, the cosmic-Z history generated from today's value equals the linear-in-scale-factor history Z(z)=Z_today/(1+z). Cosmologists deriving the BIT dark-energy shape from Recognition admissibility cite this uniqueness step. The proof unfolds the generated history, applies the identity forcing of the normalized Z-fraction, and simplifies the algebra.
Claim. For any today's cosmic-Z value $Z_t\in\mathbb{R}$, any scale-affine law (normalized $Z$-fraction with endpoints $Z_{\mathrm{frac}}(0)=0$, $Z_{\mathrm{frac}}(1)=1$, and convex interpolation in the scale factor), and any redshift $z$, the history $Z_t\cdot Z_{\mathrm{frac}}(a(z))$ equals $Z_t/(1+z)$, where $a(z)=1/(1+z)$.
background
The module closes the last shape residue in the dark-energy plan. CosmicZHistory already shows that under the BIT kernel the 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 cosmological scale factor $a(z)=1/(1+z)$.
Scale-affine ledger law is the admissibility condition: 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. Concretely, a structure ScaleAffineZLaw packages a map $Z_{\mathrm{frac}}$ with $Z_{\mathrm{frac}}(0)=0$, $Z_{\mathrm{frac}}(1)=1$, and the convex-interpolation identity $Z_{\mathrm{frac}}((1-a)\cdot 0+a\cdot 1)=(1-a)Z_{\mathrm{frac}}(0)+a,Z_{\mathrm{frac}}(1)$. The generated history is $Z_{\mathrm{from,scale}}(Z_t,\mathrm{law},z)=Z_t\cdot Z_{\mathrm{frac}}(a(z))$.
Upstream, scaleAffine_forces_identity already proves $Z_{\mathrm{frac}}(a)=a$ for every scale factor $a$. The linear reference history is defined by $\mathrm{linearZ}(Z_t,z)=Z_t/(1+z)$.
proof idea
Short algebraic reduction. Unfold the three definitions: the generated history $Z_t\cdot Z_{\mathrm{frac}}(a(z))$, the linear target $Z_t/(1+z)$, and $a(z)=1/(1+z)$. Rewrite with scaleAffine_forces_identity, which replaces $Z_{\mathrm{frac}}(a)$ by $a$, leaving $Z_t\cdot a(z)=Z_t\cdot(1/(1+z))$. Finish with mul_one_div to match the linear form.
why it matters
This is the redshift-history half of the scale-law certificate: cosmicZScaleLawCert packages it as redshift_history_forced alongside identity forcing, canonical deviation, and canonical kernel. Immediately downstream, scaleAffine_forces_canonical_deviation funexts this equality to obtain $\delta w(z)=\delta w_0/(1+z)$ under the BIT kernel, which is the module's stated endpoint for the dark-energy shape.
In the broader derivation chain, noHidden_forces_linearZ reduces the no-hidden-scale-coordinate hypothesis to a scale-affine law and then applies this theorem, so the linear history is forced once intermediate scale coordinates are forbidden. That is the Recognition reading of "no new physical input selects a preferred intermediate $a$": the ledger stays uniform in the scale-factor coordinate from $a=0$ to $a=1$, uniquely fixing $Z/Z_{\mathrm{today}}=a$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.