redshift_ratio
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.