canonicalSigma
plain-language theorem explainer
The definition supplies the canonical sigma functional as the sum of natural logarithms over the components of a real vector of length n. Researchers constructing recognition cost systems cite it when completing the quadruple of positive reals, J-cost, sigma, and wallpaper number W. The implementation consists of a direct summation matching the conservation functional stated in Definition 2.7.
Claim. Let $n$ be a natural number and let $x=(x_1,…,x_n)$ be a vector in $ℝ^n$. The canonical sigma is the map $σ(x)=∑_{i=1}^n log x_i$ (defined on positive coordinates).
background
The CostAlgebra module assembles the algebraic structure for recognition costs. It uses the J-cost induced by a multiplicative recognizer, which satisfies the Recognition Composition Law J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y). The canonical sigma is introduced as the conservation functional that completes the cost system quadruple together with J and the wallpaper number W. Upstream, the canonical arithmetic object supplies the initial Peano structure that remains realization-independent at this stage.
proof idea
The definition is a direct one-line sum that applies the summation operator to the natural logarithm of each coordinate over the finite index set.
why it matters
This definition supplies the sigma component required by canonicalRecognitionCostSystem, which assembles the full recognition cost system on the positive reals. It realizes the conservation functional needed in the Recognition framework and supports the forcing chain steps that derive J-uniqueness, the self-similar fixed point phi, the eight-tick octave, and three spatial dimensions. The result feeds the mass ladder and the alpha band (137.030,137.039) without introducing new open questions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.