ExportSplitHypothesis
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove the split holds for any concrete PDE solution.
- Does not define the predicates ExportEvent, ForcingEvent, NegativeSigmaEvent or ConcavityEvent.
- Does not address vanishing of the tail flux or boundary term.
- Does not incorporate J-cost, phi-ladder or Recognition Composition Law.
formal statement (Lean)
760structure ExportSplitHypothesis
761 (ExportEvent ForcingEvent NegativeSigmaEvent ConcavityEvent : ℝ → ℝ → Prop) : Prop where
762 split :
763 ∀ (ε r : ℝ),
764 0 < ε →
765 0 < r →
766 ExportEvent ε r →
767 ForcingEvent ε r ∨ NegativeSigmaEvent ε r ∨ ConcavityEvent ε r
768
769/-- **Export ⇒ payment/absorption/concavity** (spec layer).
770
771This mirrors TeX Lemma `lem:export_forces_payment_on_cylinder`, but keeps the PDE objects abstract.
772The only nontrivial content should sit inside:
773- `ExportSplitHypothesis` (selection + bridge into one of the three channels),
774- `NoRigidRotationAbsorptionHypothesis` (forcing ⇒ payment ∨ absorption),
775- `NegativeSigmaForcesBandPaymentHypothesis` (negative injection ⇒ band payment). -/