domainCost
plain-language theorem explainer
Domain cost assigns to a mass–energy pair the recognition cost of their ratio. DNA-storage density arguments in RS use it as the local cost on the (m,e) plane. The body is a one-line wrapper of the standard J-cost on m/e.
Claim. For real $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 module treats DNA storage density in Recognition Science units: empirical figures (Church et al., ~2.15×10^17 bytes/g) are compared to a structural φ-ladder count of bytes per gram. Status is structural (no sorry, no axioms).
The only primitive needed here is the J-cost. Upstream it is defined uniformly as $J(x)=\frac12(x+x^{-1})-1$, the unique cost forced by the Recognition Composition Law (T5). Doc-comments call it “the RS recognition cost of a positive ratio” and note that a genuine distinction (ratio ≠ 1) has strictly positive cost.
Domain cost simply specialises that functional to a mass-over-energy ratio, the natural dimensionless argument when storage density is read as an information-per-mass figure against an energy scale.
proof idea
Definitional one-liner: domainCost m e is exactly Jcost (m/e). No lemmas, no tactics; the equality is by unfolding.
why it matters
Gives the module a named cost on the (m,e) plane so later certificates (canonicalThreshold, DNAStorageCert, cert) can speak about non-negativity and threshold crossings without re-inlining J. It sits under the T5 uniqueness of J and the RCL, and under the module’s structural claim that DNA density is a φ-power count rather than an independent empirical constant. No downstream theorems are wired yet (used_by is empty); the immediate consumers are the sibling lemmas domainCost_nonneg and domainCost_at_eq.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.