ExactShellGaugeUVStatus
plain-language theorem explainer
Status ledger for the exact-shell Gaussian-UV path-sum module: seven boolean flags recording which Stage-1 shell and Stage-2 regularized-limit claims are proved. The two open boundaries (regulator removal and continuum limit) are locked false by protocol. Anyone auditing Seven Gaps or FullTheoryLedger cites this record. Pure structure definition; field docs name the kernel theorems that ground each true flag.
Claim. A status record of seven booleans for the exact-shell Gaussian-UV module: (i) shell structure proved, (ii) entropy bound proved, (iii) UV summability proved, (iv) cutoff limit proved, (v) nonvacuity proved, (vi) regulator-removal proved, (vii) continuum limit claimed. Every true flag must be grounded in a named kernel theorem; flags (vi) and (vii) are required to stay false here (complexity cutoff is not mesh refinement).
background
This module organizes the quotient-class path-sum configuration space into exact complexity shells (no size caps) and studies the shell-resummed path sum with an explicit Gaussian UV regulator $\exp(-\rho n^2)$. The regulator is inserted by hand; the action/phase on classes is a free parameter. Nothing here is physical continuum limit: complexity cutoff is not mesh refinement.
Stage 1 covers shell structure: complexity is relabeling-invariant, the cap-free exact class with global relabeling is a setoid, each exact complexity shell is finite, and the shell entropy bound $\mathrm{card}(\mathrm{ExactPathClass}, n)\le (n+1)^{12(n+1)}$ holds. Stage 2 covers the regularized limit: the per-class measure $1/|\mathrm{Aut}|$, modulus bounds, summability of the shell series for every $\rho>0$, convergence of cutoff partial sums to $Z_{\mathrm{RS,uv}}$, and nonvacuity at zero phase.
Regulator removal ($\rho\to 0^+$) is only a named open proposition: existence of $\lim_{\rho\to 0^+} Z_{\mathrm{RS,uv}}(\rho,\mathrm{phase})$. Even if proved, it would still not be the continuum limit.
proof idea
No proof body: this is a structure declaration. Each field is a Bool annotated by a doc-comment that names the kernel theorem(s) the flag is meant to track (complexity_congr, exactSetoid, instFintypeExactPathClass, shell_index_unique, toExact_relax for shell structure; exactPathClass_card_le for the entropy bound; summable_zRSUVShell; zRSUVCutoff_tendsto; Z_RS_uv_zeroPhase_re_pos; and the open HasZRSRegulatorRemoval). Grounding of true flags is deferred to the companion instance and its grounding lemma.
why it matters
This is the honesty ledger for the exact-shell Gaussian-UV half of Seven Gaps. The canonical instance exactShellGaugeUVStatus fills the first five flags true and keeps regulator removal and continuum limit false, so downstream audits cannot silently promote OPEN items. Module protocol is binding: path_sum_continuum_limit and gap2_continuum_and_measure stay RED; this module flips no FullTheoryLedger flag.
In the broader Recognition gravity stack, the path sum is a configuration-space object on exact complexity shells, not a derived continuum spacetime measure. The structure makes the boundary explicit: Gaussian UV regularization and shell finiteness are theorem-backed; $\rho\to 0^+$ removal and mesh-refinement continuum limits are not claimed here. That separation keeps the Seven Gaps panel-locked disclosures enforceable in Lean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.