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. -/
depends on (15)
Lean names referenced from this declaration's body.