redshift_ratio
Consecutive boundary redshifts satisfy boundaryRedshift(k+1)/boundaryRedshift(k) = phi for each natural number k. Recognition Science cosmologists cite this to anchor the geometric progression of the five reionization epochs. The proof is a direct algebraic reduction that unfolds the power definition of boundaryRedshift, applies the successor exponent rule, and normalizes with ring.
claimFor every natural number $k$, the ratio of the boundary redshift at rung $k+1$ to the boundary redshift at rung $k$ equals the golden ratio phi, where the boundary redshift at rung $m$ is defined to be phi to the power $m$.
background
The module models five canonical epochs of reionization (configDim D = 5): cosmic dark ages (z > 20), first stars (z ~ 20), galaxy formation (z ~ 15), bulk reionization (z ~ 7-10), and saturation (z < 6). Each boundary redshift occupies one rung on a geometric ladder. The upstream definition supplies boundaryRedshift(k : ℕ) : ℝ := phi ^ k, which is the explicit power form used throughout.
proof idea
The term proof unfolds boundaryRedshift, invokes pow_pos phi_pos k to secure positivity of phi^k, rewrites the division via div_eq_iff, applies pow_succ to the numerator, and closes with ring.
why it matters in Recognition Science
This supplies the phi_ratio field inside the downstream reionizationCert record that assembles the full ReionizationCert. It confirms the self-similar phi scaling of boundary redshifts across the reionization epochs, consistent with the Recognition Science forcing chain in which phi is the self-similar fixed point. No open questions are addressed.
scope and limits
- Does not compute numerical redshift values for any epoch.
- Does not derive the five epoch boundaries from first principles.
- Does not incorporate observational constraints on reionization timing.
- Does not extend the ratio result to other cosmological observables.
Lean usage
example (k : ℕ) : boundaryRedshift (k + 1) / boundaryRedshift k = phi := redshift_ratio kformal statement (Lean)
32theorem redshift_ratio (k : ℕ) :
33 boundaryRedshift (k + 1) / boundaryRedshift k = phi := by
proof body
Term-mode proof.
34 unfold boundaryRedshift
35 have hpos : (0 : ℝ) < phi ^ k := pow_pos phi_pos k
36 rw [div_eq_iff hpos.ne', pow_succ]
37 ring
38