domainCost_at_eq
plain-language theorem explainer
Equal nonzero scale arguments make the domain cost vanish. Cosmology arguments that normalize ratios on the phi-ladder cite this diagonal zero. The proof unfolds the cost, reduces the ratio to 1, and applies the unit root of J.
Claim. For every real number $r \neq 0$, the domain cost of the pair $(r,r)$ is zero.
background
This module gives a structural expression for the Hubble constant from the Recognition Science phi-ladder: $H_0 = \phi^k / \tau_{\mathrm{universe}}$, aimed at the Planck value $67.4,\mathrm{km/s/Mpc}$ with $\tau_{\mathrm{universe}} = 13.8,\mathrm{Gyr}$. Status is fully proved (no sorry, no axioms).
The underlying cost is the J-cost $J(x) = (x+x^{-1})/2-1$, also written $(x-1)^2/(2x)$. Domain cost evaluates that cost on a ratio of real scale parameters. The key upstream fact is Jcost_unit0: $J(1)=0$, the unique minimum of $J$ on the positive reals.
proof idea
One-line wrapper. Unfold the definition of domain cost (a J-cost of a ratio). Rewrite $r/r$ to $1$ by div_self using $r\neq 0$. Finish with the lemma that $J(1)=0$.
why it matters
Supplies the on-diagonal normalization for domain cost inside the Hubble-from-J-cost development. Sibling results (domainCost_nonneg, canonicalThreshold, HubblePrecise2Cert) build the residual-cost and certificate layer that ties $H_0$ to a phi-ladder rung and the universe age. Zero cost when the two scales match is the baseline against which cosmological mismatch is measured, consistent with T5/T6 (J uniqueness and phi as self-similar fixed point). No downstream dependents are recorded yet; the lemma is local infrastructure for the certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.