jcost_unbounded_near_zero
plain-language theorem explainer
J-cost diverges to positive infinity as its argument approaches zero from above. Any physicist working on thermodynamic selection for recognition ledgers cites this to establish that the entropy cost of non-existence is unbounded. The proof splits into cases on the sign of the target bound C and then constructs an explicit small ε whose J-cost exceeds C via direct substitution into the squared expression for J.
Claim. For any real number $C$, there exists $ε > 0$ such that $J(ε) > C$, where $J(x) = (x-1)^2/(2x)$ for $x > 0$.
background
The J-cost function is defined via the squared-ratio form $J(x) = (x-1)^2/(2x)$ for positive reals, with a unique minimum of zero at $x=1$. This module formalizes the pre-Big-Bang thermodynamic selection claim that entropy non-decrease emerges as a selection principle on closed recognition ledgers, with the two key structural facts being the minimum at unity and the divergence of J at the boundaries of the positive reals. Upstream lemmas establish the squared expression and the ground-state value $J(1)=0$.
proof idea
The tactic proof begins with case analysis on whether C is negative. For negative C it invokes the unit lemma to take ε=1. For nonnegative C it explicitly constructs ε=1/(2C+4), applies the squared-form lemma to rewrite the cost, simplifies the resulting rational expression by field_simp and ring, and closes the inequality with nlinarith after clearing the denominator.
why it matters
This theorem supplies the nothing_diverges field in the thermodynamicSelectionCert definition, which bundles the structural inputs for the pre-Big-Bang thermodynamic selection claim. It directly supports the compactness of sublevel sets by showing divergence as x approaches 0 from above, complementing the companion result for x to infinity. Within the Recognition framework it underwrites the emergence of the second law as a selection principle on closed ledgers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.