Jmetric
plain-language theorem explainer
The definition constructs a distance on positive reals from the J-cost by taking its square root after scaling by two. Researchers deriving metric properties from the Recognition Composition Law would reference this construction. It is introduced as a direct definition that subsequent lemmas unfold to prove non-negativity and symmetry.
Claim. Let $J(x) = (x + x^{-1})/2 - 1$. Define $d(x) = sqrt(2 J(x))$ for positive real $x$.
background
The Cost module defines the J-cost function as $J(x) = (x + x^{-1})/2 - 1$, equivalent to $cosh(log x) - 1$. Jmetric applies the square root to twice this value, as noted in the module's documentation that this yields the absolute logarithm and thereby a metric. This occurs in the setting of exploring cost functions that satisfy the Recognition Composition Law, building on the J-uniqueness from the forcing chain.
proof idea
This declaration is a one-line definition that directly applies the real square root to the expression 2 times Jcost x. No additional lemmas are used in its own body.
why it matters
It serves as the foundation for multiple lemmas in the same module that establish metric-like properties, such as non-negativity and symmetry. The construction aligns with the framework's emphasis on logarithmic distances in the context of the eight-tick octave and spatial dimensions. It precedes the demonstration that the triangle inequality fails for this function, directing attention instead to submultiplicative bounds from the J-cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.