Pith. sign in
module module moderate

IndisputableMonolith.Cosmology.Reionization_Redshift_RS

show as:
view Lean formalization →

RS-native treatment of the cosmic reionization redshift via a domain cost and a canonical threshold built from the Recognition cost functional. Cosmologists comparing RS predictions to the observed reionization window would cite the certificate bundle. The module packages nonnegativity and positivity lemmas plus an inhabited certificate, not a full dynamical derivation.

claimDefine a domain cost $C$ on the reionization sector, a canonical threshold $\theta>0$, and a certificate asserting that the RS reionization redshift sits where $C$ meets $\theta$. The certificate is inhabited; $C$ is nonnegative and $\theta$ is positive.

background

Recognition Science fixes constants in RS-native units and measures mismatch with the J-cost $J(x)=(x+x^{-1})/2-1$ from the Cost layer. The Constants import supplies the fundamental tick $\tau_0=1$. Cosmic reionization is the epoch when the intergalactic medium becomes ionized; standard cosmology places it near $z\sim 6$--$10$.

This module stays inside that cost language. It introduces a domain cost for the reionization sector, equality and nonnegativity facts for that cost, and a positive canonical threshold against which the cost is compared. The local goal is a lightweight certificate object, not a full radiative-transfer model.

proof idea

Definition-heavy module with short supporting lemmas. Domain cost and the canonical threshold are introduced as defs; nonnegativity of the cost and positivity of the threshold are recorded as easy facts. The certificate type packages the comparison, and inhabitation is a one-line constructor application. No deep tactic scripts or forcing-chain steps appear here.

why it matters in Recognition Science

Places reionization on the same cost-and-threshold footing used elsewhere in the RS cosmology stack, so redshift predictions can be stated as certificate inhabitation rather than free parameters. Downstream use is not yet wired in this mirror (no used_by edges). It sits beside other cosmology certificates that convert RS ladder and cost structure into observational windows, without claiming the full T0--T8 forcing chain inside this file.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)