domainCost_at_eq
plain-language theorem explainer
When both arguments of the domain cost are the same nonzero real, the cost is exactly zero. Information and bandwidth proofs in the RS stack cite this as the diagonal normalization of mismatch cost. The argument is a one-line wrapper: unfold the cost, collapse the self-ratio to 1, and apply the unit-zero lemma for J.
Claim. For every real $r\neq 0$, the domain cost of the matched pair $(r,r)$ vanishes: the cost of the ratio $r/r$ is zero.
background
This module gives the Recognition Science reading of Shannon channel capacity. Classically $C=B\log_2(1+\mathrm{SNR})$; at phi-resonance RS forces $\mathrm{SNR}=\phi^D=\phi^3$, so the structural factor is $\log_2(\phi^3+1)$. Status is structural: zero sorry, zero axiom.
The underlying cost is the unique nonnegative $J$ fixed by the Recognition Composition Law, with closed form $J(x)=(x+x^{-1})/2-1$, also written $(x-1)^2/(2x)$. Domain cost is that $J$ applied to a ratio of two real scales: it scores mismatch between a working scale and a reference.
Upstream, the unit lemma records $J(1)=0$. That is the normalization any equal-argument evaluation must hit.
proof idea
One-line wrapper on the definition. Unfold domain cost (J of the ratio of the two arguments). Rewrite the self-division $r/r$ to $1$ via the nonzero hypothesis. Finish by the unit lemma $J(1)=0$.
why it matters
Gives the diagonal baseline for the information-cost layer in Bandwidth_Phi_RS: matched scales cost nothing, so thresholds and certificates measure genuine mismatch. Siblings cover nonnegativity of domain cost, the canonical positive threshold, and the BandwidthPhiCert package that packages the structural SNR claim $\phi^3$.
Aligns with T5 J-uniqueness and the RCL normalization $J(1)=0$. The module frames capacity $C_{\mathrm{RS}}=B\log_2(\phi^3+1)$ as structural; this lemma is local infrastructure for that story. The dependency graph currently shows no external consumers, so it is in-module support rather than a cross-module hinge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.