thermodynamicSelectionCert
plain-language theorem explainer
The thermodynamicSelectionCert packages five structural facts about the J-cost function into a single certificate for thermodynamic selection. Researchers formalizing pre-Big-Bang cosmology would reference it to establish that entropy non-decrease follows from J-cost monotonicity on closed ledgers. The definition constructs the record by direct assignment of the ground-state uniqueness, non-negativity, boundary divergence, and sublevel boundedness theorems.
Claim. A thermodynamic selection certificate for the J-cost function $J : (0,∞) → ℝ$ consists of: (i) $J(x)=0$ iff $x=1$ for all $x>0$; (ii) $J(x)≥0$ for all $x>0$; (iii) ∀C∈ℝ ∃ε>0 with $J(ε)>C$; (iv) ∀C∈ℝ ∃R>1 with $J(R)>C$; (v) ∀c≥0 the sublevel set {x>0 | J(x)≤c} is bounded.
background
In the Recognition Science framework the J-cost function measures the recognition defect of a positive real scale factor, with a unique minimum of zero at unity. The module formalizes the pre-Big-Bang claim that the second law emerges as a selection principle: on a closed ledger, J-cost cannot decrease spontaneously along any recognition-decreasing path. The certificate structure requires five properties drawn from the Cost module: ground-state uniqueness of the minimum, non-negativity (entropy floor), divergence to infinity as x→0⁺ and as x→+∞, and boundedness of sublevel sets. These are supplied by the upstream theorems jcost_ground_state, jcost_entropy_floor, jcost_unbounded_near_zero, jcost_unbounded_at_infinity, and sublevel_set_has_bounds.
proof idea
The definition is a direct record construction that assigns the five fields of ThermodynamicSelectionCert to the corresponding upstream theorems: ground_state receives jcost_ground_state, entropy_floor receives jcost_entropy_floor, nothing_diverges receives jcost_unbounded_near_zero, infinity_diverges receives jcost_unbounded_at_infinity, and sublevel_bounded receives sublevel_set_has_bounds.
why it matters
This definition supplies the structural certificate required by the pre-Big-Bang scaffold in the cosmology module. It encodes the monotone recognition selection principle that J-cost is non-decreasing along any descent path from the boundary toward the minimum at one. The certificate closes the structural inputs needed to derive thermodynamic selection from the Recognition Composition Law. No downstream uses are recorded yet; the declaration stands as the interface between the Cost module and cosmological applications of the second law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.