Jcost_finite_on_pos
plain-language theorem explainer
J-cost remains bounded above by (x + x^{-1})/2 for every positive real x. Physicists modeling black hole interiors in Recognition Science cite the result to confirm finite recognition cost throughout the interior rather than a curvature singularity. The proof is a one-line term-mode wrapper that unfolds the Jcost definition and discharges the inequality by linear arithmetic.
Claim. For every real number $x > 0$, the J-cost satisfies $Jcost(x) ≤ (x + x^{-1})/2$.
background
In the Recognition Science treatment of ultramassive black holes, J-cost quantifies recognition strain on a positive ratio x. The module formalizes the interior as a maximal but finite J-cost state. Upstream, cost is defined as the J-cost of a recognition event (ObserverForcing) and as the derived cost of a multiplicative recognizer comparator (MultiplicativeRecognizerL4). The local setting is the no-singularity theorem for masses ≳ 10¹⁰ M☉, with TON 618 as example, where J-cost finiteness replaces the classical singularity.
proof idea
The proof unfolds the definition of Jcost and applies linarith to verify the inequality holds directly.
why it matters
This result supplies the key step in the No Singularity Theorem of the UltramassiveBH module, showing J-cost finite on (0,∞) so the interior is a maximal J-cost configuration, not a curvature singularity. It supports the RS entropy formula S_BH = (ln φ) · A/(4ℓ₀²) and the T5 J-uniqueness landmark. No downstream uses appear yet; the declaration closes the finite-cost hypothesis for the gravity domain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.