JcostN_dAlembert
plain-language theorem explainer
The N-dimensional d'Alembert identity equates JcostN on the componentwise product plus JcostN on the componentwise quotient to twice the sum of the separate JcostN values plus twice their product. Researchers extending the Recognition Composition Law to vector inputs for the phi-ladder mass formulas would cite this when deriving submultiplicative bounds on costs. The argument maps the weighted log-aggregates to positive scalars u and v, reduces the vector equation to the scalar dalembert_identity, and substitutes the definitions back.
Claim. Let $J_α(z)$ denote the N-dimensional J-cost $J(∏_i z_i^{α_i})$ for weight vector $α ∈ ℝ^n$. For positive vectors $x, y ∈ ℝ^n$, $J_α(x ⊙ y) + J_α(x ⊘ y) = 2 J_α(x) + 2 J_α(y) + 2 J_α(x) J_α(y)$, where ⊙ and ⊘ are the componentwise product and quotient.
background
The module develops the multidimensional d'Alembert identity as the vector form of the Recognition Composition Law. Core definitions are the weighted dot product dot(α, t) = ∑ α_i t_i, the Hadamard product with components x_i y_i, the Hadamard quotient with components x_i / y_i, and the N-dimensional cost JcostN(α, z) = Jcost(exp(dot(α, log z))), where Jcost is the base scalar function. The local setting is the extension of the one-dimensional RCL to arbitrary dimension n under the positivity hypotheses on x and y.
proof idea
Introduce scalars u = exp(dot α (log x)) and v = exp(dot α (log y)). Apply dot_log_hadamardMul and dot_log_hadamardDiv to obtain JcostN α (hadamardMul x y) = Jcost(u v) and JcostN α (hadamardDiv x y) = Jcost(u / v). Invoke the scalar dalembert_identity on u and v to reach the target right-hand side in terms of Jcost u and Jcost v, then rewrite those terms as JcostN α x and JcostN α y by definition of JcostN.
why it matters
This supplies the exact equality used by the downstream lemma JcostN_submult to obtain the submultiplicative bound JcostN(α, x ⊙ y) ≤ 2 JcostN(α, x) + 2 JcostN(α, y) + 2 JcostN(α, x) JcostN(α, y) via non-negativity of the quotient term. It extends the scalar dalembert_identity to the vector setting required for the Recognition Composition Law in the phi-ladder and eight-tick octave constructions. No open scaffolding remains in this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.