Jmetric_triangle_FALSE
plain-language theorem explainer
Jmetric_triangle_FALSE establishes that Jmetric fails the triangle inequality Jmetric(ab) ≤ Jmetric(a) + Jmetric(b) for all positive reals a and b. Researchers deriving bounds in Recognition Science cost models would cite it to select the correct submultiplicative relation instead of metric assumptions. The proof exhibits a concrete counterexample at a=2 and b=3, reduces via explicit Jmetric evaluations at 2, 3 and 6, and invokes a precomputed numerical violation to obtain a contradiction by linear arithmetic.
Claim. It is not the case that $Jmetric(ab) ≤ Jmetric(a) + Jmetric(b)$ holds for all positive real numbers $a$ and $b$, where $Jmetric(x) := √(2 ⋅ Jcost(x))$.
background
In the Cost module, Jcost is the function obeying the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). Jmetric is defined by Jmetric(x) := √(2 Jcost(x)), described in its documentation as producing |log| and therefore a metric. The local setting concerns valid algebraic inequalities for this cost function rather than metric axioms. Upstream Jcost_submult supplies the correct bound Jcost(xy) ≤ 2Jcost(x) + 2Jcost(y) + 2Jcost(x)Jcost(y) obtained from d'Alembert's identity together with nonnegativity of Jcost(x/y). The present theorem also draws on the explicit point evaluations Jmetric_val_2, Jmetric_val_3, Jmetric_val_6 and the comparison sqrt_triangle_violation.
proof idea
The tactic proof assumes the universal triangle inequality, instantiates it at a=2 and b=3, rewrites the resulting claim using the value theorems for Jmetric at 2, 3 and 6, then applies sqrt_triangle_violation to produce a strict numerical inequality that contradicts the assumption; linarith closes the contradiction.
why it matters
The declaration rules out an invalid triangle inequality for Jmetric and thereby directs attention to the submultiplicative bound proved in Jcost_submult. It occupies a clarifying role inside the Cost module by preventing the importation of metric properties that do not follow from the Recognition Composition Law. No downstream uses are recorded, yet the result reinforces the framework's reliance on d'Alembert-derived bounds over metric assumptions in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.