Jmetric_nonneg
plain-language theorem explainer
Jmetric is shown to be non-negative for positive real inputs. Workers on Recognition Science cost structures cite this when confirming that the derived metric satisfies the zero lower bound. The argument is a direct one-line application of square-root non-negativity to the definition Jmetric x := sqrt(2 * Jcost x).
Claim. Let $J$ denote the J-cost function. For every real number $x > 0$, $0 ≤ √(2 · J(x)).
background
In the Cost module, Jcost supplies the base recognition cost while Jmetric is defined as the square root of twice that cost. The upstream definition states that this construction recovers the absolute logarithm and therefore functions as a metric on the positive reals. The hypothesis 0 < x ensures the argument of the square root remains non-negative, consistent with the identity event at unit state that places the cost minimum at x = 1.
proof idea
The proof is a one-line wrapper that applies Real.sqrt_nonneg directly to the body of the Jmetric definition.
why it matters
This lemma secures the non-negativity axiom required for Jmetric to serve as a distance in the Recognition framework. It rests on the J-uniqueness property (T5) that forces J(x) = (x + x^{-1})/2 - 1 and on the metric interpretation supplied by the Jmetric definition. No downstream results yet reference it, but the result is prerequisite for any further metric verification inside the cost domain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.