IndisputableMonolith.NavierStokes.RM2U.NonParasitism
IndisputableMonolith/NavierStokes/RM2U/NonParasitism.lean · 1145 lines · 61 declarations
show as:
view math explainer →
1import IndisputableMonolith.NavierStokes.RM2U.Core
2import IndisputableMonolith.NavierStokes.RM2U.EnergyIdentity
3import IndisputableMonolith.NavierStokes.RM2U.RM2Closure
4
5/-!
6# RM2U.NonParasitism (the single hard gate)
7
8This file is where the RS-aligned “non-parasitism” content should ultimately live.
9
10**Intent:** isolate the only genuinely hard statement as a single hypothesis (temporarily),
11so the rest of the RM2U → RM2 pipeline is clean and checkable.
12
13Non-parasitism, in the PDE translation used by the manuscript, is:
14
15> The tail-flux / boundary term at infinity vanishes for the relevant \(\ell=2\) coefficient.
16
17In Lean, this is `TailFluxVanish P.A P.A'`.
18-/
19
20namespace IndisputableMonolith
21namespace NavierStokes
22namespace RM2U
23
24open MeasureTheory Set Filter
25
26/-- Temporary hypothesis: “non-parasitism” for a fixed time-slice coefficient profile. -/
27structure NonParasitismHypothesis (P : RM2URadialProfile) : Prop where
28 tailFluxVanish : TailFluxVanish P.A P.A'
29
30/-!
31## Research bets as isolated interfaces
32
33These are *interfaces*, not proofs: each corresponds to one of the bet docs:
34
35- `docs/RM2U_BET_1_ATTACK.md`
36- `docs/RM2U_BET_2_ATTACK.md`
37- `docs/RM2U_BET_3_ATTACK.md`
38
39Keeping these in this file ensures the rest of the RM2U→RM2 pipeline remains purely algebraic.
40-/
41
42/-- **Bet 1 (integrability route)**: prove integrability of the tail-flux boundary term
43`(-A) * (A' * r^2)` and its derivative on `(1,∞)`. -/
44structure Bet1BoundaryIntegrableHypothesis (P : RM2URadialProfile) : Prop where
45 hB_int :
46 IntegrableOn (fun x : ℝ => (-P.A x) * ((P.A' x) * (x ^ 2))) (Set.Ioi (1 : ℝ)) volume
47 hB'_int :
48 IntegrableOn
49 (fun x : ℝ =>
50 (-(P.A' x)) * ((P.A' x) * (x ^ 2)) + (-P.A x) * ((P.A'' x) * (x ^ 2) + (P.A' x) * (2 * x)))
51 (Set.Ioi (1 : ℝ)) volume
52
53theorem nonParasitism_of_bet1 (P : RM2URadialProfile) (h : Bet1BoundaryIntegrableHypothesis P) :
54 NonParasitismHypothesis P :=
55 ⟨RM2U.tailFluxVanish_of_integrable (P := P) h.hB_int h.hB'_int⟩
56
57/-!
58### Bet 1 helper: `B ∈ L¹((1,∞))` from a weighted \(L^2\) hypothesis
59
60The boundary term is:
61
62`B(r) = (-A r) * (A' r * r^2) = ((-A r) * r) * ((A' r) * r)`.
63
64So a **checkable sufficient condition** for `B ∈ L¹((1,∞))` is:
65
66- `A(r) * r ∈ L²((1,∞))` and
67- `A'(r) * r ∈ L²((1,∞))`.
68
69The second condition is already implied by `CoerciveL2Bound` (since it is exactly
70`(A')^2 * r^2` integrable). The first is a genuinely stronger tail/moment condition that might be
71provable from additional PDE input or a non-resonant-scale argument.
72-/
73
74/-- If `A(r) * r ∈ L²((1,∞))` and `A'(r) * r ∈ L²((1,∞))`, then the boundary term
75`B(r)=(-A) * (A'*r^2)` is integrable on `(1,∞)`. -/
76theorem bet1_boundaryTerm_integrable_of_L2_mul_r
77 (P : RM2URadialProfile)
78 (hA2r : IntegrableOn (fun r : ℝ => (P.A r) ^ 2 * (r ^ 2)) (Set.Ioi (1 : ℝ)) volume)
79 (hA'2r : IntegrableOn (fun r : ℝ => (P.A' r) ^ 2 * (r ^ 2)) (Set.Ioi (1 : ℝ)) volume) :
80 IntegrableOn (fun r : ℝ => (-P.A r) * ((P.A' r) * (r ^ 2))) (Set.Ioi (1 : ℝ)) volume := by
81 classical
82 -- Work on the restricted measure.
83 let μ := (volume.restrict (Set.Ioi (1 : ℝ)))
84
85 -- Show `(-A r)*r ∈ L²` and `(A' r)*r ∈ L²`.
86 have hcontA : ContinuousOn P.A (Set.Ioi (1 : ℝ)) := by
87 intro x hx
88 exact (P.hA x hx).continuousAt.continuousWithinAt
89 have hcontA' : ContinuousOn P.A' (Set.Ioi (1 : ℝ)) := by
90 intro x hx
91 exact (P.hA' x hx).continuousAt.continuousWithinAt
92 have hf_meas : AEStronglyMeasurable (fun r : ℝ => (-P.A r) * r) μ := by
93 have hcont : ContinuousOn (fun r : ℝ => (-P.A r) * r) (Set.Ioi (1 : ℝ)) := by
94 simpa using (hcontA.neg.mul (continuous_id.continuousOn))
95 exact hcont.aestronglyMeasurable measurableSet_Ioi
96 have hg_meas : AEStronglyMeasurable (fun r : ℝ => (P.A' r) * r) μ := by
97 have hcont : ContinuousOn (fun r : ℝ => (P.A' r) * r) (Set.Ioi (1 : ℝ)) := by
98 simpa using (hcontA'.mul (continuous_id.continuousOn))
99 exact hcont.aestronglyMeasurable measurableSet_Ioi
100
101 have hf_L2 : MeasureTheory.MemLp (fun r : ℝ => (-P.A r) * r) 2 μ := by
102 -- use `memLp_two_iff_integrable_sq`
103 refine (MeasureTheory.memLp_two_iff_integrable_sq (μ := μ) hf_meas).2 ?_
104 -- square equals `A^2 * r^2`
105 have : Integrable (fun r : ℝ => (P.A r) ^ 2 * (r ^ 2)) μ := by
106 simpa [MeasureTheory.IntegrableOn, μ] using hA2r
107 -- rewrite the integrand
108 simpa [pow_two, μ, mul_assoc, mul_left_comm, mul_comm] using this
109
110 have hg_L2 : MeasureTheory.MemLp (fun r : ℝ => (P.A' r) * r) 2 μ := by
111 refine (MeasureTheory.memLp_two_iff_integrable_sq (μ := μ) hg_meas).2 ?_
112 have : Integrable (fun r : ℝ => (P.A' r) ^ 2 * (r ^ 2)) μ := by
113 simpa [MeasureTheory.IntegrableOn, μ] using hA'2r
114 simpa [pow_two, μ, mul_assoc, mul_left_comm, mul_comm] using this
115
116 -- L² × L² → L¹ by Hölder (p=q=2, r=1).
117 have hprod : Integrable (fun r : ℝ => ((-P.A r) * r) * ((P.A' r) * r)) μ := by
118 -- `HolderTriple 2 2 1` is an instance
119 simpa [Pi.mul_def] using (MeasureTheory.MemLp.integrable_mul (μ := μ) hf_L2 hg_L2)
120
121 -- rewrite the product as the boundary term.
122 have : Integrable (fun r : ℝ => (-P.A r) * ((P.A' r) * (r ^ 2))) μ := by
123 -- pointwise: `((-A)*r) * ((A')*r) = (-A) * (A' * r^2)`
124 refine hprod.congr ?_
125 refine (ae_restrict_mem measurableSet_Ioi).mono ?_
126 intro r hr
127 ring
128 simpa [MeasureTheory.IntegrableOn, μ] using this
129
130/-- Convenience wrapper: if `CoerciveL2Bound P` holds, it suffices to prove only the stronger
131weighted \(L^2\) tail moment `∫ (A^2 * r^2) < ∞` to get `B ∈ L¹`. -/
132theorem bet1_boundaryTerm_integrable_of_A2r_and_coercive
133 (P : RM2URadialProfile)
134 (hA2r : IntegrableOn (fun r : ℝ => (P.A r) ^ 2 * (r ^ 2)) (Set.Ioi (1 : ℝ)) volume)
135 (hCoercive : CoerciveL2Bound P) :
136 IntegrableOn (fun r : ℝ => (-P.A r) * ((P.A' r) * (r ^ 2))) (Set.Ioi (1 : ℝ)) volume :=
137 bet1_boundaryTerm_integrable_of_L2_mul_r (P := P) hA2r hCoercive.2
138
139/-!
140### Bet 1 (alternate surface): rewrite the `B'` integrand using `rm2uOp`
141
142The “raw” Bet‑1 interface requires integrability of an expression involving `A''`.
143Using the algebraic identity in `RM2U.EnergyIdentity`, we can replace that with integrability of
144the RM2U operator pairing `rm2uOp*A*r^2` plus the coercive terms (which are already the natural
145output of the RM2U energy identity).
146
147This does **not** solve Bet 1, but it shrinks the remaining analytic work to a more PDE-aligned
148pairing estimate.
149-/
150
151/-- Alternate Bet‑1 interface: keep the same boundary term `B` integrability, but replace the `B'`
152integrability surface by the RM2U operator pairing plus coercive \(L^2\) control. -/
153structure Bet1BoundaryIntegrableHypothesisAlt (P : RM2URadialProfile) : Prop where
154 hB_int :
155 IntegrableOn (fun x : ℝ => (-P.A x) * ((P.A' x) * (x ^ 2))) (Set.Ioi (1 : ℝ)) volume
156 hPair_int :
157 IntegrableOn (fun x : ℝ => (rm2uOp P x) * (P.A x) * (x ^ 2)) (Set.Ioi (1 : ℝ)) volume
158 hCoercive : CoerciveL2Bound P
159
160/-- `Bet1BoundaryIntegrableHypothesisAlt` implies the original Bet‑1 hypothesis. -/
161theorem bet1_of_bet1Alt (P : RM2URadialProfile) (h : Bet1BoundaryIntegrableHypothesisAlt P) :
162 Bet1BoundaryIntegrableHypothesis P := by
163 refine ⟨h.hB_int, ?_⟩
164 -- Work on the restricted measure.
165 let μ := (volume.restrict (Set.Ioi (1 : ℝ)))
166
167 -- Build integrability of the RM2U-rewritten RHS:
168 have hPair : Integrable (fun x : ℝ => (rm2uOp P x) * (P.A x) * (x ^ 2)) μ := by
169 simpa [IntegrableOn, μ] using h.hPair_int
170 have hA2 : Integrable (fun x : ℝ => (P.A x) ^ 2) μ := by
171 simpa [IntegrableOn, μ] using h.hCoercive.1
172 have hAprime2 : Integrable (fun x : ℝ => (P.A' x) ^ 2 * (x ^ 2)) μ := by
173 simpa [IntegrableOn, μ] using h.hCoercive.2
174
175 have hRHS :
176 Integrable
177 (fun x : ℝ =>
178 (rm2uOp P x) * (P.A x) * (x ^ 2)
179 - (P.A' x) ^ 2 * (x ^ 2)
180 - 6 * (P.A x) ^ 2) μ := by
181 -- close under subtraction and scalar multiplication
182 have h6A2 : Integrable (fun x : ℝ => 6 * (P.A x) ^ 2) μ := by
183 simpa [mul_assoc] using (hA2.const_mul (6 : ℝ))
184 exact (hPair.sub hAprime2).sub h6A2
185
186 -- Show the original Bet‑1 integrand agrees a.e. with the rewritten RHS on `(1,∞)`.
187 have hAE :
188 (fun x : ℝ =>
189 (-(P.A' x)) * ((P.A' x) * (x ^ 2))
190 + (-P.A x) * ((P.A'' x) * (x ^ 2) + (P.A' x) * (2 * x)))
191 =ᵐ[μ]
192 (fun x : ℝ =>
193 (rm2uOp P x) * (P.A x) * (x ^ 2)
194 - (P.A' x) ^ 2 * (x ^ 2)
195 - 6 * (P.A x) ^ 2) := by
196 -- pointwise on `x > 1` we can apply the algebraic lemma (`x ≠ 0`).
197 refine (ae_restrict_mem measurableSet_Ioi).mono ?_
198 intro x hx
199 have hx0 : x ≠ 0 := ne_of_gt (lt_trans (by norm_num : (0 : ℝ) < 1) (mem_Ioi.1 hx))
200 -- rewrite using the proved identity
201 simpa using (bet1_boundaryTerm_deriv_integrand_eq (P := P) (r := x) hx0)
202
203 -- Transfer integrability across the a.e. equality.
204 have : Integrable
205 (fun x : ℝ =>
206 (-(P.A' x)) * ((P.A' x) * (x ^ 2))
207 + (-P.A x) * ((P.A'' x) * (x ^ 2) + (P.A' x) * (2 * x))) μ :=
208 hRHS.congr hAE.symm
209
210 simpa [IntegrableOn, μ] using this
211
212/-- **Bet 2 (self-falsification route)**: encode “if tail-flux does *not* vanish, we reach a contradiction”.
213This keeps the interface honest while leaving the contradiction mechanism open. -/
214structure Bet2SelfFalsificationHypothesis (P : RM2URadialProfile) : Prop where
215 selfFalsify : (¬ TailFluxVanish P.A P.A') → False
216
217/-!
218## Bet 2 (prime/non-resonant scale schedule) — skeleton
219
220This section encodes a *generic* contradiction shape that could plausibly use primes/coprime
221cycles as a “non-resonant” schedule for extracting disjoint scale contributions.
222
223It does **not** prove RM2U; it just provides a clean interface:
224
225- show that **if** tail-flux does not vanish, then along some (prime) schedule one gets a uniform
226 lower bound on the tail export (a “persistent parasitism signal”);
227- independently show (from energy / budget / disjointness) that the same schedule forces the
228 absolute tail export to be summable;
229- contradiction, hence tail-flux must vanish.
230
231The only “prime content” we hard-code here is the existence of a canonical strictly increasing
232pairwise-coprime schedule `n ↦ nthPrime n`.
233-/
234
235namespace Bet2PrimeSchedule
236
237open Nat
238
239/-- Canonical prime scale schedule: `pₙ = (n)th prime`. -/
240noncomputable def nthPrime (n : ℕ) : ℕ := Nat.nth Nat.Prime n
241
242theorem nthPrime_prime (n : ℕ) : Nat.Prime (nthPrime n) := by
243 -- `Nat.prime_nth_prime` is in `Mathlib/NumberTheory/PrimeCounting`.
244 simpa [nthPrime] using (Nat.prime_nth_prime n)
245
246theorem strictMono_nthPrime : StrictMono nthPrime := by
247 simpa [nthPrime] using (Nat.nth_strictMono Nat.infinite_setOf_prime)
248
249theorem pairwise_coprime_nthPrime : Pairwise fun i j => Nat.Coprime (nthPrime i) (nthPrime j) := by
250 intro i j hij
251 have hpi : Nat.Prime (nthPrime i) := nthPrime_prime i
252 have hpj : Nat.Prime (nthPrime j) := nthPrime_prime j
253 have hne : nthPrime i ≠ nthPrime j := (strictMono_nthPrime.injective.ne hij)
254 -- Use `Nat.Prime.coprime_iff_not_dvd` + prime divisibility rigidity.
255 refine (Nat.Prime.coprime_iff_not_dvd hpi).2 ?_
256 intro hdiv
257 have : nthPrime i = nthPrime j := (Nat.prime_dvd_prime_iff_eq hpi hpj).1 hdiv
258 exact hne this
259
260/-- A “non-resonant” integer schedule: strictly increasing and pairwise coprime. -/
261structure NonResonantSchedule where
262 s : ℕ → ℕ
263 strictMono : StrictMono s
264 pairwise_coprime : Pairwise fun i j => Nat.Coprime (s i) (s j)
265
266/-- The canonical non-resonant schedule given by primes. -/
267noncomputable def canonical : NonResonantSchedule :=
268 { s := nthPrime
269 strictMono := strictMono_nthPrime
270 pairwise_coprime := pairwise_coprime_nthPrime }
271
272/-- Generic divergence fact: a uniform positive lower bound on `|a n|` prevents summability. -/
273theorem not_summable_of_uniform_abs_lowerBound {a : ℕ → ℝ} {ε : ℝ}
274 (hε : 0 < ε) (hlow : ∀ n, ε ≤ |a n|) :
275 ¬ Summable (fun n => |a n|) := by
276 intro hsum
277 have ht : Tendsto (fun n => |a n|) atTop (nhds 0) :=
278 (Summable.tendsto_atTop_zero hsum)
279 -- pick `n` large enough so `|a n| < ε`, contradicting the uniform lower bound.
280 have hEvt : ∀ᶠ n in atTop, |a n| < ε := (ht.eventually_lt_const hε)
281 rcases (Filter.eventually_atTop.1 hEvt) with ⟨N, hN⟩
282 have hcontra : ε ≤ |a N| := hlow N
283 exact (not_lt_of_ge hcontra) (hN N (le_rfl))
284
285/-- **Bet 2 prime-schedule interface**:
286if non-parasitism fails, you can lower-bound `|tailFlux|` *along the prime schedule*;
287and separately you can prove a summability/budget bound along the same schedule. -/
288structure PrimeScheduleSelfFalsification (P : RM2URadialProfile) : Prop where
289 /-- A lower bound along the prime schedule implied by failure of tail-flux vanishing. -/
290 lowerBound_of_notVanish :
291 (¬ TailFluxVanish P.A P.A') →
292 ∃ ε : ℝ, 0 < ε ∧ ∀ n : ℕ, ε ≤ |tailFlux P.A P.A' (nthPrime n)|
293 /-- A (budget/disjointness) summability statement along the same schedule. -/
294 summable_abs :
295 Summable (fun n : ℕ => |tailFlux P.A P.A' (nthPrime n)|)
296
297/-- The prime-schedule interface yields the standard Bet-2 “self-falsification” hypothesis. -/
298theorem bet2_of_primeSchedule (P : RM2URadialProfile) (h : PrimeScheduleSelfFalsification P) :
299 Bet2SelfFalsificationHypothesis P := by
300 refine ⟨?_⟩
301 intro hnot
302 rcases h.lowerBound_of_notVanish hnot with ⟨ε, hε, hlow⟩
303 have : ¬ Summable (fun n : ℕ => |tailFlux P.A P.A' (nthPrime n)|) :=
304 not_summable_of_uniform_abs_lowerBound (a := fun n => tailFlux P.A P.A' (nthPrime n)) hε hlow
305 exact this h.summable_abs
306
307end Bet2PrimeSchedule
308
309/-!
310### Optional finer-grained Bet 2 interfaces (U-4 / one-cylinder payment view)
311
312The Bet 2 execution plan (`docs/RM2U_BET_2_EXECUTION_PLAN.md`) works at the level of a *single rescaled cylinder*
313and derives a contradiction by forcing a strictly-positive “payment” lower bound on that cylinder which is then
314incompatible with a small-scale upper bound.
315
316We do **not** have the full PDE objects (ρ, ξ, σ, tail strain fields) formalized in Lean yet, so the most honest
317way to reflect that work here is as **Prop-only hypothesis interfaces** parameterized by abstract predicates.
318
319These interfaces are designed to be instantiated later once the running-max cylinder solution objects exist in Lean.
320-/
321
322namespace Bet2U4
323
324/-- Abstract normalized cylinder payments.
325
326In the TeX, these are:
327- `PayXi r := (1/r^2) ∬_{Q_r} ρ^{3/2} |∇ξ|^2`
328- `PayRho r := (1/r^2) η^{-1} ∬_{Q_r ∩ {1-2η<ρ<1-η}} |∇(ρ^{3/4})|^2`
329
330At the Lean spec layer, we keep them as uninterpreted functions `ℝ → ℝ`. -/
331structure Payments where
332 payXi : ℝ → ℝ
333 payRho : ℝ → ℝ
334 payXi_nonneg : ∀ r : ℝ, 0 ≤ payXi r
335 payRho_nonneg : ∀ r : ℝ, 0 ≤ payRho r
336
337/-- **U-4 cylinder payment upper bound (spec layer):** normalized payments become small at small scales.
338
339This mirrors TeX Hypothesis `hyp:U4_payment_upper_bound`. We keep the decay modulus abstract. -/
340structure U4PaymentUpperBoundHypothesis (P : Payments) : Prop where
341 exists_beta :
342 ∃ β : ℝ → ℝ,
343 (∀ r : ℝ, 0 < r → 0 ≤ β r) ∧
344 (∀ ε : ℝ, 0 < ε → ∃ r0 : ℝ, 0 < r0 ∧ ∀ r : ℝ, 0 < r → r ≤ r0 → β r ≤ ε) ∧
345 ∀ r : ℝ, 0 < r → P.payXi r + P.payRho r ≤ β r
346
347/-- **C2-style vanishing positive injection (spec layer):** a scale-modulus controlling the (scale-invariant)
348positive stretching injection `injPos r` on cylinders.
349
350This mirrors TeX Hypothesis `hyp:C2_vanishing_injection` in its scale-invariant form
351(`navier-dec-12-rewrite.tex`, Eq. `eq:C2-stretch-hyp`). -/
352structure C2VanishingInjectionHypothesis (injPos : ℝ → ℝ) : Prop where
353 exists_alpha :
354 ∃ α : ℝ → ℝ,
355 (∀ r : ℝ, 0 < r → 0 ≤ α r) ∧
356 (∀ ε : ℝ, 0 < ε → ∃ r0 : ℝ, 0 < r0 ∧ ∀ r : ℝ, 0 < r → r ≤ r0 → α r ≤ ε) ∧
357 ∀ r : ℝ, 0 < r → injPos r ≤ α r
358
359/-- Alias for the U-4 “rate-strengthened” injection gate: in practice one instantiates `injPos r` with
360`(1/r^2) ∬_{Q_r} ρ^{3/2} σ_+` (once the PDE objects exist in Lean). -/
361abbrev U4VanishingInjectionRateHypothesis (injPos : ℝ → ℝ) : Prop :=
362 C2VanishingInjectionHypothesis injPos
363
364/-- If the (normalized) positive injection `injPos r` vanishes at small scales, then so does the
365rescaled injection `injPos (2*r)`. This is the only “scale-change” bookkeeping we need to match the TeX
366convention where many inequalities naturally live on `Q_{2r}`. -/
367theorem c2VanishingInjection_comp_two (injPos : ℝ → ℝ) (h : C2VanishingInjectionHypothesis injPos) :
368 C2VanishingInjectionHypothesis (fun r => injPos (2 * r)) := by
369 classical
370 rcases h.exists_alpha with ⟨α, hα_nonneg, hα_lim, hInj_le⟩
371 refine ⟨fun r => α (2 * r), ?_, ?_, ?_⟩
372 · intro r hr
373 have hr2 : 0 < 2 * r := by nlinarith
374 exact hα_nonneg (2 * r) hr2
375 · intro ε hε
376 rcases hα_lim ε hε with ⟨r0, hr0, hr0_bound⟩
377 refine ⟨r0 / 2, by nlinarith, ?_⟩
378 intro r hr hrr0
379 have hr2 : 0 < 2 * r := by nlinarith
380 have h2r_le : 2 * r ≤ r0 := by nlinarith
381 simpa using hr0_bound (2 * r) hr2 h2r_le
382 · intro r hr
383 have hr2 : 0 < 2 * r := by nlinarith
384 simpa using hInj_le (2 * r) hr2
385
386/-- **C2 ⇒ U4 upper bound** (spec layer): if payments are bounded by positive injection plus a vanishing error,
387then vanishing positive injection implies vanishing payments.
388
389This abstracts the TeX deduction
390`lem:U4_payment_upper_bound_of_U4_vanishing_injection_rate` once `injPos r` is instantiated by the
391**normalized** injection `(1/r^2) ∬_{Q_r} ρ^{3/2} σ_+` and `err r` packages the lower-order running-max
392terms (e.g. the `O(r)` errors after dividing by `r^2`). -/
393theorem u4PaymentUpperBound_of_injection
394 (P : Payments) (injPos err : ℝ → ℝ)
395 (hInj : C2VanishingInjectionHypothesis injPos)
396 (hErr :
397 ∃ e : ℝ → ℝ,
398 (∀ r : ℝ, 0 < r → 0 ≤ e r) ∧
399 (∀ ε : ℝ, 0 < ε → ∃ r0 : ℝ, 0 < r0 ∧ ∀ r : ℝ, 0 < r → r ≤ r0 → e r ≤ ε) ∧
400 ∀ r : ℝ, 0 < r → err r ≤ e r)
401 (hBound : ∃ C : ℝ, 0 ≤ C ∧ ∀ r : ℝ, 0 < r → P.payXi r + P.payRho r ≤ C * injPos r + err r) :
402 U4PaymentUpperBoundHypothesis P := by
403 classical
404 rcases hInj.exists_alpha with ⟨α, hα_nonneg, hα_lim, hInj_le⟩
405 rcases hErr with ⟨e, he_nonneg, he_lim, hErr_le⟩
406 rcases hBound with ⟨C, hC0, hBound⟩
407 refine ⟨fun r => C * α r + e r, ?_, ?_, ?_⟩
408 · intro r hr
409 exact add_nonneg (mul_nonneg hC0 (hα_nonneg r hr)) (he_nonneg r hr)
410 · intro ε hε
411 -- split ε into two halves
412 have hε2 : 0 < ε / 2 := by nlinarith
413 have hpos : 0 < ε / (2 * max C 1) := by
414 have hmaxpos : 0 < max C 1 :=
415 lt_of_lt_of_le (by norm_num : (0 : ℝ) < 1) (le_max_right _ _)
416 have hden : 0 < 2 * max C 1 := by nlinarith
417 exact div_pos hε hden
418 rcases hα_lim (ε / (2 * max C 1)) hpos with ⟨rα, hrα, hrα_bound⟩
419 rcases he_lim (ε / 2) hε2 with ⟨re, hre, hre_bound⟩
420 refine ⟨min rα re, lt_min hrα hre, ?_⟩
421 intro r hr hrr0
422 have hrrα : r ≤ rα := le_trans hrr0 (min_le_left _ _)
423 have hrre : r ≤ re := le_trans hrr0 (min_le_right _ _)
424 have hα : α r ≤ ε / (2 * max C 1) := hrα_bound r hr hrrα
425 have he : e r ≤ ε / 2 := hre_bound r hr hrre
426 -- bound `C * γ r` by `ε/2`
427 have hC1 : C ≤ max C 1 := le_max_left _ _
428 have hmaxpos : 0 < max C 1 :=
429 lt_of_lt_of_le (by norm_num : (0 : ℝ) < 1) (le_max_right _ _)
430 have hCα : C * α r ≤ (max C 1) * α r := mul_le_mul_of_nonneg_right hC1 (hα_nonneg r hr)
431 have hα' : (max C 1) * α r ≤ (max C 1) * (ε / (2 * max C 1)) :=
432 mul_le_mul_of_nonneg_left hα (le_of_lt hmaxpos)
433 have hhalf : (max C 1) * (ε / (2 * max C 1)) = ε / 2 := by
434 field_simp [ne_of_gt hmaxpos]
435 have hCα' : C * α r ≤ ε / 2 := by
436 exact hCα.trans (hα'.trans (by simp [hhalf]))
437 -- combine
438 have : C * α r + e r ≤ ε / 2 + ε / 2 := add_le_add hCα' he
439 nlinarith
440 · intro r hr
441 have hPay : P.payXi r + P.payRho r ≤ C * injPos r + err r := hBound r hr
442 have hInj' : injPos r ≤ α r := hInj_le r hr
443 have hErr' : err r ≤ e r := hErr_le r hr
444 have : C * injPos r + err r ≤ C * α r + e r :=
445 add_le_add (mul_le_mul_of_nonneg_left hInj' hC0) hErr'
446 exact hPay.trans this
447
448/-- Convenience wrapper: `U4VanishingInjectionRateHypothesis` is just an alias of
449`C2VanishingInjectionHypothesis`, intended for the normalized injection rate used by U‑4. -/
450theorem u4PaymentUpperBound_of_u4InjectionRate
451 (P : Payments) (injRate err : ℝ → ℝ)
452 (hInj : U4VanishingInjectionRateHypothesis injRate)
453 (hErr :
454 ∃ e : ℝ → ℝ,
455 (∀ r : ℝ, 0 < r → 0 ≤ e r) ∧
456 (∀ ε : ℝ, 0 < ε → ∃ r0 : ℝ, 0 < r0 ∧ ∀ r : ℝ, 0 < r → r ≤ r0 → e r ≤ ε) ∧
457 ∀ r : ℝ, 0 < r → err r ≤ e r)
458 (hBound : ∃ C : ℝ, 0 ≤ C ∧ ∀ r : ℝ, 0 < r → P.payXi r + P.payRho r ≤ C * injRate r + err r) :
459 U4PaymentUpperBoundHypothesis P := by
460 simpa [U4VanishingInjectionRateHypothesis] using
461 (u4PaymentUpperBound_of_injection (P := P) (injPos := injRate) (err := err) hInj hErr hBound)
462
463/-- **U-4 payment control interface (spec layer):** the (normalized) payments are bounded by
464the (normalized) positive injection rate plus an `o(1)` error.
465
466This mirrors the TeX interface `hyp:U4_payments_controlled_by_injection_rate`.
467It is the minimal PDE analytic input needed to turn a vanishing injection rate into
468`U4PaymentUpperBoundHypothesis`. -/
469structure U4PaymentsControlledByInjectionRateHypothesis
470 (P : Payments) (injRate : ℝ → ℝ) : Prop where
471 exists_bound :
472 ∃ (C : ℝ) (err : ℝ → ℝ),
473 0 ≤ C ∧
474 (∃ e : ℝ → ℝ,
475 (∀ r : ℝ, 0 < r → 0 ≤ e r) ∧
476 (∀ ε : ℝ, 0 < ε → ∃ r0 : ℝ, 0 < r0 ∧ ∀ r : ℝ, 0 < r → r ≤ r0 → e r ≤ ε) ∧
477 ∀ r : ℝ, 0 < r → err r ≤ e r) ∧
478 ∀ r : ℝ, 0 < r → P.payXi r + P.payRho r ≤ C * injRate r + err r
479
480/-- **U-4 `PayXi` control by the (normalized) positive injection rate (spec layer). -/
481structure U4PayXiControlledByInjectionRateHypothesis
482 (P : Payments) (injRate : ℝ → ℝ) : Prop where
483 exists_bound :
484 ∃ (C : ℝ) (err : ℝ → ℝ),
485 0 ≤ C ∧
486 (∃ e : ℝ → ℝ,
487 (∀ r : ℝ, 0 < r → 0 ≤ e r) ∧
488 (∀ ε : ℝ, 0 < ε → ∃ r0 : ℝ, 0 < r0 ∧ ∀ r : ℝ, 0 < r → r ≤ r0 → e r ≤ ε) ∧
489 ∀ r : ℝ, 0 < r → err r ≤ e r) ∧
490 ∀ r : ℝ, 0 < r → P.payXi r ≤ C * injRate (2 * r) + err r
491
492/-- **U-4 `PayRho` control by the (normalized) positive injection rate (spec layer). -/
493structure U4PayRhoControlledByInjectionRateHypothesis
494 (P : Payments) (injRate : ℝ → ℝ) : Prop where
495 exists_bound :
496 ∃ (C : ℝ) (err : ℝ → ℝ),
497 0 ≤ C ∧
498 (∃ e : ℝ → ℝ,
499 (∀ r : ℝ, 0 < r → 0 ≤ e r) ∧
500 (∀ ε : ℝ, 0 < ε → ∃ r0 : ℝ, 0 < r0 ∧ ∀ r : ℝ, 0 < r → r ≤ r0 → e r ≤ ε) ∧
501 ∀ r : ℝ, 0 < r → err r ≤ e r) ∧
502 ∀ r : ℝ, 0 < r → P.payRho r ≤ C * injRate (2 * r) + err r
503
504/-- **U-4 band-budget reduction to positive injection (spec layer).**
505
506This mirrors TeX Hypothesis `hyp:U4_band_budget_controlled_by_injection_rate`: it abstracts the single
507missing analytic step in the PayRho-control gate, namely controlling the scale-critical “budget term”
508coming from the band-payment inequality by the (normalized) positive injection rate plus an `o(1)` error. -/
509structure U4BandBudgetControlledByInjectionRateHypothesis
510 (bandBudget : ℝ → ℝ) (injRate : ℝ → ℝ) : Prop where
511 exists_bound :
512 ∃ (C : ℝ) (err : ℝ → ℝ),
513 0 ≤ C ∧
514 (∃ e : ℝ → ℝ,
515 (∀ r : ℝ, 0 < r → 0 ≤ e r) ∧
516 (∀ ε : ℝ, 0 < ε → ∃ r0 : ℝ, 0 < r0 ∧ ∀ r : ℝ, 0 < r → r ≤ r0 → e r ≤ ε) ∧
517 ∀ r : ℝ, 0 < r → err r ≤ e r) ∧
518 ∀ r : ℝ, 0 < r → bandBudget r ≤ C * injRate (2 * r) + err r
519
520/-- **Bookkeeping lemma (PayRho):** if `PayRho` is bounded by a scale-critical band budget plus an `O(r)`
521term (coming from the known band-payment inequality), and that band budget is controlled by the injection
522rate plus `o(1)`, then `PayRho` is controlled by the injection rate plus `o(1)`.
523
524This isolates the PDE content to the two hypotheses; the proof here is pure algebra/ε–δ bookkeeping. -/
525theorem u4PayRhoControlledByInjectionRate_of_bandBudget
526 (P : Payments) (injRate bandBudget : ℝ → ℝ)
527 (hBand :
528 ∃ C0 : ℝ,
529 0 ≤ C0 ∧
530 ∀ r : ℝ, 0 < r → P.payRho r ≤ C0 * bandBudget r + C0 * r)
531 (hBud : U4BandBudgetControlledByInjectionRateHypothesis bandBudget injRate) :
532 U4PayRhoControlledByInjectionRateHypothesis P injRate := by
533 classical
534 rcases hBand with ⟨C0, hC00, hBand⟩
535 rcases hBud.exists_bound with ⟨C1, err1, hC10, hErr1, hBud⟩
536 rcases hErr1 with ⟨e1, he1_nonneg, he1_lim, hErr1_le⟩
537
538 -- package the new error term: `C0 * err1 r + C0 * r`
539 let err : ℝ → ℝ := fun r => C0 * err1 r + C0 * r
540 have hErr :
541 ∃ e : ℝ → ℝ,
542 (∀ r : ℝ, 0 < r → 0 ≤ e r) ∧
543 (∀ ε : ℝ, 0 < ε → ∃ r0 : ℝ, 0 < r0 ∧ ∀ r : ℝ, 0 < r → r ≤ r0 → e r ≤ ε) ∧
544 ∀ r : ℝ, 0 < r → err r ≤ e r := by
545 refine ⟨fun r => C0 * e1 r + C0 * r, ?_, ?_, ?_⟩
546 · intro r hr
547 exact
548 add_nonneg
549 (mul_nonneg hC00 (he1_nonneg r hr))
550 (mul_nonneg hC00 (le_of_lt hr))
551 · intro ε hε
552 by_cases hC0 : C0 = 0
553 · subst hC0
554 refine ⟨1, by norm_num, ?_⟩
555 intro r hr hrr0
556 -- `e r = 0`, so it suffices that `0 ≤ ε`
557 simpa using (le_of_lt hε)
558 · have hC0pos : 0 < C0 := lt_of_le_of_ne hC00 (Ne.symm hC0)
559 have hden : 0 < 2 * C0 := by nlinarith
560 have hε2 : 0 < ε / (2 * C0) := div_pos hε hden
561 rcases he1_lim (ε / (2 * C0)) hε2 with ⟨r1, hr1, hr1_bound⟩
562 refine ⟨min r1 (ε / (2 * C0)), lt_min hr1 hε2, ?_⟩
563 intro r hr hrr0
564 have hr_le_r1 : r ≤ r1 := le_trans hrr0 (min_le_left _ _)
565 have hr_le_eps : r ≤ ε / (2 * C0) := le_trans hrr0 (min_le_right _ _)
566 have he1 : e1 r ≤ ε / (2 * C0) := hr1_bound r hr hr_le_r1
567 have hC0e1 : C0 * e1 r ≤ ε / 2 := by
568 have : C0 * e1 r ≤ C0 * (ε / (2 * C0)) :=
569 mul_le_mul_of_nonneg_left he1 hC00
570 have hC0ne : C0 ≠ 0 := hC0
571 have hmul : C0 * (ε / (2 * C0)) = ε / 2 := by
572 field_simp [hC0ne]
573 exact this.trans (by simpa [hmul])
574 have hC0r : C0 * r ≤ ε / 2 := by
575 have : C0 * r ≤ C0 * (ε / (2 * C0)) :=
576 mul_le_mul_of_nonneg_left hr_le_eps hC00
577 have hC0ne : C0 ≠ 0 := hC0
578 have hmul : C0 * (ε / (2 * C0)) = ε / 2 := by
579 field_simp [hC0ne]
580 exact this.trans (by simpa [hmul])
581 have : C0 * e1 r + C0 * r ≤ ε / 2 + ε / 2 := add_le_add hC0e1 hC0r
582 nlinarith
583 · intro r hr
584 have h1 : C0 * err1 r ≤ C0 * e1 r :=
585 mul_le_mul_of_nonneg_left (hErr1_le r hr) hC00
586 have : C0 * err1 r + C0 * r ≤ C0 * e1 r + C0 * r := by
587 nlinarith [h1]
588 simpa [err] using this
589
590 refine ⟨C0 * C1, err, mul_nonneg hC00 hC10, hErr, ?_⟩
591 intro r hr
592 have hBud' : bandBudget r ≤ C1 * injRate (2 * r) + err1 r := hBud r hr
593 have hPay : P.payRho r ≤ C0 * bandBudget r + C0 * r := hBand r hr
594 have hPay' : P.payRho r ≤ C0 * (C1 * injRate (2 * r) + err1 r) + C0 * r := by
595 have : C0 * bandBudget r ≤ C0 * (C1 * injRate (2 * r) + err1 r) :=
596 mul_le_mul_of_nonneg_left hBud' hC00
597 have hAdd :
598 C0 * bandBudget r + C0 * r ≤ C0 * (C1 * injRate (2 * r) + err1 r) + C0 * r := by
599 nlinarith [this]
600 exact le_trans hPay hAdd
601 -- rearrange into `C * injRate (2*r) + err r`
602 have : P.payRho r ≤ (C0 * C1) * injRate (2 * r) + (C0 * err1 r + C0 * r) := by
603 -- expand and collect terms
604 nlinarith
605 simpa [err] using this
606
607/-- **U-4 injection/payment package (spec layer):** bundle the PDE inputs for the U‑4 upper bound:
608
6091) vanishing of the normalized positive injection rate,
6102) `PayXi` is controlled by that injection rate plus an `o(1)` error,
6113) `PayRho` is controlled by that injection rate plus an `o(1)` error.
612
613This mirrors the TeX blocker `hyp:U4_injection_payment_package` once `injRate r` is instantiated by the
614normalized injection `(1/r^2) ∬ ρ^{3/2} σ_+`. -/
615structure U4InjectionPaymentPackageHypothesis (P : Payments) (injRate : ℝ → ℝ) : Prop where
616 hInj : U4VanishingInjectionRateHypothesis injRate
617 hPayXi : U4PayXiControlledByInjectionRateHypothesis P injRate
618 hPayRho : U4PayRhoControlledByInjectionRateHypothesis P injRate
619
620/-- If payments are controlled by the injection rate and the injection rate vanishes,
621then the U‑4 payment upper bound holds (pure bookkeeping). -/
622theorem u4PaymentUpperBound_of_paymentControl
623 (P : Payments) (injRate : ℝ → ℝ)
624 (hInj : U4VanishingInjectionRateHypothesis injRate)
625 (hCtrl : U4PaymentsControlledByInjectionRateHypothesis P injRate) :
626 U4PaymentUpperBoundHypothesis P := by
627 classical
628 rcases hCtrl.exists_bound with ⟨C, err, hC0, hErr, hBound⟩
629 exact
630 u4PaymentUpperBound_of_u4InjectionRate
631 (P := P) (injRate := injRate) (err := err) hInj hErr ⟨C, hC0, hBound⟩
632
633/-- Single-entry version of `u4PaymentUpperBound_of_paymentControl`. -/
634theorem u4PaymentUpperBound_of_u4Package
635 (P : Payments) (injRate : ℝ → ℝ) (hPkg : U4InjectionPaymentPackageHypothesis P injRate) :
636 U4PaymentUpperBoundHypothesis P :=
637by
638 classical
639 rcases hPkg.hPayXi.exists_bound with ⟨Cx, errx, hCx0, hErrx, hXibound⟩
640 rcases hPkg.hPayRho.exists_bound with ⟨Cr, errr, hCr0, hErrr, hRhobound⟩
641 -- combine the two error bounds
642 rcases hErrx with ⟨eX, heX_nonneg, heX_lim, hErrx_le⟩
643 rcases hErrr with ⟨eR, heR_nonneg, heR_lim, hErrr_le⟩
644 let err : ℝ → ℝ := fun r => errx r + errr r
645 have hErr :
646 ∃ e : ℝ → ℝ,
647 (∀ r : ℝ, 0 < r → 0 ≤ e r) ∧
648 (∀ ε : ℝ, 0 < ε → ∃ r0 : ℝ, 0 < r0 ∧ ∀ r : ℝ, 0 < r → r ≤ r0 → e r ≤ ε) ∧
649 ∀ r : ℝ, 0 < r → err r ≤ e r := by
650 refine ⟨fun r => eX r + eR r, ?_, ?_, ?_⟩
651 · intro r hr
652 exact add_nonneg (heX_nonneg r hr) (heR_nonneg r hr)
653 · intro ε hε
654 have hε2 : 0 < ε / 2 := by nlinarith
655 rcases heX_lim (ε / 2) hε2 with ⟨rX, hrX, hrX_bound⟩
656 rcases heR_lim (ε / 2) hε2 with ⟨rR, hrR, hrR_bound⟩
657 refine ⟨min rX rR, lt_min hrX hrR, ?_⟩
658 intro r hr hrr0
659 have hrX' : r ≤ rX := le_trans hrr0 (min_le_left _ _)
660 have hrR' : r ≤ rR := le_trans hrr0 (min_le_right _ _)
661 have hX : eX r ≤ ε / 2 := hrX_bound r hr hrX'
662 have hR : eR r ≤ ε / 2 := hrR_bound r hr hrR'
663 have : eX r + eR r ≤ ε / 2 + ε / 2 := add_le_add hX hR
664 nlinarith
665 · intro r hr
666 have hx : errx r ≤ eX r := hErrx_le r hr
667 have hr' : errr r ≤ eR r := hErrr_le r hr
668 exact add_le_add hx hr'
669 have hBound :
670 ∃ C : ℝ,
671 0 ≤ C ∧
672 ∀ r : ℝ, 0 < r → P.payXi r + P.payRho r ≤ C * injRate (2 * r) + err r := by
673 refine ⟨Cx + Cr, add_nonneg hCx0 hCr0, ?_⟩
674 intro r hr
675 have hXi : P.payXi r ≤ Cx * injRate (2 * r) + errx r := hXibound r hr
676 have hRho : P.payRho r ≤ Cr * injRate (2 * r) + errr r := hRhobound r hr
677 have : P.payXi r + P.payRho r ≤ (Cx * injRate (2 * r) + errx r) + (Cr * injRate (2 * r) + errr r) :=
678 add_le_add hXi hRho
679 -- rearrange
680 have :
681 P.payXi r + P.payRho r ≤ (Cx + Cr) * injRate (2 * r) + (errx r + errr r) := by
682 -- `ring` works but keep it lightweight
683 nlinarith
684 simpa [err] using this
685 -- reduce to the already-proved bookkeeping lemma
686 let inj2 : ℝ → ℝ := fun r => injRate (2 * r)
687 have hInj2 : U4VanishingInjectionRateHypothesis inj2 := by
688 -- `injRate` vanishes ⇒ `injRate ∘ (2*)` vanishes (pure ε–δ bookkeeping)
689 simpa [inj2, U4VanishingInjectionRateHypothesis] using
690 (c2VanishingInjection_comp_two (injPos := injRate) (h := hPkg.hInj))
691 have hBound2 :
692 ∃ C : ℝ,
693 0 ≤ C ∧
694 ∀ r : ℝ, 0 < r → P.payXi r + P.payRho r ≤ C * inj2 r + err r := by
695 rcases hBound with ⟨C, hC0, hB⟩
696 refine ⟨C, hC0, ?_⟩
697 intro r hr
698 simpa [inj2] using hB r hr
699 exact u4PaymentUpperBound_of_u4InjectionRate (P := P) (injRate := inj2) (err := err) hInj2 hErr hBound2
700
701/-- **Route (B-ξ)** interface: “persistent perpendicular tail forcing” implies a twist-or-band payment.
702
703`ForcingEvent ε r` is an abstract predicate encoding:
704- top-band persistence on a positive-measure time set, and
705- a lower bound `|(I-ξ⊗ξ) S_tail ξ| ≥ c_* ε` on a spatial core.
706
707The conclusion is a scale-consistent lower bound on the *normalized* payments at scale `r`. -/
708structure ForcingToTwistOrBandPaymentHypothesis
709 (ForcingEvent : ℝ → ℝ → Prop) (P : Payments) : Prop where
710 exists_c :
711 ∃ c : ℝ,
712 0 < c ∧
713 ∀ (ε r : ℝ), 0 < ε → 0 < r →
714 ForcingEvent ε r →
715 c * (ε ^ 2) ≤ P.payXi r + P.payRho r
716
717/-- “Rigid-rotation absorption” guard: if the forcing persists but the payments are small,
718then the cylinder lies in a separate explicit structural class (to be ruled out elsewhere).
719
720`AbsorptionClass ε r` should encode the “ODE + affine tail” regime from the TeX
721lemma `lem:rigid_rotation_absorption_implies_structure`. -/
722structure NoRigidRotationAbsorptionHypothesis
723 (ForcingEvent AbsorptionClass : ℝ → ℝ → Prop) (P : Payments) : Prop where
724 exists_c :
725 ∃ c : ℝ,
726 0 < c ∧
727 ∀ (ε r : ℝ), 0 < ε → 0 < r →
728 ForcingEvent ε r →
729 (c * (ε ^ 2) ≤ P.payXi r + P.payRho r) ∨ AbsorptionClass ε r
730
731/-- Optional interface: persistent negative injection on the top band forces band diffusion payment.
732
733`NegativeSigmaEvent ε r` abstracts the event “σ ≤ -c_* ε on the top band for a time-thick subset”. -/
734structure NegativeSigmaForcesBandPaymentHypothesis
735 (NegativeSigmaEvent : ℝ → ℝ → Prop) (P : Payments) : Prop where
736 exists_c :
737 ∃ c : ℝ,
738 0 < c ∧
739 ∀ (ε r : ℝ), 0 < ε → 0 < r →
740 NegativeSigmaEvent ε r →
741 c * (ε ^ 2) ≤ P.payRho r
742
743/-- **No persistent null alignment (spec layer):** a “large tail strain” event forces a nontrivial interaction with the
744vorticity direction (i.e. avoids the null-eigenvector cone everywhere on a time-thick top band set).
745
746At the spec layer this is an abstract implication between two events. -/
747structure NoPersistentNullAlignmentHypothesis
748 (TailLargeEvent HitEvent : ℝ → ℝ → Prop) : Prop where
749 exists_c :
750 ∃ c : ℝ,
751 0 < c ∧
752 ∀ (ε r : ℝ), 0 < ε → 0 < r →
753 TailLargeEvent ε r →
754 HitEvent ε r
755
756/-- **S3-P bookkeeping (spec layer):** export persistence splits into one of the three “cost channels”.
757
758This is intentionally abstract: it packages the output of the selection/drift-control machinery together with
759the algebraic split (`σ` vs perpendicular forcing) into a single logical splitter. -/
760structure ExportSplitHypothesis
761 (ExportEvent ForcingEvent NegativeSigmaEvent ConcavityEvent : ℝ → ℝ → Prop) : Prop where
762 split :
763 ∀ (ε r : ℝ),
764 0 < ε →
765 0 < r →
766 ExportEvent ε r →
767 ForcingEvent ε r ∨ NegativeSigmaEvent ε r ∨ ConcavityEvent ε r
768
769/-- **Export ⇒ payment/absorption/concavity** (spec layer).
770
771This mirrors TeX Lemma `lem:export_forces_payment_on_cylinder`, but keeps the PDE objects abstract.
772The only nontrivial content should sit inside:
773- `ExportSplitHypothesis` (selection + bridge into one of the three channels),
774- `NoRigidRotationAbsorptionHypothesis` (forcing ⇒ payment ∨ absorption),
775- `NegativeSigmaForcesBandPaymentHypothesis` (negative injection ⇒ band payment). -/
776structure ExportForcesPaymentHypothesis
777 (ExportEvent AbsorptionClass ConcavityEvent : ℝ → ℝ → Prop) (P : Payments) : Prop where
778 exists_c :
779 ∃ c : ℝ,
780 0 < c ∧
781 ∀ (ε r : ℝ), 0 < ε → 0 < r →
782 ExportEvent ε r →
783 (c * (ε ^ 2) ≤ P.payXi r + P.payRho r) ∨ AbsorptionClass ε r ∨ ConcavityEvent ε r
784
785namespace ExportForcesPaymentHypothesis
786
787/-- Build the export→payment bookkeeping lemma from the three abstract implication interfaces. -/
788theorem of_split
789 {ExportEvent ForcingEvent NegativeSigmaEvent ConcavityEvent AbsorptionClass : ℝ → ℝ → Prop}
790 (P : Payments)
791 (hSplit : ExportSplitHypothesis ExportEvent ForcingEvent NegativeSigmaEvent ConcavityEvent)
792 (hForcing : NoRigidRotationAbsorptionHypothesis ForcingEvent AbsorptionClass P)
793 (hNeg : NegativeSigmaForcesBandPaymentHypothesis NegativeSigmaEvent P) :
794 ExportForcesPaymentHypothesis ExportEvent AbsorptionClass ConcavityEvent P := by
795 classical
796 rcases hForcing.exists_c with ⟨cF, hcF_pos, hcF⟩
797 rcases hNeg.exists_c with ⟨cN, hcN_pos, hcN⟩
798 refine ⟨min cF cN, lt_min hcF_pos hcN_pos, ?_⟩
799 intro ε r hε hr hExport
800 have hcases := hSplit.split ε r hε hr hExport
801 rcases hcases with hF | hrest
802 · -- forcing channel
803 have hF' := hcF ε r hε hr hF
804 rcases hF' with hPay | hAbs
805 · left
806 have hmin : min cF cN ≤ cF := min_le_left _ _
807 exact (mul_le_mul_of_nonneg_right hmin (sq_nonneg ε)).trans hPay
808 · right
809 exact Or.inl hAbs
810 · rcases hrest with hNegEvent | hConc
811 · -- negative-sigma channel gives band payment, hence total payment
812 have hRho : cN * (ε ^ 2) ≤ P.payRho r := hcN ε r hε hr hNegEvent
813 left
814 have hmin : min cF cN ≤ cN := min_le_right _ _
815 have : min cF cN * (ε ^ 2) ≤ cN * (ε ^ 2) :=
816 mul_le_mul_of_nonneg_right hmin (sq_nonneg ε)
817 have hRho' : P.payRho r ≤ P.payXi r + P.payRho r :=
818 le_add_of_nonneg_left (P.payXi_nonneg r)
819 exact this.trans (hRho.trans hRho')
820 · right
821 exact Or.inr hConc
822
823end ExportForcesPaymentHypothesis
824
825/-- **K-ODE interface (step 1):** absorption-class ⇒ quantitative affine ansatz on a smaller cylinder.
826
827At the spec layer, both “absorption class” and “affine ansatz class” are abstract predicates on `(ε,r)`. -/
828structure AbsorptionImpliesAffineAnsatzHypothesis
829 (AbsorptionClass AffineAnsatzClass : ℝ → ℝ → Prop) : Prop where
830 implies :
831 ∀ (ε r : ℝ), 0 < ε → 0 < r →
832 AbsorptionClass ε r → AffineAnsatzClass ε r
833
834/-- **K-ODE interface (step 2):** the affine-ansatz class is impossible for running-max ancient elements
835below some scale (the ODE contradiction endpoint).
836
837This is the abstraction of TeX Lemma `lem:affine_mode_ode_contradiction`. -/
838structure AffineAnsatzImpossibleHypothesis (AffineAnsatzClass : ℝ → ℝ → Prop) : Prop where
839 impossible :
840 ∀ (ε0 : ℝ),
841 0 < ε0 →
842 ∃ r0 : ℝ,
843 0 < r0 ∧
844 ∀ r : ℝ, 0 < r → r ≤ r0 → AffineAnsatzClass ε0 r → False
845
846/-- **K-ODE input:** time-variation control for an abstract “tail strain at the origin” signal `S(t)`.
847
848This mirrors TeX Hypothesis `hyp:tail_strain_time_variation`.
849We keep it fully abstract (it will later be instantiated by `t ↦ S_tail^{(k)}(0,t)` once those objects exist in Lean). -/
850structure TailStrainTimeVariationHypothesis (α : Type) [NormedAddCommGroup α] (S : ℝ → α) : Prop where
851 exists_modulus :
852 ∃ ω : ℝ → ℝ,
853 (∀ r : ℝ, 0 < r → 0 ≤ ω r) ∧
854 (∀ ε : ℝ, 0 < ε → ∃ r0 : ℝ, 0 < r0 ∧ ∀ r : ℝ, 0 < r → r ≤ r0 → ω r ≤ ε) ∧
855 ∀ r : ℝ, 0 < r →
856 ∀ t s : ℝ,
857 t ∈ Set.Icc (-(r ^ 2)) 0 →
858 s ∈ Set.Icc (-(r ^ 2)) 0 →
859 ‖S t - S s‖ ≤ ω r
860
861/-- Alias matching TeX Hypothesis `hyp:tail_vorticity_L2_time_modulus`.
862
863At the spec layer we keep the ambient normed space abstract; in the intended instantiation,
864`β` is an `L^2`-type tail space and `Ω` is the truncated tail vorticity. -/
865abbrev TailVorticityL2TimeModulusHypothesis
866 (β : Type) [NormedAddCommGroup β] (Ω : ℝ → β) : Prop :=
867 TailStrainTimeVariationHypothesis β Ω
868
869/-- **Bridge helper:** if `Ω` has a short-window time-modulus and `S` is Lipschitz in `Ω`,
870then `S` inherits a short-window time-modulus.
871
872This mirrors the TeX bridge `hyp:tail_vorticity_L2_time_modulus ⇒ hyp:tail_strain_time_variation`
873once the explicit Biot–Savart pairing is packaged as a Lipschitz map on the chosen normed space. -/
874theorem tailStrainTimeVariation_of_lipschitz
875 {α β : Type} [NormedAddCommGroup α] [NormedAddCommGroup β]
876 {Ω : ℝ → β} {S : ℝ → α}
877 (hΩ : TailStrainTimeVariationHypothesis β Ω)
878 (hLip : ∃ C : ℝ, 0 ≤ C ∧ ∀ t s : ℝ, ‖S t - S s‖ ≤ C * ‖Ω t - Ω s‖) :
879 TailStrainTimeVariationHypothesis α S := by
880 classical
881 rcases hΩ.exists_modulus with ⟨μ, hμ_nonneg, hμ_lim, hμ⟩
882 rcases hLip with ⟨C, hC0, hLip⟩
883 refine ⟨fun r => C * μ r, ?_, ?_, ?_⟩
884 · intro r hr
885 exact mul_nonneg hC0 (hμ_nonneg r hr)
886 · intro ε hε
887 by_cases hCpos : 0 < C
888 · have hε' : 0 < ε / C := by exact div_pos hε hCpos
889 rcases hμ_lim (ε / C) hε' with ⟨r0, hr0, hr0μ⟩
890 refine ⟨r0, hr0, ?_⟩
891 intro r hr hrr0
892 have : μ r ≤ ε / C := hr0μ r hr hrr0
893 -- multiply by C (positive) to get the desired bound
894 have : C * μ r ≤ C * (ε / C) := mul_le_mul_of_nonneg_left this (le_of_lt hCpos)
895 simpa [mul_assoc, mul_div_cancel₀, ne_of_gt hCpos] using this
896 · -- If `C ≤ 0`, then `C * μ r ≤ 0 ≤ ε` for all small windows.
897 have hCnonpos : C ≤ 0 := le_of_not_gt hCpos
898 refine ⟨1, by norm_num, ?_⟩
899 intro r hr _
900 have : C * μ r ≤ 0 := by exact mul_nonpos_of_nonpos_of_nonneg hCnonpos (hμ_nonneg r hr)
901 exact this.trans (le_of_lt hε)
902 · intro r hr t s ht hs
903 have h1 : ‖S t - S s‖ ≤ C * ‖Ω t - Ω s‖ := hLip t s
904 have h2 : ‖Ω t - Ω s‖ ≤ μ r := hμ r hr t s ht hs
905 exact h1.trans (mul_le_mul_of_nonneg_left h2 hC0)
906
907/-- **Absorption elimination (U-4):** the abstract absorption class cannot occur below some scale.
908
909This mirrors TeX Hypothesis `hyp:absorption_class_impossible`. -/
910structure AbsorptionClassImpossibleHypothesis (AbsorptionClass : ℝ → ℝ → Prop) : Prop where
911 impossible :
912 ∀ (η ε0 : ℝ),
913 0 < η →
914 0 < ε0 →
915 ∃ r0 : ℝ,
916 0 < r0 ∧
917 ∀ r : ℝ, 0 < r → r ≤ r0 → AbsorptionClass ε0 r → False
918
919/-- **Concavity/peak channel elimination (spec layer):** the concavity event cannot occur below some scale.
920
921This is the abstract way to “kill (P3)” if it is not already absorbed into `payXi`/`payRho`. -/
922structure ConcavityImpossibleHypothesis (ConcavityEvent : ℝ → ℝ → Prop) : Prop where
923 impossible :
924 ∀ (ε0 : ℝ),
925 0 < ε0 →
926 ∃ r0 : ℝ,
927 0 < r0 ∧
928 ∀ r : ℝ, 0 < r → r ≤ r0 → ConcavityEvent ε0 r → False
929
930/-- **U-4 one-cylinder contradiction (spec layer):** export persistence at a fixed level is impossible below some scale.
931
932This mirrors TeX Lemma `lem:U4_contradiction_from_export`, but keeps the PDE objects abstract. -/
933structure U4NoExportHypothesis (ExportEvent : ℝ → ℝ → Prop) : Prop where
934 impossible :
935 ∀ (ε0 : ℝ),
936 0 < ε0 →
937 ∃ r0 : ℝ,
938 0 < r0 ∧
939 ∀ r : ℝ, 0 < r → r ≤ r0 → ExportEvent ε0 r → False
940
941namespace U4NoExportHypothesis
942
943/-- Build the U-4 contradiction from:
944- an export→(payment ∨ absorption ∨ concavity) lower bound,
945- an upper bound on payments as `r → 0`,
946- impossibility of absorption below some scale,
947- impossibility of the concavity channel below some scale.
948
949All constants/moduli remain abstract; this lemma is pure bookkeeping. -/
950theorem of_u4
951 {ExportEvent AbsorptionClass ConcavityEvent : ℝ → ℝ → Prop}
952 (P : Payments)
953 (η : ℝ) (hη : 0 < η)
954 (hExport : ExportForcesPaymentHypothesis ExportEvent AbsorptionClass ConcavityEvent P)
955 (hUpper : U4PaymentUpperBoundHypothesis P)
956 (hAbs : AbsorptionClassImpossibleHypothesis AbsorptionClass)
957 (hConc : ConcavityImpossibleHypothesis ConcavityEvent) :
958 U4NoExportHypothesis ExportEvent := by
959 classical
960 rcases hExport.exists_c with ⟨c, hc_pos, hc⟩
961 rcases hUpper.exists_beta with ⟨β, hβ_nonneg, hβ_lim, hβ⟩
962 refine ⟨?_⟩
963 intro ε0 hε0
964 -- pick a scale where the payment upper bound beats `c * ε0^2`
965 have hpos : 0 < c * (ε0 ^ 2) := mul_pos hc_pos (sq_pos_of_pos hε0)
966 rcases hβ_lim (c * (ε0 ^ 2) / 2) (by nlinarith) with ⟨rβ, hrβ_pos, hrβ⟩
967 -- pick scales killing absorption + concavity at level ε0
968 rcases hAbs.impossible η ε0 hη hε0 with ⟨rAbs, hrAbs_pos, hrAbs⟩
969 rcases hConc.impossible ε0 hε0 with ⟨rConc, hrConc_pos, hrConc⟩
970 refine ⟨min rβ (min rAbs rConc), ?_, ?_⟩
971 · exact lt_min hrβ_pos (lt_min hrAbs_pos hrConc_pos)
972 · intro r hr hrr0 hEv
973 have hrβ' : r ≤ rβ := le_trans hrr0 (min_le_left _ _)
974 have hrAbs' : r ≤ rAbs := le_trans (le_trans hrr0 (min_le_right _ _)) (min_le_left _ _)
975 have hrConc' : r ≤ rConc := le_trans (le_trans hrr0 (min_le_right _ _)) (min_le_right _ _)
976 have hcases := hc ε0 r hε0 hr hEv
977 rcases hcases with hPay | hrest
978 · -- contradict payment lower bound with the U4 upper bound
979 have hUp : P.payXi r + P.payRho r ≤ β r := hβ r hr
980 have hβsmall : β r ≤ c * (ε0 ^ 2) / 2 := hrβ r hr hrβ'
981 have : c * (ε0 ^ 2) ≤ β r := le_trans hPay hUp
982 -- but `β r < c*ε0^2` by `hβsmall`
983 have : c * (ε0 ^ 2) ≤ c * (ε0 ^ 2) / 2 := this.trans hβsmall
984 nlinarith
985 · rcases hrest with hAbsEv | hConcEv
986 · exact hrAbs r hr hrAbs' hAbsEv
987 · exact hrConc r hr hrConc' hConcEv
988
989end U4NoExportHypothesis
990
991/-- **Bridge (profile → cylinder):** if tail-flux does not vanish, then “export persists” occurs at arbitrarily small scales.
992
993This isolates the PDE/compactness work needed to connect the time-slice profile statement
994`¬ TailFluxVanish P.A P.A'` to the U‑4 cylinder predicates. -/
995structure TailFluxNonVanishImpliesExportAtSmallScales
996 (P : RM2URadialProfile) (ExportEvent : ℝ → ℝ → Prop) : Prop where
997 to_export :
998 (¬ TailFluxVanish P.A P.A') →
999 ∃ ε0 : ℝ, 0 < ε0 ∧
1000 ∀ r0 : ℝ, 0 < r0 → ∃ r : ℝ, 0 < r ∧ r ≤ r0 ∧ ExportEvent ε0 r
1001
1002/-- Package the U‑4 contradiction into the time-slice Bet2 interface once the profile→cylinder bridge is supplied. -/
1003theorem bet2SelfFalsification_of_u4
1004 (P : RM2URadialProfile) {ExportEvent : ℝ → ℝ → Prop}
1005 (hBridge : TailFluxNonVanishImpliesExportAtSmallScales P ExportEvent)
1006 (hNoExport : U4NoExportHypothesis ExportEvent) :
1007 Bet2SelfFalsificationHypothesis P := by
1008 classical
1009 refine ⟨?_⟩
1010 intro hnot
1011 rcases hBridge.to_export hnot with ⟨ε0, hε0, hsmall⟩
1012 rcases hNoExport.impossible ε0 hε0 with ⟨r0, hr0, hno⟩
1013 rcases hsmall r0 hr0 with ⟨r, hr, hrr0, hEv⟩
1014 exact hno r hr hrr0 hEv
1015
1016/-- **E-gate interface (one way to eliminate absorption):** a quasi-2D smallness condition forces triviality.
1017
1018At the spec layer this is an abstract predicate `Quasi2DEvent` (encoding a scale-invariant smallness statement on a cylinder)
1019and a conclusion `TrivialEvent` (encoding the contradiction / triviality outcome). -/
1020structure Quasi2DEliminationHypothesis (Quasi2DEvent TrivialEvent : Prop) : Prop where
1021 elim : Quasi2DEvent → TrivialEvent
1022
1023/-- **Backward uniqueness import (Lei–Yang–Yuan 2024, IMRN):**
1024within the bounded mild + bounded-vorticity class, the solution is uniquely determined by its final data.
1025
1026At the spec layer we keep the “solution objects” abstract as a type `Sol` and encode only the logical shape. -/
1027structure BackwardUniquenessNSHypothesis
1028 (Sol : Type) (IsBoundedMild HasBoundedVorticity : Sol → Prop)
1029 (AgreeAtTime CoincideUpTo : Sol → Sol → ℝ → Prop) : Prop where
1030 backward_unique :
1031 ∀ (u₁ u₂ : Sol) (T : ℝ),
1032 IsBoundedMild u₁ →
1033 HasBoundedVorticity u₁ →
1034 IsBoundedMild u₂ →
1035 HasBoundedVorticity u₂ →
1036 AgreeAtTime u₁ u₂ T →
1037 CoincideUpTo u₁ u₂ T
1038
1039/-- **E-gate bridge (LYY style):** a quasi-2D event produces a comparison mild solution in an eliminable subclass,
1040with the same final data at time `T`. This is designed to be paired with `BackwardUniquenessNSHypothesis`. -/
1041structure Quasi2DToComparisonSolutionHypothesis
1042 (Sol : Type)
1043 (IsBoundedMild HasBoundedVorticity : Sol → Prop)
1044 (Quasi2DEvent : Sol → Prop) (EliminableSubclass : Sol → Prop)
1045 (AgreeAtTime : Sol → Sol → ℝ → Prop) : Prop where
1046 exists_comparison :
1047 ∀ (u : Sol) (T : ℝ),
1048 IsBoundedMild u →
1049 HasBoundedVorticity u →
1050 Quasi2DEvent u →
1051 ∃ u₂ : Sol,
1052 IsBoundedMild u₂ ∧
1053 HasBoundedVorticity u₂ ∧
1054 EliminableSubclass u₂ ∧
1055 AgreeAtTime u₂ u T
1056
1057/-- **E-gate bridge (pure symmetry propagation):** from a quasi-2D event we can extract a *nontrivial symmetry*
1058of the final data, so the symmetry-pushforward solution agrees at time `T`.
1059
1060This is the “free comparison solution” route: if `Act g u` is always a solution whenever `u` is, then no existence theory is needed. -/
1061structure Quasi2DToExactSymmetryHypothesis
1062 (Sol Sym : Type)
1063 (IsBoundedMild HasBoundedVorticity : Sol → Prop)
1064 (Act : Sym → Sol → Sol) (Nontrivial : Sym → Prop)
1065 (Quasi2DEvent : Sol → Prop) (AgreeAtTime : Sol → Sol → ℝ → Prop) : Prop where
1066 exists_symm :
1067 ∀ (u : Sol) (T : ℝ),
1068 IsBoundedMild u →
1069 HasBoundedVorticity u →
1070 Quasi2DEvent u →
1071 ∃ g : Sym, Nontrivial g ∧ AgreeAtTime (Act g u) u T
1072
1073/-- **E-gate elimination of the symmetry class:** any nontrivial symmetry-invariant candidate is impossible. -/
1074structure SymmetryClassImpossibleHypothesis
1075 (Sol Sym : Type) (Act : Sym → Sol → Sol) (Nontrivial : Sym → Prop)
1076 (CoincideUpTo : Sol → Sol → ℝ → Prop) (TrivialEvent : Prop) : Prop where
1077 elim :
1078 ∀ (u : Sol) (T : ℝ),
1079 (∃ g : Sym, Nontrivial g ∧ CoincideUpTo (Act g u) u T) →
1080 TrivialEvent
1081
1082end Bet2U4
1083
1084theorem nonParasitism_of_bet2 (P : RM2URadialProfile) (h : Bet2SelfFalsificationHypothesis P) :
1085 NonParasitismHypothesis P := by
1086 classical
1087 refine ⟨?_⟩
1088 by_contra hnot
1089 exact (h.selfFalsify hnot)
1090
1091/-- **Bet 3 (inheritance route)**: directly assume the coercive \(L^2\) bound for the profile.
1092This closes RM2, but does not (by itself) explain *why* the tail flux vanishes. -/
1093structure Bet3CoerciveL2Hypothesis (P : RM2URadialProfile) : Prop where
1094 coercive : CoerciveL2Bound P
1095
1096theorem rm2Closed_of_bet3 (P : RM2URadialProfile) (h : Bet3CoerciveL2Hypothesis P) :
1097 RM2Closed P.A :=
1098 RM2U.rm2Closed_of_coerciveL2Bound (P := P) h.coercive
1099
1100/-!
1101## End-to-end closure wrappers (so bets plug into RM2)
1102
1103These are purely compositional: they do not add any new mathematics, they just make it explicit
1104how each bet closes the simplified `RM2Closed` target once the missing “tailFlux → coercive” step
1105is supplied (as an interface in `RM2U.EnergyIdentity`).
1106-/
1107
1108theorem rm2Closed_of_nonParasitism
1109 (P : RM2URadialProfile)
1110 (hNP : NonParasitismHypothesis P)
1111 (hTC : TailFluxVanishImpliesCoerciveHypothesis P) :
1112 RM2Closed P.A :=
1113 RM2U.rm2Closed_of_coerciveL2Bound (P := P)
1114 (RM2U.coerciveL2Bound_of_tailFluxVanish (P := P) hTC hNP.tailFluxVanish)
1115
1116theorem rm2Closed_of_bet1
1117 (P : RM2URadialProfile)
1118 (h1 : Bet1BoundaryIntegrableHypothesis P)
1119 (hTC : TailFluxVanishImpliesCoerciveHypothesis P) :
1120 RM2Closed P.A :=
1121 rm2Closed_of_nonParasitism (P := P) (nonParasitism_of_bet1 (P := P) h1) hTC
1122
1123theorem rm2Closed_of_bet2
1124 (P : RM2URadialProfile)
1125 (h2 : Bet2SelfFalsificationHypothesis P)
1126 (hTC : TailFluxVanishImpliesCoerciveHypothesis P) :
1127 RM2Closed P.A :=
1128 rm2Closed_of_nonParasitism (P := P) (nonParasitism_of_bet2 (P := P) h2) hTC
1129
1130/-!
1131## Planned endgame theorem (currently a placeholder target)
1132
1133Ultimately we want to connect this to the *running-max ancient element* extracted in
1134`navier-dec-12-rewrite.tex`:
1135
1136`runningMaxAncientElement → NonParasitismHypothesis (the associated RM2U profile)`.
1137
1138We do **not** state it yet, because the repository does not currently contain a Lean definition
1139of the running-max ancient element in velocity/vorticity variables.
1140-/
1141
1142end RM2U
1143end NavierStokes
1144end IndisputableMonolith
1145