AbsorptionClassImpossibleHypothesis
plain-language theorem explainer
AbsorptionClassImpossibleHypothesis packages the claim that an arbitrary absorption predicate on pairs of reals cannot hold for radii below a positive threshold r0, once η and ε0 are fixed and positive. Workers on the RM2U Navier-Stokes closure cite it to discharge the absorption channel inside the U-4 bookkeeping step. The declaration is a bare structure definition whose single field simply records the quantified negation; no lemmas or tactics are invoked.
Claim. Let AbsorptionClass : ℝ → ℝ → Prop. The predicate AbsorptionClassImpossibleHypothesis(AbsorptionClass) asserts ∀ η > 0, ∀ ε₀ > 0, ∃ r₀ > 0 such that ∀ r ∈ (0, r₀], AbsorptionClass(ε₀, r) is false.
background
The RM2U.NonParasitism module isolates the single hard gate of the pipeline: non-parasitism is the statement that the tail-flux or boundary term at infinity vanishes for the ℓ=2 coefficient in the PDE translation. The present structure supplies the abstract elimination of the absorption class below a scale, exactly as described in the module doc-comment and mirroring the TeX hypothesis hyp:absorption_class_impossible. This keeps the remainder of the RM2U → RM2 pipeline free of hidden assumptions.
proof idea
The declaration is a structure definition whose single field 'impossible' directly encodes the universal quantification ∀ η > 0, ∀ ε₀ > 0, ∃ r₀ > 0, ∀ r ≤ r₀, AbsorptionClass ε₀ r → False. No upstream lemmas are applied; the construction is the hypothesis itself.
why it matters
The structure is required by the downstream theorem of_u4, which assembles the U-4 contradiction from an export lower bound, a payment upper bound, and the two impossibility hypotheses (absorption and concavity). It therefore supplies the concrete mechanism for killing the absorption channel (P3) inside the non-parasitism gate. In the Recognition framework it maintains the clean separation of the single hard statement so that the boundary-term vanishing can be treated as an isolated hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.