Cost Ndim Core Dot Log Hadamard Div

The quotient rule

The declaration dot_log_hadamardDiv is a theorem in the Recognition Science framework's machine-checked library of formal theorems. It concerns the weighted log aggregate, a tool that combines several positive numbers into one representative value. The theorem states that the log aggregate of a componentwise quotient equals the difference of the log aggregates: log(x/y) = log(x) - log(y), applied separately to each component and then summed with weights. In plain terms, dividing two vectors component by component, then taking the weighted log sum, gives the same result as subtracting their individual weighted log sums.

This is the multi-dimensional analogue of the familiar logarithm rule from high school algebra, lifted into the framework's cost structure. The framework models recognition costs as functions of positive vectors, and this theorem is a building block for showing how those costs behave under scaling and inversion. It is one of several similar lemmas: multiplication becomes addition, inversion becomes negation, and division becomes subtraction, all in the log-coordinate view. These identities are what allow the framework to treat ratios of components as differences of logarithms, a step that appears in later derivations.

The theorem is proved in the Lean 4 proof assistant, and the proof is axiom-clean, meaning it relies only on the standard axioms of the underlying type theory. The declaration itself is a theorem, not a definition or a hypothesis. It does not, however, claim anything about the physical meaning of the weights, the values of the components, or the interpretation of the aggregate as a cost. It is a purely formal statement about real numbers and logarithms, valid for any positive vectors and any real weights.

/-- Log-aggregate of a componentwise quotient. -/
theorem dot_log_hadamardDiv {n : ℕ} (α x y : Vec n)
    (hx : ∀ i, 0 < x i) (hy : ∀ i, 0 < y i) :
    dot α (logVec (hadamardDiv x y)) = dot α (logVec x) - dot α (logVec y) := by
  unfold dot logVec hadamardDiv
  calc
    ∑ i : Fin n, α i * Real.log (x i / y i)
        = ∑ i : Fin n, α i * (Real.log (x i) - Real.log (y i)) := by
            refine Finset.sum_congr rfl ?_
            intro i hi
            rw [Real.log_div (show x i ≠ 0 from (hx i).ne') (show y i ≠ 0 from (hy i).ne')]
    _ = ∑ i : Fin n, (α i * Real.log (x i) - α i * Real.log (y i)) := by
          refine Finset.sum_congr rfl ?_
          intro i hi
          ring
    _ = (∑ i : Fin n, α i * Real.log (x i)) - (∑ i : Fin n, α i * Real.log (y i)) := by
          simp [Finset.sum_sub_distrib]

What this page does not claim

The theorem does not assign physical meaning to the weights or components. The theorem does not prove any property of the full cost function beyond the algebraic identity itself. The theorem does not address what happens when any component is zero or negative.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Cost/Ndim/Core.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: