Payments
plain-language theorem explainer
Payments abstracts normalized cylinder payments as a pair of nonnegative real functions on the positive reals. Workers on the RM2U non-parasitism gate cite it to parameterize every payment-related hypothesis in the Navier-Stokes pipeline. The declaration is a bare structure definition carrying only the two functions and their nonnegativity axioms.
Claim. A structure consisting of two functions $p_ξ, p_ρ : ℝ → ℝ$ such that $p_ξ(r) ≥ 0$ and $p_ρ(r) ≥ 0$ for all $r ∈ ℝ$, where $p_ξ$ abstracts the normalized integral $(1/r²) ∬_{Q_r} ρ^{3/2} |∇ξ|² and $p_ρ$ abstracts $(1/r²) η^{-1} ∬_{Q_r ∩ {1-2η<ρ<1-η}} |∇(ρ^{3/4})|².
background
The RM2U.NonParasitism module isolates the single hard non-parasitism statement (tail-flux vanishing for the ℓ=2 coefficient) as a hypothesis so the remainder of the RM2U → RM2 pipeline stays checkable. Payments supplies the abstract carrier for the normalized payments that appear in every subsequent interface hypothesis.
proof idea
This is a structure definition with no proof body. It introduces the two payment functions together with the two nonnegativity fields and stops.
why it matters
Payments is the common type parameter for ExportForcesPaymentHypothesis, ForcingToTwistOrBandPaymentHypothesis, NegativeSigmaForcesBandPaymentHypothesis, NoRigidRotationAbsorptionHypothesis, and the bookkeeping theorems of_split and of_u4. It mirrors the TeX hypothesis for the U-4 cylinder payment upper bound and keeps all constants and moduli abstract until the final contradiction step that closes the non-parasitism gate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.