NonParasitismHypothesis
plain-language theorem explainer
NonParasitismHypothesis isolates the condition that the tail flux vanishes at infinity for a radial profile in the RM2U Navier-Stokes setting. Analysts deriving fluid equations from Recognition Science cite the interface to quarantine the sole analytic difficulty from the algebraic closure steps. The declaration is a bare structure whose single field packages the TailFluxVanish predicate on the profile coefficients.
Claim. Let $P$ be a radial profile with coefficient functions $A$ and $A'$. The non-parasitism hypothesis for $P$ holds precisely when the tail-flux boundary term vanishes at infinity, i.e., when the integrability condition on $(-A)(A' r^2)$ over $(1,∞)$ is satisfied.
background
The RM2U.NonParasitism module isolates the non-parasitism condition as a temporary hypothesis so the RM2U to RM2 pipeline stays algebraic and checkable. Non-parasitism is the statement that the tail-flux boundary term at infinity vanishes for the relevant ℓ=2 coefficient. Upstream structures from LedgerFactorization calibrate the J-cost while IntegrationGap supplies the active-edge count per fundamental tick at D=3.
proof idea
The declaration is a structure definition that directly wraps the TailFluxVanish predicate as its sole field. No lemmas are applied; it serves purely as an interface for the three bet hypotheses.
why it matters
Downstream theorems nonParasitism_of_bet1, nonParasitism_of_bet2 and rm2Closed_of_nonParasitism invoke this hypothesis to reach RM2Closed. It supplies the single hard gate in the Recognition Science derivation of Navier-Stokes, allowing the rest of the pipeline to proceed without resolving the integrability question. The open question it touches is whether the condition follows from the Galerkin construction or from self-falsification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.