cert
plain-language theorem explainer
Packages three elementary facts about the domain cost (vanishes on the diagonal, is nonnegative, and has a positive canonical threshold) into a single inhabited certificate for the Penrose-process-from-J-cost module. Anyone citing the structural Penrose-efficiency claim in this file reaches for this bundle. Construction is pure field-wiring of three already-proved sibling lemmas.
Claim. There is a certificate consisting of: (i) $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$; (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive.
background
The module derives Penrose-process extraction efficiency from the Recognition Science J-cost. In RS units the efficiency is written $\eta_{\mathrm{Penrose}}=J(\varphi),(\Omega_H/\Omega_{\mathrm{ISCO}})$; at maximal Kerr this evaluates to about $J(\varphi)\cdot\varphi\approx 0.191$ (19.1%), against an empirical ceiling near 20.7%.
The J-cost is the unique nonnegative cost forced by the Recognition Composition Law, $J(x)=(x+x^{-1})/2-1$, minimized at the identity $x=1$. Upstream, cost_nonneg records that every recognition event has nonnegative cost via $J\ge 0$ on positive reals.
Locally, domainCost is the two-argument cost used for the mass/energy parameters of the process, canonicalThreshold is the positive cutoff against which extraction is compared, and PenroseProcess3Cert is the structure that packages the three elementary properties needed before efficiency comparisons are well-defined.
proof idea
One-line structure instance. The three fields of PenroseProcess3Cert are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity for positive arguments), and canonicalThreshold_pos (strict positivity of the threshold). No extra algebra is performed at this site.
why it matters
Gives an inhabited certificate that the domain-cost side conditions for the Penrose-from-J-cost argument are satisfied, so the module can claim a structural theorem with zero sorry and zero axioms. The parent narrative is the Plan v7 efficiency identity $\eta_{\mathrm{Penrose}}=J(\varphi),(\Omega_H/\Omega_{\mathrm{ISCO}})$, tying black-hole energy extraction to the same J forced at T5 and the golden ratio fixed at T6. No downstream consumers are recorded yet; the immediate sibling cert_inhabited is the natural next step that turns this definition into a propositional witness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.