Jmetric
Jmetric is defined as the square root of twice the J-cost function on positive reals. Researchers deriving bounds or symmetry properties in the Cost module cite this construction when building distance-like functions from the base J. The definition is a direct one-line abbreviation that downstream lemmas immediately apply to verify non-negativity and symmetry.
claimDefine $J(x) := (x + x^{-1})/2 - 1$ for $x > 0$. Then set $d(x) := (2 J(x))^{1/2}$.
background
In the Cost module the sibling definition Jcost supplies the base function $J(x) = (x + x^{-1})/2 - 1$, equivalently cosh(log x) - 1. Jmetric is constructed directly from this by taking the positive square root after scaling by 2. The module imports only Mathlib and works entirely within real analysis on the multiplicative group of positive reals.
proof idea
One-line definition: Jmetric x is set to Real.sqrt (2 * Jcost x). No tactics or lemmas appear in the body; all properties are proved in separate declarations that unfold this definition.
why it matters in Recognition Science
Jmetric supplies the candidate distance derived from J-cost and is referenced by ten downstream results in the same module, including Jmetric_nonneg, Jmetric_symm, Jmetric_exp_sinh and the quadratic lower bound for cosh. The declaration comment states that the construction yields |log|, supporting metric-like behavior in the Recognition framework. The triangle inequality fails (see Jmetric_triangle_FALSE), so the definition feeds submultiplicativity arguments instead.
scope and limits
- Does not prove the triangle inequality.
- Does not claim exact equality to |log x|.
- Does not define behavior for non-positive arguments.
- Does not link to the phi-ladder or mass formulas.
formal statement (Lean)
339noncomputable def Jmetric (x : ℝ) : ℝ := Real.sqrt (2 * Jcost x)
proof body
Definition body.
340
341/-- Jmetric(1) = 0 -/