NegativeSigmaForcesBandPaymentHypothesis
plain-language theorem explainer
NegativeSigmaForcesBandPaymentHypothesis defines an abstract interface asserting that a persistent negative-sigma event on the top band forces a lower bound on the normalized band-diffusion payment payRho at least proportional to ε squared. Researchers closing the RM2U non-parasitism gate for Navier-Stokes would cite this when packaging the selection-drift output into the three cost channels. As a structure definition it introduces the hypothesis with no proof obligations or hidden assumptions.
Claim. Let NegativeSigmaEvent : ℝ → ℝ → Prop abstract the event σ ≤ −c_* ε on the top band for a time-thick subset. Let P be the payments structure whose payRho component is the normalized cylinder integral (1/r²) η^{-1} ∬_{Q_r ∩ {1−2η<ρ<1−η}} |∇(ρ^{3/4})|^2. Then there exists c > 0 such that ∀ ε, r > 0, NegativeSigmaEvent ε r implies c ε² ≤ P.payRho r.
background
The module RM2U.NonParasitism isolates the single hard non-parasitism statement as a temporary hypothesis so the rest of the RM2U → RM2 pipeline remains checkable. Non-parasitism is defined as the vanishing of the tail-flux / boundary term at infinity for the relevant ℓ=2 coefficient, written TailFluxVanish P.A P.A'. Payments is the sibling structure that packages the two normalized cylinder payments: payRho r measures the diffusion cost on the annular top band while payXi r measures the vorticity cost.
proof idea
This declaration is a structure definition with an empty proof body. It simply packages the existential statement on c together with the universal quantification over ε and r into a single Prop-valued interface.
why it matters
The structure supplies the NegativeSigmaEvent → payRho implication used by ExportSplitHypothesis and the of_split theorem to assemble the full export→payment bookkeeping. It therefore occupies the spec-layer slot for the negative-injection forcing channel inside the single hard gate that the module keeps separate from the rest of the RM2U closure. The surrounding module doc-comment states that this gate is the only genuinely hard statement that must eventually be discharged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.