regulatorRemovalNoGoStatus_grounded
plain-language theorem explainer
Status ledger for the zero-phase regulator-removal no-go is fully grounded: each true proof flag is paired with its kernel theorem (shell-mass identity, shell-mass divergence, zero-phase refutation), and the oscillatory-removal flag is recorded open with no claim. Gravity auditors cite it to certify that the module's Boolean ledger is not decorative. The proof is a four-component term pairing `rfl` on each flag with the named kernel results.
Claim. The regulator-removal no-go status record satisfies: (i) the shell-mass identity flag is true and for all $v,e,t\in\mathbb{N}$, $\sum_{c\in Q(v,e,t)}\mu(c)=|\mathrm{ExactComplex}(v,e,t)|/(v!\,e!\,t!)$ where $Q$ is the quotient by global relabeling equivalence; (ii) the shell-mass divergence flag is true and $\mathrm{shellMass}\,n$ is unbounded above; (iii) the zero-phase removal-refuted flag is true and regulator removal fails for the zero phase $S\equiv 0$; (iv) the oscillatory-removal flag is true (recorded open).
background
This module sits in the Seven Gaps gravity stack and treats the Gaussian-UV-regulated path sum $Z_{\mathrm{RS},\mathrm{uv}}$ on exact combinatorial complexes. An ExactComplex of signature $(v,e,t)$ carries exactly $v$ vertices, $e$ edges and $t$ tetrahedra with incidence data and no cap inequalities. Global relabeling equivalence is a setoid on each signature; the quotient carries the descended per-class measure $\mu=1/|\mathrm{Aut}|$ (classMuOn).
Shell mass is the sum of those class measures on the $n$-shell. The zero phase assigns action $S\equiv 0$ to every path class. Regulator removal (HasZRSRegulatorRemoval) is the named open asking whether $\lim_{\rho\to 0^+} Z_{\mathrm{RS},\mathrm{uv}}(\rho,\mathrm{phase})$ exists in $\mathbb{C}$. The module already proves the absolute/positive-term route is dead at zero phase: shell masses diverge (labeled entropy beats the $v!,e!,t!$ gauge volume via Burnside/orbit-stabilizer), so positivity gives a single-shell lower bound that blows any putative limit.
The status record packages those kernel facts as Boolean flags plus the honest OPEN boundary for oscillatory phases.
proof idea
Pure term-mode pairing. The goal is a four-fold conjunction of (flag $=$ true $\land$ kernel statement). Each flag equality is discharged by rfl against the status definition. The three kernel conjuncts are supplied directly by the already-proved lemmas sum_classMuOn_eq_card_div_factorials (Burnside identity for every signature), shellMass_unbounded (divergence via the $(n,n,n)$ lower bound), and not_hasZRSRegulatorRemoval_zeroPhase (positivity lower-bound contradiction). The final OPEN flag is again rfl. No new analysis is performed here.
why it matters
Without this grounding theorem the status ledger would be a free-floating Boolean record. Downstream, OscillatoryRemovalOpen is the definition-level Prop that the ledger marks open: existence of some phase (in particular a genuine oscillatory action phase) for which regulator removal holds. The doc-comment stresses that every true flag is kernel-tied and that the OPEN flag carries no claim on that Prop.
In the Recognition gravity program this closes the absolute-route half of the continuum-limit gap at zero phase while keeping the oscillatory half honestly open. It does not flip any FullTheoryLedger or CampaignLedger flag. The zero-phase no-go is quantitative and fully checked; the remaining question is whether unit-phase cancellation can tame the same diverging shell masses. That is the binding honesty boundary of the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.