Pith. sign in
module module high

IndisputableMonolith.Cosmology.CosmicInflationFromJCost

show as:
view Lean formalization →

CosmicInflationFromJCost certifies that inflation terminates once J-cost crosses the canonical threshold from the reusable J-band template. Recognition Science cosmologists cite it to tie the J-functional directly to early-universe termination. The module assembles its content from the imported six-clause template and sibling definitions for the model and its certification.

claimInflation ends when J-cost on the relevant ratio crosses the canonical threshold: $J(r) \ge \theta_{\rm canon}$ with $\theta_{\rm canon}$ fixed by the band template.

background

The module sits in the Cosmology domain and imports CanonicalJBand. Its doc-comment states that the six-clause J-cost-on-ratio template is used across the master cert chain for B-tier openings and domain certs; each such cert proves matched-zero $J(1)=0$ and nonneg $J(x)\ge 0$ for $x>0$.

Recognition Science defines $J(x)=(x+x^{-1})/2-1$ and applies it to cosmology via the forcing chain landmarks T5 (J-uniqueness) and T6 (phi fixed point). The module therefore inherits the reusable template to formalize inflation termination.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies CosmicInflationCert and inflation_ends_at_threshold to the master cert chain referenced in the CanonicalJBand doc-comment. It fills the cosmology slot that links J-cost crossing to inflation end, advancing the T5-T8 chain into the early universe.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (5)