domainCost_nonneg
plain-language theorem explainer
This theorem establishes non-negativity of the domain cost for positive real parameters m and e. Model builders in Recognition Science cite it when assembling lattice certificates that treat J-cost as a metric on the phi-ladder. The proof is a one-line wrapper that unfolds the definition and applies the known non-negativity of J on positive arguments.
Claim. For positive real numbers $m$ and $e$, $J(m/e) ≥ 0$, where $J(x) = (x + x^{-1})/2 - 1$.
background
The module RecognitionLattice3 equips the integer lattice {phi^k : k in Z} with J-cost as distance, so that d(k,j) = |J(phi^(k-j))|. The ground state sits at k=0 where J=0. The definition domainCost m e is exactly J(m/e), turning the ratio of two positive reals into a lattice distance. Upstream, Jcost_nonneg proves J(x) ≥ 0 for x > 0 by rewriting J(x) as (x-1)^2/(2x) or by the AM-GM inequality x + 1/x ≥ 2.
proof idea
One-line wrapper. Unfold domainCost to obtain Jcost(m/e), then invoke Jcost_nonneg on the strictly positive quantity m/e supplied by div_pos hm he.
why it matters
The result supplies the cost_nonneg field inside RecogLattice3Cert and the corresponding Muong23Cert. These certificates certify that J-cost behaves as a non-negative distance on the phi-ladder, closing the structural requirements for the Recognition Lattice. It directly supports the non-negativity half of the metric axioms needed for T5 J-uniqueness and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.