Jcost_lower_bound
plain-language theorem explainer
The inequality establishes that recognition cost J(x) is bounded below by 1/(2x) - 1 for every positive real x, implying divergence to infinity as x approaches zero from above. Researchers modeling ultramassive black holes or recognition processes cite it to confirm finite-cost interiors rather than singularities. The proof unfolds the Jcost definition and applies linear arithmetic after deriving non-negativity of x.
Claim. For every real number $x > 0$, $1/(2x) - 1 ≤ J(x)$, where $J$ denotes the recognition cost function.
background
The J-cost function, imported from JcostCore, quantifies recognition cost for positive real parameters and satisfies the Recognition Composition Law. The UltramassiveBH module places this in the setting of ultramassive black holes, where J-cost remains finite on (0, ∞) and the interior is a maximal J-cost state, not a curvature singularity. The module also records the RS entropy S_BH = (ln φ) · A/(4ℓ₀²) and Hawking temperature in native units.
proof idea
The proof unfolds Jcost to expose its explicit form, obtains 0 ≤ x from the hypothesis 0 < x via le_of_lt, and concludes the inequality by linarith.
why it matters
The result is invoked in nothing_costs_arbitrarily_large to witness the Meta-Principle that cost becomes arbitrarily large for small positive x. It supplies the key step for the no-singularity theorem in the ultramassive black hole treatment and the associated paper RS_TON618_Ultramassive_Black_Holes.tex. The bound reinforces J-cost finiteness on (0, ∞) while allowing divergence at the boundary, consistent with the forcing chain and phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.