Cost Ndim Calibration Sq Norm

The squared norm

The squared norm is a standard way to measure the size of a vector: add the squares of its entries. For a vector α with n entries, it is written as the dot product of α with itself, ∑ αᵢ². In the Recognition Science framework, this quantity appears in the calibration of recognition costs, the price a system pays for registering an event in its ledger.

The framework's machine-checked library of formal theorems defines this squared norm and proves what happens when all entries of the vector are equal, a condition it calls uniform weights. If every entry is the same number a, then the squared norm is exactly n times a². If the entries are uniform and their sum is 1, then each entry must be 1/n. If, in addition, the squared norm itself is 1, then a² equals 1/n. These are simple algebraic facts, each proved in the library.

In Recognition Science, these facts support a calibration step: when costs are spread evenly across n dimensions and the total cost is fixed, the per-dimension cost scales as 1/n. The squared norm is the tool that makes this scaling explicit. The declaration sqNorm establishes the definition and the uniform-weight theorems that follow from it.

What sqNorm does not claim is any physical content. It does not say that costs must be uniform, that n must be three, or that the squared norm is the only possible cost measure. It is a definitional building block, not a law of nature. The theorems about uniform weights are conditional: they hold when the uniformity assumption is supplied.

theorem sqNorm_uniform {n : ℕ} {α : Vec n}
    (hU : UniformWeights α) :
    ∃ a : ℝ, sqNorm α = (n : ℝ) * a ^ 2 := by
  rcases hU with ⟨a, ha⟩
  refine ⟨a, ?_⟩
  unfold sqNorm dot
  simp [ha, pow_two, Finset.card_univ]

/-- If weights are uniform and sum to one, each weight is `1/n` (for `n > 0`). -/
theorem uniform_weight_of_sum_one {n : ℕ} {α : Vec n}
    (hn : 0 < n) (hU : UniformWeights α) (hsum : weightSum α = 1) :
    ∃ a : ℝ, (∀ i : Fin n, α i = a) ∧ a = 1 / (n : ℝ) := by
  rcases hU with ⟨a, ha⟩
  have hna : (n : ℝ) ≠ 0 := by
    exact_mod_cast (Nat.ne_of_gt hn)
  have hsum' : (n : ℝ) * a = 1 := by
    simpa [weightSum, ha, Finset.card_univ] using hsum
  have ha_val : a = 1 / (n : ℝ) := by
    apply (eq_div_iff hna).2
    linarith [hsum']
  exact ⟨a, ha, ha_val⟩

/-- Under uniform weights, unit squared norm gives `a² = 1/n` (for `n > 0`). -/
theorem uniform_sqNorm_one {n : ℕ} {α : Vec n}
    (hn : 0 < n) (hU : UniformWeights α) (hcurv : sqNorm α = 1) :
    ∃ a : ℝ, (∀ i : Fin n, α i = a) ∧ a ^ 2 = 1 / (n : ℝ) := by
  rcases hU with ⟨a, ha⟩
  have hna : (n : ℝ) ≠ 0 := by
    exact_mod_cast (Nat.ne_of_gt hn)
  have hnorm : (n : ℝ) * a ^ 2 = 1 := by
    simpa [sqNorm, dot, ha, pow_two, Finset.card_univ] using hcurv
  have hsquare : a ^ 2 = 1 / (n : ℝ) := by
    apply (eq_div_iff hna).2
    linarith [hnorm]
  exact ⟨a, ha, hsquare⟩

What this page does not claim

The squared norm does not prove that costs must be uniform. The squared norm does not determine the number of dimensions n. The squared norm is not claimed to be the only possible cost measure.

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