ProjectedPDEPairingHypothesisAt
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not specify explicit functional forms for F or At.
- Does not prove existence of such F and At.
- Does not address the full 3D Navier-Stokes projection.
- Does not derive the RM2U operator from the underlying J-cost.
- Does not supply numerical values for the bounding constants.
formal statement (Lean)
40structure ProjectedPDEPairingHypothesisAt (P : RM2URadialProfile) (a : ℝ)
41 (At F : ℝ → ℝ) : Prop where
42 /-- Pointwise relation on `(1,∞)`: `rm2uOp = F - At`. -/
43 hDecomp : ∀ r ∈ Set.Ioi (1 : ℝ), rm2uOp P r = F r - At r
44 /-- Interval-integrability of the forcing pairing on `[a,R]` (needed for linearity). -/
45 hForceInt :
46 ∀ R : ℝ, a ≤ R → IntervalIntegrable (fun x : ℝ => (F x) * (P.A x) * (x ^ 2)) volume a R
47 /-- Interval-integrability of the time-derivative pairing on `[a,R]` (needed for linearity). -/
48 hTimeInt :
49 ∀ R : ℝ, a ≤ R → IntervalIntegrable (fun x : ℝ => (At x) * (P.A x) * (x ^ 2)) volume a R
50 /-- Uniform bound on the forcing pairing on `[a,R]`. -/
51 hForcePair :
52 ∃ CF : ℝ, ∀ R : ℝ, a ≤ R → |∫ x in a..R, (F x) * (P.A x) * (x ^ 2)| ≤ CF
53 /-- Uniform bound on the time-derivative pairing on `[a,R]`. -/
54 hTimePair :
55 ∃ CT : ℝ, ∀ R : ℝ, a ≤ R → |∫ x in a..R, (At x) * (P.A x) * (x ^ 2)| ≤ CT
56
57/-- Build the `TailFluxVanishImpliesCoerciveHypothesisAt` interface from a projected PDE pairing
58decomposition plus the remaining local/interval hypotheses.
59
60This isolates the *single* extra analytic step that the TeX manuscript is implicitly using:
61bounding `∫ (F - A_t) A r^2` by bounding the two pairings separately.
62-/
63theorem TailFluxVanishImpliesCoerciveHypothesisAt.of_projectedPDEPairing
64 (P : RM2URadialProfile) (a : ℝ)
65 (hbase : TailFluxVanishImpliesCoerciveHypothesisAt P a)
66 {At F : ℝ → ℝ} (hpde : ProjectedPDEPairingHypothesisAt P a At F) :
67 TailFluxVanishImpliesCoerciveHypothesisAt P a := by
proof body
Definition body.
68 classical
69 refine
70 { ha1 := hbase.ha1
71 hA2_local := hbase.hA2_local
72 hA'2_local := hbase.hA'2_local
73 hA'_int := hbase.hA'_int
74 hV'_int := hbase.hV'_int
75 hf := hbase.hf
76 hg := hbase.hg
77 hPairBound := ?_ }
78
79 rcases hpde.hForcePair with ⟨CF, hCF⟩
80 rcases hpde.hTimePair with ⟨CT, hCT⟩
81 refine ⟨CF + CT, ?_⟩
82 intro R haR
83
84 -- Rewrite `rm2uOp` to `F - At` on `[a,R]` (note: `[a,R] ⊆ (1,∞)` because `1 < a`).
85 have hcongr :
86 (∫ x in a..R, (rm2uOp P x) * (P.A x) * (x ^ 2)) =
87 ∫ x in a..R, ((F x) - (At x)) * (P.A x) * (x ^ 2) := by
88 refine intervalIntegral.integral_congr ?_
89 intro x hx
90 have hx' : x ∈ Set.Icc a R := by
91 simpa [Set.uIcc_of_le haR] using hx
92 have hx1 : x ∈ Set.Ioi (1 : ℝ) := lt_of_lt_of_le hbase.ha1 hx'.1
93 simp [hpde.hDecomp x hx1]
94
95 -- Triangle inequality: split the pairing into force and time-derivative parts.
96 have hsplit :
97 |∫ x in a..R, ((F x) - (At x)) * (P.A x) * (x ^ 2)|
98 ≤ |∫ x in a..R, (F x) * (P.A x) * (x ^ 2)|
99 + |∫ x in a..R, (At x) * (P.A x) * (x ^ 2)| := by
100 -- `∫ ((F-At)*A*r^2) = ∫ (F*A*r^2) - ∫ (At*A*r^2)`.
101 have hsub :
102 (∫ x in a..R, ((F x) - (At x)) * (P.A x) * (x ^ 2)) =
103 (∫ x in a..R, (F x) * (P.A x) * (x ^ 2))
104 - ∫ x in a..R, (At x) * (P.A x) * (x ^ 2) := by
105 -- pointwise: `(F-At)*A*r^2 = (F*A*r^2) - (At*A*r^2)`
106 have hpt :
107 (fun x : ℝ => ((F x) - (At x)) * (P.A x) * (x ^ 2)) =
108 fun x : ℝ => (F x) * (P.A x) * (x ^ 2) - (At x) * (P.A x) * (x ^ 2) := by
109 funext x
110 ring
111 -- linearity requires interval integrability
112 simpa [hpt] using
113 (intervalIntegral.integral_sub (μ := volume) (a := a) (b := R)
114 (hf := hpde.hForceInt R haR) (hg := hpde.hTimeInt R haR))
115
116 -- `|u - v| = |u + (-v)| ≤ |u| + |v|`
117 set u : ℝ := ∫ x in a..R, (F x) * (P.A x) * (x ^ 2)
118 set v : ℝ := ∫ x in a..R, (At x) * (P.A x) * (x ^ 2)
119 have : |u - v| ≤ |u| + |v| := by
120 -- triangle inequality in `ℝ` written via the norm
121 simpa [Real.norm_eq_abs, sub_eq_add_neg, u, v] using (norm_add_le u (-v))
122 simpa [hsub, u, v] using this
123
124 calc
125 |∫ x in a..R, (rm2uOp P x) * (P.A x) * (x ^ 2)|
126 = |∫ x in a..R, ((F x) - (At x)) * (P.A x) * (x ^ 2)| := by
127 simp [hcongr]
128 _ ≤ |∫ x in a..R, (F x) * (P.A x) * (x ^ 2)|
129 + |∫ x in a..R, (At x) * (P.A x) * (x ^ 2)| := hsplit
130 _ ≤ CF + CT := by
131 exact add_le_add (hCF R haR) (hCT R haR)
132
133end RM2U
134end NavierStokes
135end IndisputableMonolith