InflationReheatCert
plain-language theorem explainer
InflationReheatCert packages a CanonicalCert to certify the reheating temperature scale in RS-native cosmology. A researcher tracing the thermal history from the J-cost inflaton potential would cite it to locate T_reh at the φ-ladder position -39/2. The declaration is a one-line structure definition that reuses the upstream six-clause J-band certificate as its sole field.
Claim. The reheating certificate is the structure whose base field holds a canonical J-band certificate satisfying $J(1)=0$, $J(x)=J(1/x)$ for $x≠0$, $J(φ)>0$ with $0.11<J(φ)<0.13$, and $J(φ^{-2})>0$.
background
The module derives the reheating temperature from the inflationary epoch and inflaton potential in Recognition Science. In native units the temperature is given by $T_{reh}=(E_{coh}/ℓ_P)·φ^{-N_e/2}$ with $N_e=44$, which simplifies to $φ^{-39/2}≈10^{-12}$. This places the scale between rungs 19 and 20 on the φ-ladder, just below the abiogenesis threshold $Z_{life}=φ^{19}$ (MODULE_DOC). The upstream CanonicalCert supplies the six properties of the J-function required for all domain certificates: $J(1)=0$, invariance under $x↔1/x$, $J(φ)>0$ inside the band (0.11,0.13), and $J(φ^{-2})>0$.
proof idea
The declaration is a one-line structure definition that introduces InflationReheatCert with a single field base of type CanonicalCert.
why it matters
It supplies the certificate required by the downstream inflationReheatCert definition, thereby embedding the reheating scale into the cosmology module. The placement at rung -39/2 realizes the prediction that reheating occurs just below the life rung $φ^{19}$, linking the J-uniqueness theorem (T5) and the phi fixed point (T6) to the mass ladder and Berry creation threshold. This step closes the structural account of the transition from inflation to the standard thermal history.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.