domainCost_at_eq
plain-language theorem explainer
The theorem shows that domain cost on the recognition lattice is zero precisely when the two real arguments coincide and are nonzero. Muon g-2 modelers and lattice certifiers cite it to fix the ground-state energy. The proof is a one-line wrapper that unfolds the definition, simplifies the ratio, and applies the J-cost unit lemma.
Claim. For every real number $r$ with $r ≠ 0$, domainCost$(r,r) = 0$, where domainCost$(m,e) := J(m/e)$ and $J$ satisfies $J(1) = 0$.
background
The Recognition Lattice3 module equips the set of powers of phi with a metric given by the absolute J-cost of their ratio. The definition domainCost$(m,e)$ is exactly Jcost of the ratio $m/e$, so the cost vanishes when the arguments are equal. Upstream Jcost_unit0 states that Jcost 1 = 0 and records the explicit form J(x) = (x-1)^2/(2x). The module document states that the ground state sits at rung zero with J = 0 and the first excited state at rung one.
proof idea
This is a one-line wrapper. It unfolds domainCost to obtain Jcost(r/r), rewrites the ratio to 1 by div_self under the hypothesis r ≠ 0, and finishes by exact application of Jcost_unit0.
why it matters
The result supplies the cost_at_eq field required by both RecogLattice3Cert and Muong23Cert. It anchors the zero-cost ground state at rung zero on the phi-ladder, consistent with the Recognition Composition Law and the eight-tick octave. The declaration closes the structural theorem for the lattice with no axioms or sorrys.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.