ThermodynamicSelectionCert
plain-language theorem explainer
The ThermodynamicSelectionCert structure bundles five properties of the J-cost function that certify the structural prerequisites for thermodynamic selection. A cosmologist working on pre-Big-Bang models would cite it to establish that J-cost has a unique minimum at unity together with boundary divergence and compact sublevel sets. The definition is a direct packaging of five lemmas already proved for Jcost in the Cost module.
Claim. A certificate asserting that the J-cost function $J$ on positive reals satisfies: $J(x)=0$ if and only if $x=1$; $J(x)geq 0$ for all $x>0$; $J$ diverges to infinity as $x to 0^+$ and as $x to +infty$; and every sublevel set ${x>0 mid J(x)leq c}$ is bounded for $cgeq 0$.
background
In Recognition Science the J-cost function quantifies recognition defect for a positive real $x$, given explicitly by $J(x)=(x-1)^2/(2x)$ and equivalently by $(x+x^{-1})/2-1$. The module ThermodynamicSelectionCert supplies the structural inputs needed to derive the second law as a selection principle on closed recognition ledgers, where entropy non-decrease is equivalent to non-decreasing J-cost along any path from the boundary toward the fixed point at unity. The five fields encode uniqueness of the minimum, non-negativity, boundary divergence, and compactness of sublevel sets, all of which follow from the forcing chain and the recognition composition law.
proof idea
This is a structure definition that aggregates five properties of Jcost. Each field is populated directly by a sibling lemma: ground_state by jcost_ground_state, entropy_floor by jcost_entropy_floor, nothing_diverges by jcost_unbounded_near_zero, infinity_diverges by jcost_unbounded_at_infinity, and sublevel_bounded by sublevel_set_has_bounds. No additional tactics or reductions are performed.
why it matters
The certificate supplies the exact structural facts required by the downstream definition thermodynamicSelectionCert, which in turn grounds the claim that the second law emerges from recognition selection in pre-Big-Bang cosmology. It closes the SCAFFOLD tagged in the module documentation by confirming J-uniqueness at unity and compactness of sublevel sets. In the larger framework it anchors T5 (J-uniqueness) and the recognition composition law while leaving open the explicit derivation of monotonicity along arbitrary steepest-descent paths.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.