of_split
plain-language theorem explainer
The lemma assembles an export event on a cylinder into a payment bound, absorption class, or concavity outcome by routing through three abstract channels. Researchers closing the RM2U non-parasitism gate in the Navier-Stokes pipeline cite it to discharge the bookkeeping step before invoking the tail-flux hypothesis. The proof extracts positive constants from the forcing and negative-sigma interfaces, takes their minimum, performs case analysis on the split, and verifies the scaled inequality in each branch.
Claim. Assume every export event splits into a forcing event, negative-sigma event, or concavity event. Assume a forcing event yields either a cylinder payment bound of order $c_F ε^2$ or membership in the absorption class. Assume a negative-sigma event yields a band payment bound of order $c_N ε^2$. Then every export event yields either a cylinder payment bound of order $c ε^2$, membership in the absorption class, or a concavity event, where $c = min(c_F, c_N)$.
background
Payments is the abstract structure carrying two normalized cylinder integrals: payXi(r) bounds the ξ-gradient energy and payRho(r) bounds the top-band diffusion energy, both required to be nonnegative. ExportSplitHypothesis packages the selection machinery into a logical splitter that sends any ExportEvent(ε,r) into exactly one of three channels. NoRigidRotationAbsorptionHypothesis supplies a constant c_F such that a forcing event forces either the payment sum or the absorption class. NegativeSigmaForcesBandPaymentHypothesis supplies c_N such that a negative-sigma event forces the band payment. The module isolates the single hard non-parasitism statement (tail-flux vanishing at infinity for the ℓ=2 coefficient) so that the remainder of the RM2U pipeline stays checkable.
proof idea
The term proof begins by invoking classical logic, extracts the witnessing constants c_F and c_N from the two payment hypotheses, and refines the target structure with their minimum. It then applies the splitter to obtain a case distinction on the export event. In the forcing branch it re-applies the absorption hypothesis and routes the payment subcase through the min inequality; in the negative-sigma branch it routes the band payment through the same min and adds the nonnegativity of payXi; the concavity branch is immediate.
why it matters
This declaration discharges the interface lemma that lets the single hard non-parasitism hypothesis (TailFluxVanish) sit cleanly above the rest of the RM2U pipeline. It directly implements the bookkeeping step required by the manuscript lemma on export forcing payment, using only the three abstract channel hypotheses. No downstream uses are recorded yet; the declaration therefore functions as an internal closure that keeps the Navier-Stokes non-parasitism gate modular.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.