linearZ_antitone
plain-language theorem explainer
The linear scale-factor cosmic-Z history is non-increasing in redshift: less Z is accumulated at earlier epochs. For nonnegative Z_today and 0 ≤ z1 ≤ z2 one has Z_lin(z2) ≤ Z_lin(z1). Cosmologists reducing the BIT dark-energy shape (U5) cite this monotonicity. Proof unfolds the closed form, checks positive denominators, and applies generalized congruence.
Claim. Let $Z_t \ge 0$ and $0 \le z_1 \le z_2$. Writing $Z_{\mathrm{lin}}(Z_t,z) := Z_t/(1+z)$ for the linear-in-scale-factor cosmic-Z history, one has $Z_{\mathrm{lin}}(Z_t,z_2) \le Z_{\mathrm{lin}}(Z_t,z_1)$.
background
This module treats cosmic Z-history as the remaining degree of freedom in the BIT dark-energy equation of state. Under the BIT kernel one has $w(z) = -1 + \delta w \cdot Z(z)/Z_{\mathrm{today}}$, so the normalized deviation equals the normalized Z-history (shape reduction). Deriving the dark-energy shape is therefore exactly the problem of deriving $Z(z)$.
The linear-accumulation premise takes $Z(z) = Z_{\mathrm{today}} \cdot a(z) = Z_{\mathrm{today}}/(1+z)$ on $z \ge 0$. The declaration linearZ is that closed form. Physically one expects less integrated Z-complexity at higher redshift (earlier epochs), so the history should be non-increasing in $z$. The present lemma records that elementary fact for nonnegative $Z_{\mathrm{today}}$.
Boundary conditions forced by the setup are $Z(0) = Z_{\mathrm{today}}$ and $Z \to 0$ in the deep past, recovering $\Lambda$CDM early.
proof idea
Unfold the definition $Z_{\mathrm{lin}}(Z_t,z) = Z_t/(1+z)$. From $z_1,z_2 \ge 0$ obtain $1+z_1 > 0$ and $1+z_2 > 0$ by linear arithmetic. Generalized congruence (gcongr) then yields the reciprocal inequality in the denominators and multiplies through by the nonnegative numerator $Z_t$, giving $Z_t/(1+z_2) \le Z_t/(1+z_1)$. No external lemmas are required.
why it matters
Monotonicity is part of the honest residue of U5 in Recognition Science cosmology. The module proves that under BIT the dark-energy shape problem reduces exactly to the cosmic-Z accumulation history, and that linear-in-$a$ accumulation forces the canonical kernel $\delta w(z) = \delta w_0/(1+z)$. Antitonicity confirms that this history places less Z at earlier epochs, matching the required early-universe recovery of $\Lambda$CDM.
Sibling results include positivity of the linear history, its value today, and the conditional theorem that linear accumulation forces the canonical BIT kernel. The remaining open question, stated in the module, is why accumulation is linear in the scale factor rather than in cosmic time or $a^p$; this lemma does not address that premise, only its elementary order properties.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.