meanLevel
plain-language theorem explainer
Arithmetic mean of a finite field of recognition levels: total level sum divided by the number of sites. Cosmology and forward-dynamics proofs cite it as the conserved centre that pair resolution leaves fixed and about which variance is measured. The body is a one-line quotient of the already-defined level sum by cardinality.
Claim. For a finite configuration $x:\{0,\ldots,n-1\}\to\mathbb{R}$, the mean level is $\overline{x}:=\frac{1}{n}\sum_{k} x_k$, i.e. the level sum divided by the number of sites.
background
The module formalizes Phase-7 forward dynamics on a field of recognition levels $x:\mathrm{Fin},n\to\mathbb{R}$. Each tick forces a recognition event that resolves a coupled pair $(i,j)$ by sending both endpoints to their mean (the $\sigma=0$, $J$-minimal move). The conserved bulk quantity is the level sum $\sum_k x_k$; the mean is that sum normalized by $n$.
Variance is defined as spread about this mean and serves as the Lyapunov function of the descent: each resolution lowers variance by exactly $(x_i-x_j)^2/2$. The mean is therefore the natural centre for measuring that spread and for stating conservation under pair resolution.
Upstream, levelSum is the un-normalized sum. The module reuses $J$-cost nonnegativity from RefineTrigger and $\varphi$ from Constants; no new axioms.
proof idea
Pure definition: unfold as level sum divided by $n$ cast to $\mathbb{R}$. No tactics, no lemmas. Downstream proofs that need mean conservation simply rewrite with the companion fact that pair resolution preserves the level sum, hence preserves the mean.
why it matters
Anchors the Lyapunov analysis of recognition equilibrium. Variance is defined as spread about this mean; the theorem that pair resolution preserves the mean is the first rewrite step in the exact variance drop law (decrement $(x_i-x_j)^2/2$). That law is the module's central convergence fact: strict descent until every coupled pair is equal, with ground state exactly the consensus configuration where total recognition cost vanishes.
In the broader RS picture this is the closed-system half of cosmogenesis dynamics: resolutions conserve $\sigma$ (via level-sum, hence mean), while conjugate births supply the open input that keeps structure from homogenizing. Without a fixed mean, the variance Lyapunov statement would not close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.