ConcavityImpossibleHypothesis
plain-language theorem explainer
ConcavityImpossibleHypothesis encodes the claim that for any positive epsilon0, concavity events are forbidden below some positive radius r0. Workers on the RM2U pipeline cite it to close the concavity channel when building the U-4 contradiction. The declaration is a bare structure definition that introduces the impossible field with no computational content or proof steps.
Claim. Let $C : ℝ → ℝ → Prop$ be a concavity event predicate. The hypothesis asserts that for every $ε_0 > 0$ there exists $r_0 > 0$ such that for all $r$ with $0 < r ≤ r_0$, $C(ε_0, r)$ is false.
background
The RM2U.NonParasitism module isolates the single hard non-parasitism gate so that the remainder of the RM2U to RM2 pipeline stays checkable. Non-parasitism itself is the statement that the tail-flux boundary term at infinity vanishes for the relevant ℓ=2 coefficient, written TailFluxVanish P.A P.A'. The present structure supplies the abstract concavity-channel elimination needed when that gate is not already absorbed into payment or absorption predicates. Upstream constants supply the RS-native gauge U (with c = 1) and the scale function scale(k) := phi^k that furnishes the dimensional context for the radius r0.
proof idea
The declaration is a structure definition whose single field impossible directly encodes the required universal-existential statement. No lemmas are applied; the body is the literal quantification over ε0 and r0 together with the negation of the concavity event for small r.
why it matters
The structure is consumed by the of_u4 theorem, which assembles the full U-4 contradiction from an export-to-payment lower bound, an upper bound on payments as r → 0, and the two impossibility hypotheses for absorption and concavity. It therefore supplies the spec-layer device for eliminating channel (P3) when that channel has not already been folded into payXi or payRho. In the Recognition framework this keeps the Navier-Stokes non-parasitism gate cleanly separated from the rest of the pipeline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.