PenroseProcess3Cert
plain-language theorem explainer
Certificate packing three structural hypotheses for Penrose-process efficiency from J-cost: domain cost vanishes on the diagonal, is nonnegative for positive mass/energy, and the canonical threshold is positive. Gravity workers cite it when wiring eta_Penrose = J(phi)*(Omega_H/Omega_ISCO). Pure structure; inhabitance is separate via cert.
Claim. A certificate consisting of three properties: (i) for every nonzero real $r$, the domain cost at $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost at $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
The module derives Penrose-process extraction efficiency from the Recognition Science J-cost. Classically, a Penrose process extracts rotational energy from a Kerr black hole by splitting a particle in the ergosphere; the theoretical maximum for extremal Kerr is about 20.7%. Here the claimed RS formula is $\eta_{\mathrm{Penrose}} = J(\varphi),(\Omega_H/\Omega_{\mathrm{ISCO}})$, which at maximal Kerr gives $\eta \sim J(\varphi)\cdot\varphi \approx 0.191$ (19.1%), consistent with the empirical ceiling.
Domain cost is the local cost functional on mass/energy coordinates used in this gravity module (built from the global J-cost $J(x)=(x+x^{-1})/2-1$). The upstream fact cost_nonneg states that every recognition event has nonnegative cost, via Jcost_nonneg on a positive state. The canonical threshold is the positive cutoff against which extraction efficiency is compared.
This structure does not prove efficiency; it packages the three algebraic side-conditions the later certificate and inhabitance theorems discharge.
proof idea
No proof body: this is a structure declaration (three fields, each a Prop). Inhabitance is supplied downstream by cert, which fills the fields with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. Nonemptiness is then cert_inhabited : Nonempty PenroseProcess3Cert := ⟨cert⟩.
why it matters
Gives a single named bundle for the structural side-conditions of the Plan-v7 Penrose-from-J-cost claim (module status: structural theorem, 0 sorry, 0 axiom). Downstream, cert is the concrete inhabitant and cert_inhabited records nonemptiness, so later gravity lemmas can assume one object rather than three separate hypotheses.
In the RS forcing chain the cost is the unique J from T5 (and RCL); $\varphi$ is the T6 fixed point. The numerical target $\eta\sim J(\varphi)\cdot\varphi\approx 19.1%$ versus the classical 20.7% max is the empirical check this certificate supports. It does not itself compute $\Omega_H/\Omega_{\mathrm{ISCO}}$ or close the full efficiency identity; it only locks the cost and threshold hygiene those steps need.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.