ExportSplitHypothesis
plain-language theorem explainer
ExportSplitHypothesis encodes the logical disjunction that any export persistence event for positive ε and r must fall into one of three cost channels: forcing, negative sigma, or concavity. Researchers assembling the RM2U non-parasitism gate cite it when bridging selection machinery to payment identities. The structure is introduced directly as a single universal quantification over the three-way split.
Claim. Let $E, F, N, C : (0,∞) × (0,∞) → Prop$ be predicates on positive reals. The hypothesis asserts that whenever $E(ε, r)$ holds, at least one of $F(ε, r)$, $N(ε, r)$, or $C(ε, r)$ is true.
background
The RM2U.NonParasitism module isolates non-parasitism as the vanishing of the tail-flux or boundary term at infinity for the ℓ=2 coefficient, expressed in Lean as TailFluxVanish. ExportSplitHypothesis supplies the S3-P bookkeeping layer that packages the output of selection and drift-control into an algebraic split across σ versus perpendicular forcing. It interfaces with the sibling structures NoRigidRotationAbsorptionHypothesis, which requires either sufficient payments or an explicit absorption class when forcing persists, and NegativeSigmaForcesBandPaymentHypothesis, which forces band diffusion payment from persistent negative injection on the top band.
proof idea
The declaration is a direct structure definition whose single field is the universal statement enforcing the disjunction. No lemmas or tactics are applied; it functions as an interface hypothesis whose content is supplied by the caller.
why it matters
This supplies the core splitter consumed by the downstream theorem of_split, which assembles the full export-to-payment bookkeeping lemma from the three abstract interfaces. It occupies the spec layer in the RM2U to RM2 pipeline, keeping the non-parasitism gate checkable while deferring concrete PDE content. In the Recognition Science setting it supports translation of forcing-chain steps into fluid boundary constraints without introducing hidden hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.