domainCost
plain-language theorem explainer
Defines the domain cost of a mass-to-energy (or scale) ratio as the Recognition J-cost of that ratio. Used inside the hydrogen Balmer-line module to score how far a candidate spectral ratio sits from unity. Pure abbreviation: one application of J to m/e.
Claim. For real numbers $m$ and $e$, the domain cost is $J(m/e)$, where $J(x)=\frac{x+x^{-1}}{2}-1$ is the Recognition cost of a positive ratio.
background
The ambient module derives Balmer emission structure (Hα 656 nm, Hβ 486 nm, Hγ 434 nm) from the φ-ladder. The module note records that adjacent Balmer wavelengths stand in ratio ≈1.35 ∼ φ^{0.8}, so spectral spacing is read as a discrete rung step rather than a free fit.
The only primitive needed here is the Recognition cost $J$. Across the codebase it is fixed as $J(x)=\frac12(x+x^{-1})-1$ for $x>0$. Upstream docs state that this is the unique cost forced by the Recognition Composition Law, that $J(1)=0$, and that any genuine distinction (ratio ≠ 1) has strictly positive cost. Domain cost simply feeds the ratio $m/e$ into that functional.
proof idea
Definitional one-liner. No tactics: domainCost m e is definitionally Jcost (m / e). All analytic content (non-negativity, equality cases, thresholds) is deferred to sibling lemmas such as domainCost_nonneg and domainCost_at_eq.
why it matters
Local scaffolding for the structural hydrogen-spectrum certificate in this module (siblings HydrogenSpect3Cert, cert, canonicalThreshold). It packages the T5 J-uniqueness cost so Balmer ratio tests can be written as cost comparisons rather than ad-hoc numerics. Downstream of the forcing chain landmark $J(x)=\cosh(\log x)-1$, and upstream of any claim that a measured wavelength ratio sits below a canonical φ-ladder threshold. No external used_by edges are recorded yet; the immediate consumers are the non-negativity and certificate lemmas in the same file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.