NoRigidRotationAbsorptionHypothesis
plain-language theorem explainer
The declaration defines a structural hypothesis guarding against rigid-rotation absorption in the RM2U non-parasitism setting for Navier-Stokes. A researcher working on regularity via the Recognition Science pipeline would cite it to separate persistent forcing from an explicit structural class. The definition encodes an existential positive lower bound on the sum of normalized cylinder payments whenever the forcing predicate holds, unless the cylinder satisfies the AbsorptionClass predicate.
Claim. Let ForcingEvent and AbsorptionClass be predicates on pairs of positive reals. Let P be a Payments structure with nonnegative payXi and payRho functions. The hypothesis holds if there exists c > 0 such that for all ε, r > 0, whenever ForcingEvent ε r is true then c ε² ≤ payXi(r) + payRho(r) or AbsorptionClass ε r holds.
background
In the RM2U.NonParasitism module the single hard gate is isolated as a hypothesis so the RM2U to RM2 pipeline remains checkable. Non-parasitism itself is the statement that the tail-flux boundary term at infinity vanishes for the relevant ℓ=2 coefficient, written TailFluxVanish P.A P.A'. The Payments structure abstracts the normalized cylinder payments: payXi(r) is the (1/r²) double integral over Q_r of ρ^{3/2} |∇ξ|² and payRho(r) is the analogous integral of |∇(ρ^{3/4})|² over the annular slice 1-2η < ρ < 1-η.
proof idea
This is a structure definition that directly encodes the guard as an existential quantifier over c > 0 together with the universal implication over ε, r. No lemmas are invoked; the declaration serves as an interface hypothesis whose body is the stated Prop.
why it matters
The hypothesis is used by ExportSplitHypothesis and the of_split theorem that assembles the export-to-payment bookkeeping from the three abstract implication interfaces. It fills the role of forcing any persistent forcing event with small payments into the AbsorptionClass, which is intended to be ruled out via the TeX lemma on rigid-rotation absorption implying structure. In the Recognition Science framework it supports the non-parasitism gate inside the Navier-Stokes translation while remaining compatible with the upstream forces, band, and for structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.