domainCost
plain-language theorem explainer
The domain cost of a pair of reals is the recognition cost of their ratio: J(m/e). Anyone working the eight-tick lattice derivation or threshold comparisons cites this abbreviation. It is a one-line definition wrapping the unique RS cost functional on the quotient.
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 cost of a positive ratio.
background
The module derives the eight-tick cycle as a structural theorem: with spatial dimension $D=3$, one full traversal of the recognition lattice has $2^D=8$ binary states, so the octave period is forced (T7/T8 in the forcing chain). Status is zero sorry and zero axiom.
The underlying cost is the J-functional $J(x)=\frac{1}{2}(x+x^{-1})-1$, the unique nonnegative cost of a positive ratio forced by the Recognition Composition Law. Upstream copies state the same formula and note that a genuine distinction (ratio not one) has strictly positive cost. Domain cost simply feeds the ratio $m/e$ into that functional, treating $m$ and $e$ as the two scales whose mismatch is being priced.
proof idea
Pure definitional abbreviation: expand to $J(m/e)$ with no further proof obligations. Nonnegativity, special values, and threshold comparisons live in sibling lemmas, not here.
why it matters
Gives a named handle for pricing a two-scale mismatch inside the eight-tick derivation session. The parent module forces $8=2^3$ from $D=3$; domain cost is the local cost language for comparing magnitudes (mass-like versus energy-like scales) against canonical thresholds that appear as siblings. It sits on the T5 J-uniqueness landmark: once J is fixed by the composition law, every ratio cost is an instance of that same functional. No downstream uses are recorded in the graph yet; the definition is scaffolding vocabulary for the certificate and threshold lemmas in the same file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.