levelSum
plain-language theorem explainer
The total sum of recognition levels on a finite configuration x : Fin n → ℝ; this is the conserved sigma of the Phase-7 forward dynamics. Cosmology and descent arguments cite it whenever pair resolution or mean-level statistics appear. It is the ordinary sum over Fin n, marked noncomputable only because the codomain is ℝ.
Claim. For $n \in \mathbb{N}$ and a level field $x : \{0,\ldots,n-1\} \to \mathbb{R}$, the level sum (sigma) is $\sum_{k} x_k$.
background
The module formalizes Phase-7 forward dynamics on a field of recognition levels $x : \mathrm{Fin}, n \to \mathbb{R}$. Each tick resolves one coupled pair $(i,j)$ by sending both endpoints to their arithmetic mean: the unique sigma-preserving, $J$-minimal move. The module proves that this resolution conserves the level sum, drops variance by exactly $(x_i - x_j)^2/2$, and that the zero of total recognition cost is consensus on every edge.
Sigma is this total level sum. Mean level is sigma divided by $n$; variance is the Lyapunov function of the closed-system descent. In the open (driven) extension, conjugate births $(\pm u)$ also conserve charge sum, so sigma $= 0$ can be maintained through the whole evolution. $J$-cost and $\varphi$ are imported from RefineTrigger and Constants; no new axioms.
proof idea
Pure definition: unfold to the Mathlib sum $\sum_{k : \mathrm{Fin}, n} x, k$. No lemmas, no tactics. Downstream proofs (e.g. pair-resolve conservation) unfold this name and split the sum into the resolved pair plus the complementary indices.
why it matters
Sigma is the conserved quantity that makes the forward dynamics a constrained descent rather than an arbitrary flow. The Equilibrium package records three laws: sigma conserved under every pair resolve, exact variance drop, and variance nonincreasing; all three mention this sum. meanLevel is defined as levelSum$/n$, so every mean-centered variance identity routes through it. pairResolve_levelSum is the first discharged convergence fact of the Python cosmogenesis script: resolving a pair leaves the total level unchanged.
In the broader Recognition chain this is the continuum bookkeeping dual of charge conservation under eight-tick cadence and conjugate birth. Closed-system descent relaxes to consensus; conserved-sigma births are the forced open input that keeps non-homogeneous structure alive. No forcing-chain step (T5–T8) is proved here; the declaration only names the quantity those dynamics conserve.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.