Literal recursive forcing is an actual smooth cylinder L² path

Only the already constructed prefix fields, the true time derivative of the previous corrector, its scalar-pressure gradient, and the actual coefficient paths enter. No equation or cancellation for the new profile is assumed.

noncomputable def EulerPacketCylinderField.PrefixFields.nonlinear {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {p : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} (F : PrefixFields P T p a) (C : CoefficientData P T O) (hp : 1 ≤ p) : Field P T fun (z : EulerPacketPointJets.Domain) => EulerPacketPointJets.nonlinearGrade (p + 1) p (O.inverseFrame z) (O.normal z) (EulerPacketProfileRecursion.knownJets O p a z)

Both finite nonlinear convolutions are formed from the actual earlier fields.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def EulerPacketCylinderField.PrefixFields.knownForce {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {p : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} (F : PrefixFields P T p a) (C : CoefficientData P T O) (hp : 1 ≤ p) (hT : 0 < T) {correctorT : EulerPacketProfileRecursion.VectorField} (Ct : Field P T correctorT) (hCt : TimeDerivative ⋯ (F.corrector (p - 1) ⋯) Ct) (pressure : Field P T (pressureGradient (a (p - 1)).highPressure)) : Field P T (EulerPacketProfileRecursion.knownForce O p a)

The manuscript's exact knownForce expression has a genuine path and all spatial derivatives.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def EulerPacketCylinderField.PrefixFields.meanForce {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {p : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} (F : PrefixFields P T p a) (C : CoefficientData P T O) (hp : 1 ≤ p) (hT : 0 < T) {correctorT : EulerPacketProfileRecursion.VectorField} (Ct : Field P T correctorT) (hCt : TimeDerivative ⋯ (F.corrector (p - 1) ⋯) Ct) (pressure : Field P T (pressureGradient (a (p - 1)).highPressure)) : Field P T (EulerPacketProfileRecursion.meanForce O p a)

The actual mean-force raw field is also represented in cylinder L².

Equations

• F.meanForce C hp hT Ct hCt pressure = (F.knownForce C hp hT Ct hCt pressure).angleMean.congr ⋯

noncomputable def EulerPacketCylinderField.PrefixFields.highForce {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {p : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} (F : PrefixFields P T p a) (C : CoefficientData P T O) (hp : 2 ≤ p) (hT : 0 < T) {correctorT : EulerPacketProfileRecursion.VectorField} (Ct : Field P T correctorT) (hCt : TimeDerivative ⋯ (F.corrector (p - 1) ⋯) Ct) (pressure : Field P T (pressureGradient (a (p - 1)).highPressure)) (newMean : Field P T (EulerPacketProfileRecursion.meanResult O p a).1) : Field P T (EulerPacketProfileRecursion.highForce O p a)

Once the actual new mean has been supplied, the exact high-force expression is admissible as a path.

Equations

• One or more equations did not get rendered due to their size.