redshift_one_pos
plain-language theorem explainer
The master-plan reference redshift z = 1 is strictly positive. Cosmology proofs that need a concrete positive-z test point (for the RS vs ΛCDM w(z) discriminator) cite this fact. The proof unfolds the definition to the literal 1 and discharges positivity by numeric normalization.
Claim. The fixed reference redshift $z=1$ satisfies $0 < z$.
background
Track 4.C of the quantum-gravity master plan asks for a falsifiable dark-energy equation of state w(z) that differs at sub-leading order from ΛCDM's constant w = -1. This module supplies the structural algebraic discriminator: an RS placeholder linear in redshift, w_RS_linear(z) := -1 + φ^{-44} · z, where the rung-44 scale φ^{-44} is the same forcing factor that appears in baryogenesis (η_B = φ^{-44}).
The definition redshift_one is the concrete master-plan sample point z = 1.0 (the real number 1). Downstream inequalities that claim the RS form strictly exceeds -1 at any positive redshift need that sample point to be positive; this lemma records that elementary fact.
The module is closed as a structural theorem (zero sorry, zero RS-internal axiom). The full FPT cosmic Z-aging dynamics that would fix the true z-dependence remain future work; only the linear placeholder and its positivity/discriminator package are shipped here.
proof idea
One-line tactic proof. Unfold redshift_one to the literal real 1, then apply norm_num to obtain 0 < 1. No lemmas beyond the definition and numeric normalization are required.
why it matters
The lemma is a tiny but necessary positivity witness inside the Track 4.C structural package. Sibling results (w_RS_linear_distinct_from_LCDM_at_positive_z, the absolute deviation bound, and the falsifier threshold built from φ^{-44}) all rely on having at least one certified positive redshift at which the RS form separates from ΛCDM's w = -1.
In the broader Recognition framework the same rung-44 scale links cosmology to baryogenesis on the φ-ladder. Establishing that the master-plan sample redshift is positive keeps the discriminator non-vacuous and ready for the master certificate darkEnergyWofZStructuralCert. No used_by edges are recorded yet; the lemma is infrastructure for those sibling inequalities rather than a parent theorem itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.