exactShellGaugeUVStatus_grounded
plain-language theorem explainer
Grounding certificate for the exact-shell Gaussian-UV path-sum ledger: every true status flag is paired with its kernel theorem (nonempty shells, entropy bound, summability, cutoff convergence, zero-phase nonvacuity), and the two open flags (regulator removal, continuum limit) are recorded false. Gravity auditors cite it to verify the honesty protocol rather than to extract new analysis. The proof is a pure term pairing of rfl with the five Stage-1/2 theorems.
Claim. The exact-shell Gaussian-UV status record is grounded: shell structure holds and every complexity shell $n$ is nonempty; the entropy bound holds with $\lvert\mathrm{ExactPathClass}(n)\rvert \le (n+1)^{12(n+1)}$; UV summability holds so that for every $\rho>0$ and every phase the shell series is summable; cutoff partial sums tend to the regulated path sum $Z_{\mathrm{RS}}^{\mathrm{uv}}(\rho,\mathrm{phase})$; at zero phase the real part is positive; regulator-removal and continuum-limit flags remain false.
background
This module builds the Recognition path sum on exact complexity shells: for each $n$, the type of combinatorially distinct exact complexes of complexity exactly $n$ is the disjoint union over shell signatures of the quotient of labeled exact complexes by global relabeling. No size-cap type appears in the shell definition. The Gaussian UV regulator $\exp(-\rho n^2)$ is inserted by hand; the phase on classes is an arbitrary parameter, not a derived action.
Upstream Stage-1 results supply the combinatorial skeleton: every shell is inhabited (witness: $n$ isolated vertices), and the shell cardinality obeys $\mathrm{card}\le(n+1)^{12(n+1)}$. Stage-2 supplies the regulated shell term, its modulus bound, summability of the shell series for every $\rho>0$, and convergence of complexity-cutoff partial sums to the tsum $Z_{\mathrm{RS}}^{\mathrm{uv}}$.
The status record is a ledger of five proved stages plus two deliberately open flags. The module doc is explicit that regulator removal ($\rho\to 0^+$) and any physical continuum limit stay unclaimed; complexity cutoff is not mesh refinement.
proof idea
Pure term-mode pairing. Each true flag is discharged by rfl against the status record definition, conjoined with the corresponding kernel theorem: unbounded support of exact path classes; the shell entropy bound; summability of the regulated shell series (for arbitrary positive $\rho$ and phase); cutoff-to-tsum convergence; and positivity of the real part of the zero-phase regulated sum. The two open flags are closed by rfl to false. No new analysis is performed.
why it matters
In the Seven Gaps honesty protocol this is the audit hinge: status Booleans cannot drift from the mathematics. Downstream, the named open HasZRSRegulatorRemoval is the proposition that $Z_{\mathrm{RS}}^{\mathrm{uv}}(\rho,\mathrm{phase})$ admits a limit as $\rho\to 0^+$ along positive neighborhoods; the grounding theorem forces regulator_removal_proved = false, so nothing in the ledger pretends that open is closed. Continuum-limit claims stay red in the full theory ledger.
Within Recognition gravity this sits under the path-sum measure program, not under the T0–T8 forcing chain. It certifies that the Gaussian-UV shell series is a well-defined complex number for every $\rho>0$, while keeping the mathematical regulator and the missing $\rho\to 0$ step visibly separate from derived physics (action, continuum, FullTheoryLedger flags).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.