domainCost
plain-language theorem explainer
Defines the domain cost of a mass–energy pair as the recognition cost of their ratio. Anyone working the RS pi–phi structural relation cites this as the local cost functional on (m,e). The body is a one-line abbreviation of J applied to m/e.
Claim. For real $m$ and $e$, the domain cost is $J(m/e)$, where $J(x)=\frac{1}{2}(x+x^{-1})-1$ is the recognition cost of a positive ratio.
background
The module develops the RS structural claim that $\pi$ is approximated by $4/\sqrt{\varphi}$ (about $3.146$, $0.15%$ off $\pi$), with status STRUCTURAL THEOREM and no sorry or axiom. The only cost primitive in play is the J-cost $J(x)=\frac12(x+x^{-1})-1$, forced uniquely by the Recognition Composition Law (T5 in the forcing chain).
Upstream, every import path exposes the same $J$: "the RS recognition cost of a positive ratio," equivalently "the unique cost functional forced by the Recognition Composition Law." Domain cost simply specializes that functional to a mass-over-energy ratio, the natural dimensionless argument when comparing geometric and dynamical scales in the pi–phi relation.
proof idea
Pure definitional abbreviation: domain cost of $(m,e)$ is exactly $J(m/e)$. No lemmas, no tactics; the body is the single application of the imported J-cost to the ratio.
why it matters
Supplies the local cost functional used by the sibling lemmas that establish non-negativity, evaluation identities, and the canonical threshold feeding PiPhiRelRS and its certificate. In the broader framework it is the T5 J-cost restricted to mass–energy ratios, the same $J$ that appears in the RCL and in the forcing chain. With no downstream edges yet recorded, its role is internal scaffolding for the pi–phi structural theorem rather than a leaf cited from outside the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.