Cost Ndim Bridge

The quadratic bridge

The cost ndim bridge is a machine-checked relation inside Recognition Science's cost ledger. It connects two ways of writing a quadratic cost over a vector of recognition errors. The additive form, additive quadratic, is half the sum of the squared errors. The multiplicative form, multiplicative quadratic, is half the square of a weighted sum of the same errors, using a weight vector. The bridge is the identity that the additive form always equals the multiplicative form plus a third term, the compensatory quadratic.

That identity is established as a theorem: for any dimension and any weight vector, the additive quadratic cost decomposes exactly into the multiplicative quadratic cost plus the compensatory term. The proof is a direct algebraic expansion, tagged THEOREM. The same module establishes a second fact: when the weight vector has squared norm at most one, the multiplicative cost is bounded above by the additive cost. From that bound follows the third result, that the compensatory term is nonnegative under the same normalization.

In plain language, the bridge says that a multiplicative reading of errors never exceeds the additive reading when weights are normalized, and the gap between them is always a nonnegative remainder. The remainder is what the multiplicative form leaves out. The module does not yet connect this decomposition to the forcing chain that fixes the cost function J, nor does it say how the weight vector is chosen. Those links remain open.

THEOREM additive_decomposition · IndisputableMonolith/Cost/Ndim/Bridge.lean

THEOREM multiplicative_le_additive_of_sqNorm_le_one · IndisputableMonolith/Cost/Ndim/Bridge.lean

THEOREM compensatory_nonneg_of_sqNorm_le_one · IndisputableMonolith/Cost/Ndim/Bridge.lean

What this page does not claim

No claim that the weight vector is derived from the forcing chain. No claim that the bridge fixes the cost function J. No claim that the bridge establishes three spatial dimensions.

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: