Pith. sign in
module module moderate

IndisputableMonolith.Cosmology.InflationReheatTemperature

show as:
view Lean formalization →

The module supplies the J-band certification for the inflation reheat temperature in Recognition Science cosmology. Researchers deriving post-inflation scales from the phi-ladder cite it to anchor the temperature to RS-native units. The module applies the six-clause J-cost template from CanonicalJBand to establish matched-zero and nonnegativity for the reheat ratio.

claimThe reheat temperature $T_{ m rh}$ satisfies the canonical J-band conditions $J(T_{ m rh} au_0) = 0$ and $J(x) \geq 0$ for $x > 0$, where $ au_0$ is the RS time quantum.

background

The module sits in the cosmology domain of Recognition Science, which derives all scales from the J-functional equation and the T0-T8 forcing chain. It imports CanonicalJBand, whose doc-comment states that the six-clause J-cost-on-ratio template is used across the master cert chain for domain certifications, and Constants, which defines the RS time quantum $ au_0 = 1$ tick.

No new mathematical objects are introduced. The module simply instantiates the reusable template for the specific case of the inflation reheat temperature.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds the master cert chain for B-tier whole-science openings described in the CanonicalJBand documentation. It supplies the inflation reheat temperature slot among the domain certs in the Recognition Science framework.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (2)