pith. sign in
module module high

IndisputableMonolith.Cosmology.ThermodynamicSelectionCert

show as:
view Lean formalization →

The Cosmology.ThermodynamicSelectionCert module certifies an entropy floor by showing J-cost is non-negative. Cosmologists applying Recognition Science to early-universe bounds would cite it when linking cost functions to thermodynamic selection on the phi-ladder. The module assembles direct consequences from imported Cost definitions and the RS time quantum without internal derivations.

claim$J(x) = (x + x^{-1})/2 - 1$ satisfies $J(x) > 0$ except at the fixed point, establishing the entropy floor for thermodynamic selection certification.

background

The module sits in the cosmology domain and imports the RS time quantum τ₀ = 1 tick from Constants together with the cost functional from the Cost module. It defines supporting objects including jcost_entropy_floor, jcost_ground_state, jcost_unbounded_near_zero, jcost_unbounded_at_infinity, and sublevel_set_has_bounds before reaching ThermodynamicSelectionCert. These rest on the Recognition Composition Law and the J-function properties already fixed in the upstream Cost module.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the entropy floor required for thermodynamic selection in cosmology and thereby supports downstream derivations that connect J-cost bounds to the forcing chain steps T5 through T8. It supplies the non-negativity needed to close cost arguments on the phi-ladder when deriving spatial dimension D = 3 and the alpha band.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (7)