cosmic_censorship_automatic
plain-language theorem explainer
The declaration shows that J-cost remains non-negative and equals the squared deviation formula for every positive real argument. Physicists modeling black hole interiors in Recognition Science would cite it to confirm the absence of curvature singularities. The proof is a direct term application of the non-negativity lemma together with the algebraic identity lemma for J-cost.
Claim. For every real $x > 0$, the J-cost function satisfies $0 ≤ J(x)$ and $J(x) = (x-1)^2/(2x)$.
background
J-cost is the recognition cost induced by a multiplicative recognizer on positive ratios, equivalently expressed as $J(x) = (x + x^{-1})/2 - 1$ or the closed form $(x-1)^2/(2x)$. The upstream lemmas Jcost_nonneg and Jcost_eq_sq establish non-negativity via the AM-GM inequality and the algebraic identity via field simplification and ring tactics. In the ultramassive black hole module the local setting treats the black hole interior as a maximal J-cost state rather than a curvature singularity, with the no-singularity theorem resting on J-cost finiteness for all $x > 0$.
proof idea
The proof is a one-line term that pairs the non-negativity result Jcost_nonneg (applied to the strict positivity hypothesis) with the equality Jcost_eq_sq (applied after converting positivity to non-zero via ne_of_gt).
why it matters
This result directly implements the module claim that there are no singularities to censor, satisfying the weak cosmic censorship conjecture trivially because J(x) stays finite for all $x > 0$ while $x=0$ is excluded by the meta-principle that J approaches infinity at zero. It closes the no-singularity theorem for ultramassive black holes and connects to the Recognition Science forcing chain through J-uniqueness and the phi-ladder that keep costs bounded away from zero.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.