canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold used in the J-cost Penrose-process efficiency bound is strictly positive. Gravity and Kerr-efficiency arguments cite it to keep the efficiency scale above zero. The proof is a one-line unfold of the threshold definition followed by linear arithmetic from the bound φ > 1.5.
Claim. The canonical threshold is strictly positive: $0 < \ thr_{\mathrm{can}}$.
background
The module derives a structural efficiency bound for the Penrose process from the Recognition Science J-cost. In RS units the claimed form is $\eta_{\mathrm{Penrose}} = J(\varphi),(\Omega_H/\Omega_{\mathrm{ISCO}})$, which at maximal Kerr reduces to about $J(\varphi)\cdot\varphi \approx 0.191$ (19.1%), consistent with the empirical ceiling near 20.7%.
The golden ratio $\varphi = (1+\sqrt{5})/2$ is the self-similar fixed point forced by the T5–T6 segment of the unified forcing chain. The upstream lemma supplies the elementary numerical bound $\varphi > 1.5$ (from $\sqrt{5} > 2$). The canonical threshold is the scalar scale appearing in the local efficiency certificate; its positivity is the first arithmetic gate before nonnegativity of domain cost and the inhabited certificate.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then discharge $0 < \cdots$ by linarith using the imported fact $\varphi > 1.5$. No further lemmas or case splits.
why it matters
Keeps the Penrose-process efficiency scale strictly above zero inside the J-cost gravity module. The module presents a structural (0-sorry, 0-axiom) certificate that $\eta_{\mathrm{Penrose}} \sim J(\varphi)\cdot\varphi \approx 19.1%$ at maximal Kerr, aligned with the empirical maximum near 20.7%. The result sits downstream of the T5 J-uniqueness and T6 $\varphi$-forcing landmarks and of the elementary bound $\varphi > 1.5$. No further used-by edges are recorded in the current graph; it is a local positivity gate for the certificate constructors in the same file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.