dot_log_hadamardDiv
plain-language theorem explainer
dot_log_hadamardDiv establishes that the weighted logarithmic aggregate of a componentwise quotient equals the difference of the aggregates on numerator and denominator. Cost modelers in Recognition Science cite it when decomposing reciprocal terms inside n-dimensional J-cost expressions. The proof unfolds the vector operations then applies the real logarithm quotient identity followed by summation linearity.
Claim. $∑_{i} α_i log(x_i / y_i) = ∑_{i} α_i log x_i - ∑_{i} α_i log y_i$ for weight vector α and positive component vectors x, y in ℝ^n.
background
Module Cost.Ndim.Core lifts the scalar kernel to n dimensions by defining the weighted log aggregate. Vec n is the type Fin n → ℝ. dot α t is the sum ∑ α_i t_i. logVec applies the natural logarithm to each component. hadamardDiv forms the componentwise quotient x_i / y_i. aggregate is then defined as exp(dot α logVec x).
proof idea
Tactic-mode calc proof. Unfold dot, logVec and hadamardDiv. Rewrite the summand via Real.log_div using the positivity hypotheses. Distribute multiplication inside the sum with ring. Split the resulting difference of sums via Finset.sum_sub_distrib.
why it matters
Feeds JcostN_dAlembert, which encodes the n-dimensional form of the Recognition Composition Law. The identity closes the log-division step required to lift scalar J-cost addition formulas to vector aggregates. It supports the phi-ladder and eight-tick octave constructions by guaranteeing consistent cost decomposition across dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.