bh_interior_finite_cost
plain-language theorem explainer
The theorem bounds the J-cost from above for any x lying in a closed interval [a, B] with a positive. Astrophysicists working on ultramassive black holes cite the result to confirm that every finite region of the interior carries only finite recognition cost. The proof unfolds the J-cost definition, records positivity of x together with the reciprocal inequality x^{-1} ≤ a^{-1}, and closes the bound by linear arithmetic.
Claim. Let $x,a,B$ be real numbers satisfying $0<a≤x≤B$. Then the J-cost of $x$ obeys $J(x)≤(B+a^{-1})/2$.
background
In the Recognition Science model of ultramassive black holes the J-cost function is the recognition cost attached to a positive real variable, given explicitly by $J(x)=(x+x^{-1})/2-1$. The module establishes that this cost remains finite on every bounded interval inside the black-hole interior, replacing the classical curvature singularity with a maximal but finite J-cost state. The local setting draws on the convexity of J-cost minimization and the discrete φ-tier structure of physical quantities supplied by the upstream structures PhysicsComplexityStructure, PhiForcingDerived and SpectralEmergence.
proof idea
The tactic proof first unfolds the definition of J-cost. It then obtains positivity of x from the chain 0<a≤x and the reciprocal bound x^{-1}≤a^{-1} from the monotonicity lemma inv_anti₀. Linear arithmetic finishes the inequality.
why it matters
The declaration supplies one concrete step in the no-singularity theorem stated in the module documentation: J-cost is finite everywhere on (0,∞) and the black-hole interior is therefore a maximal J-cost configuration rather than a curvature singularity. It aligns with the Recognition Science forcing chain (T5 J-uniqueness and T6 phi fixed point) by keeping all recognition costs finite inside any finite spatial region. No downstream theorems are recorded yet, so the result currently functions as a supporting lemma for the broader ultramassive-BH bundle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.