 907/-- **Absorption elimination (U-4):** the abstract absorption class cannot occur below some scale.
 908
 909This mirrors TeX Hypothesis `hyp:absorption_class_impossible`. -/
 910structure AbsorptionClassImpossibleHypothesis (AbsorptionClass : ℝ → ℝ → Prop) : Prop where
 911  impossible :
 912    ∀ (η ε0 : ℝ),
 913      0 < η →
 914        0 < ε0 →
 915          ∃ r0 : ℝ,
 916            0 < r0 ∧
 917              ∀ r : ℝ, 0 < r → r ≤ r0 → AbsorptionClass ε0 r → False
 918
 919/-- **Concavity/peak channel elimination (spec layer):** the concavity event cannot occur below some scale.
 920
 921This is the abstract way to “kill (P3)” if it is not already absorbed into `payXi`/`payRho`. -/
 922structure ConcavityImpossibleHypothesis (ConcavityEvent : ℝ → ℝ → Prop) : Prop where
 923  impossible :
 924    ∀ (ε0 : ℝ),
 925      0 < ε0 →
 926        ∃ r0 : ℝ,
 927          0 < r0 ∧
 928            ∀ r : ℝ, 0 < r → r ≤ r0 → ConcavityEvent ε0 r → False
 929
 930/-- **U-4 one-cylinder contradiction (spec layer):** export persistence at a fixed level is impossible below some scale.
 931
 932This mirrors TeX Lemma `lem:U4_contradiction_from_export`, but keeps the PDE objects abstract. -/
 933structure U4NoExportHypothesis (ExportEvent : ℝ → ℝ → Prop) : Prop where
 934  impossible :
 935    ∀ (ε0 : ℝ),
 936      0 < ε0 →
 937        ∃ r0 : ℝ,
 938          0 < r0 ∧
 939            ∀ r : ℝ, 0 < r → r ≤ r0 → ExportEvent ε0 r → False
 940

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.