Pith. sign in
module module moderate

IndisputableMonolith.Cosmology.Inflation_Parameters5

show as:
view Lean formalization →

Module packaging Recognition Science inflation parameters via a domain cost functional and a positive canonical threshold, together with a certificate bundle that packages the numerical claims. Cosmologists working in the RS ladder would cite the certificate and the nonnegativity/positivity lemmas. The file is mostly definitions plus short algebraic positivity checks against the imported J-cost and constants.

claimDefines a domain cost $C_{\mathrm{dom}}$ on inflation-relevant scales, proves $C_{\mathrm{dom}}\ge 0$ and an evaluation identity, introduces a canonical threshold $\theta_*>0$, and packages these into an inhabited inflation-parameter certificate (parameter set 5).

background

Recognition Science treats cosmological epochs through the same cost functional that forces the forcing chain: the J-cost $J(x)=(x+x^{-1})/2-1$ from the Cost import, with RS-native units from Constants ($\tau_0=1$ tick, $\varphi$-ladder scales). Inflation parameters are not free fits; they are read off thresholds and domain costs on that ladder.

This module sits in the Cosmology domain and introduces a domain-level cost, its pointwise evaluation identity, nonnegativity, and a canonical positive threshold. Those pieces are then bundled into InflationParam5Cert, an inhabited certificate object meant to freeze the fifth parameter package for downstream cosmology claims.

Upstream material is thin: only Constants (time quantum $\tau_0$) and Cost are imported. No external inflation theorem is assumed; the local content is definitional plus elementary positivity.

proof idea

Definition-heavy module. Domain cost and the canonical threshold are introduced as defs; nonnegativity and positivity are short lemmas reducing to properties of the imported cost functional and constant arithmetic. The certificate structure is a Prop/record packaging those facts, discharged by an inhabitation witness (cert / cert_inhabited). No deep tactic proof or external analytic estimate appears at module scope.

why it matters in Recognition Science

Gives Cosmology a frozen, citable parameter-set-5 certificate built from RS cost and threshold data rather than phenomenological tuning. Downstream used-by edges are empty in the current graph, so this file is a leaf packaging layer: it standardizes the inflation-parameter interface for later spectral-index, e-fold, or energy-scale theorems once those land. It ties inflation numerics to the same J-cost and $\varphi$-native units used in the T5–T8 forcing chain, keeping cosmological claims inside the RS unit system ($c=1$, ladder masses, etc.).

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)