Jcost_submult
plain-language theorem explainer
The submultiplicative inequality for the J-cost function follows directly from the d'Alembert identity by non-negativity of the conjugate term. Researchers working on Recognition Science cost structures or defect distances cite this lemma when bounding products in the phi-ladder or coherence calculations. The proof is a short term-mode reduction that applies dalembert_identity, invokes Jcost_nonneg on the ratio, and closes with linarith.
Claim. For all $x, y > 0$, $J(xy) ≤ 2J(x) + 2J(y) + 2J(x)J(y)$, where $J(z) := (z + z^{-1})/2 - 1$.
background
The J-cost function is defined by $J(z) = (z + z^{-1})/2 - 1$ for $z > 0$, equivalently $(z-1)^2/(2z)$, and is nonnegative by AM-GM as shown in Jcost_nonneg. The Cost module develops this as the core cost structure, with the d'Alembert identity supplying the addition formula $J(xy) + J(x/y) = 2J(x) + 2J(y) + 2J(x)J(y)$ for positive arguments. Upstream, dalembert_identity is the key algebraic identity while Jcost_nonneg supplies the sign needed to drop the ratio term.
proof idea
The proof is a short term-mode reduction. It applies dalembert_identity to obtain the equality $J(xy) + J(x/y) = 2J(x) + 2J(y) + 2J(x)J(y)$, uses Jcost_nonneg on the positive ratio $x/y$ to establish nonnegativity of the second term, and concludes the inequality by linarith.
why it matters
Jcost_submult supplies the submultiplicative bound used in defectDist_quasi_triangle_local (local quasi-triangle for defect distance) and Jcost_prod_bound. It is invoked in ladder_cascade_bound for the phi-ladder and in symmetry_breaking_mechanism. Within the framework it supplies the cost control required for the eight-tick octave and phi-ladder mass formulas, while downstream results such as Jmetric_triangle_FALSE show why the stronger triangle inequality fails.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.