scaleFactor_pos
plain-language theorem explainer
For every redshift z ≥ 0 the cosmological scale factor a(z) = 1/(1+z) is strictly positive. Cosmologists and RS ledger arguments that normalize Z-history against a(z) cite this to keep denominators and convex weights well-defined. The proof unfolds the definition, obtains 1+z > 0 by linear arithmetic, and finishes with positivity.
Claim. For every real redshift $z \ge 0$, the cosmological scale factor $a(z) = 1/(1+z)$ satisfies $a(z) > 0$.
background
In standard FLRW cosmology the scale factor is tied to redshift by $a = 1/(1+z)$, with $a=1$ today and $a \to 0$ in the early universe. This module defines that map as scaleFactor and uses it as the geometric coordinate against which the cosmic-Z ledger is compared.
The module setting is the last shape residue in the dark-energy plan. Upstream, CosmicZHistory already gives $\delta w(z) = \delta w_0 \cdot Z(z)/Z_{\mathrm{today}}$ under the BIT kernel, so the dark-energy shape is exactly the normalized cosmic-Z history. The remaining question is why that normalized history should equal $a(z)$.
The answer is the scale-affine ledger law: 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. Positivity of $a(z)$ for $z \ge 0$ is the elementary analytic fact that keeps that interpolation and all later normalizations well-defined.
proof idea
One short tactic proof. Unfold the definition $a(z)=1/(1+z)$. From the hypothesis $z \ge 0$ obtain $1+z > 0$ by linarith. The Mathlib positivity tactic then concludes that the reciprocal is strictly positive.
why it matters
This is a supporting positivity lemma inside CosmicZScaleLaw, the module that forces the normalized Z-history to equal the scale factor under the scale-affine ledger admissibility law. With $a(z)>0$ in hand, later siblings can safely form ratios, convex combinations, and the identity $Z/Z_{\mathrm{today}}=a$, which under the BIT kernel yields $\delta w(z)=\delta w_0/(1+z)$.
No downstream consumers are recorded yet; the lemma exists so that the scale-affine forcing chain and the certification object CosmicZScaleLawCert can quote a clean positivity fact rather than re-proving $1+z>0$ inline. It does not itself touch T0–T8 or the RCL; it is pure real analysis in service of the cosmology ledger identification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.