unnormalized_torus_weight_suppressed
plain-language theorem explainer
For any real action on the path-sum state space, the μ-weighted unitary summand of the embedded periodic Freudenthal torus of side N has complex modulus at most N^{-3}. Path-sum auditors in the Seven Gaps gravity lane cite this as the Aut-vacuity landmine: unnormalized torus contributions cannot be claimed nonvanishing or dominant unless they survive explicit 1/|Aut| suppression. The proof collapses the product norm to the already-proved bound μ(T_N) ≤ N^{-3} by unitarity of the phase weight.
Claim. For every natural number $N \ge 1$ and every real-valued action $S$ on bounded complexes of edge budget $7N^3$, $$\|\mu(T_N)\cdot U_S(T_N)\| \le N^{-3},$$ where $T_N$ is the canonical periodic Freudenthal torus embedded as a bounded complex, $\mu$ is its symmetry factor, and $U_S(T_N)$ is the unitary weight of $S$ on $T_N$.
background
This sits in Seven Gaps Phase 2b, lane O (path-sum probes C3 and C6). The module is explicitly non-flag-bearing: it attaches geometry to the scoped path-sum state space and records Aut-vacuity facts, claiming nothing about measures, limits, or continuum values.
The object $T_N$ is freudenthalBoundedComplex N: the canonical periodic Freudenthal triangulation of the $N\times N\times N$ torus, packaged as a BoundedComplex with edge budget $7N^3$. Vertex, edge, and tet counts match the geometric source ($nV=N^3$, $nE=7N^3$, $nT=6N^3$). Probe C6 shows the translation group $\mathbb{Z}_N^3$ embeds into the relabeling automorphism group of this image, so $|\mathrm{Aut}(T_N)|\ge N^3$ and therefore $\mu(T_N)\le N^{-3}$ (mu_freudenthal_le_inv_cube). Here $\mu$ is the positive symmetry factor on labeled complexes (mu_pos); the unitary weight is the pure phase associated to a real action $S$, hence has modulus one.
proof idea
Short rewrite chain, then one upstream inequality. Factor the complex modulus of the product into a product of moduli (norm_mul). The real symmetry factor, viewed in $\mathbb{C}$, contributes its absolute value (Complex.norm_real, Real.norm_eq_abs); positivity (mu_pos) drops the absolute value. The unitary weight has modulus one (unitaryWeight_norm), so the product collapses to $\mu(T_N)$ itself (mul_one). Finish by the already-proved Aut bound mu_freudenthal_le_inv_cube N.
why it matters
Doc-comment labels this the panel-mandated rejection criterion in summand form. Any future-wave claim that the unnormalized contribution $\mu(T_N)\exp(iS(T_N))$ is nonvanishing or dominant is potentially $0=0$ unless it explicitly survives the $1/|\mathrm{Aut}|$ suppression recorded here.
Downstream, mu_torusClassMember_le lifts the same $N^{-3}$ ceiling from the canonical representative to every labeled member of the torus relabeling class (via $\mu$ being a class function). Together these close the Aut-vacuity landmine for the Freudenthal torus inside the path-sum state space, while remaining inside the probe-only charter of Phase 2b: provenance and rejection criteria, not continuum path-sum evaluation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.