Cost Ndim Bridge Dot Sq Le Sq Norm Mul

The squared dot-product bound

The Cauchy-Schwarz inequality is one of the oldest workhorses of linear algebra. In its squared form, for any two vectors α and ε, the square of their dot product is at most the product of their squared norms: (α·ε)² ≤ (α·α)(ε·ε). This is not a new fact; it is a standard result taught in every first course. What the Recognition Science library adds is a machine-checked proof of this exact inequality, written in the framework's own notation for vectors and dot products. The declaration dot_sq_le_sqNorm_mul establishes precisely this bound: for any natural number n and any two n-dimensional real vectors α and ε, the square of the dot product is bounded above by the product of the squared norm of α and the sum of the squares of the components of ε.

The proof is not a long chain of novel reasoning. It unfolds the definition of the dot product and then applies a pre-existing lemma about sums of squares, Finset.sum_mul_sq_le_sq_mul_sq. In plain terms, the machine checks that the squared dot product inequality follows directly from the sum version of Cauchy-Schwarz. The declaration is a formal bridge: it connects the framework's own vocabulary of vectors and dot products to a classical inequality that mathematicians have used for over a century. This matters because the framework's later cost definitions rely on this bound to compare two quadratic forms, the additive and the multiplicative, and to show that under a normalization condition one never exceeds the other.

In Recognition Science, the framework uses this inequality to reason about cost, a measure of how much a recognition event deviates from a perfect match. Two quadratic approximations appear: an additive one that sums the squares of errors, and a multiplicative one that squares a weighted sum. The bound dot_sq_le_sqNorm_mul is the tool that lets the framework prove that when the weight vector α has squared norm at most one, the multiplicative cost is never larger than the additive cost. A second theorem, multiplicative_le_additive_of_sqNorm_le_one, states this comparison directly, and a third, compensatory_nonneg_of_sqNorm_le_one, shows the difference, the compensatory term, is nonnegative under the same condition.

What the declaration does not claim is anything about the framework's deeper structure. It does not prove the uniqueness of the cost function J, it does not derive the golden ratio, and it does not force three spatial dimensions. It is a single, narrow, classical inequality, formally verified. The theorem is true for any real vectors, with no additional assumptions about recognition, ledgers, or physics. It is a piece of standard mathematics, placed inside the framework's library so that later arguments can use it as a trusted step. The payoff is not a new mathematical discovery but a verified foundation: when the framework later compares costs, it can rely on this bound without rechecking the algebra.

/-- 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

The declaration does not prove the uniqueness of the cost function J or any result about the golden ratio. The inequality is classical Cauchy-Schwarz, not a new framework-specific discovery. The theorem applies to arbitrary real vectors, not only to vectors arising from recognition processes.

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: