Jmetric_val_2
plain-language theorem explainer
The metric built from the J-cost function evaluates to sqrt(1/2) at argument 2. Researchers testing submultiplicativity bounds or counterexamples in the cost domain cite this concrete value. The proof reduces the claim by unfolding the metric definition then applies numerical simplification.
Claim. Let $J$ denote the cost function. Define the metric by $d(x) := (2 J(x))^{1/2}$. Then $d(2) = (1/2)^{1/2}$.
background
The Cost module introduces the J-cost function on positive reals and derives a metric from it. The definition states that the square root of twice the J-cost yields the absolute logarithm and forms a metric. The sole upstream dependency is this definition of the metric itself.
proof idea
The proof unfolds the metric and cost definitions, reducing the equality to an arithmetic identity. The norm_num tactic then confirms the numerical value directly.
why it matters
This evaluation supplies the concrete number used in the downstream counterexample that the naive triangle inequality fails for the metric. The parent result instead directs attention to the submultiplicativity bound on the underlying cost. It anchors a specific computation inside the Recognition Science cost framework near the J-uniqueness step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.