Jmetric_val_6
plain-language theorem explainer
Evaluation of the J-metric at argument 6 yields sqrt(25/6). Researchers verifying explicit numerical instances of the cost-derived metric cite this result when testing bounds or counterexamples. The proof reduces directly by unfolding the definition and applying numerical normalization.
Claim. The J-metric satisfies $J(6) = sqrt(25/6)$, where $J(x) = sqrt(2 * Jcost(x))$ and Jcost is the underlying recognition cost function.
background
The J-metric is defined as the square root of twice the J-cost, converting the recognition deviation J into a distance function that recovers the absolute logarithm. This evaluation occurs in the Cost module, which assembles symmetry, nonnegativity, and composition properties of the J-cost for use in the Recognition framework. The upstream definition states that the square root of 2J yields a metric.
proof idea
The proof unfolds the J-metric definition to expose the J-cost at 6, then applies numerical normalization to obtain the explicit square root of 25/6.
why it matters
This supplies a concrete numerical instance referenced in the demonstration that the naive triangle inequality fails for the J-metric, directing attention to submultiplicativity bounds instead. It belongs to the standard pointwise analysis of cost functions, supporting verification steps inside the Recognition Science derivation of the forcing chain and derived constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.