domainCost
plain-language theorem explainer
The cost of a domain ratio maps any pair of real numbers m and e to the J-cost of their ratio. Physicists investigating the muon anomalous magnetic moment within Recognition Science would cite this when constructing cost certificates for lattice models. It is supplied as a direct one-line definition delegating to the J-cost operator.
Claim. For real numbers $m$ and $e$, the domain cost is given by $J_ {cost}(m/e)$.
background
The Muon g-2 from J-Cost module develops a structural account of the muon anomaly by expressing discrepancies through the J-cost function. J-cost applies the J function from the forcing chain, where J(x) satisfies J(x) = (x + x^{-1})/2 - 1, to ratios of physical scales such as mass and energy. The module records that the implied Delta a_mu equals J(phi) * alpha / (2 pi) and exceeds the experimental value by a factor of roughly 100, marking the construction as a structural placeholder.
proof idea
This is a one-line definition that applies the Jcost function directly to the quotient of its two real arguments.
why it matters
This definition supplies the core cost measure that feeds the RecogLattice3Cert structure and the Muong23Cert in the muon g-2 module. It connects the J-uniqueness property (T5) of the forcing chain to concrete physics calculations, although the module documentation notes the resulting discrepancy is too large by two orders of magnitude. The same definition appears in the RecognitionLattice3 foundation, establishing the basic cost of a ratio in the lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.