A single fixed radius bounds all recursively constructed joined-source profiles.
One complete quantitative recursion step, using the actual mean and joined transverse solvers.
theorem
EulerPacketCylinderField.ProfileBudget.joinedStep
{P : ℝ}
[Fact (0 < P)]
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(L : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6)
(N : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(W : L.GradeGuards N)
(LM : EulerMeanPacketProvider.Budget M 6 L.R)
(WM : LM.GradeGuards)
{O : EulerPacketProfileRecursion.Operators}
(C : CoefficientData P M.T O)
(BC : CoefficientBudget C)
(hmean : O.meanSolve = EulerMeanPacketProvider.meanSolve M)
(hhigh : O.highSolve = EulerTransversePacketJoin.highSolve τ hτ hτT B)
(hcorrector : O.curlCorrector = D.curlCorrector P)
(hRc : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) BC.Rc ≤ L.R)
(hcost : BC.termCost ≤ L.R)
(S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 M.T))
{p : ℕ}
{a : ℕ → EulerPacketProfileRecursion.Profile}
(hp : 2 ≤ p)
(G : (i : ℕ) → i < p → ProfileRegularity P M.T ⋯ D.support (a i))
(hG : ∀ (i : ℕ) (hi : i < p), 1 ≤ i → ProfileBudget (G i hi) S L.R i)
(hc₀ : (a 0).corrector = 0)
(hB₁ : (a 1).mean = 0)
(hA :
∀ i < p,
∀ (t : ↑(Set.Icc 0 M.T)) (x : EulerSmoothLimit.Space) (θ : ℝ),
inner ℝ (O.normal (↑t, x, θ)) ((a i).high (↑t, x, θ)) = 0)
(c : ℝ)
(hc : 0 < c)
(hprofile : timeProfileChange (S.high p) hTime = c • L.fullProfile)
(H : ProfileRegularity P M.T ⋯ D.support (EulerPacketProfileRecursion.step O p a))
:
ProfileBudget H S L.R p
theorem
EulerPacketCylinderField.joinedSource_profile_budgets
(P : ℝ)
[Fact (0 < P)]
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(L : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6)
(N : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(W : L.GradeGuards N)
(LM : EulerMeanPacketProvider.Budget M 6 L.R)
(WM : LM.GradeGuards)
(BC : CoefficientBudget (joinedSourceCoefficientData P M D τ hτ hτT B hTime))
(hRc : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) BC.Rc ≤ L.R)
(hcost : BC.termCost ≤ L.R)
(S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 M.T))
(α : ℝ)
(hα : 0 < α)
(hgrowth : timeProfileChange S.growth hTime = α • L.fullProfile)
(primary : EulerPacketProfileRecursion.Profile)
(hprimary : ProfileRegularity P M.T ⋯ D.support primary)
(hprimaryBudget : ProfileBudget hprimary S L.R 1)
(hprimaryMean : primary.mean = 0)
(hprimaryTangent :
∀ (t : ↑(Set.Icc 0 M.T)) (x : EulerSmoothLimit.Space) (θ : ℝ),
inner ℝ (D.normalField (↑t, x, θ)) (primary.high (↑t, x, θ)) = 0)
(p : ℕ)
:
1 ≤ p → ProfileBudget (joinedSourceProfileWitness P M D hTime τ hτ hτT B primary hprimary p) S L.R p
The hypotheses are fixed source budgets and the primary estimate. No later-grade forcing or solution estimate is assumed.