pith. sign in
module module high

IndisputableMonolith.Cost.Ndim.Calibration

show as:
view Lean formalization →

Calibration module establishes that uniform weights summing to one each equal 1/n for n>0. Researchers on N-dimensional reciprocal costs cite it to normalize coefficients before symmetry arguments. The results follow by direct reduction to the weightSum definition imported from Core.

claimIf weights $w$ are uniform with $\sum_{i=1}^n w_i=1$ and $n>0$, then $w_i=1/n$ for each $i$.

background

The module sits inside the N-dimensional reciprocal cost setting introduced in Core, where the scalar kernel is lifted through a weighted log aggregate. It supplies auxiliary definitions weightSum, sqNorm and the UniformWeights predicate together with their uniform-case lemmas. The upstream Core module supplies the foundational lifting of the J-cost function into multiple components.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

Supplies the uniform-weight normalization used by the Symmetry module to establish permutation symmetry of coefficient weights. It provides the base normalization step required before any symmetry or invariance arguments in the N-dimensional cost framework.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (7)