domainCost_at_eq
plain-language theorem explainer
domainCost_at_eq shows that the domain cost vanishes exactly when its two real arguments are equal and nonzero. Physicists constructing recognition-lattice certificates for the muon anomaly would cite this identity to anchor the zero-cost equilibrium inside Muong23Cert. The proof is a one-line wrapper that unfolds the definition of domainCost and reduces the ratio to unity before applying Jcost_unit0.
Claim. For every nonzero real number $r$, the domain cost satisfies $J(r/r)=0$, where $J$ is the J-cost function, or equivalently domainCost$(r,r)=0$.
background
The module develops a structural theorem for the muon g-2 anomaly expressed through J-cost. domainCost is defined by domainCost m e := Jcost (m/e). The lemma Jcost_unit0 states that Jcost 1 = 0, which follows directly from the explicit form J(x) = (x-1)^2/(2x). This identity is required to populate the cost_at_eq slot of the RecogLattice3Cert and Muong23Cert structures.
proof idea
The proof is a one-line wrapper. It unfolds domainCost to obtain Jcost (r/r), rewrites the ratio to 1 via div_self under the hypothesis r ≠ 0, and concludes by exact application of the lemma Jcost_unit0.
why it matters
The theorem supplies the cost_at_eq field for both the RecognitionLattice3.cert and the Muon_g-2_FromJCost.cert definitions. It fills the zero-cost equilibrium step inside the structural theorem for Delta a_mu = J(phi) * alpha / (2 pi). The result sits at the base of the J-cost machinery that later connects to the Recognition Composition Law and the T5 J-uniqueness step of the forcing chain; the module doc notes that the numerical muon prediction remains a placeholder discrepant by roughly two orders of magnitude.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.