Jcost_zero_iff_one
plain-language theorem explainer
J-cost vanishes precisely when its argument equals one for positive reals. Ultramassive black-hole analyses cite the result to confirm that the interior remains a finite-strain state rather than a singularity. The tactic proof splits the biconditional, substitutes the squared-ratio identity for J-cost, and resolves the resulting cases by linear arithmetic and positivity.
Claim. For every real $x > 0$, $J(x) = 0$ if and only if $x = 1$, where $J(x) := (x + x^{-1})/2 - 1$.
background
In the Recognition Science treatment of ultramassive black holes the J-cost function measures recognition defect or strain. It is given by the algebraic identity $J(x) = (x-1)^2/(2x)$ for $x > 0$, which follows from the definition $J(x) = (x + x^{-1})/2 - 1$. The module shows that this cost remains finite on the entire positive ray, so the black-hole interior is a maximal but finite J-cost configuration rather than a curvature singularity.
proof idea
The proof uses constructor to split the biconditional. The forward direction assumes Jcost x = 0, rewrites via Jcost_eq_sq to obtain (x-1)^2/(2x) = 0, applies div_eq_zero_iff, and cases on the factors; the denominator case is excluded by positivity of 2x while the numerator case yields x = 1 by linarith. The reverse direction substitutes x = 1 and invokes Jcost_unit0.
why it matters
The lemma supplies the uniqueness of the J-cost zero that underpins the no-singularity theorem for ultramassive black holes. It is invoked directly by the energy-processing bridge to separate equilibrium from strained states and by the graph-rigidity theorems to propagate vanishing edge costs to global constancy on connected graphs. Within the forcing chain it instantiates the J-uniqueness step (T5) that forces the self-similar fixed point phi.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.