Cost Ndim Bridge Additive Decomposition

The bridge identity

In mathematics, a quadratic form is a polynomial where every term has degree two, like x² or x² + y². The declaration additive_decomposition proves a basic identity about two such forms. For any list of numbers ε and any list of weights α, the sum of the squares of ε, multiplied by one half, equals the square of the weighted sum, multiplied by one half, plus a leftover term. In symbols: (1/2)Σεᵢ² = (1/2)(Σαᵢεᵢ)² + [(1/2)Σεᵢ² − (1/2)(Σαᵢεᵢ)²]. The leftover term is called the compensatory term, and the identity says it is exactly the difference between the two quadratic forms.

The identity itself is a tautology: it simply rearranges the definition of the compensatory term. Its meaning comes from the framework. In Recognition Science, the cost of a recognition event is a number that measures how far a guess is from reality. The additive quadratic form treats each component of the error separately and adds their squares. The multiplicative quadratic form first combines the components through a weighted sum, then squares the result. The identity says these two ways of measuring error differ by an explicit term, and the difference is controlled by the weights.

The framework's library proves more. When the weights are normalized so that the sum of their squares is at most one, the multiplicative cost is always less than or equal to the additive cost. Consequently, the compensatory term is never negative under that condition. This is a direct consequence of the Cauchy-Schwarz inequality, which bounds the square of a dot product by the product of the squared norms. The library states and proves this bound explicitly.

In Recognition Science, this bridge identity is a step toward extending the one-dimensional cost function, which is forced to be J(x) = (x + 1/x)/2 − 1, to many dimensions. The additive and multiplicative forms are two candidate generalizations, and the identity shows how they relate. It does not, however, prove that either form is the correct multi-dimensional cost. It does not derive the one-dimensional J from these forms, and it does not establish any physical law. It is a lemma about quadratic forms, not a theorem about recognition.

What the identity changes is the vocabulary. It gives the framework a precise way to speak about the gap between two natural generalizations, and it provides a bound on that gap. That bound, in turn, is what later work can use to compare candidate cost functions. The identity is a tool, not a result.

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

This does not prove that either quadratic form is the unique multi-dimensional cost function. This does not derive the one-dimensional cost function J from the additive or multiplicative forms. This does not establish any physical law or empirical prediction.

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: