ExportForcesPaymentHypothesis
plain-language theorem explainer
ExportForcesPaymentHypothesis packages the bookkeeping that any persistent export event on a cylinder must trigger either a quadratic lower bound on the sum of normalized payments or fall into an explicit absorption or concavity class. Analysts closing the non-parasitism gate in the RM2U reduction would cite it to organize the logical split. The declaration is a pure structure definition that composes three upstream implication interfaces without adding new content.
Claim. Let $E, A, C : ℝ → ℝ → Prop$ be predicates for export, absorption, and concavity events on scale-radius pairs, and let $P$ be a payments structure with components pay_ξ(r) and pay_ρ(r). The hypothesis asserts that there exists $c > 0$ such that for all ε, r > 0, if $E(ε, r)$ holds then either $c ε² ≤ pay_ξ(r) + pay_ρ(r)$ or $A(ε, r)$ or $C(ε, r)$.
background
Payments is the structure that abstracts the normalized cylinder payments from the TeX manuscript: payXi(r) corresponds to the scaled integral of ρ^{3/2} |∇ξ|² over Q_r while payRho(r) encodes the diffusion term on the top band {1-2η < ρ < 1-η}. The module RM2U.NonParasitism isolates the single hard non-parasitism statement (tail-flux vanishing at infinity for the ℓ=2 coefficient) as a temporary hypothesis so the remainder of the RM2U to RM2 pipeline stays checkable. This declaration sits downstream of the PrimitiveDistinction.from theorem, which extracts four structural conditions plus three definitional facts from seven axioms, and of the Payments definition itself.
proof idea
This is a definition that directly encodes the disjunction of the payment lower bound with the absorption and concavity classes. It is assembled by packaging the combined consequence of ExportSplitHypothesis, NoRigidRotationAbsorptionHypothesis, and NegativeSigmaForcesBandPaymentHypothesis into a single Prop; no tactics or reductions are required.
why it matters
This declaration supplies the central bookkeeping lemma that feeds the of_split and of_u4 theorems, which close the U-4 contradiction under an export event. It mirrors the TeX Lemma lem:export_forces_payment_on_cylinder at the spec layer and forms part of the non-parasitism gate required to pass from RM2U to the full RM2 closure. In the Recognition Science framework it contributes to the Navier-Stokes analysis by ensuring persistent forcing cannot evade payment without entering a ruled-out structural class.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.