NoPersistentNullAlignmentHypothesis

formal source

 744vorticity direction (i.e. avoids the null-eigenvector cone everywhere on a time-thick top band set).
 745
 746At the spec layer this is an abstract implication between two events. -/
 747structure NoPersistentNullAlignmentHypothesis
 748    (TailLargeEvent HitEvent : ℝ → ℝ → Prop) : Prop where
 749  exists_c :
 750    ∃ c : ℝ,
 751      0 < c ∧
 752        ∀ (ε r : ℝ), 0 < ε → 0 < r →
 753          TailLargeEvent ε r →
 754            HitEvent ε r
 755
 756/-- **S3-P bookkeeping (spec layer):** export persistence splits into one of the three “cost channels”.
 757
 758This is intentionally abstract: it packages the output of the selection/drift-control machinery together with
 759the algebraic split (`σ` vs perpendicular forcing) into a single logical splitter. -/
 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). -/
 776structure ExportForcesPaymentHypothesis
 777    (ExportEvent AbsorptionClass ConcavityEvent : ℝ → ℝ → Prop) (P : Payments) : Prop where