JcostN_submult
plain-language theorem explainer
The lemma establishes a submultiplicative bound on the n-dimensional J-cost under Hadamard multiplication of positive vectors. Researchers working on multidimensional extensions of the Recognition Composition Law would cite this result when bounding costs in product spaces. The proof is a one-line wrapper that subtracts the non-negative J-cost of the componentwise quotient from the d'Alembert identity.
Claim. For any natural number $n$, vector $α ∈ ℝ^n$, and positive vectors $x, y ∈ ℝ^n$ (all components strictly positive), the n-dimensional cost satisfies $JcostN(α, x ⊙ y) ≤ 2 JcostN(α, x) + 2 JcostN(α, y) + 2 JcostN(α, x) JcostN(α, y)$, where ⊙ denotes the Hadamard (componentwise) product.
background
Vec n is the type of n-component real vectors as functions from Fin n to ℝ. hadamardMul x y computes the componentwise product of two such vectors, while hadamardDiv computes the componentwise quotient. JcostN α x is the original positive-coordinate n-dimensional cost, defined via JlogN α (logVec x). The module supplies the multidimensional d'Alembert / RCL identity. The key upstream result JcostN_dAlembert states that JcostN α (hadamardMul x y) + JcostN α (hadamardDiv x y) equals the right-hand side expression 2 JcostN α x + 2 JcostN α y + 2 JcostN α x JcostN α y under the positivity hypotheses.
proof idea
The proof invokes JcostN_dAlembert to obtain the equality relating the product and quotient costs to the target expression. It then applies JcostN_nonneg to the quotient term to establish non-negativity, and concludes the desired inequality by linear arithmetic (linarith).
why it matters
This lemma supplies the inequality form of the multidimensional Recognition Composition Law, obtained by dropping the non-negative quotient term from the equality in JcostN_dAlembert. It supports bounding arguments in the cost framework for n-dimensional spaces and aligns with the RCL identity J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y) from the forcing chain. No downstream uses are recorded, but it closes the submultiplicative property for the J-cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.