jcost_unbounded_at_infinity
plain-language theorem explainer
J-cost grows without bound as its argument tends to positive infinity. Researchers formalizing thermodynamic selection on closed recognition ledgers cite the result to guarantee compactness of sublevel sets. The tactic proof splits on the sign of the target bound C, supplies an explicit witness R in each case, and reduces the target inequality through the squared expression of J.
Claim. For every real number $C$ there exists a real number $R>1$ such that $C<J(R)$, where $J(x)=((x-1)^2)/(2x)$.
background
The J-cost function is given by the identity $J(x)=((x-1)^2)/(2x)$ for $x≠0$, which follows from the upstream lemma Jcost_eq_sq by algebraic simplification of the original definition $J(x)=(x+x^{-1})/2-1$. The ThermodynamicSelectionCert module assembles structural facts needed for the pre-Big-Bang scaffold: J attains its unique minimum value 0 at $x=1$, and the sublevel sets {$x:J(x)≤c$} remain compact for every finite $c$ precisely because J diverges at both ends of the positive reals.
proof idea
The proof opens with case analysis on whether $C<0$. When $C<0$ the witness $R=2$ is inserted and Jcost_eq_sq reduces the claim to an immediate numerical inequality. When $C≥0$ the witness $R=2C+4$ is chosen; after rewriting $J(R)$ via the squared form, clearing the denominator, and applying ring_nf, the inequality is settled by nlinarith on the resulting quadratic expression.
why it matters
The theorem supplies the infinity_diverges field inside the ThermodynamicSelectionCert definition, which certifies the full structural claim that entropy non-decrease emerges as a selection principle on closed ledgers. It thereby completes the compactness argument required by the module's scaffold for monotone recognition selection. In the broader Recognition Science setting the result reinforces the J-uniqueness property at the fixed point $x=1$ and the divergence behavior that forces the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.