redshift_pos
The theorem establishes that the boundary redshift for every natural-number epoch index k is strictly positive. Cosmologists using Recognition Science to model reionization epochs cite it when confirming that the geometric ladder never crosses zero. The proof is a one-line wrapper that invokes the positivity of powers of a positive base.
claimFor every natural number $k$, the boundary redshift defined by $z_k = phi^k$ satisfies $z_k > 0$.
background
The module models reionization as five canonical epochs separated by boundaries on a geometric ladder, with each boundary redshift placed one rung higher than the last. The upstream definition supplies the explicit form boundary redshift of k equals phi to the power k, where phi is the self-similar fixed point fixed by the forcing chain. The module states that these five epochs correspond to configDim D equals 5 and lists the sequence: cosmic dark ages (z greater than 20), first stars (z approximately 20), galaxy formation (z approximately 15), bulk reionization (z approximately 7-10), and saturation (z less than 6).
proof idea
The proof is a one-line wrapper that applies the lemma pow_pos to the already-established positivity of phi and the natural number k.
why it matters in Recognition Science
The result is required by the downstream reionizationCert definition, which packages the epoch count, the phi ratio, and the positivity of all boundaries into a single certificate. It thereby closes the positivity requirement for the geometric ladder used in RS cosmology, consistent with the phi-ladder construction that descends from the eight-tick octave and the forcing chain steps T5 through T8.
scope and limits
- Does not assign numerical redshift values to any epoch.
- Does not derive the phi-ladder from the Recognition Composition Law.
- Does not incorporate observational data or constraints.
- Does not prove that five is the only possible number of epochs.
Lean usage
example (k : ℕ) : 0 < boundaryRedshift k := redshift_pos kformal statement (Lean)
39theorem redshift_pos (k : ℕ) : 0 < boundaryRedshift k :=
proof body
One-line wrapper that applies pow_pos.
40 pow_pos phi_pos k
41