Jcost_prod_bound
The bound states that J(xy) is at most 2(1 + J(x))(1 + J(y)) - 2 for positive reals x and y. Analysts deriving multiplicative cost estimates in Recognition Science cite it when controlling growth under scaling. The proof invokes the submultiplicative form of d'Alembert's identity and rewrites the right-hand side by ring algebra.
claimFor all real numbers $x, y > 0$, $J(xy) ≤ 2(1 + J(x))(1 + J(y)) - 2$, where the function $J$ is given by $J(z) = (z + z^{-1})/2 - 1$.
background
Jcost is the function defined by J(z) = (z + z^{-1})/2 - 1. The Cost module develops cost functions compatible with the Recognition Composition Law. The lemma rests on the upstream result Jcost_submult, which asserts J(xy) ≤ 2J(x) + 2J(y) + 2J(x)J(y) because J(x/y) is nonnegative by the d'Alembert identity.
proof idea
The proof applies Jcost_submult to obtain J(xy) ≤ 2J(x) + 2J(y) + 2J(x)J(y). It then rewrites the right-hand side as 2(1 + J(x))(1 + J(y)) - 2 via the ring tactic.
why it matters in Recognition Science
This lemma supplies an explicit multiplicative bound on J-cost derived from d'Alembert submultiplicativity. It supports product estimates inside the Cost module of the Recognition framework, where J-uniqueness appears in the forcing chain. No downstream uses are recorded, indicating it functions as an intermediate tool for further cost calculations.
scope and limits
- Does not apply when x or y is non-positive.
- Does not assert equality or sharpness of the bound.
- Does not extend automatically to products of three or more factors.
- Does not address the special case x = 1 or y = 1.
formal statement (Lean)
527lemma Jcost_prod_bound {x y : ℝ} (hx : 0 < x) (hy : 0 < y) :
528 Jcost (x * y) ≤ 2 * (1 + Jcost x) * (1 + Jcost y) - 2 := by
proof body
Tactic-mode proof.
529 have h := Jcost_submult hx hy
530 -- 2*(1+J(x))*(1+J(y)) - 2 = 2*(1 + J(x) + J(y) + J(x)*J(y)) - 2
531 -- = 2 + 2*J(x) + 2*J(y) + 2*J(x)*J(y) - 2
532 -- = 2*J(x) + 2*J(y) + 2*J(x)*J(y)
533 calc Jcost (x * y) ≤ 2 * Jcost x + 2 * Jcost y + 2 * Jcost x * Jcost y := h
534 _ = 2 * (1 + Jcost x) * (1 + Jcost y) - 2 := by ring
535
536/-! ## Small-strain Taylor expansion -/
537