redshift_half_pos
plain-language theorem explainer
The master-plan reference redshift z = 1/2 is strictly positive. Cosmology proofs that evaluate the RS dark-energy equation of state at a fixed positive z cite this fact. The proof unfolds the definition 1/2 and discharges positivity by numerical normalization.
Claim. The fixed reference redshift $z = 1/2$ satisfies $0 < 1/2$.
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 discriminator: an RS placeholder linear in redshift, w_RS(z) = -1 + φ^{-44} · z, where φ^{-44} is the same rung-44 scale that appears in baryogenesis (η_B = φ^{-44}).
The constant redshift_half is the master-plan sample point z = 0.5, defined as the real number 1/2. Sibling lemmas use positive redshifts to show that the RS linear form strictly exceeds -1 and is therefore distinct from ΛCDM at any z > 0. Positivity of this sample point is the elementary arithmetic fact needed before those comparisons can fire at z = 1/2.
proof idea
One-line tactic proof: unfold the definition redshift_half := 1/2, then apply norm_num to obtain 0 < 1/2 in ℝ. No external lemmas are required beyond the definition itself.
why it matters
The module closes the structural half of Track 4.C: RS predicts a φ^{-44}-suppressed deviation of w(z) from -1, while the full FPT cosmic Z-aging dynamics remain future work. A concrete positive sample redshift is part of that scaffolding; without 0 < z one cannot instantiate the discriminator inequalities at a master-plan benchmark.
No downstream theorem currently lists this lemma as a dependency in the graph, but the sibling cluster (w_RS_linear_distinct_from_LCDM_at_positive_z, deviation magnitude, falsifier threshold) is exactly the place where a fixed positive z is consumed. The eight-tick and D = 3 forcing chain are upstream of φ itself; here only the rung-44 scale and the structural w(z) form are in play.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.