The actual fixed-base residual in every common chart

Pressure and error are normalized values of the same final Cartesian base. The equation is derived from its proved residual identity on the entire free auxiliary lift, rather than only on a physical graph.

theorem NavierStokes.ActualBaseResidual.graphResidual_scaled_viscosity {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : Set E} {U : Set F} {Γ : E → F} {l v ε μ : ℝ} {R : F → ℝ} {Vr Vθ Vz Vt : F → F} {Sr Sθ Sz St : E → E} {r : E → ℝ} (G : PhysicalResidualBridge.PullbackData Ω U Γ l v R Vr Vθ Vz Vt Sr Sθ Sz St r) (hl : l ≠ 0) (hμ : μ = v * ε / l) {a : F → Fin 3 → ℝ} {p : F → ℝ} (ha : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : F) => a y i) U) (hp : ContDiffOn ℝ (↑⊤) p U) {x : E} (hx : x ∈ Ω) (hr : r x ≠ 0) (i : Fin 3) : PhysicalResidualBridge.graphResidual μ r Sr Sθ Sz St (fun (y : E) (j : Fin 3) => v * a (Γ y) j) (fun (y : E) => v ^ 2 * p (Γ y)) x i = v ^ 2 * l * PhysicalResidualBridge.graphResidual ε R Vr Vθ Vz Vt a p (Γ x) i

The derivative calculation permits a non-unit source viscosity and a non-injective coordinate map. This is used to keep every auxiliary value free.

theorem NavierStokes.ActualBaseResidual.graphResidual_congr {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set E} (hU : IsOpen U) (ε : ℝ) (R : E → ℝ) (Vr Vθ Vz Vt : E → E) {a b : E → Fin 3 → ℝ} {p q : E → ℝ} (ha : ∀ (j : Fin 3), Set.EqOn (fun (x : E) => a x j) (fun (x : E) => b x j) U) (hp : Set.EqOn p q U) {x : E} (hx : x ∈ U) (i : Fin 3) : PhysicalResidualBridge.graphResidual ε R Vr Vθ Vz Vt a p x i = PhysicalResidualBridge.graphResidual ε R Vr Vθ Vz Vt b q x i

The full residual depends only on germs, including its second derivatives.

@[reducible, inline]

abbrev NavierStokes.ActualBaseResidual.Point : Type

Point: an abbreviation for CommonBaseContext.Point.

Equations

• NavierStokes.ActualBaseResidual.Point = NavierStokes.CommonBaseContext.Point

@[reducible, inline]

abbrev NavierStokes.ActualBaseResidual.Full : Type

Full: an abbreviation for Point × ℝ.

Equations

• NavierStokes.ActualBaseResidual.Full = (NavierStokes.ActualBaseResidual.Point × ℝ)

@[reducible, inline]

abbrev NavierStokes.ActualBaseResidual.Space : Type

Space: an abbreviation for ProblemStatement.Space.

Equations

• NavierStokes.ActualBaseResidual.Space = NavierStokes.ProblemStatement.Space

@[reducible, inline]

abbrev NavierStokes.ActualBaseResidual.SpaceTime : Type

Space time: an abbreviation for ProblemStatement.SpaceTime.

Equations

• NavierStokes.ActualBaseResidual.SpaceTime = NavierStokes.ProblemStatement.SpaceTime

theorem NavierStokes.ActualBaseResidual.graphResidual_invariant (θ : Full) (ε : ℝ) (R : Full → ℝ) (Vr Vθ Vz Vt : Full → Full) (a : Full → Fin 3 → ℝ) (p : Full → ℝ) (hR : CopyAngularInvariance.Invariant θ R) (hr : CopyAngularInvariance.Invariant θ Vr) (htheta : CopyAngularInvariance.Invariant θ Vθ) (hz : CopyAngularInvariance.Invariant θ Vz) (ht : CopyAngularInvariance.Invariant θ Vt) (ha : CopyAngularInvariance.Invariant θ a) (hp : CopyAngularInvariance.Invariant θ p) (i : Fin 3) : CopyAngularInvariance.Invariant θ fun (x : Full) => PhysicalResidualBridge.graphResidual ε R Vr Vθ Vz Vt a p x i

Translation invariance propagates through every derivative in the residual.

noncomputable def NavierStokes.ActualBaseResidual.domain : Set Full

Domain, given by {x | 0 < x.1.1 ∧ 0 < x.1.2.1.1}.

Equations

• NavierStokes.ActualBaseResidual.domain = {x : NavierStokes.ActualBaseResidual.Full | 0 < x.1.1 ∧ 0 < x.1.2.1.1}

noncomputable def NavierStokes.ActualBaseResidual.timeDomain : Set Full

Time domain, given by {x | 0 < x.1.2.1.1}.

Equations

• NavierStokes.ActualBaseResidual.timeDomain = {x : NavierStokes.ActualBaseResidual.Full | 0 < x.1.2.1.1}

theorem NavierStokes.ActualBaseResidual.domain_open : IsOpen domain

theorem NavierStokes.ActualBaseResidual.timeDomain_open : IsOpen timeDomain

noncomputable def NavierStokes.ActualBaseResidual.cylinderLinear (h Q : ℝ) : Full →L[ℝ] SpaceTime

Cylinder linear, bundling toFun, map_add, map_smul, cont.

Equations

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

noncomputable def NavierStokes.ActualBaseResidual.cylinderPoint (h Q : ℝ) (x : Full) : SpaceTime

Cylinder point, given by (1 - Q * x.1.2.1.1, AxisymmetricResidual.pack (Real.sqrt Q * x.1.1) x.2 (Q ^ CoordinateAlgebra.D h * x.1.2.1.2)).

Equations

• NavierStokes.ActualBaseResidual.cylinderPoint h Q x = (1 - Q * x.1.2.1.1, NavierStokes.AxisymmetricResidual.pack (√Q * x.1.1) x.2 (Q ^ NavierStokes.CoordinateAlgebra.D h * x.1.2.1.2))

theorem NavierStokes.ActualBaseResidual.cylinderPoint_eq (h Q : ℝ) (x : Full) : cylinderPoint h Q x = (1, 0) + (cylinderLinear h Q) x

theorem NavierStokes.ActualBaseResidual.cylinderPoint_smooth (h Q : ℝ) : ContDiff ℝ (↑⊤) (cylinderPoint h Q)

theorem NavierStokes.ActualBaseResidual.cylinderPoint_hasFDerivAt (h Q : ℝ) (x : Full) : HasFDerivAt (cylinderPoint h Q) (cylinderLinear h Q) x

noncomputable def NavierStokes.ActualBaseResidual.physicalPoint (h Q : ℝ) (x : Full) : SpaceTime

Physical point, given by ((cylinderPoint h Q x).1, CylindricalResidual.chart (cylinderPoint h Q x).2).

Equations

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

theorem NavierStokes.ActualBaseResidual.physicalPoint_smooth (h Q : ℝ) : ContDiff ℝ (↑⊤) (physicalPoint h Q)

theorem NavierStokes.ActualBaseResidual.physicalPoint_time {h Q : ℝ} (hQ : 0 < Q) {x : Full} (hx : 0 < x.1.2.1.1) : (physicalPoint h Q x).1 < 1

theorem NavierStokes.ActualBaseResidual.profilePoint_chart (t : ℝ) (q : Space) : AxisymmetricFields.profilePoint t (CylindricalResidual.chart q) = (t, q.ofLp 0 ^ 2 / 2, q.ofLp 2)

theorem NavierStokes.ActualBaseResidual.physicalPoint_profile {h Q : ℝ} (hQ : 0 ≤ Q) (x : Full) : AxisymmetricFields.profilePoint (physicalPoint h Q x).1 (physicalPoint h Q x).2 = (1 - Q * x.1.2.1.1, Q * x.1.1 ^ 2 / 2, Q ^ CoordinateAlgebra.D h * x.1.2.1.2)

theorem NavierStokes.ActualBaseResidual.physicalPoint_zero_angle (h : ℝ) (n : ℕ) (x : Point) : physicalPoint h (ChartScales.Q n) (x, 0) = BaseContextAssembly.physicalPoint h n x

theorem NavierStokes.ActualBaseResidual.scale_identities {Q : ℝ} (hQ : 0 < Q) (h : ℝ) : Q ^ CoordinateAlgebra.D h * Q ^ h = √Q ∧ Q * Q ^ h = Q ^ CoordinateAlgebra.A h * √Q ∧ Q ^ h = Q ^ CoordinateAlgebra.A h * 1 / √Q ∧ (Q ^ CoordinateAlgebra.A h) ^ 2 * √Q = Q ^ (2 * CoordinateAlgebra.A h + 1 / 2)

The elementary power identities used by the actual chart differential.

theorem NavierStokes.ActualBaseResidual.cylinderPullback {Q : ℝ} (hQ : 0 < Q) (h : ℝ) (k : ℕ) : PhysicalResidualBridge.PullbackData domain BaseResidual.past (cylinderPoint h Q) (√Q) (Q ^ CoordinateAlgebra.A h) LinearWaveResidual.coordinateRadius (LinearWaveResidual.spaceDirection 0) (LinearWaveResidual.spaceDirection 1) (LinearWaveResidual.spaceDirection 2) LinearWaveResidual.physicalTimeDirection (PhysicalResidualTZ.graphRadialTZ (PhysicalResidualBridge.commonGraph Q h k)) PhysicalResidualTZ.graphAngularTZ (PhysicalResidualTZ.graphAxialTZ (PhysicalResidualBridge.commonGraph Q h k)) (PhysicalResidualTZ.graphTemporalTZ (PhysicalResidualBridge.commonGraph Q h k)) PhysicalResidualBridge.ScaledGraph.radius

The cylinder pullback forgets the auxiliary coordinate. Its derivative still matches all common-chart directions, whatever the common cover index.

noncomputable def NavierStokes.ActualBaseResidual.cartesianCylinder (x : SpaceTime) : SpaceTime

Cartesian cylinder, given by (x.1, CylindricalResidual.chart x.2).

Equations

• NavierStokes.ActualBaseResidual.cartesianCylinder x = (x.1, NavierStokes.CylindricalResidual.chart x.2)

theorem NavierStokes.ActualBaseResidual.cartesianCylinder_smooth : ContDiff ℝ (↑⊤) cartesianCylinder

theorem NavierStokes.ActualBaseResidual.velocityComponents_smooth {u : ProblemStatement.VelocityField} (hu : ContDiffOn ℝ (↑⊤) u BaseResidual.past) : ContDiffOn ℝ (↑⊤) (CylindricalResidual.velocityComponents u) BaseResidual.past

theorem NavierStokes.ActualBaseResidual.pressurePullback_smooth {p : ProblemStatement.PressureField} (hp : ContDiffOn ℝ (↑⊤) p BaseResidual.past) : ContDiffOn ℝ (↑⊤) (CylindricalResidual.pressurePullback p) BaseResidual.past

theorem NavierStokes.ActualBaseResidual.axisymmetric_components (b f u : AxisymmetricFields.Profile) (t : ℝ) (q : Space) : (CylindricalResidual.frame (-q.ofLp 1)) (AxisymmetricResidual.velocity b f u (t, CylindricalResidual.chart q)) = AxisymmetricResidual.velocity b f u (t, AxisymmetricResidual.pack (q.ofLp 0) 0 (q.ofLp 2))

Axisymmetry of the complete curl field, in cylindrical components.

noncomputable def NavierStokes.ActualBaseResidual.profileAtScale (h Q : ℝ) (x : Point) : AxisymmetricFields.ProfilePoint

Profile at scale, given by (1 - Q * x.2.1.1, (Q * x.1 ^ 2 / 2, Q ^ CoordinateAlgebra.D h * x.2.1.2)).

Equations

• NavierStokes.ActualBaseResidual.profileAtScale h Q x = (1 - Q * x.2.1.1, Q * x.1 ^ 2 / 2, Q ^ NavierStokes.CoordinateAlgebra.D h * x.2.1.2)

noncomputable def NavierStokes.ActualBaseResidual.profileJacobian (h Q : ℝ) (x : Point) : Point →L[ℝ] AxisymmetricFields.ProfilePoint

Profile jacobian as an element of Point →L[ℝ] AxisymmetricFields.ProfilePoint.

Equations

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

theorem NavierStokes.ActualBaseResidual.profileJacobian_apply (h Q : ℝ) (x d : Point) : (profileJacobian h Q x) d = (-Q * d.2.1.1, Q * x.1 * d.1, Q ^ CoordinateAlgebra.D h * d.2.1.2)

theorem NavierStokes.ActualBaseResidual.profileAtScale_hasFDerivAt (h Q : ℝ) (x : Point) : HasFDerivAt (profileAtScale h Q) (profileJacobian h Q x) x

theorem NavierStokes.ActualBaseResidual.normalized_profile_radialDiv (o : MeanIncrementBounds.Operators Point) (n : ℕ) (hR : o.radius = fun (x : Point) => x.1) (heR : o.eR = (1, 0, 0)) {w : ℝ × ℝ} (hvR : o.vR = (0, 0, w)) {Q : ℝ} (hQ : 0 < Q) (h k : ℝ) (S : AxisymmetricFields.Profile) {x : Point} (hx : 0 < x.1) (hS : DifferentiableAt ℝ S (profileAtScale h Q x)) : o.radialDiv k (fun (x : ℕ) (y : Point) => Q ^ (2 * CoordinateAlgebra.A h) * S (profileAtScale h Q y)) n x = Q ^ (2 * CoordinateAlgebra.A h + 1 / 2) * LeadingStress.radialDivergence k S (profileAtScale h Q x)

A direct derivative calculation for the normalized stress profile.

theorem NavierStokes.ActualBaseResidual.tangentialStressForce_components (theta axial : AxisymmetricFields.Profile) (t : ℝ) (q : Space) (hr : 0 < q.ofLp 0) : (CylindricalResidual.frame (-q.ofLp 1)) (SlowResidualMatching.tangentialStressForce theta axial t (CylindricalResidual.chart q)) = AxisymmetricResidual.pack 0 (-LeadingStress.radialDivergence 2 theta (t, q.ofLp 0 ^ 2 / 2, q.ofLp 2)) (-LeadingStress.radialDivergence 1 axial (t, q.ofLp 0 ^ 2 / 2, q.ofLp 2))

Rotation of the actual Cartesian tangential stress force.

theorem NavierStokes.ActualBaseResidual.band_power_product (n m : ℕ) (a : ℝ) : ChartScales.Q m ^ a * (ChartScales.Q n / ChartScales.Q m) ^ a = ChartScales.Q n ^ a

Exact cancellation of a positive band ratio, at every real exponent.

theorem NavierStokes.ActualBaseResidual.cylinderPoint_bandChart (h : ℝ) (n m k : ℕ) (x : Point) (theta : ℝ) : cylinderPoint h (ChartScales.Q m) ((GaugeStateCoherence.bandChartEquiv h n m k) x, theta) = cylinderPoint h (ChartScales.Q n) (x, theta)

theorem NavierStokes.ActualBaseResidual.physicalPoint_bandChart (h : ℝ) (n m k : ℕ) (x : Point) (theta : ℝ) : physicalPoint h (ChartScales.Q m) ((GaugeStateCoherence.bandChartEquiv h n m k) x, theta) = physicalPoint h (ChartScales.Q n) (x, theta)

noncomputable def NavierStokes.ActualBaseResidual.pressureAtScale {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) (Q : ℝ) (x : Full) : ℝ

The normalized pressure of the actual summed base, at arbitrary positive scale.

Equations

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

noncomputable def NavierStokes.ActualBaseResidual.errorAtScale {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) (Q : ℝ) (x : Full) : Fin 3 → ℝ

The normalized Cartesian error, expressed in the cylindrical frame.

Equations

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

noncomputable def NavierStokes.ActualBaseResidual.velocityAtScale {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) (Q : ℝ) (x : Full) : Fin 3 → ℝ

Velocity at scale as an element of Fin 3 → ℝ.

Equations

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

noncomputable def NavierStokes.ActualBaseResidual.stressAtScale {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) (Q : ℝ) (x : Full) : Fin 3 → ℝ

Stress at scale as an element of Fin 3 → ℝ.

Equations

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

noncomputable def NavierStokes.ActualBaseResidual.basePressure {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B n : ℕ) : Full → ℝ

Base pressure, given by pressureAtScale H v upper B (ChartScales.Q n).

Equations

• NavierStokes.ActualBaseResidual.basePressure H v upper B n = NavierStokes.ActualBaseResidual.pressureAtScale H v upper B (NavierStokes.ChartScales.Q n)

noncomputable def NavierStokes.ActualBaseResidual.baseError {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B n : ℕ) : Full → Fin 3 → ℝ

Base error, given by errorAtScale H v upper B (ChartScales.Q n).

Equations

• NavierStokes.ActualBaseResidual.baseError H v upper B n = NavierStokes.ActualBaseResidual.errorAtScale H v upper B (NavierStokes.ChartScales.Q n)

theorem NavierStokes.ActualBaseResidual.pressureAtScale_smooth {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) {Q : ℝ} (hQ : 0 < Q) : ContDiffOn ℝ (↑⊤) (pressureAtScale H v upper B Q) timeDomain

theorem NavierStokes.ActualBaseResidual.errorAtScale_smooth {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) {Q : ℝ} (hQ : 0 < Q) (i : Fin 3) : ContDiffOn ℝ (↑⊤) (fun (x : Full) => errorAtScale H v upper B Q x i) timeDomain

theorem NavierStokes.ActualBaseResidual.basePressure_smooth {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B n : ℕ) : ContDiffOn ℝ (↑⊤) (basePressure H v upper B n) timeDomain

theorem NavierStokes.ActualBaseResidual.baseError_smooth {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B n : ℕ) (i : Fin 3) : ContDiffOn ℝ (↑⊤) (fun (x : Full) => baseError H v upper B n x i) timeDomain

theorem NavierStokes.ActualBaseResidual.scaled_residual {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) {Q : ℝ} (hQ : 0 < Q) (k : ℕ) {x : Full} (hx : x ∈ domain) (i : Fin 3) : PhysicalResidualBridge.graphResidual (Q ^ F.data.h) PhysicalResidualBridge.ScaledGraph.radius (PhysicalResidualTZ.graphRadialTZ (PhysicalResidualBridge.commonGraph Q F.data.h k)) PhysicalResidualTZ.graphAngularTZ (PhysicalResidualTZ.graphAxialTZ (PhysicalResidualBridge.commonGraph Q F.data.h k)) (PhysicalResidualTZ.graphTemporalTZ (PhysicalResidualBridge.commonGraph Q F.data.h k)) (velocityAtScale H v upper B Q) (pressureAtScale H v upper B Q) x i = stressAtScale H v upper B Q x i + errorAtScale H v upper B Q x i

The actual base PDE after anisotropic scaling. No auxiliary point is restricted to the image of a physical graph.

theorem NavierStokes.ActualBaseResidual.actual_velocity_components {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) {t : ℝ} (ht : t < 1) (q : Space) : (CylindricalResidual.frame (-q.ofLp 1)) (FinalSlowBase.velocity H v upper B (t, CylindricalResidual.chart q)) = FinalSlowBase.velocity H v upper B (t, AxisymmetricResidual.pack (q.ofLp 0) 0 (q.ofLp 2))

Cylindrical components of the actual summed velocity equal its values on the zero-angle ray. This uses its defining curl, including every slow order.

theorem NavierStokes.ActualBaseResidual.velocityAtScale_eq_baseComponents {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) (index : ℕ → ℕ) (n : ℕ) {x : Full} (hx : x ∈ domain) : velocityAtScale H v upper B (ChartScales.Q n) x = PhysicalResidualBridge.baseComponents (CommonBaseContext.context H v upper B index) n x

The directly normalized velocity is exactly the fixed base stored by CommonBaseContext; the common cover index affects only derivative directions.

theorem NavierStokes.ActualBaseResidual.profileAtScale_eq_physicalProfile {F : OutgoingProfile.Profile} (n : ℕ) (x : Point) : AxisymmetricFields.profilePoint (BaseContextAssembly.physicalPoint F.data.h n x).1 (BaseContextAssembly.physicalPoint F.data.h n x).2 = profileAtScale F.data.h (ChartScales.Q n) x

theorem NavierStokes.ActualBaseResidual.virtualTheta_eq {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) (index : ℕ → ℕ) (n : ℕ) {x : Point} (hx : 0 < x.1) : (CommonBaseContext.context H v upper B index).virtualTheta n x = ChartScales.Q n ^ (2 * CoordinateAlgebra.A F.data.h) * SlowBorelBase.baseStressTheta (FinalSlowBase.scales H v upper B) F.data.h W.axis.normalization (FinalSlowBase.coefficients H v) (profileAtScale F.data.h (ChartScales.Q n) x)

theorem NavierStokes.ActualBaseResidual.virtualAxial_eq {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) (index : ℕ → ℕ) (n : ℕ) {x : Point} (hx : 0 < x.1) : (CommonBaseContext.context H v upper B index).virtualAxial n x = ChartScales.Q n ^ (2 * CoordinateAlgebra.A F.data.h) * SlowBorelBase.baseStressAxial (FinalSlowBase.scales H v upper B) F.data.h W.axis.normalization (FinalSlowBase.coefficients H v) (profileAtScale F.data.h (ChartScales.Q n) x)

theorem NavierStokes.ActualBaseResidual.radialDiv_germ_eq (o : MeanIncrementBounds.Operators Point) (k : ℝ) {f g : MeanIncrementBounds.Field Point} {n : ℕ} {x : Point} (he : f n =ᶠ[nhds x] g n) : o.radialDiv k f n x = o.radialDiv k g n x

Equality of genuine germs transports both pieces of the radial operator.

theorem NavierStokes.ActualBaseResidual.stressAtScale_eq_virtualDivergence {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) (index : ℕ → ℕ) (n : ℕ) {x : Full} (hx : x ∈ domain) : stressAtScale H v upper B (ChartScales.Q n) x = LiftedMeanResidual.virtualDivergence (CommonBaseContext.context H v upper B index) n x

The scaled physical stress force is exactly the fixed context's virtual radial divergence, including its connection terms.

theorem NavierStokes.ActualBaseResidual.velocityAtScale_smooth {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) {Q : ℝ} (hQ : 0 < Q) (i : Fin 3) : ContDiffOn ℝ (↑⊤) (fun (x : Full) => velocityAtScale H v upper B Q x i) timeDomain

theorem NavierStokes.ActualBaseResidual.baseComponents_smooth {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) (index : ℕ → ℕ) (n : ℕ) (i : Fin 3) : ContDiffOn ℝ (↑⊤) (fun (x : PhysicalResidualBridge.Cylinder) => PhysicalResidualBridge.baseComponents (CommonBaseContext.context H v upper B index) n x i) domain

theorem NavierStokes.ActualBaseResidual.fixed_base_residual {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) (index : ℕ → ℕ) (n : ℕ) {x : Full} (hx : x ∈ domain) (i : Fin 3) : PhysicalResidualBridge.graphResidual (ChartScales.Q n ^ F.data.h) PhysicalResidualBridge.ScaledGraph.radius (PhysicalResidualTZ.graphRadialTZ (PhysicalResidualBridge.commonGraph (ChartScales.Q n) F.data.h (index n))) PhysicalResidualTZ.graphAngularTZ (PhysicalResidualTZ.graphAxialTZ (PhysicalResidualBridge.commonGraph (ChartScales.Q n) F.data.h (index n))) (PhysicalResidualTZ.graphTemporalTZ (PhysicalResidualBridge.commonGraph (ChartScales.Q n) F.data.h (index n))) (PhysicalResidualBridge.baseComponents (CommonBaseContext.context H v upper B index) n) (basePressure H v upper B n) x i = LiftedMeanResidual.virtualDivergence (CommonBaseContext.context H v upper B index) n x i + baseError H v upper B n x i

The fixed-base equation required by initialization, on the entire free lift. It is derived from FinalSlowBase.residual_identity.

theorem NavierStokes.ActualBaseResidual.pressureAtScale_angle_eq {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) (Q : ℝ) (x : Point) (theta : ℝ) : pressureAtScale H v upper B Q (x, theta) = pressureAtScale H v upper B Q (x, 0)

theorem NavierStokes.ActualBaseResidual.basePressure_angle_eq {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B n : ℕ) (x : Point) (theta : ℝ) : basePressure H v upper B n (x, theta) = basePressure H v upper B n (x, 0)

theorem NavierStokes.ActualBaseResidual.baseError_angular_continuous {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B n : ℕ) {x : Point} (hx : 0 < x.2.1.1) (i : Fin 3) : Continuous fun (theta : ℝ) => baseError H v upper B n (x, theta) i

noncomputable def NavierStokes.ActualBaseResidual.fixedPressure {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B n : ℕ) (x : Point) : ℝ

The pressure stored separately from the correction's pressure increment.

Equations

• NavierStokes.ActualBaseResidual.fixedPressure H v upper B n x = NavierStokes.ActualBaseResidual.basePressure H v upper B n (x, 0)

theorem NavierStokes.ActualBaseResidual.basePressure_eq_fixedPressure {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B n : ℕ) (x : Full) : basePressure H v upper B n x = fixedPressure H v upper B n x.1

theorem NavierStokes.ActualBaseResidual.basePressure_band {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B n m k : ℕ) (x : Point) (theta : ℝ) : basePressure H v upper B n (x, theta) = (ChartScales.Q n / ChartScales.Q m) ^ (2 * CoordinateAlgebra.A F.data.h) * basePressure H v upper B m ((GaugeStateCoherence.bandChartEquiv F.data.h n m k) x, theta)

Full band transition. The auxiliary cover is arbitrary because this is the same physical base field on every free lift.

theorem NavierStokes.ActualBaseResidual.baseError_band {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B n m k : ℕ) (x : Point) (theta : ℝ) (i : Fin 3) : baseError H v upper B n (x, theta) i = (ChartScales.Q n / ChartScales.Q m) ^ (2 * CoordinateAlgebra.A F.data.h + 1 / 2) * baseError H v upper B m ((GaugeStateCoherence.bandChartEquiv F.data.h n m k) x, theta) i

noncomputable def NavierStokes.ActualBaseResidual.errorState {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) : CorrectionState.State Point

Error state, bundling mean, pressure, oscillation, oscillatoryPressure and the required compatibility proofs.

Equations

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

theorem NavierStokes.ActualBaseResidual.errorState_band {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) (U : Set Point) (n m k : ℕ) : PhysicalResidualNaturality.StateOn U (GaugeStateCoherence.bandChartEquiv F.data.h n m k) (GaugeStateCoherence.bandVelocityScale F.data.h n m) (GaugeStateCoherence.bandScale n m) (errorState H v upper B) (errorState H v upper B) n m

The genuine excluded base error satisfies the full free-lift state law, with constants dictated by the physical scaling.

theorem NavierStokes.ActualBaseResidual.fixedPressure_band {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) (U : Set Point) (n m k : ℕ) : PhysicalResidualNaturality.ScalarOn U (GaugeStateCoherence.bandChartEquiv F.data.h n m k) (GaugeStateCoherence.bandVelocityScale F.data.h n m * GaugeStateCoherence.bandVelocityScale F.data.h n m) (fixedPressure H v upper B n) (fixedPressure H v upper B m)

theorem NavierStokes.ActualBaseResidual.baseError_angle_eq {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B n : ℕ) {x : Point} (hR : 0 < x.1) (hT : 0 < x.2.1.1) (theta : ℝ) (i : Fin 3) : baseError H v upper B n (x, theta) i = baseError H v upper B n (x, 0) i

The actual excluded error has no angular dependence on positive time and radius; this follows from the proved base equation.

theorem NavierStokes.ActualBaseResidual.baseError_auxiliary_eq {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B n : ℕ) (R : ℝ) (s Y Y' : ℝ × ℝ) (theta : ℝ) : baseError H v upper B n ((R, s, Y), theta) = baseError H v upper B n ((R, s, Y'), theta)

theorem NavierStokes.ActualBaseResidual.basePressure_auxiliary_eq {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B n : ℕ) (R : ℝ) (s Y Y' : ℝ × ℝ) (theta : ℝ) : basePressure H v upper B n ((R, s, Y), theta) = basePressure H v upper B n ((R, s, Y'), theta)

theorem NavierStokes.ActualBaseResidual.errorState_common {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) (U : Set Point) (n k : ℕ) : PhysicalResidualNaturality.StateOn U (CommonBaseContext.coverLift k) 1 1 (errorState H v upper B) (errorState H v upper B) n n

Fixed-band common-cover specialization of the same physical error field.

theorem NavierStokes.ActualBaseResidual.fixedPressure_common {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) (U : Set Point) (n k : ℕ) : PhysicalResidualNaturality.ScalarOn U (CommonBaseContext.coverLift k) 1 (fixedPressure H v upper B n) (fixedPressure H v upper B n)