domainCost
plain-language theorem explainer
Domain cost scores a mass-to-energy ratio by the RS J-cost: J(m/e) = (m/e + e/m)/2 - 1. Anyone working the golden-angle certificate or related threshold lemmas in this module cites it as the local cost on a two-scale pair. The body is a one-line abbreviation of the global Jcost functional.
Claim. For real numbers $m$ and $e$, the domain cost is $J(m/e)$, where $J(x) = \frac{1}{2}(x + x^{-1}) - 1$ is the Recognition Science cost of a positive ratio.
background
The module fixes the golden angle in RS units: $\theta_G = 2\pi,\varphi^{-2} = 2\pi(1 - 1/\varphi)$, about $137.508^\circ$, the angle that appears in phyllotaxis. Status is structural (no sorry, no axioms).
The underlying cost is the unique J-functional forced by the Recognition Composition Law (T5): $J(x) = \frac12(x + x^{-1}) - 1$, also written $\cosh(\log x) - 1$. Upstream copies of Jcost state the same formula and record that a genuine distinction (ratio not one) has strictly positive cost, and that $J$ is nonnegative on positives.
Here the two arguments are treated as a mass-like scale $m$ and an energy-like scale $e$; their ratio is the only input the cost sees.
proof idea
Pure definitional abbreviation: domainCost m e is definitionally Jcost (m / e). No tactics, no lemmas, no side conditions in the body. Nonnegativity and evaluation identities are proved in sibling lemmas, not here.
why it matters
Gives the module a named two-argument cost so golden-angle thresholds and certificates can speak about mass/energy mismatch without reopening the global Jcost API. Siblings (domainCost_nonneg, domainCost_at_eq, canonicalThreshold, GoldenAngleCert) build the local certificate stack on top of this alias. Framework landmark: T5 J-uniqueness and the RCL, which force the same $J$ used everywhere else in the monolith. No open scaffold: claim status is definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.