sqrt_triangle_violation
plain-language theorem explainer
The declaration proves the concrete inequality sqrt(25/6) > sqrt(1/2) + sqrt(4/3). Researchers checking subadditivity of Jmetric in the Cost module cite it to exhibit failure of the direct triangle inequality on that function. The proof is a tactic-mode calculation that applies square-root monotonicity and sum-of-squares expansion, reduces via norm_num, and finishes with a linarith step on a rewritten comparison of square roots.
Claim. $√(25/6) > √(1/2) + √(4/3)$
background
In the Cost module Jcost satisfies the Recognition Composition Law and the submultiplicative bound Jcost(xy) ≤ 2 Jcost(x) + 2 Jcost(y) + 2 Jcost(x) Jcost(y) that follows from d'Alembert's identity together with nonnegativity of Jcost(x/y). Jmetric is defined by Jmetric(x) := √(2 Jcost(x)), which the module documentation states yields the absolute logarithm and forms a metric. The present theorem supplies a specific numerical witness that the naive triangle inequality Jmetric(ab) ≤ Jmetric(a) + Jmetric(b) fails for certain positive a and b. It sits inside the same module that imports the meta-realization structure for.
proof idea
The tactic proof first records nonnegativity of the right-hand side, rewrites the goal as a strict inequality, then applies sqrt monotonicity and the identity (u+v)^2 = u^2 + v^2 + 2uv. After canceling squares with sq_sqrt and norm_num it reduces to showing 2(√2/√3) < 7/3. Both sides are rewritten as square roots, the comparison lemma is applied again, and norm_num discharges the final numerical inequality.
why it matters
Jmetric_triangle_FALSE invokes this result to prove that the naive triangle inequality does not hold for Jmetric and therefore that the submultiplicative bound from Jcost_submult must be used instead. In the Recognition Science setting the declaration underscores that cost composition follows the forcing-derived submultiplicativity rather than an assumed metric triangle inequality on Jmetric. It closes a potential gap by exhibiting an explicit counterexample to the incorrect bound.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.