domainCost_at_eq
plain-language theorem explainer
Equal nonzero radial arguments make the domain cost vanish. Penrose-process and gravity modules use this as the on-diagonal normalization of the J-cost domain functional. The proof unfolds the definition, collapses the ratio to 1, and quotes the unit root of J.
Claim. For every real $r \neq 0$, the domain cost at equal arguments is zero: if the cost is $J(r/r)$ with $J$ the Recognition cost, then that value equals $0$.
background
The module derives Penrose-process efficiency from the Recognition J-cost, aiming at $\eta_{\mathrm{Penrose}} = J(\varphi),(\Omega_H/\Omega_{\mathrm{ISCO}})$ and the maximal-Kerr figure $\sim 19.1%$ against an empirical ceiling near $20.7%$. Status is structural: zero sorry, zero axioms.
The domain cost is the J-cost of a radial ratio (unfolded in the proof as $J(r_1/r_2)$). The Recognition cost satisfies $J(1)=0$, recorded upstream as the unit lemma $J_{\mathrm{cost}}(1)=0$, equivalently $J(x)=(x-1)^2/(2x)$ at $x=1$. That unit root is the only external fact needed here.
Local siblings package nonnegativity, a canonical threshold, and the Penrose-process certificate that consumes this normalization.
proof idea
One-line wrapper. Unfold the domain-cost definition so the goal is $J(r/r)=0$. Rewrite $r/r=1$ by the nonzero hypothesis via div_self, then apply the upstream unit lemma $J(1)=0$.
why it matters
Gives the on-diagonal vanishing that any ratio-based cost must satisfy before efficiency ratios are meaningful. In the Penrose module this underwrites the structural claim that efficiency is a pure multiple of $J(\varphi)$ times a kinematic horizon/ISCO factor, tying gravity phenomenology to the T5 J-uniqueness landmark and the golden fixed point $\varphi$ from T6. No downstream edges are recorded yet; the immediate consumers are the sibling certificate and threshold lemmas in the same file. Closes a trivial but mandatory normalization step so the $19.1%$ maximal-Kerr prediction sits on a proved zero of the cost, not an ad-hoc convention.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.