domainCost_at_eq
plain-language theorem explainer
Whenever both arguments of the domain cost agree and are nonzero, the cost is exactly zero. Collapse-threshold and GRW-rate arguments that normalize J at matched scales cite this identity. The proof unfolds the cost to J of a ratio, cancels the ratio to 1, and applies the unit root of J.
Claim. For every real $r \neq 0$, the domain cost evaluated on the diagonal vanishes: if the cost is $J(r/r)$ (with $J$ the Recognition cost), then $J(r/r) = 0$.
background
The ambient module builds an objective (GRW-style) collapse threshold from the Recognition J-cost. Status is structural: zero sorry, zero axiom. The intended rate formula is $\lambda = J(\varphi)/(m_{\mathrm{nucleon}}\varphi^{20})$; the module records that matching the experimental $10^{-16},\mathrm{s}^{-1}$ scale is off by many orders, so the work is structural rather than numerical.
The cost $J$ is the unique nonnegative functional forced by the Recognition Composition Law, with closed form $J(x)=(x+x^{-1})/2-1$ (equivalently $(x-1)^2/(2x)$). In particular $J(1)=0$. Domain cost is the local specialization that feeds a ratio of two real scales into $J$; on the diagonal that ratio is identically one whenever the common scale is nonzero.
Upstream, Jcost_unit0 states exactly $J(1)=0$ by unfolding the definition of $J$.
proof idea
One-line wrapper. Unfold the definition of domain cost so the goal becomes $J(r/r)=0$. Rewrite $r/r=1$ via the nonzero hypothesis, then apply the upstream lemma $J(1)=0$.
why it matters
Diagonal vanishing is the normalization step for any collapse or threshold certificate built from domain cost in this module (nonnegativity, canonical threshold positivity, and the WFCollapse3 certificate siblings). It anchors the claim that matched scales carry zero J-defect before a threshold comparison is imposed.
In the broader forcing chain, $J$ is the T5-unique cost; its unit root is the algebraic reason the eight-tick and $\varphi$-ladder constructions can treat the identity scale as cost-free. The module itself flags that the GRW numerical match remains off by ~38 orders, so this lemma closes only the algebraic side of the structural theorem, not the phenomenological gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.