of_u4
plain-language theorem explainer
The declaration shows that an export event forcing a payment lower bound of order epsilon squared or an absorption or concavity channel, combined with a payment upper bound that vanishes at small scales and the impossibility of absorption and concavity below certain radii, implies that the export event itself cannot occur below some scale. Analysts of the Navier-Stokes regularity problem in the Recognition Science framework would cite this to close the U-4 cylinder contradiction. The argument extracts constants via rcases, selects a common min-
Claim. Let $P$ be a payments structure with nonnegative components pay$ _xi(r)$ and pay$ _rho(r)$. Suppose the export-forces-payment hypothesis holds with constant $c>0$, so an export event at scales $varepsilon,r>0$ implies $c varepsilon^2 leq$ pay$ _xi(r)+$pay$ _rho(r)$ or absorption or concavity at that scale. Suppose the U-4 payment upper bound holds via a modulus $beta(r)$ that can be made arbitrarily small for small $r$. Assume absorption is impossible below a scale depending on $eta,varepsilon_0>0$, and concavity is impossible below a scale depending on $varepsilon_0>0$. Then export events cannot occur below some scale depending on $varepsilon_0$.
background
In the RM2U.NonParasitism module the local setting isolates non-parasitism as the single hard gate: tail-flux vanishing for the ell=2 coefficient on cylinders, formalized as the target U4NoExportHypothesis. The Payments structure abstracts normalized cylinder payments as uninterpreted nonnegative functions payXi and payRho, mirroring the TeX integrals over Q_r with the rho^{3/2} and rho^{3/4} weights. The ExportForcesPaymentHypothesis encodes the lower-bound implication from export to payment or absorption or concavity; U4PaymentUpperBoundHypothesis supplies the vanishing modulus beta; AbsorptionClassImpossibleHypothesis and ConcavityImpossibleHypothesis supply the scale-dependent exclusions. Upstream arithmetic le_trans chains the radius inequalities while RS-native units U fix the gauge with c=1.
proof idea
The term proof opens with classical, rcases the exists_c from the export-forces hypothesis and exists_beta from the payment upper bound, then refines the target impossible statement. It invokes the limit property of beta to obtain r_beta where beta is less than half the payment lower bound, pulls rAbs from absorption impossibility and rConc from concavity impossibility, and takes their minimum as the common r0. For any smaller r the export event triggers a case split on the or: the payment branch derives c varepsilon^2 leq beta(r) < c varepsilon^2/2 via the upper bound and limit, contradicting by nlinarith; the absorption and concavity branches are discharged directly by the impossibility statements.
why it matters
This bookkeeping result supplies the U-4 one-cylinder contradiction that supports the non-parasitism hypothesis (tail-flux vanishing) in the RM2U to RM2 pipeline. It fills the abstract step in the manuscript lemma on export-forced contradiction while keeping all PDE estimates as future hypotheses. Within the Recognition Science framework it isolates the only genuinely hard statement so the remainder of the Navier-Stokes translation remains checkable; it touches the open question of discharging the absorption and concavity impossibilities with concrete estimates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.