mu_freudenthal_le_inv_cube
plain-language theorem explainer
The path-sum symmetry factor of the side-N periodic Freudenthal torus is at most 1/N³. Gravity and path-sum workers cite this as the Aut-vacuity landmine: translations alone force that suppression. Proof is a short comparison: |Aut| ≥ N³ from the translation embedding, and μ unfolds to the reciprocal of |Aut|.
Claim. For every positive integer $N$, if $T_N$ is the bounded complex packaging the canonical periodic Freudenthal torus of side $N$, then its path-sum symmetry factor satisfies $\mu(T_N)\le 1/N^3$.
background
Lane O of Seven Gaps Phase 2b records path-sum probes only. It attaches the canonical periodic Freudenthal torus (side $N\ge 1$) to the scoped state space BoundedComplex with edge budget $7N^3$, preserving vertex/edge/tet counts ($nV=N^3$, $nE=7N^3$, $nT=6N^3$) and incidence maps, while dropping edge-in-tet and metric fields. No continuum, measure, or path-sum value is claimed.
Probe C6 checks that the translation group $\mathbb{Z}_N^3$ embeds into the relabeling automorphisms of that image: the map is injective, sends $0$ to the identity, and preserves addition. The immediate cardinality consequence is $|\mathrm{Aut}(T_N)|\ge N^3$.
The scalar $\mu$ on a bounded complex is the reciprocal of the automorphism-group cardinality (the symmetry factor in the path-sum measure). The inequality here is exactly that factor versus the translation-orbit size.
proof idea
Cast $N>0$ to reals and obtain $N^3>0$ by pow_pos. Apply autCard_ge_translations to get $N^3\le|\mathrm{Aut}(T_N)|$ after a natural-number cast. Unfold the definition of $\mu$ (reciprocal of automorphism cardinality) and finish with one_div_le_one_div_of_le, which reverses the inequality under positive denominators.
why it matters
This is the measure-form landmine of probe C6: any unnormalized torus contribution is suppressed by at least the translation orbit. Downstream, mu_torusClassMember_le lifts the bound to every labeled class representative via congruence of $\mu$; tendsto_mu_freudenthal_zero squeezes the labeled masses to $0$ as $N\to\infty$; torus_classMass_le_fiberCard_div_cube converts it into the honest class-mass bound (fiber card over $N^3$, not absolute $N^{-3}$ pushforward suppression); and unnormalized_torus_weight_suppressed upgrades it to the panel rejection criterion: for any real action $S$, $|\mu(T_N),e^{iS(T_N)}|\le N^{-3}$.
In the gravity path-sum setting this blocks future-wave claims that the bare torus summand is nonvanishing or dominant unless they explicitly beat the $1/|\mathrm{Aut}|$ factor. It does not itself evaluate any continuum path sum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.