Cost Ndim Calibration

Uniform weight calibration

Recognition cost in Recognition Science can involve many dimensions at once. A vector of weights, one per dimension, records how much each direction contributes to the total cost. Calibration is the step that turns a bare vector into a definite scale: it imposes a constraint, such as the weights summing to one or the squared norm equaling one, and then solves for what each weight must be.

When the weights are uniform, meaning every entry has the same value, the solution is exact and unique. If the weights sum to one and there are n dimensions with n greater than zero, each weight must equal 1/n. If instead the squared norm is one, each weight squared equals 1/n. Both results are established in Lean 4 without assumptions beyond the uniform condition and the chosen constraint.

These theorems give the calibration a fixed meaning: uniform weights under a unit total are not arbitrary, they are forced to a single value. The same holds for unit squared norm, which ties each weight to the inverse square root of the dimension count. This is what the module establishes in plain language: under uniform weights, the calibration constraint determines the weight scale completely.

THEOREM uniform_weight_of_sum_one · IndisputableMonolith/Cost/Ndim/Calibration.lean

THEOREM uniform_sqNorm_one · IndisputableMonolith/Cost/Ndim/Calibration.lean

What this page does not claim

Not a derivation of the full cost function J(x). Not a claim about non-uniform weights. Not a physical measurement or empirical check.

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: