domainCost_at_eq
plain-language theorem explainer
Equal nonzero arguments make the domain cost vanish: the cost of a real against itself is zero. Gap-45 certificate work and any nonnegativity or threshold argument on domain cost cite this unit normalization. Proof is a one-line unfold of the cost, rewrite of the self-ratio to 1, and the unit-zero lemma for J.
Claim. For every real $r \neq 0$, the domain cost of $r$ against itself is zero.
background
Module Gap45_Exact_v2 records the structural identity gap-45 $= 45 = D^2(D+2) = 9\cdot 5$ forced by $D=3$ spatial dimensions (T8), linking the classical $45^\circ$ angle and related numerology into the Recognition forcing chain. Status is a structural theorem block with no sorry and no axioms.
The cost $J$ is the unique nonnegative functional from the Recognition Composition Law, with closed form $J(x)=(x+x^{-1})/2-1$ (equivalently $(x-1)^2/(2x)$). Domain cost applies $J$ to the ratio of two nonzero reals, so it measures mismatch of a pair on the multiplicative line.
Upstream, Jcost_unit0 states $J(1)=0$ by direct simplification of that definition; the present lemma is the diagonal specialization of domain cost to that unit zero.
proof idea
One-line wrapper. Unfold the domain-cost definition so the goal becomes $J(r/r)=0$. Rewrite the self-ratio to $1$ by div_self (using $r\neq 0$), then finish with the upstream unit-zero lemma $J(1)=0$.
why it matters
Infrastructure for the Gap-45 exactness certificate and its siblings (domain-cost nonnegativity, canonical threshold positivity, and the inhabited Gap45ExactV2Cert). It encodes the fixed-point property that equal arguments carry zero cost, which is exactly $J(1)=0$ after the ratio is formed.
The module ties gap-45 to $D=3$ via $D^2(D+2)$, so this lemma sits under T8 (three spatial dimensions) and T5 (J-uniqueness). The dependency graph currently lists no downstream parents; the lemma is local scaffolding for the certificate rather than a cited parent theorem. No open question is closed here; it only normalizes the diagonal.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.