Jcost_prod_bound
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.