domainCost
plain-language theorem explainer
Defines the domain cost of a mass-to-energy ratio as the recognition cost J of that ratio. Anyone working the Fibonacci–phi limit or ladder thresholds in RS cites it as the local cost on a scale pair (m,e). The body is a one-line abbreviation of Jcost applied to m/e.
Claim. For real numbers $m$ and $e$, the domain cost is $J(m/e)$, where $J(x)=(x+x^{-1})/2-1$ is the recognition cost of a positive ratio.
background
The module treats the classical limit $F_{n+1}/F_n\to\varphi$ as the attractor of the J-cost recursion: $\varphi$ is the self-similar fixed point forced in the RS chain (T5–T6). Status is structural (no sorry, no axioms).
The recognition cost is $J(x)=(x+x^{-1})/2-1$, equivalently $\cosh(\log x)-1$. Upstream docs call it the unique cost forced by the Recognition Composition Law, nonnegative for $x>0$, and strictly positive when the ratio is not one. Domain cost simply evaluates that functional on a mass–energy (or scale) ratio $m/e$.
Sibling lemmas in the file (nonnegativity, evaluation identities, canonical threshold, FibLimitCert) build the certificate that Fibonacci ratios approach $\varphi$ in the J-metric.
proof idea
Pure definitional abbreviation: no tactics, no lemmas. The right-hand side is the shared Jcost from Cost (and re-exports), applied to the quotient $m/e$. Downstream proofs unfold or rewrite via the companion equality lemma for this def.
why it matters
Gives the module a named cost on scale pairs so the Fibonacci–phi convergence can be stated as J-cost attraction rather than bare ratio limits. That matches the RS reading of $\varphi$ as the J-recursion fixed point (T5 J-uniqueness, T6 phi forced). No current used-by edges are recorded; siblings such as domainCost_nonneg, canonicalThreshold, and FibLimitCert are the immediate consumers that turn the def into a limit certificate. It does not itself prove the limit; it supplies the cost language the certificate uses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.