ProjectedPDEPairingHypothesisAt
plain-language theorem explainer
The declaration defines a hypothesis interface that decomposes the RM2U operator as rm2uOp(P) = F - At on (1, ∞) together with interval integrability and uniform bounds on the weighted pairings against P.A r². Researchers deriving Navier-Stokes from Recognition Science would cite it to bridge the projected PDE to the coercive L2 bound. The structure encodes the single analytic step of splitting the pairing integral so that separate bounds on the force and time-derivative terms yield the required combined bound.
Claim. Let $P$ be an RM2U radial profile and $a$ a real number. Functions $F, A_t : ℝ → ℝ$ satisfy the projected PDE pairing hypothesis at $a$ when rm2uOp$(P)(r) = F(r) - A_t(r)$ for all $r > 1$, the maps $x ↦ F(x) P.A(x) x^2$ and $x ↦ A_t(x) P.A(x) x^2$ are interval integrable on every $[a,R]$ with $R ≥ a$, and constants $C_F, C_T$ exist such that the absolute values of the integrals of these maps over $[a,R]$ remain bounded by $C_F$ and $C_T$ respectively.
background
The RM2U.ProjectedPDE module supplies a Lean-facing hypothesis interface that matches the TeX lemma on A-evolution, rewritten in operator language as rm2uOp$(P) = F - A_t$. This layer isolates the analytic step of bounding the single pairing integral by controlling the force and time-derivative contributions separately. The local setting assumes an RM2URadialProfile $P$ and a lower cutoff $a > 1$, with the operator rm2uOp drawn from the imported EnergyIdentity module. Upstream structures such as LedgerFactorization supply the underlying J-cost and phi-ladder conventions used to calibrate the radial profile.
proof idea
The declaration is a structure definition. Its associated theorem of_projectedPDEPairing is a one-line wrapper that copies the base fields from hbase, then extracts the separate uniform bounds CF and CT from hpde.hForcePair and hpde.hTimePair. It rewrites the rm2uOp pairing via intervalIntegral.integral_congr using hDecomp, splits the integral with intervalIntegral.integral_sub and the triangle inequality via norm_add_le, and concludes by add_le_add on the separate bounds.
why it matters
This hypothesis interface feeds directly into TailFluxVanishImpliesCoerciveHypothesisAt, which unlocks the already-proved coerciveL2Bound_of_tailFluxVanish. It fills the precise analytic gap identified in the TeX manuscript for the A-evolution step within the Recognition Science Navier-Stokes derivation. The construction stays inside the phi-forcing framework (T5 J-uniqueness, T8 D = 3) while leaving open the question of exhibiting explicit F and At that realize the decomposition for a concrete radial profile.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.