OscillatoryRemovalOpen
plain-language theorem explainer
Names the open proposition that some phase assignment on exact path classes makes the Gaussian-regulated RS path sum admit a ρ→0⁺ limit. Zero-phase removal is already refuted by positivity; oscillation could cancel shell masses and is not decided here. Status ledgers cite this Prop as the honest open boundary. Body is a one-line existential definition, not a theorem.
Claim. There exists a phase map $\mathrm{phase}_n$ from exact path classes of size $n$ to $\mathbb{R}$ such that the Gaussian-regulated quotient path sum $Z_{\mathrm{RS}}^{\mathrm{uv}}$ admits a finite limit as the regulator $\rho\to 0^+$.
background
This module sits in the Seven Gaps gravity stack. It proves a kernel no-go for regulator removal of the Gaussian-regulated quotient path sum $Z_{\mathrm{RS}}^{\mathrm{uv}}$ at zero phase: shell masses diverge (labeled entropy beats the $v!,e!,t!$ gauge volume via a Burnside/orbit-stabilizer identity), and nonnegativity lets a single shell lower-bound the regulated sum, blocking any $\rho\to 0^+$ limit.
HasZRSRegulatorRemoval is the predicate that such a continuum limit exists for a given phase. Exact path classes are the gauge-quotiented complexes of fixed signature. The zero-phase refutation uses positivity of every regulated term; that argument does not transport to oscillatory phases, where unit-modulus cancellations might tame the diverging shells.
The module therefore isolates the residual question as a named open Prop rather than a claimed theorem.
proof idea
No proof. The declaration is a definition-level Prop: the existential assertion that some phase assignment on exact path classes satisfies regulator removal. There is no tactic block, no lemma application, and no claim that the Prop holds or fails.
why it matters
Marks the binding honesty boundary of the regulator-removal no-go. Downstream, RegulatorRemovalNoGoStatus and regulatorRemovalNoGoStatus set oscillatory_removal_open := true and document that every other flag is kernel-grounded while this one records an open definition-level Prop with no claim. The module flips no FullTheoryLedger or CampaignLedger flag.
In the Recognition gravity program this separates a finished zero-phase obstruction (shell-mass divergence plus positivity) from the unresolved oscillatory case, where cancellations could still permit continuum removal. It is the explicit residual gap after the zero-phase theorem, not a scaffolding stub pretending to be settled.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.