Cost Ndim Bridge Multiplicative Quadratic

Quadratic bridge

In recognition, the framework's word for the act of matching an observation to an expected pattern, a cost function assigns a number to how far off the match is. The declaration multiplicativeQuadratic defines one such measure: half the square of the dot product between a vector of weights α and a vector of errors ε. It is called multiplicative because the errors enter through their product with the weights, not as separate squared terms.

The plain alternative is additiveQuadratic, which is half the sum of the squared errors, treating each component independently. The framework proves a bridge between the two: the additive cost always equals the multiplicative cost plus a leftover term called compensatoryQuadratic. This is not a numerical coincidence but an identity, written as additiveQuadratic ε = multiplicativeQuadratic α ε + compensatoryQuadratic α ε, and it holds for any number of components n.

The identity gains teeth from a classical inequality. Cauchy-Schwarz, the standard result that the square of a dot product never exceeds the product of the squared lengths, gives the bound (dot α ε)² ≤ (dot α α) * (sum of εᵢ²). When the weights are normalized so that dot α α ≤ 1, the multiplicative cost is always at most the additive cost, and the compensatory term is never negative. In words: with weights kept small, the multiplicative view never overestimates the error that the additive view reports.

In Recognition Science, this bridge is a definitional scaffold, not a physical law. It sets up how a multidimensional recognition error can be decomposed into a weighted projection and a residual, a structure later theory builds on. The declarations are formal definitions in the framework's machine-checked library of formal theorems, and the identity and bounds are proved there. What the bridge does not do is force any particular value for the weights α, nor does it say how recognition errors arise in the first place.

theorem additive_decomposition {n : ℕ} (α ε : Vec n) :
    additiveQuadratic ε
      = multiplicativeQuadratic α ε + compensatoryQuadratic α ε := by
  unfold compensatoryQuadratic
  ring

/-- If `‖α‖² ≤ 1`, multiplicative quadratic cost is bounded by additive quadratic cost. -/
theorem multiplicative_le_additive_of_sqNorm_le_one {n : ℕ}
    (α ε : Vec n) (hα : dot α α ≤ 1) :
    multiplicativeQuadratic α ε ≤ additiveQuadratic ε := by
  have hsq : (dot α ε) ^ 2 ≤ ∑ i : Fin n, (ε i) ^ 2 := by
    have hcs : (dot α ε) ^ 2 ≤ (dot α α) * (∑ i : Fin n, (ε i) ^ 2) :=
      dot_sq_le_sqNorm_mul α ε
    have hsum_nonneg : 0 ≤ ∑ i : Fin n, (ε i) ^ 2 := by
      exact Finset.sum_nonneg (fun i _ => sq_nonneg (ε i))
    have hmul : (dot α α) * (∑ i : Fin n, (ε i) ^ 2) ≤ 1 * (∑ i : Fin n, (ε i) ^ 2) :=
      mul_le_mul_of_nonneg_right hα hsum_nonneg
    exact le_trans hcs (by simpa using hmul)
  have hhalf : (0 : ℝ) ≤ 1 / 2 := by norm_num
  have hscaled := mul_le_mul_of_nonneg_left hsq hhalf
  simpa [multiplicativeQuadratic, additiveQuadratic, one_mul] using hscaled

/-- Under normalized weights (`‖α‖² ≤ 1`), the compensatory term is nonnegative. -/
theorem compensatory_nonneg_of_sqNorm_le_one {n : ℕ}
    (α ε : Vec n) (hα : dot α α ≤ 1) :
    0 ≤ compensatoryQuadratic α ε := by
  unfold compensatoryQuadratic
  have hle := multiplicative_le_additive_of_sqNorm_le_one α ε hα
  linarith

What this page does not claim

The bridge does not determine the weight vector α from any principle. It does not establish that recognition errors are quadratic in nature. It does not connect the multiplicative cost to the one-dimensional cost function J(x).

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/Bridge.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: