scaleFactor

In standard FLRW cosmology the scale factor $a$ is normalized so that $a=1$ today and redshift obeys $1+z=1/a$, hence $a(z)=1/(1+z)$. The present module works inside that convention.

CosmicZHistory already shows that, under the BIT kernel, the dark-energy shape residue satisfies $\delta w(z)=\delta w_0\cdot Z(z)/Z_{\mathrm{today}}$. The remaining question is why the normalized cosmic-Z history should equal the scale factor. The module answers by imposing a scale-affine ledger law: along the cosmic interval from the early endpoint $a=0$ to today $a=1$, equal scale-factor fractions carry equal recognition-ledger fractions.

The two upstream scale names in the dependency graph are unrelated (a $\phi$-power ladder and a coefficient rescaling of virtue actions). They do not define this cosmological $a(z)$.

Pure definition: the right-hand side is the arithmetic expression $1/(1+z)$. No lemmas are applied and no tactics run. Downstream lemmas unfold this definition and then use elementary real arithmetic (norm_num, linarith, positivity, div_le_one).

This is the coordinate map that turns the scale-affine ledger admissibility condition into a concrete redshift law. ZfromScaleLaw builds the cosmic-Z history by evaluating the law's normalized fraction on $a(z)$. The theorem scaleAffine_forces_linearZ then shows that any such law forces $Z(z)=Z_{\mathrm{today}}/(1+z)$, i.e. the linear-in-scale-factor history. Companion facts record $a(0)=1$, positivity, and $a(z)\le 1$ for $z\ge 0$.

Together these close the last shape residue in the dark-energy plan: under the named admissibility law the BIT kernel yields $\delta w(z)=\delta w_0/(1+z)$. The status is theorem conditional on that law, with zero sorry and no new axioms.