scaleFactor_le_one
plain-language theorem explainer
For redshift $z\ge 0$, the cosmological scale factor $a(z)=1/(1+z)$ never exceeds unity. Anyone deriving the RS dark-energy shape $\delta w(z)=\delta w_0\,a(z)$ from the scale-affine ledger law needs this elementary bound. The proof unfolds the definition, checks $1+z>0$, and applies the division inequality with linarith.
Claim. For every real redshift $z\ge 0$, the cosmological scale factor $a(z)=1/(1+z)$ satisfies $a(z)\le 1$.
background
In standard FLRW cosmology the scale factor is normalized so that $a=1$ today and $a\to 0$ in the early universe; redshift is related by $a=1/(1+z)$. This module adopts exactly that definition as scaleFactor.
The surrounding development starts from the BIT-kernel identity $\delta w(z)=\delta w_0\cdot Z(z)/Z_{\mathrm{today}}$ already proved in CosmicZHistory. The remaining shape residue is why the normalized cosmic-$Z$ history should equal the scale factor itself. The module's answer is the scale-affine ledger law: equal scale-factor fractions carry equal recognition-ledger fractions between the early endpoint $a=0$ and today $a=1$.
Under that admissibility condition the normalized $Z$-history is forced to be $a$, yielding $\delta w(z)=\delta w_0/(1+z)$. The present lemma is the elementary comparison $a(z)\le 1$ on the physical half-line $z\ge 0$, used to keep the normalized history inside the unit interval.
proof idea
One short tactic block. Unfold $a(z)=1/(1+z)$. From the hypothesis $z\ge 0$ obtain $1+z>0$ by linarith. Rewrite the goal with the Mathlib lemma that $x/y\le 1$ iff $x\le y$ when $y>0$, then finish by linarith on $1\le 1+z$.
why it matters
The lemma sits in the Cosmic Z Scale Law module, which closes the last shape residue of the dark-energy plan: once the scale-affine ledger law is admitted, the BIT kernel plus $Z/Z_{\mathrm{today}}=a$ produces $\delta w(z)=\delta w_0/(1+z)$ with no free function. The bound $a\le 1$ for $z\ge 0$ keeps the normalized history inside the convex interval between the early zero-complexity endpoint and today, which is precisely the geometric content of the scale-affine condition stated in the module doc.
No downstream theorem currently cites it (used-by is empty), so it functions as local infrastructure for the sibling results that force the identity map, the linear-$Z$ law, and the canonical kernel. It does not touch the forcing chain T0–T8 or the RCL directly; it is pure FLRW bookkeeping inside the RS cosmology layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.