module module moderate

`IndisputableMonolith.Gravity.SevenGaps.RegulatorRemovalNoGo`

Finite-group infrastructure for the full relabeling gauge group on exact-complexity shells at signature (v, e, t): independent permutations of vertices, edges, and tetrahedra. It supplies orbit-cardinality, torsor, and Burnside-style counting lemmas used when attacking naive removal of the Gaussian UV regulator. Downstream signature-blocker and continuum-cutoff modules import this algebra. Content is group actions and finite counting, not analytic estimates.

claimAt fixed signature $(v,e,t)$, the relabeling gauge group is $S_v\times S_e\times S_t$, acting by independent permutations of the vertex, edge, and tetrahedron index sets on exact complexes and $\sigma$-configurations. The module records the induced actions, the orbit/torsor equivalences, and the identity that the sum of orbit cardinalities equals the Burnside count of labeled configurations in each exact shell.

background

In the Seven Gaps gravity stack, path-sum configuration space is organized into exact complexity shells (no size caps in the shell definition). The parent module ExactShellGaugeUV proves that the shell-resummed path sum with Gaussian UV weight $\exp(-\rho\cdot n^2)$ converges for every regulator strength $\rho>0$.

Configurations at a combinatorial signature $(v,e,t)$ still carry a large discrete redundancy: one may independently permute vertex, edge, and tetrahedron labels. The full relabeling gauge group is the product of the three symmetric groups on those index sets. Quotienting by this action is the natural route from labeled complexes to gauge-invariant path-sum weights.

This module packages that group, its action on exact complexes and $\sigma$-data, and the elementary finite-group facts (orbit cards, torsor equivalences, summed-orbit identities) needed before any asymptotic or continuum argument about removing $\rho$ or a complexity cutoff.

proof idea

Definition-heavy module with standard finite-group lemmas, not a single deep theorem.

It introduces the relabel triple (the product of three symmetric groups), the action maps on exact complexes and on $\sigma$-configurations, and extensionality lemmas for those actions. From there it builds the relabeling equivalence on $\sigma$-data, finiteness of the exact-relabel type, and a torsor equivalence relating stabilizers to orbits.

Orbit cardinality and the summed-card identities are then elementary consequences: counting orbits via the group order and relating the sum of orbit sizes to the Burnside-weighted count of labeled shells. No analytic estimates or regulator limits are proved here; the module stops at exact combinatorial equalities.

why it matters in Recognition Science

Regulator removal and continuum limits in the Seven Gaps program cannot be honest without controlling gauge redundancy on each exact shell. This module is the shared algebraic substrate for those attacks.

It is imported by the Gap-2 signature-blocker attack, whose doc-comment records that uniform single-signature mass concentration for large shells is refuted as an asymptotic strategy under the banked Burnside identity. The orbit-sum lemmas here are exactly the counting input to that diagnosis.

It is also imported by the phased-quotient continuum blocker (P2-a), which isolates the Cauchy criterion for removing the complexity cutoff from the phased quotient path sum. Gauge-fixed shell counts enter any comparison of finite quotient sums along a cutoff sequence.

Within the broader RS gravity story, this sits downstream of exact-shell UV regularization and upstream of no-go or stall results on taking $\rho\to 0$ or sending cutoffs to infinity without additional structure.

scope and limits

Does not prove convergence or divergence of the path sum as the UV regulator strength tends to zero.
Does not establish single-signature mass concentration for large exact shells.
Does not remove the complexity cutoff from the phased quotient sum or prove the Cauchy criterion.
Does not treat continuous diffeomorphisms; only finite relabeling of vertex, edge, and tetrahedron indices.
Does not compute numerical shell masses or evaluate the Gaussian-regulated sum.

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Gravity.SevenGaps.Gap2SignatureBlockerAttack module_import
IndisputableMonolith.Gravity.SevenGaps.ZqContinuumBlocker module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.ExactShellGaugeUV module_import

declarations in this module (29)

abbrev RelabelTriple L83
theorem relabelTriple_card L88
def act L102
def actRelabel L108
theorem exactComplex_ext L123
theorem sigma_relabel_ext L136
def relabelSigmaEquiv L166
instance instFiniteExactRelabel L178
def torsorEquiv L187
def orbitCard L209
theorem sum_card_relabel L213
theorem sum_card_relabel_eq_orbit L226
theorem orbitCard_mul_autCard L255
instance instFintypeExactQuotient L265
class is L270
theorem classMuOn_out L271
theorem fiber_card L283
theorem sum_orbitCard L296
theorem sum_classMuOn_eq_card_div_factorials L314
def cubeSig L345
theorem cube_sum_le_shellMass L353
theorem shellMass_lower L387
theorem shellMass_unbounded L430
theorem single_shell_re_lower_bound L450
theorem not_hasZRSRegulatorRemoval_zeroPhase L474
def OscillatoryRemovalOpen L509
structure RegulatorRemovalNoGoStatus L518
def regulatorRemovalNoGoStatus L531
theorem regulatorRemovalNoGoStatus_grounded L540