Jmetric_val_3
plain-language theorem explainer
The evaluation establishes that the J-metric at argument 3 equals sqrt(4/3). Researchers examining cost axioms and metric properties in Recognition Science cite this value when testing submultiplicativity or constructing counterexamples. The proof is a one-line term reduction that unfolds the definitions of Jmetric and Jcost then applies norm_num to the resulting arithmetic.
Claim. $J_mathrm{metric}(3) = sqrt(4/3)$, where $J_mathrm{metric}(x) := sqrt(2 cdot J_mathrm{cost}(x))$ and $J_mathrm{cost}$ is the cost function satisfying the Recognition Composition Law.
background
In the Cost module the J-metric is defined by Jmetric(x) := Real.sqrt(2 * Jcost x). The accompanying doc-comment states that the square root of 2*J recovers the absolute logarithm and thereby supplies a metric on the positive reals. The theorem supplies the concrete numerical instance at the integer 3, obtained directly from the upstream definition of Jmetric.
proof idea
The proof is a term-mode one-liner: it unfolds Jmetric and Jcost, then invokes norm_num to reduce the arithmetic expression sqrt(2 * ((3 + 1/3)/2 - 1)) to sqrt(4/3).
why it matters
This evaluation feeds the downstream theorem Jmetric_triangle_FALSE, which exhibits the failure of the naive triangle inequality for Jmetric and therefore recommends the submultiplicative bound Jcost_submult instead. Within the Recognition Science framework the result instantiates the J-uniqueness relation (T5) at a specific point, providing a checkable datum for the eight-tick octave and the phi-ladder constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.