unitaryWeight_norm
plain-language theorem explainer
For every real action S on the bounded configuration class and every labeled complex K, the unitary weight exp(i S(K)) has complex modulus exactly 1. Anyone assembling the scoped Z_RS path sum or bounding individual summands cites this. The proof is a one-line application of the standard identity ‖exp(i θ)‖ = 1 for real θ.
Claim. Fix a size bound $B\in\mathbb{N}$, a real action $S$ on the class of bounded combinatorial complexes of size at most $B$, and a configuration $K$ in that class. The unitary weight $w(K)=\exp(i\,S(K))$ satisfies $\|w(K)\|=1$.
background
Lane 2 of the Seven Gaps program builds a proved path-sum measure for $Z_{RS}$ on a scoped configuration class. Configurations are BoundedComplex B: combinatorial incidence data (vertices, edges, tetrahedra) capped by a fixed lattice-scale bound $B$, with the metric field dropped so every edge sits at the substrate mesh. This is the CDT-style equilateral class used throughout the module.
The path sum is $Z=\sum_K \mu(K),w(K)$ with symmetry factor $\mu(K)=1/|\mathrm{Aut},K|$. The unitary instance takes $w(K)=\exp(i,S(K))$ for a real action $S$. Unit modulus of each weight is the elementary input that turns the already-proved measure bounds $|Z|\le\sum\mu$ and $|Z|\le\mathrm{card}$ into statements about $Z_{RS}$ itself.
No Recognition-Science forcing step is invoked here: the claim is pure complex analysis on the weight, independent of the J-cost, $\varphi$-ladder, or eight-tick structure.
proof idea
One-line term proof. Apply the Mathlib identity Complex.norm_exp_I_mul_ofReal at the real number $S(K)$: for any real $\theta$, $|\exp(i\theta)|=1$. Instantiating $\theta:=S(K)$ yields $|\mathrm{unitaryWeight},S,K|=1$ with no further casework.
why it matters
This is the first of the four conjuncts in zRS_scoped_wellDefined, the honest scoped $Z_{RS}$ theorem: unit-modulus weights, relabeling invariance of the weight, the UV bound $|Z_{RS}|\le\mathrm{card}$, and invariance under equivalence-preserving reindexing. Without unit modulus the card bound would not specialize to the unitary instance.
It is also the rewrite step inside unnormalized_torus_weight_suppressed, the panel-mandated landmine: every $\mu$-weighted unitary summand of the embedded Freudenthal torus is forced to modulus $\le N^{-3}$. That rejection criterion multiplies $\mu$ by the unitary weight and collapses the weight norm via this lemma.
In the broader RS gravity lane this closes the elementary analytic gap between the combinatorial measure $(\mu,\mathrm{Aut})$ and the unitary path sum, so later claims about UV finiteness and torus suppression rest on a proved rather than postulated weight norm.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.