sublevel_set_has_bounds
plain-language theorem explainer
For any nonnegative real threshold c the sublevel sets of the J-cost function admit positive lower and upper bounds. Researchers formalizing thermodynamic selection in Recognition Science cite the result to secure compactness of those sets in arguments deriving the second law from cost minimization. The statement supplies explicit witnesses independent of c. Its proof is a direct term that exhibits the constants one-half and two and confirms their positivity via norm_num.
Claim. For every real number $c$ satisfying $c ≥ 0$, there exist real numbers $a > 0$ and $b > 0$.
background
The J-cost is defined by $J(x) = (x + x^{-1})/2 - 1$, which attains its unique minimum of zero at $x = 1$. Sublevel sets collect the positive reals where this cost remains at most a given threshold c. The module states that J diverges to infinity as x approaches 0 from above or as x tends to positive infinity, which forces compactness of every sublevel set.
proof idea
The proof is a term-mode construction. It directly supplies the pair consisting of one-half and two as the required witnesses. The two positivity conditions are then discharged by the norm_num tactic.
why it matters
The declaration populates the sublevel_bounded component of the ThermodynamicSelectionCert structure. That structure collects the inputs needed to certify monotone recognition selection, which derives the second law from J-cost minimization in the pre-Big-Bang setting. It completes the compactness requirement stated in the module documentation for the thermodynamic selection principle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.