domainCost_at_eq
plain-language theorem explainer
On the diagonal, domain cost vanishes: any nonzero real scale compared to itself has cost zero. Cosmology arguments that place the inflaton on a pure phi-ladder rung use this to clear self-matched thresholds. The proof is a one-line unfold that reduces the ratio to 1 and quotes J(1)=0.
Claim. For every real $r \neq 0$, the domain cost of the diagonal pair $(r,r)$ is zero.
background
The module is a structural (0-sorry) derivation of the inflaton mass from the Recognition Science phi-ladder: $m_{\mathrm{inflaton}} = \varphi^k E_{\mathrm{coh}}$, with the target band near $10^{13},\mathrm{GeV}$ at rung $k \approx 57$ (and a lower check at $k=53$).
Domain cost is the cost of a scale ratio, built from the RS cost functional $J$ (Lean Jcost). Upstream records the closed form $J(x)=(x-1)^2/(2x)$ and the unit identity $J(1)=0$. That unit identity is exactly the diagonal case: when the two arguments coincide and are nonzero, the ratio is 1 and the cost collapses.
Local siblings package nonnegativity, a canonical threshold, and the inhabited inflaton-mass certificate that sits on this infrastructure.
proof idea
One-line wrapper. Unfold the definition of domain cost (which feeds the ratio of its two arguments into $J$), rewrite $r/r=1$ by div_self using the hypothesis $r\neq 0$, then apply the upstream unit lemma $J(1)=0$.
why it matters
Zero diagonal cost is the baseline that lets later threshold comparisons measure genuine off-diagonal mismatch rather than a self-cost artifact. Inside this module it supports the structural inflaton-mass certificate (siblings InflatonMass3Cert, cert, canonicalThreshold): the mass is read as a pure phi-ladder rung times the coherence energy, with no residual diagonal penalty.
Framework-wise this is the local instance of T5 J-uniqueness: cost vanishes only at the self-similar fixed ratio 1, consistent with the Recognition Composition Law and the forcing chain that pins $\varphi$ and the octave. No external used-by edges are recorded yet; the lemma is internal scaffolding for the cosmology certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.