Pith. sign in
module module moderate

IndisputableMonolith.Cosmology.HorizonProblem3_FromJCost

show as:
view Lean formalization →

Packages a J-cost reading of the cosmological horizon problem: a domain cost built from J, its nonnegativity, a strictly positive canonical threshold, and an inhabited certificate bundling those facts. Cosmologists in the RS stack cite the certificate when linking causal disconnection to cost. The module is mostly definitions plus short positivity lemmas imported from the Cost layer.

claimFrom the J-cost $J(x)=\frac{x+x^{-1}}{2}-1$, the module defines a domain cost on cosmological patches, proves that cost is nonnegative, fixes a canonical threshold that is strictly positive, and packages both facts into an inhabited certificate for the third RS horizon-problem statement.

background

The classical horizon problem asks why widely separated CMB patches share a common temperature despite lying outside each other's particle horizons in standard FLRW expansion. Recognition Science routes the question through the unique cost functional $J(x)=\cosh(\log x)-1$ forced at T5 of the unified forcing chain, rather than through an inflaton potential.

This module lives in the Cosmology domain. It imports RS constants (including the native time quantum) and the Cost layer, then introduces a domain-level cost assembled from $J$, an evaluation identity for that cost, nonnegativity, a canonical positive threshold, and a certificate type with an inhabited instance that exposes the pair of facts to downstream consumers.

proof idea

Definitional module with elementary lemmas, not a deep derivation. The domain cost is defined from the imported Cost primitives; nonnegativity is inherited from J-cost positivity; the canonical threshold is a fixed positive RS scale whose positivity is a one-line fact. The certificate is a structure whose fields are exactly those lemmas, and inhabitation is by direct construction. No substantial tactic script beyond assembling the bundle.

why it matters in Recognition Science

Gives the Cosmology domain a J-cost certificate for the horizon problem, tying causal disconnection of early patches to the same cost that T5 forces unique in the foundation chain. No downstream used-by edges are recorded yet; the inhabited certificate is the standard RS handoff pattern so later cosmology or phenomenology modules can assume the bundle without re-proving cost facts. It does not replace inflation phenomenology, but it records the RS-native cost obstruction that any such dynamics must clear.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)