scaleFactor_today
plain-language theorem explainer
At redshift zero the cosmological scale factor equals one, fixing today's normalization. Anyone citing the RS dark-energy shape or the scale-affine ledger law needs this anchor. The proof unfolds a(z)=1/(1+z) and evaluates at z=0 by arithmetic.
Claim. With the cosmological scale factor defined by $a(z)=1/(1+z)$ for real redshift $z$, one has $a(0)=1$.
background
The module Cosmic Z Scale Law closes a shape residue in the RS dark-energy plan. CosmicZHistory already 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 remaining question is why that normalized history should equal the usual scale factor $a(z)=1/(1+z)$.
The answer is framed as a scale-affine ledger admissibility law: along the cosmic interval from the early endpoint $a=0$ to today $a=1$, equal scale-factor fractions carry equal recognition-ledger fractions, so the normalized Z-fraction preserves convex interpolation between the endpoints. Under that law one obtains $Z/Z_{\mathrm{today}}=a$ and thus $\delta w(z)=\delta w_0/(1+z)$.
The local definition is the standard FLRW scale factor as a function of redshift, $a(z)=1/(1+z)$. Today means $z=0$, so the normalization $a(0)=1$ is the right-hand endpoint of that interval.
proof idea
One-line definitional evaluation. Unfold the definition $a(z)=1/(1+z)$, substitute $z=0$, and finish by numeric normalization: $1/(1+0)=1$. No external lemmas are required.
why it matters
This is the trivial but necessary normalization pin for the whole Cosmic Z Scale Law development. Sibling results (positivity and $a\le 1$ for $z\ge 0$, the scale-affine forcing theorems, and the certificate CosmicZScaleLawCert) all treat today as the unit endpoint $a=1$. Without $a(0)=1$, the statement that the normalized Z-history equals the scale factor would be off by a constant.
In the module narrative, the scale-affine ledger law forces $Z/Z_{\mathrm{today}}=a$ between the early zero-complexity endpoint and today; this theorem names the today endpoint. Downstream dark-energy shape claims that write $\delta w(z)=\delta w_0/(1+z)$ inherit that pin. No used_by edges are recorded yet; the declaration is infrastructure inside the module rather than a widely imported lemma.
It does not itself invoke the forcing chain T0–T8 or the RCL; it is pure FLRW bookkeeping inside the RS cosmology layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.