Pith. sign in
module module moderate

IndisputableMonolith.Cosmology.CMBTemp3_FromJCost

show as:
view Lean formalization →

Certification module that ties the CMB temperature scale (~3 K) to the Recognition Science J-cost. Cosmologists in the RS program would cite it for the temperature-from-cost claim. It packages a domain cost, a positive canonical threshold, and an inhabited certificate rather than a single deep derivation.

claimThe module defines a domain cost built from the J-cost, a positive canonical threshold $T_*$, and a certificate asserting that the CMB temperature scale of order $3\,\mathrm{K}$ arises from that cost structure in RS-native units.

background

Recognition Science measures mismatch with the J-cost $J(x)=(x+x^{-1})/2-1$, brought in from the Cost module. Constants supplies the RS time quantum $\tau_0=1$ tick and the native unit conventions ($c=1$, and related scalings).

In the cosmology layer one asks whether the observed CMB temperature is forced by the same cost geometry that drives the forcing chain (J-uniqueness through dimension and octave structure). This module sets up the cost-on-domain and threshold objects used to state that claim cleanly.

proof idea

Definition-heavy module, not a single deep proof. It introduces a domain cost and records elementary facts (pointwise evaluation identity, nonnegativity), defines a positive canonical threshold, then packages a CMB-temperature certificate type together with an inhabited instance. The module-level argument is structural packaging of cost and threshold into a cert, not a multi-step analytic derivation.

why it matters in Recognition Science

Places the ~3 K CMB temperature inside the RS cost framework, linking a primary cosmological observable to J-cost. The dependency graph currently shows no downstream consumers, so the module stands as a self-contained Cosmology-domain certificate. It complements mass-ladder and coupling-band results elsewhere in the monolith by extending the same cost language to the thermal sky.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)