Jcost_weak_triangle_FALSE
plain-language theorem explainer
The proposed weak triangle inequality J(xy) ≤ 2(J(x) + J(y)) + 2√(J(x)J(y)) fails for the J-cost function on positive reals. Researchers establishing submultiplicative bounds from the Recognition Composition Law cite this to discard an incorrect candidate before adopting the valid form derived from d'Alembert's identity. The proof assumes the universal statement, instantiates it at the counterexample x = y = 10, simplifies the explicit definition of J, and applies nlinarith with nonnegativity facts to reach a contradiction.
Claim. It is false that for all positive real numbers $x, y$, $J(xy) ≤ 2(J(x) + J(y)) + 2√(J(x)J(y))$, where $J(z) := (z + z^{-1})/2 - 1$.
background
Jcost is the function $J(z) = (z + z^{-1})/2 - 1$ for $z > 0$, equivalently cosh(log z) - 1. It supplies the native cost measure in Recognition Science and obeys the Recognition Composition Law $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$. The Cost module assembles elementary properties of this function, including nonnegativity, symmetry, and the correct submultiplicative bound Jcost_submult.
proof idea
The term proof assumes the universal quantification over positive x and y. It instantiates the assumption at x = y = 10, simplifies Jcost(100) and the proposed right-hand side via the explicit definition, then invokes nlinarith together with sq_nonneg and sqrt_nonneg to obtain the contradiction that 49.005 > 24.3.
why it matters
The declaration eliminates an erroneous candidate inequality, steering subsequent cost arguments toward the proved submultiplicative form Jcost_submult that follows directly from d'Alembert's identity. It belongs to the chain of basic J-cost lemmas that support later developments in the Recognition framework, such as mass formulas on the phi-ladder and bounds involving the eight-tick octave. No theorems depend on it, confirming its role as a corrective note rather than a reusable lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.