hadamardMul
plain-language theorem explainer
Componentwise multiplication on n-dimensional vectors supplies the Hadamard product needed to lift scalar J-cost to vector aggregates. Researchers extending the Recognition Composition Law to multiple components cite this construction when proving d'Alembert-type identities. The definition is a direct pointwise operation on coordinate functions from Fin n to reals.
Claim. For vectors $x, y : Fin n → ℝ$, the componentwise product $x ⊙ y$ is defined by $(x ⊙ y)_i = x_i y_i$ for each $i : Fin n$.
background
Vec is the abbreviation for n-component real vectors represented as coordinate functions Fin n → ℝ. The module defines the multi-component reciprocal cost by lifting the scalar kernel through a weighted log aggregate. The single upstream dependency is the Vec abbreviation itself, which supplies the function representation used for all subsequent dot products and logarithmic transforms.
proof idea
The definition is a direct pointwise operation that maps each coordinate i to the ordinary product of the input coordinates at i.
why it matters
This definition feeds the componentwise product into the proofs of dot_log_hadamardMul, JcostN_dAlembert, and JcostN_submult, which together establish the Recognition Composition Law in n dimensions. It thereby supports the extension of T5 J-uniqueness and the eight-tick octave structure to vector-valued costs. The construction closes the multiplicative step required before the phi-ladder mass formulas can be applied componentwise.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.