domainCost
plain-language theorem explainer
Domain cost between real parameters m and e is introduced as the J-cost of their ratio. Lattice builders working on the phi-powered recognition structure cite this definition when assembling the metric on integer-indexed rungs. The definition is a direct substitution of the ratio into the preexisting J-cost function.
Claim. The cost function on the recognition domain is given by $c(m,e) := J(m/e)$, where $J$ denotes the J-cost.
background
The RecognitionLattice3 module constructs a lattice on the set of powers of phi indexed by integers, taking J-cost of the ratio of two powers as the distance. The metric is therefore $d(k,j) = |J(phi^{k-j})|$, with ground state at the zero rung where the ratio equals one and J-cost vanishes. The supplied definition supplies the explicit map used for all subsequent lattice certificates and appears identically in the muon g-2 derivation module.
proof idea
Direct definition that substitutes the ratio m/e into the J-cost function.
why it matters
This definition supplies the cost map required by the RecogLattice3Cert structure, which records the zero-cost equality case and nonnegativity needed for a metric on the lattice. It is also invoked directly in the muon g-2 certification theorems. The construction realizes the distance on the phi-ladder described in the module documentation and aligns with the J-uniqueness step of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.