inflationReheatCert
plain-language theorem explainer
The declaration supplies a certificate instance for the post-inflation reheating temperature computed in RS-native units. Cosmologists using the Recognition framework cite it to locate the inflaton decay scale on the phi-ladder. The definition is a direct one-line construction that populates the base field of the required structure with the canonical certificate.
Claim. The reheating-temperature certificate is the structure whose sole field is the canonical certificate, yielding the energy scale $T_ {reh} = phi^{-39/2}$ in RS units.
background
The module treats the transition from inflation to the hot Big Bang. The inflationary epoch supplies $N_e = 44$ e-folds; the reheating temperature is the scale at which the inflaton decays and thermal equilibrium begins. In RS-native units this temperature is expressed as $T_{reh} = (E_{coh}/ell_P)cdot phi^{-N_e/2} = phi^{-39/2} approx 10^{-12}$, placing it at rung $-39/2$ on the phi-ladder, just below the abiogenesis rung $Z_{life} = phi^{19}$. The structure InflationReheatCert is defined to carry a single field of type CanonicalCert.
proof idea
The definition is a one-line wrapper that constructs the required structure by assigning the canonical certificate to its base field.
why it matters
This definition fixes the concrete reheating scale required by the cosmology module and thereby completes the structural claim that the temperature lies between rungs 19 and 20. It supplies the certificate referenced by downstream cosmology results and anchors the coincidence with the abiogenesis rung noted in the module documentation. The construction rests on the upstream CanonicalCert and the phi-ladder constants already established in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.