Actual common pressure and a canonically normalized scalar graph pressure constructed from all-order drift-aware input budgets.

noncomputable def EulerAllOrderDriftCorrection.Budget.commonPressure (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 period))

The actual signed L² pressure of the family constructed from drift-aware budgets.

Equations

• EulerAllOrderDriftCorrection.Budget.commonPressure period B = EulerCorrectionAssembly.FiniteFamily.commonPressure period (EulerAllOrderDriftCorrection.Budget.family period B)

theorem EulerAllOrderDriftCorrection.Budget.signedPressurePath_value_common (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (q : ℕ) (hq : 6 ≤ q) (t : ↑(Set.Icc 0 T)) : EulerCylinderSobolevSpace.value period ((EulerCorrectionAssembly.FiniteFamily.signedPressurePath period (family period B) q hq) t) = (commonPressure period B) t

Every constructed finite signed pressure realizes this same common L² pressure.

theorem EulerAllOrderDriftCorrection.Budget.commonPressure_gradient (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (t : ↑(Set.Icc 0 T)) : (commonPressure period B) t ∈ EulerLiftedGradientSpace.gradientSpace period A.κ A.direction

The constructed pressure lies in the genuine closed lifted gradient space.

noncomputable def EulerAllOrderDriftCorrection.Budget.pressureTower (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) : EulerAllOrderCorrectionData.FieldTower period T

Actual continuous Sobolev realizations at every order of the same constructed pressure.

Equations

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

theorem EulerAllOrderDriftCorrection.Budget.pressureTower_value (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (q : ℕ) (t : ↑(Set.Icc 0 T)) : EulerCylinderSobolevSpace.value period (((pressureTower period B).realization q) t) = (commonPressure period B) t

The all-order tower represents exactly the pressure selected from the finite construction.

theorem EulerAllOrderDriftCorrection.Budget.pressure_eq_realization (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (q : ℕ) (hq : 6 ≤ q) (t : ↑(Set.Icc 0 T)) : EulerCorrectionOperators.CorrectionData.pressure period (EulerAllOrderCorrectionData.Data.atOrder period A q) hq t ((solution period B q hq) t) = ((pressureTower period B).realization q) t

Evaluating the genuine finite-order pressure solver on the constructed correction gives exactly the corresponding realization of the common pressure tower.

noncomputable def EulerAllOrderDriftCorrection.Budget.pointPressure (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period) : EulerLiftedGradientSpace.Vector3

Bounded Sobolev evaluation fixes a canonical pointwise representative of the pressure.

Equations

• EulerAllOrderDriftCorrection.Budget.pointPressure period B t x = EulerCorrectionAssembly.FiniteFamily.pointPressure period (EulerAllOrderDriftCorrection.Budget.family period B) t x

theorem EulerAllOrderDriftCorrection.Budget.pointPressure_ae (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (t : ↑(Set.Icc 0 T)) : ↑↑((commonPressure period B) t) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] pointPressure period B t

The canonical representative agrees almost everywhere with the actual constructed pressure.

theorem EulerAllOrderDriftCorrection.Budget.pointPressure_joint_continuous (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) : Continuous (Function.uncurry (pointPressure period B))

The selected actual pressure representative is jointly continuous, including endpoint times.

theorem EulerAllOrderDriftCorrection.Budget.pointPressure_smooth (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period) : ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period (pointPressure period B t) x)

The same pressure representative is smooth in all cylinder coordinates at every time.

noncomputable def EulerAllOrderDriftCorrection.Budget.graphPressure (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (k : ℝ) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.Vector3) : EulerLiftedGradientSpace.Vector3

The actual graph pressure-gradient vector field of the constructed correction.

Equations

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

theorem EulerAllOrderDriftCorrection.Budget.graphPressure_joint_continuous (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (k : ℝ) : Continuous (Function.uncurry (graphPressure period B k))

The actual graph vector field is jointly continuous in time and space.

theorem EulerAllOrderDriftCorrection.Budget.graphPressure_has_potential (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (k : ℝ) (hk : k * A.κ = 1) (t : ↑(Set.Icc 0 T)) : ∃ (q : EulerLiftedGradientSpace.Vector3 → ℝ), ContDiff ℝ (↑⊤) q ∧ ∀ (x : EulerLiftedGradientSpace.Vector3), gradient q x = graphPressure period B k t x

Reciprocal-frequency graph restriction of the actual pressure has a genuine smooth potential.

noncomputable def EulerAllOrderDriftCorrection.Budget.normalizedGraphPotential (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (k : ℝ) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.Vector3) : ℝ

The scalar graph pressure constructed by radial integration, with its additive gauge fixed at zero.

Equations

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

theorem EulerAllOrderDriftCorrection.Budget.normalizedGraphPotential_zero (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (k : ℝ) (t : ↑(Set.Icc 0 T)) : normalizedGraphPotential period B k t 0 = 0

The constructed scalar pressure vanishes at the origin at every time.

theorem EulerAllOrderDriftCorrection.Budget.normalizedGraphPotential_joint_continuous (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (k : ℝ) : Continuous (Function.uncurry (normalizedGraphPotential period B k))

Fixing the gauge by the same radial formula at every time preserves joint continuity.

theorem EulerAllOrderDriftCorrection.Budget.normalizedGraphPotential_smooth (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (k : ℝ) (hk : k * A.κ = 1) (t : ↑(Set.Icc 0 T)) : ContDiff ℝ (↑⊤) (normalizedGraphPotential period B k t)

The actual normalized scalar pressure is spatially smooth on each time slice.

theorem EulerAllOrderDriftCorrection.Budget.normalizedGraphPotential_gradient (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (k : ℝ) (hk : k * A.κ = 1) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.Vector3) : gradient (normalizedGraphPotential period B k t) x = A.κ • pointPressure period B t (EulerGraphPressurePotential.cylinderGraph period k A.direction x)

Its actual scalar gradient is precisely the signed pressure from the constructed correction.

theorem EulerAllOrderDriftCorrection.Budget.normalizedGraphPotential_unique (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (k : ℝ) (t : ↑(Set.Icc 0 T)) (q : EulerLiftedGradientSpace.Vector3 → ℝ) (hq : ContDiff ℝ (↑⊤) q) (hgrad : ∀ (x : EulerLiftedGradientSpace.Vector3), gradient q x = graphPressure period B k t x) (hq0 : q 0 = 0) : normalizedGraphPotential period B k t = q

No second normalized smooth potential can represent the same actual graph pressure.

theorem EulerAllOrderDriftCorrection.Budget.commonPressure_odd (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (P : EulerCorrectionAssembly.ParityData period A) (t : ↑(Set.Icc 0 T)) : -(EulerCylinderReflection.reflection period) ((commonPressure period B) t) = (commonPressure period B) t

Prescribed odd data produce an odd actual common pressure gradient.

theorem EulerAllOrderDriftCorrection.Budget.pointPressure_odd (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (P : EulerCorrectionAssembly.ParityData period A) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period) : pointPressure period B t (-x) = -pointPressure period B t x

Oddness holds pointwise for the canonical pressure representative.

theorem EulerAllOrderDriftCorrection.Budget.graphPressure_odd (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (P : EulerCorrectionAssembly.ParityData period A) (k : ℝ) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.Vector3) : graphPressure period B k t (-x) = -graphPressure period B k t x

The signed pressure gradient remains odd after physical phase-graph restriction.

theorem EulerAllOrderDriftCorrection.Budget.normalizedGraphPotential_even (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (P : EulerCorrectionAssembly.ParityData period A) (k : ℝ) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.Vector3) : normalizedGraphPotential period B k t (-x) = normalizedGraphPotential period B k t x

The same canonical normalization makes the scalar graph pressure exactly even.

theorem EulerAllOrderDriftCorrection.exists_normalized_pressure (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (k : ℝ) (hk : k * A.κ = 1) : ∃ (p : ↑(Set.Icc 0 T) → EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (Q : ↑(Set.Icc 0 T) → EulerLiftedGradientSpace.Vector3 → ℝ), (∀ (t : ↑(Set.Icc 0 T)), ↑↑((Budget.commonPressure period B) t) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] p t) ∧ Continuous (Function.uncurry p) ∧ (∀ (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period (p t) x)) ∧ Continuous (Function.uncurry Q) ∧ (∀ (t : ↑(Set.Icc 0 T)), Q t 0 = 0) ∧ (∀ (t : ↑(Set.Icc 0 T)), ContDiff ℝ (↑⊤) (Q t)) ∧ ∀ (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.Vector3), gradient (Q t) x = A.κ • p t (EulerGraphPressurePotential.cylinderGraph period k A.direction x)

The all-order drift-aware input budget constructs a common actual pressure, a jointly continuous smooth spatial representative, and a canonically normalized smooth scalar graph potential. No correction solution or pressure is assumed.

theorem EulerAllOrderDriftCorrection.exists_odd_normalized_pressure (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (P : EulerCorrectionAssembly.ParityData period A) (k : ℝ) (hk : k * A.κ = 1) : ∃ (p : ↑(Set.Icc 0 T) → EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (Q : ↑(Set.Icc 0 T) → EulerLiftedGradientSpace.Vector3 → ℝ), (∀ (t : ↑(Set.Icc 0 T)), ↑↑((Budget.commonPressure period B) t) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] p t) ∧ Continuous (Function.uncurry p) ∧ (∀ (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period (p t) x)) ∧ (∀ (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period), p t (-x) = -p t x) ∧ Continuous (Function.uncurry Q) ∧ (∀ (t : ↑(Set.Icc 0 T)), Q t 0 = 0) ∧ (∀ (t : ↑(Set.Icc 0 T)), ContDiff ℝ (↑⊤) (Q t)) ∧ (∀ (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.Vector3), Q t (-x) = Q t x) ∧ ∀ (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.Vector3), gradient (Q t) x = A.κ • p t (EulerGraphPressurePotential.cylinderGraph period k A.direction x)

With parity of the prescribed data, the same constructed pressure representative is odd and its canonically normalized scalar graph potential is even.