Cost Ndim Bridge Additive Quadratic

The additive quadratic cost

In mathematics, a quadratic form is a polynomial where every term has degree two, such as x² + y². The Recognition Science declaration additiveQuadratic defines one such form for any number of dimensions: it takes a vector of residuals, squares each entry, sums them, and multiplies by one half. Written out, for a vector ε with n components, the cost is (1/2) * (ε₁² + ε₂² + ... + εₙ²). This is the simplest smooth way to penalize errors, and it appears throughout statistics and physics as the basis of least squares and energy calculations.

The declaration also introduces two related forms. multiplicativeQuadratic squares a weighted sum of the residuals, (1/2) * (α·ε)², where α is a vector of weights. compensatoryQuadratic is simply their difference, additive minus multiplicative. A proved theorem, additive_decomposition, states that the additive form always equals the multiplicative form plus the compensatory term. This is an algebraic identity, true for any vectors α and ε, and it holds because the definitions are built that way.

The framework proves more than the identity. A second theorem, dot_sq_le_sqNorm_mul, is the squared Cauchy-Schwarz inequality: the square of a dot product is at most the product of the squared norms. From this, the library derives a comparison: if the weights α satisfy ||α||² ≤ 1, then the multiplicative quadratic cost is always less than or equal to the additive quadratic cost. A corollary states that under the same condition, the compensatory term is nonnegative, meaning the additive cost is the larger of the two.

In Recognition Science, this matters because cost is the forced price of a recognition event, and the framework's central theorem forces a specific one-dimensional cost function. The additive quadratic form is a candidate for extending that cost to multiple dimensions, and these declarations establish its basic algebraic behavior. What they do not establish is that this form is the unique or forced cost in higher dimensions. The one-dimensional uniqueness theorem does not automatically generalize, and no such forcing result appears in this file.

The practical upshot is a clean, machine-checked toolkit for comparing two natural quadratic costs. A reader can rely on the decomposition identity and the inequality as proved facts, usable in any further argument about multi-dimensional recognition costs. The question of which cost the framework actually forces in n dimensions remains open, and these definitions are the groundwork, not the answer.

/-- Quadratic additive approximation `1/2 * Σ εᵢ²`. -/
noncomputable def additiveQuadratic {n : ℕ} (ε : Vec n) : ℝ :=
  (1 / 2 : ℝ) * ∑ i : Fin n, (ε i) ^ 2

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

/-- Squared Cauchy-Schwarz bound in our notation. -/
theorem dot_sq_le_sqNorm_mul {n : ℕ} (α ε : Vec n) :
    (dot α ε) ^ 2 ≤ (dot α α) * (∑ i : Fin n, (ε i) ^ 2) := by
  unfold dot
  simpa [pow_two] using
    (Finset.sum_mul_sq_le_sq_mul_sq (s := (Finset.univ : Finset (Fin n))) α ε)

/-- 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 declaration does not prove that additiveQuadratic is the unique or forced cost in n dimensions. The one-dimensional uniqueness theorem for J does not automatically apply to this multi-dimensional form. No claim is made here about which multi-dimensional cost the framework ultimately forces.

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: