Muong23Cert
plain-language theorem explainer
Muong23Cert bundles the zero-cost condition at equal arguments for domainCost, non-negativity of that cost for positive inputs, and positivity of the canonical threshold. Physicists deriving the muon g-2 anomaly from J-cost in Recognition Science cite this structure to certify the prerequisite properties before instantiating a concrete certificate. The declaration is a direct structure definition that collects the three properties from the module's domainCost and canonicalThreshold definitions.
Claim. The structure asserts that domainCost$(r,r)=0$ for all $r≠0$, that domainCost$(m,e)≥0$ whenever $m>0$ and $e>0$, and that canonicalThreshold$>0$, where domainCost$(m,e):=J(m/e)$ and canonicalThreshold$:=ϕ-3/2$.
background
In this module the domain cost is defined by domainCost m e := Jcost (m / e). The canonical threshold is defined as phi - 3/2. The structure collects the minimality and positivity properties needed for the J-cost treatment of the muon anomaly. Upstream, cost_nonneg from ObserverForcing states that the cost of any recognition event is non-negative, while the lattice definitions supply the explicit forms of domainCost and canonicalThreshold.
proof idea
This is a structure definition that directly encodes the three fields. No lemmas are applied; the fields simply reference the module-local definitions of domainCost and canonicalThreshold together with the non-negativity result imported from ObserverForcing.
why it matters
Muong23Cert is instantiated by the cert definition and shown nonempty by cert_inhabited, supplying the structural certificate for the muon g-2 calculation. It occupies the placeholder slot in the Recognition Science derivation of Delta a_mu = J(phi) * alpha / (2 pi), where the module notes that the resulting value exceeds the experimental discrepancy by a factor of roughly 100.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.