unitaryWeight
plain-language theorem explainer
Defines the unitary path-sum weight w(K)=exp(i S(K)) on bounded combinatorial complexes at fixed lattice scale. Gravity and path-sum authors cite it as the standard complex phase factor for the scoped Z_RS measure. The body is a one-line complex exponential of a real action cast to ℂ.
Claim. For a bound $B\in\mathbb{N}$ and a real-valued action $S$ on the finite set of bounded combinatorial complexes of size at most $B$, the unitary weight is the map $K\mapsto \exp(i\,S(K))\in\mathbb{C}$.
background
Lane 2 of the Seven Gaps program builds a proved path-sum measure for $Z_{RS}$ on a scoped configuration class. A BoundedComplex B is a combinatorial triangulation at fixed lattice scale: at most $B$ vertices, edges, and tetrahedra, with abstract incidence maps and no metric field (CDT-style; edge length fixed at the substrate mesh). The class is finite via an explicit coding equivalence.
The path sum is $Z(B,w)=\sum_K \mu(K),w(K)$ with symmetry factor $\mu(K)=1/|\mathrm{Aut},K|$. The module proves finiteness, $0<\mu\le 1$, relabeling invariance of $\mu$, and modulus bounds on $Z$. The unitary instance takes $w=\exp(iS)$ for a real action $S$; the intended $S$ for $Z_{RS}$ is the sinh recognition action on deficit data.
This definition supplies that weight map. Downstream, unit modulus and the scoped well-definedness package for $Z_{RS}$ are stated as separate theorems.
proof idea
Definitional one-liner: send each complex $K$ to $\mathrm{Complex.exp}(i\cdot S(K))$ after casting the real action value to $\mathbb{C}$. No lemmas are applied; noncomputability is inherited from complex exponentiation.
why it matters
This is the honest unitary weight for the scoped $Z_{RS}$ statement in the module doc: unit-modulus weights make the proved UV bounds ($|Z|\le\sum\mu$ and $|Z|\le\mathrm{card}$) apply directly. Immediate consumers are unitaryWeight_norm ($|w(K)|=1$) and zRS_scoped_wellDefined (unit modulus, relabeling invariance of the weight, card bound, and reindexing invariance).
Class-level identities use it as well: zRS_eq_classPushforward equates the labeled unitary sum to the class pushforward when $S$ is class-constant, and classMass_eq_fiberCard_mul_mu is the fork-detector identity feeding that rewrite. Probe theorems such as unnormalized_torus_weight_suppressed multiply $\mu$ by this weight to enforce the $N^{-3}$ landmine bound on Freudenthal tori. It does not itself force the recognition action or close simplicial growth; it only installs the phase factor the rest of Lane 2 quotes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.