U4NoExportHypothesis
plain-language theorem explainer
U4NoExportHypothesis encodes that export events at any fixed positive level ε₀ cannot persist below some positive radius r₀. Researchers closing the non-parasitism gate in the RM2U reduction of Navier-Stokes radial profiles would cite this structure when packaging the U-4 contradiction. The declaration is a pure structure definition whose single field directly records the quantified impossibility without invoking any lemmas.
Claim. The hypothesis states that for every ε₀ > 0 there exists r₀ > 0 such that ExportEvent(ε₀, r) is false for all r ∈ (0, r₀].
background
In the RM2U.NonParasitism module the non-parasitism condition is the vanishing of the tail-flux boundary term at infinity for the ℓ=2 coefficient. U4NoExportHypothesis abstracts the PDE objects and isolates the one-cylinder contradiction that export persistence at fixed ε₀ is impossible below some scale, mirroring the TeX lemma on U-4 contradiction from export while keeping all constants and moduli abstract. Upstream results supply RS-native units with c = 1, scales defined as powers of φ, ledger factorization structures, and phi-forcing objects that calibrate the underlying J-cost.
proof idea
This is a structure definition whose single field 'impossible' directly encodes the universal quantification over ε₀. No lemmas or tactics are applied; the declaration is pure bookkeeping that packages the impossibility statement.
why it matters
The structure supplies the U-4 contradiction hypothesis that feeds bet2SelfFalsification_of_u4 (once the profile-to-cylinder bridge is given) and of_u4. It fills the spec layer for the single hard non-parasitism gate in the RM2U to RM2 pipeline, aligning with the Recognition Science requirement that the boundary term vanishes. It touches the open question of discharging the hypothesis via concrete PDE bounds on payments, absorption, and concavity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.