Physical stage estimates from the actual native mean region

Mean families are supplied on the original normalized region (1/2,2). Only native smoothness, support, and class estimates are input. The physical stage bounds and the initialized velocity estimate are derived.

Fixed losses for the actual physical slow velocity

The compact similarity region uses the selected Borel scales and the existing prefix estimates, including the axis. Outside the positive-order support the velocity is its actual leading angular field. In the far exterior it is the physical heat field. The final rate is on the full open-past endpoint filter.

noncomputable def NavierStokes.ActualBaseVelocityBounds.endpoint : Filter ProblemStatement.SpaceTime

Endpoint, given by 𝓝[SpacetimeEndpoint.openPast 1] (1, (0 : Space)).

Equations

• NavierStokes.ActualBaseVelocityBounds.endpoint = nhdsWithin (1, 0) (NavierStokes.SpacetimeEndpoint.openPast 1)

theorem NavierStokes.ActualBaseVelocityBounds.endpoint_past : ∀ᶠ (z : ProblemStatement.SpaceTime) in endpoint, z.1 < 1

theorem NavierStokes.ActualBaseVelocityBounds.endpoint_compact : ∀ᶠ (z : ℝ × ProblemStatement.Space) in endpoint, z ∈ Metric.closedBall (1, 0) 1

theorem NavierStokes.ActualBaseVelocityBounds.q_eq (h : ℝ) (z : ProblemStatement.SpaceTime) : (SlowBorelBase.cartesianChart h z).1 = PhysicalWaveSum.physicalQ h z

theorem NavierStokes.ActualBaseVelocityBounds.endpoint_q_small {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) : ∀ᶠ (z : ProblemStatement.SpaceTime) in endpoint, 0 < PhysicalWaveSum.physicalQ h z ∧ PhysicalWaveSum.physicalQ h z ≤ 1

noncomputable def NavierStokes.ActualBaseVelocityBounds.physicalEnergy (z : ProblemStatement.SpaceTime) : ℝ

Physical energy, given by AxisymmetricFields.radialEnergy z.2.

Equations

• NavierStokes.ActualBaseVelocityBounds.physicalEnergy z = NavierStokes.AxisymmetricFields.radialEnergy z.2

theorem NavierStokes.ActualBaseVelocityBounds.physicalEnergy_smooth : ContDiff ℝ (↑⊤) physicalEnergy

theorem NavierStokes.ActualBaseVelocityBounds.X_eq (h : ℝ) (z : ProblemStatement.SpaceTime) : (SlowBorelBase.cartesianChart h z).2.1 = physicalEnergy z / PhysicalWaveSum.physicalQ h z

theorem NavierStokes.ActualBaseVelocityBounds.X_nonneg {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {z : ProblemStatement.SpaceTime} (hz : z.1 < 1) : 0 ≤ (SlowBorelBase.cartesianChart h z).2.1

theorem NavierStokes.ActualBaseVelocityBounds.rate_glue {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {l : Filter D} {q : D → ℝ} {f : D → E} {S : Set D} {m : ℕ} {r : ℝ} (hq : ∀ᶠ (z : D) in l, 0 < q z) (hleft : DiagonalResidual.JetRate (l ⊓ Filter.principal S) q f m r) (hright : DiagonalResidual.JetRate (l ⊓ Filter.principal Sᶜ) q f m r) : DiagonalResidual.JetRate l q f m r

noncomputable def NavierStokes.ActualBaseVelocityBounds.boundedApproach {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {l : Filter ProblemStatement.SpaceTime} (hl : l ≤ endpoint) (R : ℝ) (hR : ∀ᶠ (z : ProblemStatement.SpaceTime) in l, (SlowBorelBase.cartesianChart h z).2.1 ≤ R) : BaseResidual.PhysicalApproach l h 0 R

Bounded approach, bundling carrier, compact, in_carrier, past and the required compatibility proofs.

Equations

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

theorem NavierStokes.ActualBaseVelocityBounds.negative_power_le {a q x p : ℝ} (ha : 0 < a) (hq : 0 < q) (hq1 : q ≤ 1) (hax : a * q ≤ x) (hp : -2 ≤ p ∧ p ≤ 0) : x ^ p ≤ a ^ p * q ^ (-2)

Compact physical derivatives and a geometric lower bound control negative powers. No derivative bound for the output power is assumed.

noncomputable def NavierStokes.ActualBaseVelocityBounds.powerLoss (m : ℕ) : ℝ

Power loss, given by 2 * (2 * (m : ℝ) + 1).

Equations

• NavierStokes.ActualBaseVelocityBounds.powerLoss m = 2 * (2 * ↑m + 1)

theorem NavierStokes.ActualBaseVelocityBounds.powerLoss_nonneg (m : ℕ) : 0 ≤ powerLoss m

theorem NavierStokes.ActualBaseVelocityBounds.finiteRate_negative_power {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {l : Filter D} {q f : D → ℝ} {K : Set D} (hf : ContDiff ℝ (↑⊤) f) (hK : IsCompact K) (hlK : ∀ᶠ (z : D) in l, z ∈ K) (hq : ∀ᶠ (z : D) in l, 0 < q z ∧ q z ≤ 1) {a p : ℝ} (ha : 0 < a) (hlower : ∀ᶠ (z : D) in l, a * q z ≤ f z) (hp : -2 ≤ p ∧ p ≤ 0) (m : ℕ) : DiagonalResidual.FiniteJetRate l q (fun (z : D) => f z ^ p) m (-powerLoss m)

theorem NavierStokes.ActualBaseVelocityBounds.finiteRate_uniform_comp {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {l : Filter D} {q f : D → ℝ} {U : Set D} (hU : IsOpen U) (hlU : ∀ᶠ (z : D) in l, z ∈ U) (hf : ContDiffOn ℝ (↑⊤) f U) (g : ℝ → ℝ) (hg : ContDiff ℝ (↑⊤) g) {m : ℕ} {L A : ℝ} (hL : 0 ≤ L) (hA : 0 ≤ A) (hgb : ∀ i ≤ m, ∀ (x : ℝ), ‖iteratedFDeriv ℝ i g x‖ ≤ A) (hq : ∀ᶠ (z : D) in l, 0 < q z ∧ q z ≤ 1) (hr : DiagonalResidual.FiniteJetRate l q f m (-L)) : DiagonalResidual.FiniteJetRate l q (g ∘ f) m (-(L * ↑m))

theorem NavierStokes.ActualBaseVelocityBounds.finiteRate_mul {l : Filter ProblemStatement.SpaceTime} {q f g : ProblemStatement.SpaceTime → ℝ} {U : Set ProblemStatement.SpaceTime} {m : ℕ} {r s : ℝ} (hf : DiagonalResidual.FiniteJetRate l q f m r) (hg : DiagonalResidual.FiniteJetRate l q g m s) (hU : IsOpen U) (hlU : ∀ᶠ (z : ProblemStatement.SpaceTime) in l, z ∈ U) (hq : ∀ᶠ (z : ProblemStatement.SpaceTime) in l, 0 < q z) (hsf : ContDiffOn ℝ (↑⊤) f U) (hsg : ContDiffOn ℝ (↑⊤) g U) : DiagonalResidual.FiniteJetRate l q (fun (z : ProblemStatement.SpaceTime) => f z * g z) m (r + s)

noncomputable def NavierStokes.ActualBaseVelocityBounds.positiveRadius : Set ProblemStatement.SpaceTime

Positive radius, given by {z | 0 < physicalEnergy z}.

Equations

• NavierStokes.ActualBaseVelocityBounds.positiveRadius = {z : NavierStokes.ProblemStatement.SpaceTime | 0 < NavierStokes.ActualBaseVelocityBounds.physicalEnergy z}

theorem NavierStokes.ActualBaseVelocityBounds.positiveRadius_isOpen : IsOpen positiveRadius

noncomputable def NavierStokes.ActualBaseVelocityBounds.heatTime (z : ProblemStatement.SpaceTime) : ℝ

Heat time, given by 2 * (1 - z.1).

Equations

• NavierStokes.ActualBaseVelocityBounds.heatTime z = 2 * (1 - z.1)

theorem NavierStokes.ActualBaseVelocityBounds.heatTime_smooth : ContDiff ℝ (↑⊤) heatTime

noncomputable def NavierStokes.ActualBaseVelocityBounds.heatRatio (z : ProblemStatement.SpaceTime) : ℝ

Heat ratio, given by heatTime z * physicalEnergy z ^ (-1 : ℝ).

Equations

• NavierStokes.ActualBaseVelocityBounds.heatRatio z = NavierStokes.ActualBaseVelocityBounds.heatTime z * NavierStokes.ActualBaseVelocityBounds.physicalEnergy z ^ (-1)

theorem NavierStokes.ActualBaseVelocityBounds.energyPower_smooth (p : ℝ) : ContDiffOn ℝ (↑⊤) (fun (z : ProblemStatement.SpaceTime) => physicalEnergy z ^ p) positiveRadius

theorem NavierStokes.ActualBaseVelocityBounds.heatRatio_smooth : ContDiffOn ℝ (↑⊤) heatRatio positiveRadius

noncomputable def NavierStokes.ActualBaseVelocityBounds.heatModelCoefficient (C h : ℝ) (z : ProblemStatement.SpaceTime) : ℝ

Heat model coefficient as an element of ℝ.

Equations

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

theorem NavierStokes.ActualBaseVelocityBounds.doubleEnergyPower_smooth (p : ℝ) : ContDiffOn ℝ (↑⊤) (fun (z : ProblemStatement.SpaceTime) => (2 * physicalEnergy z) ^ p) positiveRadius

theorem NavierStokes.ActualBaseVelocityBounds.heatModelCoefficient_smooth (C : ℝ) {h : ℝ} (hh : 0 < h) : ContDiffOn ℝ (↑⊤) (heatModelCoefficient C h) positiveRadius

noncomputable def NavierStokes.ActualBaseVelocityBounds.heatModelVelocity (C h : ℝ) (z : ProblemStatement.SpaceTime) : ProblemStatement.Space

Heat model velocity, given by heatModelCoefficient C h z • angularVector z.

Equations

• NavierStokes.ActualBaseVelocityBounds.heatModelVelocity C h z = NavierStokes.ActualBaseVelocityBounds.heatModelCoefficient C h z • NavierStokes.BaseResidual.angularVector z

theorem NavierStokes.ActualBaseVelocityBounds.heatModelCoefficient_eq (C h : ℝ) {z : ProblemStatement.SpaceTime} (ht : z.1 < 1) (hs : 0 < physicalEnergy z) : heatModelCoefficient C h z = BaseExterior.heatCoefficient C h (AxisymmetricFields.profilePoint z.1 z.2)

theorem NavierStokes.ActualBaseVelocityBounds.heatModelVelocity_eq (C h : ℝ) {z : ProblemStatement.SpaceTime} (ht : z.1 < 1) (hs : 0 < physicalEnergy z) : heatModelVelocity C h z = BaseExterior.heatVelocity C h z

theorem NavierStokes.ActualBaseVelocityBounds.extension_uniform_jets {a : ℝ} (ha : 1 < a) (m : ℕ) : ∃ (A : ℝ), 0 ≤ A ∧ ∀ i ≤ m, ∀ (x : ℝ), ‖iteratedFDeriv ℝ i (HeatProfileExtension.extension a) x‖ ≤ A

noncomputable def NavierStokes.ActualBaseVelocityBounds.heatLoss (m : ℕ) : ℝ

Heat loss, given by powerLoss m * ((m : ℝ) + 2).

Equations

• NavierStokes.ActualBaseVelocityBounds.heatLoss m = NavierStokes.ActualBaseVelocityBounds.powerLoss m * (↑m + 2)

theorem NavierStokes.ActualBaseVelocityBounds.heatLoss_eq (m : ℕ) : heatLoss m = (4 * ↑m + 2) * (↑m + 2)

theorem NavierStokes.ActualBaseVelocityBounds.heatLoss_nonneg (m : ℕ) : 0 ≤ heatLoss m

theorem NavierStokes.ActualBaseVelocityBounds.heat_velocity_rate {l : Filter ProblemStatement.SpaceTime} (hl : l ≤ endpoint) {h R : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hR : 0 < R) (hlR : ∀ᶠ (z : ProblemStatement.SpaceTime) in l, R < (SlowBorelBase.cartesianChart h z).2.1) (C : ℝ) (m : ℕ) : DiagonalResidual.FiniteJetRate l (PhysicalWaveSum.physicalQ h) (BaseExterior.heatVelocity C h) m (-heatLoss m)

theorem NavierStokes.ActualBaseVelocityBounds.monomial_rate {l : Filter ProblemStatement.SpaceTime} {h lo hi : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (A : BaseResidual.PhysicalApproach l h lo hi) {f : SlowBorelBase.Inner → ℝ} (hf : ContDiff ℝ (↑⊤) f) (b : ℝ) (m : ℕ) : DiagonalResidual.FiniteJetRate l (PhysicalWaveSum.physicalQ h) (BaseResidual.cartesianMonomial h b f) m (b - ↑m)

noncomputable def NavierStokes.ActualBaseVelocityBounds.leadingVelocity (h C : ℝ) (d : SlowBorelBase.Coefficients) (z : ProblemStatement.SpaceTime) : ProblemStatement.Space

Leading velocity, given by (C⁻¹ * cartesianMonomial h (-CoordinateAlgebra.A h - 1 / 2) (d.phi 0) z) • angularVector z.

Equations

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

theorem NavierStokes.ActualBaseVelocityBounds.leadingVelocity_eq (h C : ℝ) (d : SlowBorelBase.Coefficients) (z : ProblemStatement.SpaceTime) : leadingVelocity h C d z = AxisymmetricResidual.velocity (fun (x : AxisymmetricFields.ProfilePoint) => 0) (BaseExterior.leadingAngular h C d) (fun (x : AxisymmetricFields.ProfilePoint) => 0) z

theorem NavierStokes.ActualBaseVelocityBounds.leadingVelocity_rate {l : Filter ProblemStatement.SpaceTime} {h C lo hi : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (A : BaseResidual.PhysicalApproach l h lo hi) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) (m : ℕ) : DiagonalResidual.FiniteJetRate l (PhysicalWaveSum.physicalQ h) (leadingVelocity h C d) m (-CoordinateAlgebra.A h - 1 / 2 - ↑m)

theorem NavierStokes.ActualBaseVelocityBounds.restricted_mem {D : Type u_1} (l : Filter D) (S : Set D) : ∀ᶠ (z : D) in l ⊓ Filter.principal S, z ∈ S

theorem NavierStokes.ActualBaseVelocityBounds.heatLoss_controls_core {h : ℝ} (hh1 : h < 1 / 2) (m : ℕ) : -heatLoss m ≤ -CoordinateAlgebra.A h - 2 * (↑m + 1)

theorem NavierStokes.ActualBaseVelocityBounds.heatLoss_controls_middle {h : ℝ} (hh1 : h < 1 / 2) (m : ℕ) : -heatLoss m ≤ -CoordinateAlgebra.A h - 1 / 2 - ↑m

theorem NavierStokes.ActualBaseVelocityBounds.heatLoss_mono {n m : ℕ} (hnm : n ≤ m) : heatLoss n ≤ heatLoss m

theorem NavierStokes.ActualBaseVelocityBounds.actual_exterior_coefficients {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) : BaseExterior.ExteriorCoefficients (FinalSlowBase.coefficients H v) (AssembledSlowBase.nominalOuterX W)

The support and zero-mass identities are consequences of the actual coefficient construction, not hypotheses on the final velocity.

theorem NavierStokes.ActualBaseVelocityBounds.actual_leading_eq {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) : Set.EqOn (FinalSlowBase.velocity H v upper B) (leadingVelocity F.data.h W.axis.normalization (FinalSlowBase.coefficients H v)) (BaseExterior.cartesianExterior F.data.h (AssembledSlowBase.nominalOuterX W))

theorem NavierStokes.ActualBaseVelocityBounds.actual_bounded_rate {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) {l : Filter ProblemStatement.SpaceTime} (hl : l ≤ endpoint) (hbox : ∀ᶠ (z : ProblemStatement.SpaceTime) in l, (SlowBorelBase.cartesianChart F.data.h z).2.1 ≤ FinalSlowBase.boxRadius W upper) (m : ℕ) : DiagonalResidual.FiniteJetRate l (PhysicalWaveSum.physicalQ F.data.h) (FinalSlowBase.velocity H v upper B) m (-CoordinateAlgebra.A F.data.h - 2 * (↑m + 1))

theorem NavierStokes.ActualBaseVelocityBounds.actual_middle_rate {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) {l : Filter ProblemStatement.SpaceTime} (hl : l ≤ endpoint) {R : ℝ} (hR : ∀ᶠ (z : ProblemStatement.SpaceTime) in l, (SlowBorelBase.cartesianChart F.data.h z).2.1 ≤ R) (houter : ∀ᶠ (z : ProblemStatement.SpaceTime) in l, AssembledSlowBase.nominalOuterX W < (SlowBorelBase.cartesianChart F.data.h z).2.1) (m : ℕ) : DiagonalResidual.FiniteJetRate l (PhysicalWaveSum.physicalQ F.data.h) (FinalSlowBase.velocity H v upper B) m (-CoordinateAlgebra.A F.data.h - 1 / 2 - ↑m)

theorem NavierStokes.ActualBaseVelocityBounds.actual_outer_rate {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) {l : Filter ProblemStatement.SpaceTime} (hl : l ≤ endpoint) (houter : ∀ᶠ (z : ProblemStatement.SpaceTime) in l, AssembledSlowBase.nominalOuterX W < (SlowBorelBase.cartesianChart F.data.h z).2.1) (m : ℕ) : DiagonalResidual.JetRate l (PhysicalWaveSum.physicalQ F.data.h) (FinalSlowBase.velocity H v upper B) m (-heatLoss m)

The entire region outside the coefficient support, including unbounded similarity radii, has one fixed polynomial loss.

theorem NavierStokes.ActualBaseVelocityBounds.outer_lt_box {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (upper : ℝ) : AssembledSlowBase.nominalOuterX W < FinalSlowBase.boxRadius W upper

theorem NavierStokes.ActualBaseVelocityBounds.velocity_rate {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B m : ℕ) : DiagonalResidual.JetRate endpoint (PhysicalWaveSum.physicalQ F.data.h) (FinalSlowBase.velocity H v upper B) m (-heatLoss m)

Full physical endpoint estimate for the actual constructed base. The universal loss (4*m+2)*(m+2) depends only on derivative order. Constants and the eventual neighborhood may depend on the fixed base data.

theorem NavierStokes.ActualBaseVelocityBounds.velocity_finite_rate {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B m : ℕ) : DiagonalResidual.FiniteJetRate endpoint (PhysicalWaveSum.physicalQ F.data.h) (FinalSlowBase.velocity H v upper B) m (-heatLoss m)

A common constant and neighborhood control the entire finite jet.

theorem NavierStokes.ActualBaseVelocityBounds.exists_fixed_loss {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B m : ℕ) : ∃ (L : ℝ), 0 ≤ L ∧ DiagonalResidual.JetRate (nhdsWithin (1, 0) (SpacetimeEndpoint.openPast 1)) (PhysicalWaveSum.physicalQ F.data.h) (FinalSlowBase.velocity H v upper B) m (-L)

Public statement with the endpoint filter and existential loss explicit.

Initial physical velocity bounds from the actual base and native data

The base potential is the anchored TailGaugePotential.finalPotential. Its curl is the constructed FinalSlowBase.velocity. Only the finite initialization potential pays the derivative used by the curl estimate; no growth estimate on the base potential or its gauge is required.

Finite background bounds from the raw increments

The raw-stage interface starts at index one. A bound for the actual initialized stage is therefore kept explicit. Together with the raw increment bounds it controls every finite prefix with one derivative-loss function, independent of the number of correction stages.

theorem NavierStokes.MixedFiniteBackground.raw_jetRate {D : Type u_1} {V : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup V] [NormedSpace ℝ V] {l : Filter D} {q : D → ℝ} {A : ℕ → D → V} {g L : ℕ → ℝ} {C : ℕ → ℕ → ℝ} {S : Set D} (hraw : CutStageEstimates.RawStageBounds q A g L C (fun (x x_1 : ℕ) => 0) S) (hS : ∀ᶠ (x : D) in l, x ∈ S) (hq : ∀ᶠ (x : D) in l, 0 < q x ∧ q x ≤ 1) {j : ℕ} (hj : 1 ≤ j) (m : ℕ) : DiagonalResidual.JetRate l q (A j) m (g j - L m)

theorem NavierStokes.MixedFiniteBackground.uncutPrefix_succ {D : Type u_1} {V : Type u_2} [NormedAddCommGroup V] (A : ℕ → D → V) (N : ℕ) : DiagonalJetBounds.uncutPrefix A (N + 1) = fun (x : D) => DiagonalJetBounds.uncutPrefix A N x + A N x

theorem NavierStokes.MixedFiniteBackground.nonemptyPrefix_jetRate {D : Type u_1} {V : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup V] [NormedSpace ℝ V] {l : Filter D} {q : D → ℝ} {A : ℕ → D → V} {U : Set D} {m : ℕ} {r : ℝ} (hU : IsOpen U) (hlU : ∀ᶠ (x : D) in l, x ∈ U) (hA : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (A j) U) (hzero : DiagonalResidual.JetRate l q (A 0) m r) (hpos : ∀ (j : ℕ), 1 ≤ j → DiagonalResidual.JetRate l q (A j) m r) (J : ℕ) : DiagonalResidual.JetRate l q (DiagonalJetBounds.uncutPrefix A (J + 1)) m r

theorem NavierStokes.MixedFiniteBackground.prefix_background {D : Type u_1} {V : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup V] [NormedSpace ℝ V] {l : Filter D} {q : D → ℝ} {A : ℕ → D → V} {g L Lzero : ℕ → ℝ} {C : ℕ → ℕ → ℝ} {U S : Set D} (hU : IsOpen U) (hlU : ∀ᶠ (x : D) in l, x ∈ U) (hS : ∀ᶠ (x : D) in l, x ∈ S) (hq : ∀ᶠ (x : D) in l, 0 < q x ∧ q x ≤ 1) (hA : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (A j) U) (hraw : CutStageEstimates.RawStageBounds q A g L C (fun (x x_1 : ℕ) => 0) S) (hg : ∀ (j : ℕ), 1 ≤ j → 0 ≤ g j) (hzero : ∀ (m : ℕ), DiagonalResidual.JetRate l q (A 0) m (-Lzero m)) (J m : ℕ) : DiagonalResidual.JetRate l q (DiagonalJetBounds.uncutPrefix A (J + 1)) m (-max (L m) (Lzero m))

noncomputable def NavierStokes.MixedFiniteBackground.backgroundLoss (LA LB LAzero LBzero : ℕ → ℝ) (m : ℕ) : ℝ

The one derivative needed for the potential is paid independently of the correction index. The direct field pays no curl derivative.

Equations

• NavierStokes.MixedFiniteBackground.backgroundLoss LA LB LAzero LBzero m = max (max (LA (m + 1)) (LAzero (m + 1))) (max (LB m) (LBzero m))

theorem NavierStokes.MixedFiniteBackground.mixed_background {l : Filter ProblemStatement.SpaceTime} {q : ProblemStatement.SpaceTime → ℝ} {A B : ℕ → ProblemStatement.VelocityField} {g LA LB LAzero LBzero : ℕ → ℝ} {CA CB : ℕ → ℕ → ℝ} {U S : Set ProblemStatement.SpaceTime} (hU : IsOpen U) (hlU : ∀ᶠ (x : ProblemStatement.SpaceTime) in l, x ∈ U) (hS : ∀ᶠ (x : ProblemStatement.SpaceTime) in l, x ∈ S) (hq : ∀ᶠ (x : ProblemStatement.SpaceTime) in l, 0 < q x ∧ q x ≤ 1) (hA : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (A j) U) (hB : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (B j) U) (hrawA : CutStageEstimates.RawStageBounds q A g LA CA (fun (x x_1 : ℕ) => 0) S) (hrawB : CutStageEstimates.RawStageBounds q B g LB CB (fun (x x_1 : ℕ) => 0) S) (hg : ∀ (j : ℕ), 1 ≤ j → 0 ≤ g j) (hzeroA : ∀ (m : ℕ), DiagonalResidual.JetRate l q (A 0) m (-LAzero m)) (hzeroB : ∀ (m : ℕ), DiagonalResidual.JetRate l q (B 0) m (-LBzero m)) (J m : ℕ) : DiagonalResidual.JetRate l q (MixedDiagonalResidual.uncutVelocity A B J) m (-backgroundLoss LA LB LAzero LBzero m)

noncomputable def NavierStokes.MixedFiniteBackground.stageVelocity (A B : ℕ → ProblemStatement.VelocityField) (j : ℕ) : ProblemStatement.VelocityField

Stage velocity, defined pointwise by SpatialCurl.spatialCurl (A j) x + B j x.

Equations

• NavierStokes.MixedFiniteBackground.stageVelocity A B j x = NavierStokes.SpatialCurl.spatialCurl (A j) x + B j x

theorem NavierStokes.MixedFiniteBackground.uncutVelocity_zero (A B : ℕ → ProblemStatement.VelocityField) : MixedDiagonalResidual.uncutVelocity A B 0 = stageVelocity A B 0

theorem NavierStokes.MixedFiniteBackground.uncutVelocity_eq_stagePrefix {U : Set ProblemStatement.SpaceTime} (hU : IsOpen U) (A B : ℕ → ProblemStatement.VelocityField) (hA : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (A j) U) (J : ℕ) : Set.EqOn (MixedDiagonalResidual.uncutVelocity A B J) (DiagonalJetBounds.uncutPrefix (stageVelocity A B) (J + 1)) U

noncomputable def NavierStokes.MixedFiniteBackground.initialBackgroundLoss (Lzero LA LB : ℕ → ℝ) (m : ℕ) : ℝ

This version only needs a bound for the initialized physical velocity. It imposes no growth assumption on the gauge of the initial potential.

Equations

• NavierStokes.MixedFiniteBackground.initialBackgroundLoss Lzero LA LB m = max (Lzero m) (max (LA (m + 1)) (LB m))

theorem NavierStokes.MixedFiniteBackground.mixed_background_from_initial {l : Filter ProblemStatement.SpaceTime} {q : ProblemStatement.SpaceTime → ℝ} {A B : ℕ → ProblemStatement.VelocityField} {g LA LB Lzero : ℕ → ℝ} {CA CB : ℕ → ℕ → ℝ} {U S : Set ProblemStatement.SpaceTime} (hU : IsOpen U) (hlU : ∀ᶠ (x : ProblemStatement.SpaceTime) in l, x ∈ U) (hS : ∀ᶠ (x : ProblemStatement.SpaceTime) in l, x ∈ S) (hq : ∀ᶠ (x : ProblemStatement.SpaceTime) in l, 0 < q x ∧ q x ≤ 1) (hA : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (A j) U) (hB : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (B j) U) (hrawA : CutStageEstimates.RawStageBounds q A g LA CA (fun (x x_1 : ℕ) => 0) S) (hrawB : CutStageEstimates.RawStageBounds q B g LB CB (fun (x x_1 : ℕ) => 0) S) (hg : ∀ (j : ℕ), 1 ≤ j → 0 ≤ g j) (hzero : ∀ (m : ℕ), DiagonalResidual.JetRate l q (MixedDiagonalResidual.uncutVelocity A B 0) m (-Lzero m)) (J m : ℕ) : DiagonalResidual.JetRate l q (MixedDiagonalResidual.uncutVelocity A B J) m (-initialBackgroundLoss Lzero LA LB m)

noncomputable def NavierStokes.InitializedPhysicalBackground.seedPotentialLoss (h waveAlpha waveShift meanAlpha : ℝ) (m : ℕ) : ℝ

The loss for the actual finite initialization potential, before curl. The offsets absorb its own native homogeneity, without a positivity assumption on the initialization gain.

Equations

• NavierStokes.InitializedPhysicalBackground.seedPotentialLoss h waveAlpha waveShift meanAlpha m = NavierStokes.PhysicalStageBounds.potentialLoss h (-(h * waveAlpha + waveShift)) (-(h * meanAlpha)) m

noncomputable def NavierStokes.InitializedPhysicalBackground.seedDirectLoss (h meanAlpha : ℝ) (m : ℕ) : ℝ

Seed direct loss, given by directLoss h (-(h * meanAlpha)) m.

Equations

• NavierStokes.InitializedPhysicalBackground.seedDirectLoss h meanAlpha m = NavierStokes.PhysicalStageBounds.directLoss h (-(h * meanAlpha)) m

noncomputable def NavierStokes.InitializedPhysicalBackground.initialLoss (h waveAlpha waveShift potentialAlpha directAlpha : ℝ) (m : ℕ) : ℝ

This loss depends only on fixed initialization data and derivative order. It has no later correction-stage parameter.

Equations

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

theorem NavierStokes.InitializedPhysicalBackground.initialLoss_nonneg (h waveAlpha waveShift potentialAlpha directAlpha : ℝ) (m : ℕ) : 0 ≤ initialLoss h waveAlpha waveShift potentialAlpha directAlpha m

theorem NavierStokes.InitializedPhysicalBackground.endpoint_sublevel {h qbig : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hqbig : 0 < qbig) : ∀ᶠ (w : ProblemStatement.SpaceTime) in ActualBaseVelocityBounds.endpoint, w ∈ CutStageEstimates.physicalSublevel h qbig

theorem NavierStokes.InitializedPhysicalBackground.spatialCurl_add_on {U : Set ProblemStatement.SpaceTime} (hU : IsOpen U) {A B : ProblemStatement.VelocityField} (hA : ContDiffOn ℝ (↑⊤) A U) (hB : ContDiffOn ℝ (↑⊤) B U) : Set.EqOn (SpatialCurl.spatialCurl fun (w : ProblemStatement.SpaceTime) => A w + B w) (fun (w : ProblemStatement.SpaceTime) => SpatialCurl.spatialCurl A w + SpatialCurl.spatialCurl B w) U

theorem NavierStokes.InitializedPhysicalBackground.spatialCurl_smoothOn {U : Set ProblemStatement.SpaceTime} (hU : IsOpen U) {A : ProblemStatement.VelocityField} (hA : ContDiffOn ℝ (↑⊤) A U) : ContDiffOn ℝ (↑⊤) (SpatialCurl.spatialCurl A) U

theorem NavierStokes.InitializedPhysicalBackground.potentialIncrement_rate {h : ℝ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (WA : PhysicalStageBounds.WaveData h D I K (Fin 3)) (MA : PhysicalStageBounds.MeanData h (CoordinateAlgebra.A h - 1 / 2)) (hh : 0 < h) (hh1 : h < 1 / 2) {qbig : ℝ} (hqbig : 0 < qbig) (hq : qbig ≤ ChartScales.Q MA.firstBand) (m : ℕ) : DiagonalResidual.JetRate ActualBaseVelocityBounds.endpoint (PhysicalWaveSum.physicalQ h) (PhysicalStageBounds.potentialIncrement WA MA) m (-seedPotentialLoss h WA.alpha WA.shift MA.alpha m)

This applies the actual native-copy estimate at initialization, where the positive-stage RawStageBounds interface is not available.

theorem NavierStokes.InitializedPhysicalBackground.directIncrement_rate {h : ℝ} (MB : PhysicalStageBounds.MeanData h (CoordinateAlgebra.A h)) (hh : 0 < h) (hh1 : h < 1 / 2) {qbig : ℝ} (hqbig : 0 < qbig) (hq : qbig ≤ ChartScales.Q MB.firstBand) (m : ℕ) : DiagonalResidual.JetRate ActualBaseVelocityBounds.endpoint (PhysicalWaveSum.physicalQ h) MB.family.angularField m (-seedDirectLoss h MB.alpha m)

noncomputable def NavierStokes.InitializedPhysicalBackground.initializedPotential {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (upper : ℝ) (B : ℕ) (WA : PhysicalStageBounds.WaveData F.data.h D I K (Fin 3)) (MA : PhysicalStageBounds.MeanData F.data.h (CoordinateAlgebra.A F.data.h - 1 / 2)) : ProblemStatement.VelocityField

Initialized potential, defined pointwise by `TailGaugePotential.finalPotential H v upper B w

• potentialIncrement WA MA w`.

Equations

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

noncomputable def NavierStokes.InitializedPhysicalBackground.initializedVelocity {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (upper : ℝ) (B : ℕ) (WA : PhysicalStageBounds.WaveData F.data.h D I K (Fin 3)) (MA : PhysicalStageBounds.MeanData F.data.h (CoordinateAlgebra.A F.data.h - 1 / 2)) (MB : PhysicalStageBounds.MeanData F.data.h (CoordinateAlgebra.A F.data.h)) : ProblemStatement.VelocityField

Literal curl of the initialized potential plus the direct angular initialization. The latter is not differentiated as a potential.

Equations

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

theorem NavierStokes.InitializedPhysicalBackground.initializedPotential_smooth {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (upper : ℝ) (B : ℕ) (WA : PhysicalStageBounds.WaveData F.data.h D I K (Fin 3)) (MA : PhysicalStageBounds.MeanData F.data.h (CoordinateAlgebra.A F.data.h - 1 / 2)) {qbig : ℝ} (hq : qbig ≤ ChartScales.Q MA.firstBand) : ContDiffOn ℝ (↑⊤) (initializedPotential H v upper B WA MA) (CutStageEstimates.physicalSublevel F.data.h qbig)

theorem NavierStokes.InitializedPhysicalBackground.initializedVelocity_decomposition {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (upper : ℝ) (B : ℕ) (WA : PhysicalStageBounds.WaveData F.data.h D I K (Fin 3)) (MA : PhysicalStageBounds.MeanData F.data.h (CoordinateAlgebra.A F.data.h - 1 / 2)) (MB : PhysicalStageBounds.MeanData F.data.h (CoordinateAlgebra.A F.data.h)) {qbig : ℝ} (hq : qbig ≤ ChartScales.Q MA.firstBand) : Set.EqOn (initializedVelocity H v upper B WA MA MB) (fun (w : ProblemStatement.SpaceTime) => FinalSlowBase.velocity H v upper B w + SpatialCurl.spatialCurl (PhysicalStageBounds.potentialIncrement WA MA) w + MB.family.angularField w) (CutStageEstimates.physicalSublevel F.data.h qbig)

The only use of the anchored gauge is its proved equality of curls.

theorem NavierStokes.InitializedPhysicalBackground.initializedVelocity_smooth {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (upper : ℝ) (B : ℕ) (WA : PhysicalStageBounds.WaveData F.data.h D I K (Fin 3)) (MA : PhysicalStageBounds.MeanData F.data.h (CoordinateAlgebra.A F.data.h - 1 / 2)) (MB : PhysicalStageBounds.MeanData F.data.h (CoordinateAlgebra.A F.data.h)) {qbig : ℝ} (hqA : qbig ≤ ChartScales.Q MA.firstBand) (hqB : qbig ≤ ChartScales.Q MB.firstBand) : ContDiffOn ℝ (↑⊤) (initializedVelocity H v upper B WA MA MB) (CutStageEstimates.physicalSublevel F.data.h qbig)

theorem NavierStokes.InitializedPhysicalBackground.initializedVelocity_rate {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (upper : ℝ) (B : ℕ) (WA : PhysicalStageBounds.WaveData F.data.h D I K (Fin 3)) (MA : PhysicalStageBounds.MeanData F.data.h (CoordinateAlgebra.A F.data.h - 1 / 2)) (MB : PhysicalStageBounds.MeanData F.data.h (CoordinateAlgebra.A F.data.h)) (m : ℕ) : DiagonalResidual.JetRate ActualBaseVelocityBounds.endpoint (PhysicalWaveSum.physicalQ F.data.h) (initializedVelocity H v upper B WA MA MB) m (-initialLoss F.data.h WA.alpha WA.shift MA.alpha MB.alpha m)

Initial physical velocity bound from native initialization data and the actual constructed base. There is no initial-velocity rate premise.

theorem NavierStokes.InitializedPhysicalBackground.initializedVelocity_finite_rate {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (upper : ℝ) (B : ℕ) (WA : PhysicalStageBounds.WaveData F.data.h D I K (Fin 3)) (MA : PhysicalStageBounds.MeanData F.data.h (CoordinateAlgebra.A F.data.h - 1 / 2)) (MB : PhysicalStageBounds.MeanData F.data.h (CoordinateAlgebra.A F.data.h)) (m : ℕ) : DiagonalResidual.FiniteJetRate ActualBaseVelocityBounds.endpoint (PhysicalWaveSum.physicalQ F.data.h) (initializedVelocity H v upper B WA MA MB) m (-DiagonalResidual.maxJetLoss (initialLoss F.data.h WA.alpha WA.shift MA.alpha MB.alpha) m)

theorem NavierStokes.InitializedPhysicalBackground.uncutVelocity_zero_eq_initialized {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (upper : ℝ) (B : ℕ) (WA : ℕ → PhysicalStageBounds.WaveData F.data.h D I K (Fin 3)) (MA : ℕ → PhysicalStageBounds.MeanData F.data.h (CoordinateAlgebra.A F.data.h - 1 / 2)) (MB : ℕ → PhysicalStageBounds.MeanData F.data.h (CoordinateAlgebra.A F.data.h)) : MixedDiagonalResidual.uncutVelocity (PhysicalStageBounds.potentialStages (TailGaugePotential.finalPotential H v upper B) WA MA) (PhysicalStageBounds.directStages MB) 0 = initializedVelocity H v upper B (WA 0) (MA 0) (MB 0)

theorem NavierStokes.InitializedPhysicalBackground.stages_initial_rate {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (upper : ℝ) (B : ℕ) (WA : ℕ → PhysicalStageBounds.WaveData F.data.h D I K (Fin 3)) (MA : ℕ → PhysicalStageBounds.MeanData F.data.h (CoordinateAlgebra.A F.data.h - 1 / 2)) (MB : ℕ → PhysicalStageBounds.MeanData F.data.h (CoordinateAlgebra.A F.data.h)) (m : ℕ) : DiagonalResidual.JetRate ActualBaseVelocityBounds.endpoint (PhysicalWaveSum.physicalQ F.data.h) (MixedDiagonalResidual.uncutVelocity (PhysicalStageBounds.potentialStages (TailGaugePotential.finalPotential H v upper B) WA MA) (PhysicalStageBounds.directStages MB) 0) m (-initialLoss F.data.h (WA 0).alpha (WA 0).shift (MA 0).alpha (MB 0).alpha m)

Direct input for MixedFiniteBackground.mixed_background_from_initial, using the actual index-zero native estimates.

theorem NavierStokes.InitializedPhysicalBackground.represented_initial_rate {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (upper : ℝ) (B : ℕ) (WA : PhysicalStageBounds.WaveData F.data.h D I K (Fin 3)) (MA : PhysicalStageBounds.MeanData F.data.h (CoordinateAlgebra.A F.data.h - 1 / 2)) (MB : PhysicalStageBounds.MeanData F.data.h (CoordinateAlgebra.A F.data.h)) {A Bdirect : ℕ → ProblemStatement.VelocityField} {U : Set ProblemStatement.SpaceTime} (hU : IsOpen U) (hlU : ∀ᶠ (w : ProblemStatement.SpaceTime) in ActualBaseVelocityBounds.endpoint, w ∈ U) (hA : Set.EqOn (A 0) (initializedPotential H v upper B WA MA) U) (hB : Set.EqOn (Bdirect 0) MB.family.angularField U) (m : ℕ) : DiagonalResidual.JetRate ActualBaseVelocityBounds.endpoint (PhysicalWaveSum.physicalQ F.data.h) (MixedDiagonalResidual.uncutVelocity A Bdirect 0) m (-initialLoss F.data.h WA.alpha WA.shift MA.alpha MB.alpha m)

An exact representation adapter for initialization assembled elsewhere. Its inputs identify the literal potential and direct angular field on an eventual open neighborhood; no bound on either initialized velocity or the base gauge is assumed.

theorem NavierStokes.InitializedPhysicalBackground.native_background_rate {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (upper : ℝ) (B : ℕ) (WA : ℕ → PhysicalStageBounds.WaveData F.data.h D I K (Fin 3)) (MA : ℕ → PhysicalStageBounds.MeanData F.data.h (CoordinateAlgebra.A F.data.h - 1 / 2)) (MB : ℕ → PhysicalStageBounds.MeanData F.data.h (CoordinateAlgebra.A F.data.h)) {qbig : ℝ} (hqbig : 0 < qbig) (hqA : ∀ (j : ℕ), qbig ≤ ChartScales.Q (MA j).firstBand) (hqB : ∀ (j : ℕ), qbig ≤ ChartScales.Q (MB j).firstBand) (g : ℕ → ℝ) (waveOffset potentialOffset directOffset : ℝ) (hg : ∀ (j : ℕ), 1 ≤ j → 0 ≤ g j) (hwave : ∀ (j : ℕ), 1 ≤ j → g j ≤ F.data.h * (WA j).alpha + (WA j).shift + waveOffset) (hpotential : ∀ (j : ℕ), 1 ≤ j → g j ≤ F.data.h * (MA j).alpha + potentialOffset) (hdirect : ∀ (j : ℕ), 1 ≤ j → g j ≤ F.data.h * (MB j).alpha + directOffset) (J m : ℕ) : DiagonalResidual.JetRate ActualBaseVelocityBounds.endpoint (PhysicalWaveSum.physicalQ F.data.h) (MixedDiagonalResidual.uncutVelocity (PhysicalStageBounds.potentialStages (TailGaugePotential.finalPotential H v upper B) WA MA) (PhysicalStageBounds.directStages MB) J) m (-MixedFiniteBackground.initialBackgroundLoss (initialLoss F.data.h (WA 0).alpha (WA 0).shift (MA 0).alpha (MB 0).alpha) (PhysicalStageBounds.potentialLoss F.data.h waveOffset potentialOffset) (PhysicalStageBounds.directLoss F.data.h directOffset) m)

Every native finite background now follows without an assumed index-zero velocity bound. Its loss is fixed for the whole sequence.

noncomputable def NavierStokes.ActualPhysicalStageBounds.region (h : ℝ) : Set PhysicalGraphBounds.Plane

Region, given by PhysicalMeanDomain.normalizedSlowDomain (2 * h) (1 / 2) 2.

Equations

• NavierStokes.ActualPhysicalStageBounds.region h = NavierStokes.PhysicalMeanDomain.normalizedSlowDomain (2 * h) (1 / 2) 2

theorem NavierStokes.ActualPhysicalStageBounds.region_open {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) : IsOpen (region h)

structure NavierStokes.ActualPhysicalStageBounds.MeanInput (h degree : ℝ) : Type

Native facts about an already constructed coherent mean family. This record neither constructs a new physical field nor assumes physical derivative bounds.

• firstBand : ℕ

  First band of MeanInput, of type ℕ.

• gapBound : ℕ

  Gap bound of MeanInput, of type ℕ.

• lowerRadius : ℝ

  Lower radius of MeanInput, of type ℝ.

• upperRadius : ℝ

  Upper radius of MeanInput, of type ℝ.

• alpha : ℝ

  Alpha of MeanInput, of type ℝ.

• family : PhysicalMeanJetBounds.CoherentFamily h degree self.firstBand self.gapBound (region h) ℝ

  Family of MeanInput, of type PhysicalMeanJetBounds.CoherentFamily h degree firstBand gapBound (region h) ℝ.

• band_four : 4 ≤ self.firstBand
• lower_pos : 0 < self.lowerRadius
• radii_lt : self.lowerRadius < self.upperRadius
• smooth (n : ℕ) : n ≥ self.firstBand → ContDiffOn ℝ (↑⊤) (self.family.native n) (PhysicalMeanDomain.slowDomain (region h))
• support : PhysicalMeanJetBounds.NativeSupport h self.lowerRadius self.upperRadius self.firstBand (region h) self.family.native
• jets : PhysicalMeanJetBounds.NativeJets self.firstBand (region h) (h * self.alpha) self.family.native

noncomputable def NavierStokes.ActualPhysicalStageBounds.MeanInput.ofMoving {h degree a b α : ℝ} {N Δ : ℕ} (R : LocalSignedRequest.SlowRegion (2 * h)) (hR : R.carrier = region h) (M : PhysicalMeanJetBounds.CoherentFamily h degree N Δ (region h) ℝ) (hN : 4 ≤ N) (ha : 0 < a) (hab : a < b) (hm : GaugeMomentBalances.MovingField R a b M.native) (hj : PhysicalMeanJetBounds.NativeJets N R.carrier (h * α) M.native) : MeanInput h degree

Package the existing moving-field and native-class theorems without changing the supplied coherent physical field.

Equations

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

theorem NavierStokes.ActualPhysicalStageBounds.MeanInput.field_smooth {h degree qbig : ℝ} (M : MeanInput h degree) (hh : 0 < h) (hh1 : h < 1 / 2) (hq : qbig ≤ ChartScales.Q M.firstBand) : ContDiffOn ℝ (↑⊤) M.family.field (CutStageEstimates.physicalSublevel h qbig)

theorem NavierStokes.ActualPhysicalStageBounds.MeanInput.angular_smooth {h degree qbig : ℝ} (M : MeanInput h degree) (hh : 0 < h) (hh1 : h < 1 / 2) (hq : qbig ≤ ChartScales.Q M.firstBand) : ContDiffOn ℝ (↑⊤) M.family.angularField (CutStageEstimates.physicalSublevel h qbig)

theorem NavierStokes.ActualPhysicalStageBounds.MeanInput.field_bound {h degree qbig : ℝ} (M : MeanInput h degree) (hh : 0 < h) (hh1 : h < 1 / 2) (hq : qbig ≤ ChartScales.Q M.firstBand) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ w ∈ CutStageEstimates.physicalSublevel h qbig, PhysicalWaveSum.physicalQ h w ≤ 1 → ‖iteratedFDeriv ℝ m M.family.field w‖ ≤ C * PhysicalWaveSum.physicalQ h w ^ (h * M.alpha - PhysicalMeanJetBounds.loss degree m)

theorem NavierStokes.ActualPhysicalStageBounds.MeanInput.angular_bound {h degree qbig : ℝ} (M : MeanInput h degree) (hh : 0 < h) (hh1 : h < 1 / 2) (hq : qbig ≤ ChartScales.Q M.firstBand) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ w ∈ CutStageEstimates.physicalSublevel h qbig, PhysicalWaveSum.physicalQ h w ≤ 1 → ‖iteratedFDeriv ℝ m M.family.angularField w‖ ≤ C * PhysicalWaveSum.physicalQ h w ^ (h * M.alpha - PhysicalMeanJetBounds.loss degree m)

theorem NavierStokes.ActualPhysicalStageBounds.MeanInput.field_bound_with_gain {h degree qbig g delta : ℝ} (M : MeanInput h degree) (hh : 0 < h) (hh1 : h < 1 / 2) (hq : qbig ≤ ChartScales.Q M.firstBand) (hg : g ≤ h * M.alpha + delta) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ w ∈ CutStageEstimates.physicalSublevel h qbig, PhysicalWaveSum.physicalQ h w ≤ 1 → ‖iteratedFDeriv ℝ m M.family.field w‖ ≤ C * PhysicalWaveSum.physicalQ h w ^ (g - (PhysicalMeanJetBounds.loss degree m + delta))

theorem NavierStokes.ActualPhysicalStageBounds.MeanInput.angular_bound_with_gain {h degree qbig g delta : ℝ} (M : MeanInput h degree) (hh : 0 < h) (hh1 : h < 1 / 2) (hq : qbig ≤ ChartScales.Q M.firstBand) (hg : g ≤ h * M.alpha + delta) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ w ∈ CutStageEstimates.physicalSublevel h qbig, PhysicalWaveSum.physicalQ h w ≤ 1 → ‖iteratedFDeriv ℝ m M.family.angularField w‖ ≤ C * PhysicalWaveSum.physicalQ h w ^ (g - (PhysicalMeanJetBounds.loss degree m + delta))

theorem NavierStokes.ActualPhysicalStageBounds.weaken_bound {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {h qbig : ℝ} {f : ProblemStatement.SpaceTime → V} {m : ℕ} {r s : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hsr : s ≤ r) (hb : ∃ (C : ℝ), 0 ≤ C ∧ ∀ w ∈ CutStageEstimates.physicalSublevel h qbig, PhysicalWaveSum.physicalQ h w ≤ 1 → ‖iteratedFDeriv ℝ m f w‖ ≤ C * PhysicalWaveSum.physicalQ h w ^ r) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ w ∈ CutStageEstimates.physicalSublevel h qbig, PhysicalWaveSum.physicalQ h w ≤ 1 → ‖iteratedFDeriv ℝ m f w‖ ≤ C * PhysicalWaveSum.physicalQ h w ^ s

theorem NavierStokes.ActualPhysicalStageBounds.add_bounds {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {h qbig : ℝ} {f g : ProblemStatement.SpaceTime → V} {m : ℕ} {r : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hf : ContDiffOn ℝ (↑⊤) f (CutStageEstimates.physicalSublevel h qbig)) (hg : ContDiffOn ℝ (↑⊤) g (CutStageEstimates.physicalSublevel h qbig)) (hfb : ∃ (C : ℝ), 0 ≤ C ∧ ∀ w ∈ CutStageEstimates.physicalSublevel h qbig, PhysicalWaveSum.physicalQ h w ≤ 1 → ‖iteratedFDeriv ℝ m f w‖ ≤ C * PhysicalWaveSum.physicalQ h w ^ r) (hgb : ∃ (C : ℝ), 0 ≤ C ∧ ∀ w ∈ CutStageEstimates.physicalSublevel h qbig, PhysicalWaveSum.physicalQ h w ≤ 1 → ‖iteratedFDeriv ℝ m g w‖ ≤ C * PhysicalWaveSum.physicalQ h w ^ r) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ w ∈ CutStageEstimates.physicalSublevel h qbig, PhysicalWaveSum.physicalQ h w ≤ 1 → ‖iteratedFDeriv ℝ m (fun (z : ProblemStatement.SpaceTime) => f z + g z) w‖ ≤ C * PhysicalWaveSum.physicalQ h w ^ r

noncomputable def NavierStokes.ActualPhysicalStageBounds.potentialIncrement {h : ℝ} {DP DS : Type} [NormedAddCommGroup DP] [NormedSpace ℝ DP] [NormedAddCommGroup DS] [NormedSpace ℝ DS] {IP : Type u_1} {KP : Type u_2} {IS : Type u_3} {KS : Type u_4} (WP : PhysicalStageBounds.WaveData h DP IP KP (Fin 3)) (WS : PhysicalStageBounds.WaveData h DS IS KS (Fin 3)) (MT MR : MeanInput h (CoordinateAlgebra.A h - 1 / 2)) : ProblemStatement.VelocityField

The four actual potential contributions of one cycle.

Equations

• NavierStokes.ActualPhysicalStageBounds.potentialIncrement WP WS MT MR w = WP.vector w + WS.vector w + MT.family.angularField w + MR.family.angularField w

noncomputable def NavierStokes.ActualPhysicalStageBounds.pressureIncrement {h : ℝ} {DP DS : Type} [NormedAddCommGroup DP] [NormedSpace ℝ DP] [NormedAddCommGroup DS] [NormedSpace ℝ DS] {IP : Type u_1} {KP : Type u_2} {IS : Type u_3} {KS : Type u_4} (WP : PhysicalStageBounds.WaveData h DP IP KP Unit) (WS : PhysicalStageBounds.WaveData h DS IS KS Unit) (MP : MeanInput h (2 * CoordinateAlgebra.A h)) : ProblemStatement.PressureField

Pressure increment, defined pointwise by WP.pressure w + WS.pressure w + MP.family.field w.

Equations

• NavierStokes.ActualPhysicalStageBounds.pressureIncrement WP WS MP w = WP.pressure w + WS.pressure w + MP.family.field w

theorem NavierStokes.ActualPhysicalStageBounds.potentialIncrement_smooth {h : ℝ} {DP DS : Type} [NormedAddCommGroup DP] [NormedSpace ℝ DP] [NormedAddCommGroup DS] [NormedSpace ℝ DS] {IP : Type u_1} {KP : Type u_2} {IS : Type u_3} {KS : Type u_4} (WP : PhysicalStageBounds.WaveData h DP IP KP (Fin 3)) (WS : PhysicalStageBounds.WaveData h DS IS KS (Fin 3)) (MT MR : MeanInput h (CoordinateAlgebra.A h - 1 / 2)) (hh : 0 < h) (hh1 : h < 1 / 2) {qbig : ℝ} (hqT : qbig ≤ ChartScales.Q MT.firstBand) (hqR : qbig ≤ ChartScales.Q MR.firstBand) : ContDiffOn ℝ (↑⊤) (potentialIncrement WP WS MT MR) (CutStageEstimates.physicalSublevel h qbig)

theorem NavierStokes.ActualPhysicalStageBounds.pressureIncrement_smooth {h : ℝ} {DP DS : Type} [NormedAddCommGroup DP] [NormedSpace ℝ DP] [NormedAddCommGroup DS] [NormedSpace ℝ DS] {IP : Type u_1} {KP : Type u_2} {IS : Type u_3} {KS : Type u_4} (WP : PhysicalStageBounds.WaveData h DP IP KP Unit) (WS : PhysicalStageBounds.WaveData h DS IS KS Unit) (MP : MeanInput h (2 * CoordinateAlgebra.A h)) (hh : 0 < h) (hh1 : h < 1 / 2) {qbig : ℝ} (hq : qbig ≤ ChartScales.Q MP.firstBand) : ContDiffOn ℝ (↑⊤) (pressureIncrement WP WS MP) (CutStageEstimates.physicalSublevel h qbig)

theorem NavierStokes.ActualPhysicalStageBounds.potentialIncrement_bound {h : ℝ} {DP DS : Type} [NormedAddCommGroup DP] [NormedSpace ℝ DP] [NormedAddCommGroup DS] [NormedSpace ℝ DS] {IP : Type u_1} {KP : Type u_2} {IS : Type u_3} {KS : Type u_4} (WP : PhysicalStageBounds.WaveData h DP IP KP (Fin 3)) (WS : PhysicalStageBounds.WaveData h DS IS KS (Fin 3)) (MT MR : MeanInput h (CoordinateAlgebra.A h - 1 / 2)) (hh : 0 < h) (hh1 : h < 1 / 2) {qbig g dw dm : ℝ} (hqT : qbig ≤ ChartScales.Q MT.firstBand) (hqR : qbig ≤ ChartScales.Q MR.firstBand) (hWP : g ≤ h * WP.alpha + WP.shift + dw) (hWS : g ≤ h * WS.alpha + WS.shift + dw) (hMT : g ≤ h * MT.alpha + dm) (hMR : g ≤ h * MR.alpha + dm) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ w ∈ CutStageEstimates.physicalSublevel h qbig, PhysicalWaveSum.physicalQ h w ≤ 1 → ‖iteratedFDeriv ℝ m (potentialIncrement WP WS MT MR) w‖ ≤ C * PhysicalWaveSum.physicalQ h w ^ (g - PhysicalStageBounds.potentialLoss h dw dm m)

theorem NavierStokes.ActualPhysicalStageBounds.pressureIncrement_bound {h : ℝ} {DP DS : Type} [NormedAddCommGroup DP] [NormedSpace ℝ DP] [NormedAddCommGroup DS] [NormedSpace ℝ DS] {IP : Type u_1} {KP : Type u_2} {IS : Type u_3} {KS : Type u_4} (WP : PhysicalStageBounds.WaveData h DP IP KP Unit) (WS : PhysicalStageBounds.WaveData h DS IS KS Unit) (MP : MeanInput h (2 * CoordinateAlgebra.A h)) (hh : 0 < h) (hh1 : h < 1 / 2) {qbig g dw dm : ℝ} (hq : qbig ≤ ChartScales.Q MP.firstBand) (hWP : g ≤ h * WP.alpha + WP.shift + dw) (hWS : g ≤ h * WS.alpha + WS.shift + dw) (hMP : g ≤ h * MP.alpha + dm) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ w ∈ CutStageEstimates.physicalSublevel h qbig, PhysicalWaveSum.physicalQ h w ≤ 1 → ‖iteratedFDeriv ℝ m (pressureIncrement WP WS MP) w‖ ≤ C * PhysicalWaveSum.physicalQ h w ^ (g - PhysicalStageBounds.pressureLoss h dw dm m)

Positive correction stages and the exact ledger gain

structure NavierStokes.ActualPhysicalStageBounds.CycleInputs (h : ℝ) (DP : Type) [NormedAddCommGroup DP] [NormedSpace ℝ DP] (IP : Type u_1) (KP : Type u_2) (DS : Type) [NormedAddCommGroup DS] [NormedSpace ℝ DS] (IS : Type u_3) (KS : Type u_4) : Type (max (max (max u_1 u_2) u_3) u_4)

Cycle inputs data, collecting particularPotential, signedPotential, particularPressure, signedPressure, temporal, rank and their compatibility conditions.

• particularPotential : ℕ → PhysicalStageBounds.WaveData h DP IP KP (Fin 3)

  Particular potential of CycleInputs, of type ℕ → PhysicalStageBounds.WaveData h DP IP KP (Fin 3).

• signedPotential : ℕ → PhysicalStageBounds.WaveData h DS IS KS (Fin 3)

  Signed potential of CycleInputs, of type ℕ → PhysicalStageBounds.WaveData h DS IS KS (Fin 3).

• particularPressure : ℕ → PhysicalStageBounds.WaveData h DP IP KP Unit

  Particular pressure of CycleInputs, of type ℕ → PhysicalStageBounds.WaveData h DP IP KP Unit.

• signedPressure : ℕ → PhysicalStageBounds.WaveData h DS IS KS Unit

  Signed pressure of CycleInputs, of type ℕ → PhysicalStageBounds.WaveData h DS IS KS Unit.

• temporal : ℕ → MeanInput h (CoordinateAlgebra.A h - 1 / 2)

  Temporal of CycleInputs, of type ℕ → MeanInput h (CoordinateAlgebra.A h - 1 / 2).

• rank : ℕ → MeanInput h (CoordinateAlgebra.A h - 1 / 2)

  Rank of CycleInputs, of type ℕ → MeanInput h (CoordinateAlgebra.A h - 1 / 2).

• angular : ℕ → MeanInput h (CoordinateAlgebra.A h)

  Angular of CycleInputs, of type ℕ → MeanInput h (CoordinateAlgebra.A h).

• pressure : ℕ → MeanInput h (2 * CoordinateAlgebra.A h)

  Pressure field of CycleInputs, of type ℕ → MeanInput h (2 * CoordinateAlgebra.A h).

noncomputable def NavierStokes.ActualPhysicalStageBounds.CycleInputs.potential {h : ℝ} {DP DS : Type} [NormedAddCommGroup DP] [NormedSpace ℝ DP] [NormedAddCommGroup DS] [NormedSpace ℝ DS] {IP : Type u_1} {KP : Type u_2} {IS : Type u_3} {KS : Type u_4} (D : CycleInputs h DP IP KP DS IS KS) (k : ℕ) : ProblemStatement.VelocityField

Potential, given by potentialIncrement (D.particularPotential k) (D.signedPotential k) (D.temporal k) (D.rank k).

Equations

• D.potential k = NavierStokes.ActualPhysicalStageBounds.potentialIncrement (D.particularPotential k) (D.signedPotential k) (D.temporal k) (D.rank k)

noncomputable def NavierStokes.ActualPhysicalStageBounds.CycleInputs.direct {h : ℝ} {DP DS : Type} [NormedAddCommGroup DP] [NormedSpace ℝ DP] [NormedAddCommGroup DS] [NormedSpace ℝ DS] {IP : Type u_1} {KP : Type u_2} {IS : Type u_3} {KS : Type u_4} (D : CycleInputs h DP IP KP DS IS KS) (k : ℕ) : ProblemStatement.VelocityField

Direct, given by (D.angular k).family.angularField.

Equations

• D.direct k = (D.angular k).family.angularField

noncomputable def NavierStokes.ActualPhysicalStageBounds.CycleInputs.pressureField {h : ℝ} {DP DS : Type} [NormedAddCommGroup DP] [NormedSpace ℝ DP] [NormedAddCommGroup DS] [NormedSpace ℝ DS] {IP : Type u_1} {KP : Type u_2} {IS : Type u_3} {KS : Type u_4} (D : CycleInputs h DP IP KP DS IS KS) (k : ℕ) : ProblemStatement.PressureField

Pressure field, given by pressureIncrement (D.particularPressure k) (D.signedPressure k) (D.pressure k).

Equations

• D.pressureField k = NavierStokes.ActualPhysicalStageBounds.pressureIncrement (D.particularPressure k) (D.signedPressure k) (D.pressure k)

structure NavierStokes.ActualPhysicalStageBounds.CycleInputs.Metadata {h : ℝ} {DP DS : Type} [NormedAddCommGroup DP] [NormedSpace ℝ DP] [NormedAddCommGroup DS] [NormedSpace ℝ DS] {IP : Type u_1} {KP : Type u_2} {IS : Type u_3} {KS : Type u_4} (D : CycleInputs h DP IP KP DS IS KS) (κ : ℝ) : Prop

Cycle k contributes physical stage k+1. These are native exponent and chart-degree comparisons, not physical estimates.

• particularPotential (k : ℕ) : ActualIterationLedger.waveNative κ (k + 1) ≤ (D.particularPotential k).alpha
• particularPotentialShift (k : ℕ) : -h ≤ (D.particularPotential k).shift
• signedPotential (k : ℕ) : ActualIterationLedger.waveNative κ (k + 1) ≤ (D.signedPotential k).alpha
• signedPotentialShift (k : ℕ) : -h ≤ (D.signedPotential k).shift
• temporal (k : ℕ) : ActualIterationLedger.meanNative κ (k + 1) ≤ (D.temporal k).alpha
• rank (k : ℕ) : ActualIterationLedger.meanNative κ (k + 1) ≤ (D.rank k).alpha
• angular (k : ℕ) : ActualIterationLedger.meanNative κ (k + 1) ≤ (D.angular k).alpha
• particularPressure (k : ℕ) : ActualIterationLedger.wavePressureNative κ (k + 1) ≤ (D.particularPressure k).alpha
• particularPressureShift (k : ℕ) : -(2 * CoordinateAlgebra.A h) ≤ (D.particularPressure k).shift
• signedPressure (k : ℕ) : ActualIterationLedger.wavePressureNative κ (k + 1) ≤ (D.signedPressure k).alpha
• signedPressureShift (k : ℕ) : -(2 * CoordinateAlgebra.A h) ≤ (D.signedPressure k).shift
• pressure (k : ℕ) : ActualIterationLedger.meanNative κ (k + 1) ≤ (D.pressure k).alpha

structure NavierStokes.ActualPhysicalStageBounds.CycleInputs.ValidScale {h : ℝ} {DP DS : Type} [NormedAddCommGroup DP] [NormedSpace ℝ DP] [NormedAddCommGroup DS] [NormedSpace ℝ DS] {IP : Type u_1} {KP : Type u_2} {IS : Type u_3} {KS : Type u_4} (D : CycleInputs h DP IP KP DS IS KS) (qbig : ℝ) : Prop

Valid scale data, collecting temporal, rank, angular, pressure.

• temporal (k : ℕ) : qbig ≤ ChartScales.Q (D.temporal k).firstBand
• rank (k : ℕ) : qbig ≤ ChartScales.Q (D.rank k).firstBand
• angular (k : ℕ) : qbig ≤ ChartScales.Q (D.angular k).firstBand
• pressure (k : ℕ) : qbig ≤ ChartScales.Q (D.pressure k).firstBand

theorem NavierStokes.ActualPhysicalStageBounds.CycleInputs.potential_bound {h κ qbig : ℝ} {DP DS : Type} [NormedAddCommGroup DP] [NormedSpace ℝ DP] [NormedAddCommGroup DS] [NormedSpace ℝ DS] {IP : Type u_1} {KP : Type u_2} {IS : Type u_3} {KS : Type u_4} (D : CycleInputs h DP IP KP DS IS KS) (H : D.Metadata κ) (Q : D.ValidScale qbig) (hh : 0 < h) (hh1 : h < 1 / 2) (hκ : κ ≤ 1 / 100000) (k m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ w ∈ CutStageEstimates.physicalSublevel h qbig, PhysicalWaveSum.physicalQ h w ≤ 1 → ‖iteratedFDeriv ℝ m (D.potential k) w‖ ≤ C * PhysicalWaveSum.physicalQ h w ^ (ActualIterationLedger.gain h (k + 1) - PhysicalStageBounds.potentialLoss h h 0 m)

theorem NavierStokes.ActualPhysicalStageBounds.CycleInputs.direct_bound {h κ qbig : ℝ} {DP DS : Type} [NormedAddCommGroup DP] [NormedSpace ℝ DP] [NormedAddCommGroup DS] [NormedSpace ℝ DS] {IP : Type u_1} {KP : Type u_2} {IS : Type u_3} {KS : Type u_4} (D : CycleInputs h DP IP KP DS IS KS) (H : D.Metadata κ) (Q : D.ValidScale qbig) (hh : 0 < h) (hh1 : h < 1 / 2) (hκ : κ ≤ 1 / 100000) (k m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ w ∈ CutStageEstimates.physicalSublevel h qbig, PhysicalWaveSum.physicalQ h w ≤ 1 → ‖iteratedFDeriv ℝ m (D.direct k) w‖ ≤ C * PhysicalWaveSum.physicalQ h w ^ (ActualIterationLedger.gain h (k + 1) - PhysicalStageBounds.directLoss h 0 m)

theorem NavierStokes.ActualPhysicalStageBounds.CycleInputs.pressure_bound {h κ qbig : ℝ} {DP DS : Type} [NormedAddCommGroup DP] [NormedSpace ℝ DP] [NormedAddCommGroup DS] [NormedSpace ℝ DS] {IP : Type u_1} {KP : Type u_2} {IS : Type u_3} {KS : Type u_4} (D : CycleInputs h DP IP KP DS IS KS) (H : D.Metadata κ) (Q : D.ValidScale qbig) (hh : 0 < h) (hh1 : h < 1 / 2) (hκ : κ ≤ 1 / 100000) (k m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ w ∈ CutStageEstimates.physicalSublevel h qbig, PhysicalWaveSum.physicalQ h w ≤ 1 → ‖iteratedFDeriv ℝ m (D.pressureField k) w‖ ≤ C * PhysicalWaveSum.physicalQ h w ^ (ActualIterationLedger.gain h (k + 1) - PhysicalStageBounds.pressureLoss h (2 * CoordinateAlgebra.A h) 0 m)

theorem NavierStokes.ActualPhysicalStageBounds.CycleInputs.potential_smooth {h qbig : ℝ} {DP DS : Type} [NormedAddCommGroup DP] [NormedSpace ℝ DP] [NormedAddCommGroup DS] [NormedSpace ℝ DS] {IP : Type u_1} {KP : Type u_2} {IS : Type u_3} {KS : Type u_4} (D : CycleInputs h DP IP KP DS IS KS) (Q : D.ValidScale qbig) (hh : 0 < h) (hh1 : h < 1 / 2) (k : ℕ) : ContDiffOn ℝ (↑⊤) (D.potential k) (CutStageEstimates.physicalSublevel h qbig)

theorem NavierStokes.ActualPhysicalStageBounds.CycleInputs.direct_smooth {h qbig : ℝ} {DP DS : Type} [NormedAddCommGroup DP] [NormedSpace ℝ DP] [NormedAddCommGroup DS] [NormedSpace ℝ DS] {IP : Type u_1} {KP : Type u_2} {IS : Type u_3} {KS : Type u_4} (D : CycleInputs h DP IP KP DS IS KS) (Q : D.ValidScale qbig) (hh : 0 < h) (hh1 : h < 1 / 2) (k : ℕ) : ContDiffOn ℝ (↑⊤) (D.direct k) (CutStageEstimates.physicalSublevel h qbig)

theorem NavierStokes.ActualPhysicalStageBounds.CycleInputs.pressure_smooth {h qbig : ℝ} {DP DS : Type} [NormedAddCommGroup DP] [NormedSpace ℝ DP] [NormedAddCommGroup DS] [NormedSpace ℝ DS] {IP : Type u_1} {KP : Type u_2} {IS : Type u_3} {KS : Type u_4} (D : CycleInputs h DP IP KP DS IS KS) (Q : D.ValidScale qbig) (hh : 0 < h) (hh1 : h < 1 / 2) (k : ℕ) : ContDiffOn ℝ (↑⊤) (D.pressureField k) (CutStageEstimates.physicalSublevel h qbig)

theorem NavierStokes.ActualPhysicalStageBounds.bound_congr {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {h qbig : ℝ} {f g : ProblemStatement.SpaceTime → V} {m : ℕ} {r : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (he : Set.EqOn f g (CutStageEstimates.physicalSublevel h qbig)) (hb : ∃ (C : ℝ), 0 ≤ C ∧ ∀ w ∈ CutStageEstimates.physicalSublevel h qbig, PhysicalWaveSum.physicalQ h w ≤ 1 → ‖iteratedFDeriv ℝ m f w‖ ≤ C * PhysicalWaveSum.physicalQ h w ^ r) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ w ∈ CutStageEstimates.physicalSublevel h qbig, PhysicalWaveSum.physicalQ h w ≤ 1 → ‖iteratedFDeriv ℝ m g w‖ ≤ C * PhysicalWaveSum.physicalQ h w ^ r

theorem NavierStokes.ActualPhysicalStageBounds.raw_of_positive_bounds {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {h qbig : ℝ} {F : ℕ → ProblemStatement.SpaceTime → V} {gain L : ℕ → ℝ} (hb : ∀ (k m : ℕ), ∃ (C : ℝ), 0 ≤ C ∧ ∀ w ∈ CutStageEstimates.physicalSublevel h qbig, PhysicalWaveSum.physicalQ h w ≤ 1 → ‖iteratedFDeriv ℝ m (F (k + 1)) w‖ ≤ C * PhysicalWaveSum.physicalQ h w ^ (gain (k + 1) - L m)) : ∃ (C : ℕ → ℕ → ℝ), (∀ (j m : ℕ), 0 ≤ C j m) ∧ CutStageEstimates.RawStageBounds (PhysicalWaveSum.physicalQ h) F gain L C (fun (x x_1 : ℕ) => 0) (PhysicalWaveSum.preterminal ∩ CutStageEstimates.physicalSublevel h qbig)

theorem NavierStokes.ActualPhysicalStageBounds.CycleInputs.represented_raw_bounds {h κ qbig : ℝ} {DP DS : Type} [NormedAddCommGroup DP] [NormedSpace ℝ DP] [NormedAddCommGroup DS] [NormedSpace ℝ DS] {IP : Type u_1} {KP : Type u_2} {IS : Type u_3} {KS : Type u_4} (D : CycleInputs h DP IP KP DS IS KS) (H : D.Metadata κ) (Q : D.ValidScale qbig) (hh : 0 < h) (hh1 : h < 1 / 2) (hκ : κ ≤ 1 / 100000) (A B : ℕ → ProblemStatement.VelocityField) (P : ℕ → ProblemStatement.PressureField) (hA : ∀ (k : ℕ), Set.EqOn (D.potential k) (A (k + 1)) (CutStageEstimates.physicalSublevel h qbig)) (hB : ∀ (k : ℕ), Set.EqOn (D.direct k) (B (k + 1)) (CutStageEstimates.physicalSublevel h qbig)) (hP : ∀ (k : ℕ), Set.EqOn (D.pressureField k) (P (k + 1)) (CutStageEstimates.physicalSublevel h qbig)) : ∃ (CA : ℕ → ℕ → ℝ) (CB : ℕ → ℕ → ℝ) (CP : ℕ → ℕ → ℝ), (∀ (j m : ℕ), 0 ≤ CA j m ∧ 0 ≤ CB j m ∧ 0 ≤ CP j m) ∧ CutStageEstimates.RawStageBounds (PhysicalWaveSum.physicalQ h) A (ActualIterationLedger.gain h) (PhysicalStageBounds.potentialLoss h h 0) CA (fun (x x_1 : ℕ) => 0) (PhysicalWaveSum.preterminal ∩ CutStageEstimates.physicalSublevel h qbig) ∧ CutStageEstimates.RawStageBounds (PhysicalWaveSum.physicalQ h) B (ActualIterationLedger.gain h) (PhysicalStageBounds.directLoss h 0) CB (fun (x x_1 : ℕ) => 0) (PhysicalWaveSum.preterminal ∩ CutStageEstimates.physicalSublevel h qbig) ∧ CutStageEstimates.RawStageBounds (PhysicalWaveSum.physicalQ h) P (ActualIterationLedger.gain h) (PhysicalStageBounds.pressureLoss h (2 * CoordinateAlgebra.A h) 0) CP (fun (x x_1 : ℕ) => 0) (PhysicalWaveSum.preterminal ∩ CutStageEstimates.physicalSublevel h qbig)

Literal sequence identities transfer the derived estimates to the actual potential/direct/pressure stages. Index zero is deliberately absent.

Initialization on the true native mean domain

noncomputable def NavierStokes.ActualPhysicalStageBounds.initialIncrement {h : ℝ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (W : PhysicalStageBounds.WaveData h D I K (Fin 3)) (MT MR : MeanInput h (CoordinateAlgebra.A h - 1 / 2)) : ProblemStatement.VelocityField

Initial increment, defined pointwise by W.vector w + MT.family.angularField w + MR.family.angularField w.

Equations

• NavierStokes.ActualPhysicalStageBounds.initialIncrement W MT MR w = W.vector w + MT.family.angularField w + MR.family.angularField w

theorem NavierStokes.ActualPhysicalStageBounds.initialIncrement_smooth {h : ℝ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (W : PhysicalStageBounds.WaveData h D I K (Fin 3)) (MT MR : MeanInput h (CoordinateAlgebra.A h - 1 / 2)) (hh : 0 < h) (hh1 : h < 1 / 2) {qbig : ℝ} (hqT : qbig ≤ ChartScales.Q MT.firstBand) (hqR : qbig ≤ ChartScales.Q MR.firstBand) : ContDiffOn ℝ (↑⊤) (initialIncrement W MT MR) (CutStageEstimates.physicalSublevel h qbig)

theorem NavierStokes.ActualPhysicalStageBounds.initialIncrement_bound {h : ℝ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (W : PhysicalStageBounds.WaveData h D I K (Fin 3)) (MT MR : MeanInput h (CoordinateAlgebra.A h - 1 / 2)) (hh : 0 < h) (hh1 : h < 1 / 2) {qbig : ℝ} (hqT : qbig ≤ ChartScales.Q MT.firstBand) (hqR : qbig ≤ ChartScales.Q MR.firstBand) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ w ∈ CutStageEstimates.physicalSublevel h qbig, PhysicalWaveSum.physicalQ h w ≤ 1 → ‖iteratedFDeriv ℝ m (initialIncrement W MT MR) w‖ ≤ C * PhysicalWaveSum.physicalQ h w ^ (-InitializedPhysicalBackground.seedPotentialLoss h W.alpha W.shift (min MT.alpha MR.alpha) m)

theorem NavierStokes.ActualPhysicalStageBounds.initialIncrement_rate {h : ℝ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (W : PhysicalStageBounds.WaveData h D I K (Fin 3)) (MT MR : MeanInput h (CoordinateAlgebra.A h - 1 / 2)) (hh : 0 < h) (hh1 : h < 1 / 2) {qbig : ℝ} (hqbig : 0 < qbig) (hqT : qbig ≤ ChartScales.Q MT.firstBand) (hqR : qbig ≤ ChartScales.Q MR.firstBand) (m : ℕ) : DiagonalResidual.JetRate ActualBaseVelocityBounds.endpoint (PhysicalWaveSum.physicalQ h) (initialIncrement W MT MR) m (-InitializedPhysicalBackground.seedPotentialLoss h W.alpha W.shift (min MT.alpha MR.alpha) m)

noncomputable def NavierStokes.ActualPhysicalStageBounds.initialPressureIncrement {h : ℝ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (W : PhysicalStageBounds.WaveData h D I K Unit) (M : MeanInput h (2 * CoordinateAlgebra.A h)) : ProblemStatement.PressureField

The finite pressure inserted at initialization, apart from the actual base pressure. Both terms retain their original native class exponents.

Equations

• NavierStokes.ActualPhysicalStageBounds.initialPressureIncrement W M w = W.pressure w + M.family.field w

noncomputable def NavierStokes.ActualPhysicalStageBounds.initialPressureLoss (h waveAlpha waveShift meanAlpha : ℝ) (m : ℕ) : ℝ

Initial pressure loss, given by PhysicalStageBounds.pressureLoss h (-(h * waveAlpha + waveShift)) (-(h * meanAlpha)) m.

Equations

• NavierStokes.ActualPhysicalStageBounds.initialPressureLoss h waveAlpha waveShift meanAlpha m = NavierStokes.PhysicalStageBounds.pressureLoss h (-(h * waveAlpha + waveShift)) (-(h * meanAlpha)) m

theorem NavierStokes.ActualPhysicalStageBounds.initialPressureIncrement_smooth {h : ℝ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (W : PhysicalStageBounds.WaveData h D I K Unit) (M : MeanInput h (2 * CoordinateAlgebra.A h)) (hh : 0 < h) (hh1 : h < 1 / 2) {qbig : ℝ} (hq : qbig ≤ ChartScales.Q M.firstBand) : ContDiffOn ℝ (↑⊤) (initialPressureIncrement W M) (CutStageEstimates.physicalSublevel h qbig)

theorem NavierStokes.ActualPhysicalStageBounds.initialPressureIncrement_bound {h : ℝ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (W : PhysicalStageBounds.WaveData h D I K Unit) (M : MeanInput h (2 * CoordinateAlgebra.A h)) (hh : 0 < h) (hh1 : h < 1 / 2) {qbig : ℝ} (hq : qbig ≤ ChartScales.Q M.firstBand) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ w ∈ CutStageEstimates.physicalSublevel h qbig, PhysicalWaveSum.physicalQ h w ≤ 1 → ‖iteratedFDeriv ℝ m (initialPressureIncrement W M) w‖ ≤ C * PhysicalWaveSum.physicalQ h w ^ (-initialPressureLoss h W.alpha W.shift M.alpha m)

theorem NavierStokes.ActualPhysicalStageBounds.initialPressureIncrement_rate {h : ℝ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (W : PhysicalStageBounds.WaveData h D I K Unit) (M : MeanInput h (2 * CoordinateAlgebra.A h)) (hh : 0 < h) (hh1 : h < 1 / 2) {qbig : ℝ} (hqbig : 0 < qbig) (hq : qbig ≤ ChartScales.Q M.firstBand) (m : ℕ) : DiagonalResidual.JetRate ActualBaseVelocityBounds.endpoint (PhysicalWaveSum.physicalQ h) (initialPressureIncrement W M) m (-initialPressureLoss h W.alpha W.shift M.alpha m)

theorem NavierStokes.ActualPhysicalStageBounds.initialDirect_rate {h : ℝ} (MB : MeanInput h (CoordinateAlgebra.A h)) (hh : 0 < h) (hh1 : h < 1 / 2) {qbig : ℝ} (hqbig : 0 < qbig) (hq : qbig ≤ ChartScales.Q MB.firstBand) (m : ℕ) : DiagonalResidual.JetRate ActualBaseVelocityBounds.endpoint (PhysicalWaveSum.physicalQ h) MB.family.angularField m (-InitializedPhysicalBackground.seedDirectLoss h MB.alpha m)

noncomputable def NavierStokes.ActualPhysicalStageBounds.initialPotential {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (upper : ℝ) (B : ℕ) (WA : PhysicalStageBounds.WaveData F.data.h D I K (Fin 3)) (MT MR : MeanInput F.data.h (CoordinateAlgebra.A F.data.h - 1 / 2)) : ProblemStatement.VelocityField

Initial potential, defined pointwise by TailGaugePotential.finalPotential H v upper B w + initialIncrement WA MT MR w.

Equations

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

noncomputable def NavierStokes.ActualPhysicalStageBounds.initialVelocity {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (upper : ℝ) (B : ℕ) (WA : PhysicalStageBounds.WaveData F.data.h D I K (Fin 3)) (MT MR : MeanInput F.data.h (CoordinateAlgebra.A F.data.h - 1 / 2)) (MB : MeanInput F.data.h (CoordinateAlgebra.A F.data.h)) : ProblemStatement.VelocityField

Initial velocity, defined pointwise by SpatialCurl.spatialCurl (initialPotential H v upper B WA MT MR) w + MB.family.angularField w.

Equations

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

theorem NavierStokes.ActualPhysicalStageBounds.initialPotential_smooth {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (upper : ℝ) (B : ℕ) (WA : PhysicalStageBounds.WaveData F.data.h D I K (Fin 3)) (MT MR : MeanInput F.data.h (CoordinateAlgebra.A F.data.h - 1 / 2)) {qbig : ℝ} (hqT : qbig ≤ ChartScales.Q MT.firstBand) (hqR : qbig ≤ ChartScales.Q MR.firstBand) : ContDiffOn ℝ (↑⊤) (initialPotential H v upper B WA MT MR) (CutStageEstimates.physicalSublevel F.data.h qbig)

theorem NavierStokes.ActualPhysicalStageBounds.initialVelocity_decomposition {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (upper : ℝ) (B : ℕ) (WA : PhysicalStageBounds.WaveData F.data.h D I K (Fin 3)) (MT MR : MeanInput F.data.h (CoordinateAlgebra.A F.data.h - 1 / 2)) (MB : MeanInput F.data.h (CoordinateAlgebra.A F.data.h)) {qbig : ℝ} (hqT : qbig ≤ ChartScales.Q MT.firstBand) (hqR : qbig ≤ ChartScales.Q MR.firstBand) : Set.EqOn (initialVelocity H v upper B WA MT MR MB) (fun (w : ProblemStatement.SpaceTime) => FinalSlowBase.velocity H v upper B w + SpatialCurl.spatialCurl (initialIncrement WA MT MR) w + MB.family.angularField w) (CutStageEstimates.physicalSublevel F.data.h qbig)

theorem NavierStokes.ActualPhysicalStageBounds.initialVelocity_rate {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (upper : ℝ) (B : ℕ) (WA : PhysicalStageBounds.WaveData F.data.h D I K (Fin 3)) (MT MR : MeanInput F.data.h (CoordinateAlgebra.A F.data.h - 1 / 2)) (MB : MeanInput F.data.h (CoordinateAlgebra.A F.data.h)) (m : ℕ) : DiagonalResidual.JetRate ActualBaseVelocityBounds.endpoint (PhysicalWaveSum.physicalQ F.data.h) (initialVelocity H v upper B WA MT MR MB) m (-InitializedPhysicalBackground.initialLoss F.data.h WA.alpha WA.shift (min MT.alpha MR.alpha) MB.alpha m)

The true-domain initialization has the same fixed loss as the prior physical-background calculation, using the minimum of the two stream classes.

theorem NavierStokes.ActualPhysicalStageBounds.represented_initial_rate {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (upper : ℝ) (B : ℕ) (WA : PhysicalStageBounds.WaveData F.data.h D I K (Fin 3)) (MT MR : MeanInput F.data.h (CoordinateAlgebra.A F.data.h - 1 / 2)) (MB : MeanInput F.data.h (CoordinateAlgebra.A F.data.h)) {A Bdirect : ℕ → ProblemStatement.VelocityField} {U : Set ProblemStatement.SpaceTime} (hU : IsOpen U) (hlU : ∀ᶠ (w : ProblemStatement.SpaceTime) in ActualBaseVelocityBounds.endpoint, w ∈ U) (hA : Set.EqOn (A 0) (initialPotential H v upper B WA MT MR) U) (hB : Set.EqOn (Bdirect 0) MB.family.angularField U) (m : ℕ) : DiagonalResidual.JetRate ActualBaseVelocityBounds.endpoint (PhysicalWaveSum.physicalQ F.data.h) (MixedDiagonalResidual.uncutVelocity A Bdirect 0) m (-InitializedPhysicalBackground.initialLoss F.data.h WA.alpha WA.shift (min MT.alpha MR.alpha) MB.alpha m)

theorem NavierStokes.ActualPhysicalStageBounds.background_from_representations {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} {DP DS : Type} [NormedAddCommGroup DP] [NormedSpace ℝ DP] [NormedAddCommGroup DS] [NormedSpace ℝ DS] {IP : Type u_3} {KP : Type u_4} {IS : Type u_5} {KS : Type u_6} (Cyc : CycleInputs F.data.h DP IP KP DS IS KS) {κ qbig : ℝ} (HM : Cyc.Metadata κ) (HQ : Cyc.ValidScale qbig) (hκ : κ ≤ 1 / 100000) (hqbig : 0 < qbig) (upper : ℝ) (bandFloor : ℕ) (WA : PhysicalStageBounds.WaveData F.data.h D I K (Fin 3)) (MT MR : MeanInput F.data.h (CoordinateAlgebra.A F.data.h - 1 / 2)) (MB : MeanInput F.data.h (CoordinateAlgebra.A F.data.h)) (hqT : qbig ≤ ChartScales.Q MT.firstBand) (hqR : qbig ≤ ChartScales.Q MR.firstBand) (hqB : qbig ≤ ChartScales.Q MB.firstBand) (A B : ℕ → ProblemStatement.VelocityField) (hA0 : Set.EqOn (A 0) (initialPotential H v upper bandFloor WA MT MR) (CutStageEstimates.physicalSublevel F.data.h qbig)) (hB0 : Set.EqOn (B 0) MB.family.angularField (CutStageEstimates.physicalSublevel F.data.h qbig)) (hA : ∀ (k : ℕ), Set.EqOn (Cyc.potential k) (A (k + 1)) (CutStageEstimates.physicalSublevel F.data.h qbig)) (hB : ∀ (k : ℕ), Set.EqOn (Cyc.direct k) (B (k + 1)) (CutStageEstimates.physicalSublevel F.data.h qbig)) (J m : ℕ) : DiagonalResidual.JetRate ActualBaseVelocityBounds.endpoint (PhysicalWaveSum.physicalQ F.data.h) (MixedDiagonalResidual.uncutVelocity A B J) m (-MixedFiniteBackground.initialBackgroundLoss (InitializedPhysicalBackground.initialLoss F.data.h WA.alpha WA.shift (min MT.alpha MR.alpha) MB.alpha) (PhysicalStageBounds.potentialLoss F.data.h F.data.h 0) (PhysicalStageBounds.directLoss F.data.h 0) m)

The finite-background consumer now uses only native wave/mean data on the true domain, plus exact initial and positive-stage identities.

Literal candidate sequence interface

theorem NavierStokes.ActualPhysicalStageBounds.candidate_raw_bounds {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {DP DS : Type} [NormedAddCommGroup DP] [NormedSpace ℝ DP] [NormedAddCommGroup DS] [NormedSpace ℝ DS] {IP : Type u_1} {KP : Type u_2} {IS : Type u_3} {KS : Type u_4} (Cyc : CycleInputs F.data.h DP IP KP DS IS KS) {κ qbig : ℝ} (HM : Cyc.Metadata κ) (HQ : Cyc.ValidScale qbig) (hκ : κ ≤ 1 / 100000) (upper : ℝ) (bandFloor : ℕ) (initial : MixedAxisPreservation.PotentialStage F.data.h (MixedAxisPreservation.localDomain F.data.h qbig)) (stages : ℕ → MixedAxisPreservation.PotentialStage F.data.h (MixedAxisPreservation.localDomain F.data.h qbig)) (angular : ℕ → DirectAngularDiagonal.AngularData (LocalAngularDiagonal.localSlowDomain F.data.h qbig)) (pInitial : ProblemStatement.PressureField) (pStages : ℕ → ProblemStatement.PressureField) (hA : ∀ (k : ℕ), Set.EqOn (Cyc.potential k) (stages k).field (CutStageEstimates.physicalSublevel F.data.h qbig)) (hB : ∀ (k : ℕ), Set.EqOn (Cyc.direct k) (LocalAngularDiagonal.rawSeries angular (k + 1)) (CutStageEstimates.physicalSublevel F.data.h qbig)) (hP : ∀ (k : ℕ), Set.EqOn (Cyc.pressureField k) (pStages k) (CutStageEstimates.physicalSublevel F.data.h qbig)) : ∃ (CA : ℕ → ℕ → ℝ) (CB : ℕ → ℕ → ℝ) (CP : ℕ → ℕ → ℝ), (∀ (j m : ℕ), 0 ≤ CA j m ∧ 0 ≤ CB j m ∧ 0 ≤ CP j m) ∧ CutStageEstimates.RawStageBounds (PhysicalWaveSum.physicalQ F.data.h) (MixedCandidateAssembly.potentialStages H v upper bandFloor initial stages) (ActualIterationLedger.gain F.data.h) (PhysicalStageBounds.potentialLoss F.data.h F.data.h 0) CA (fun (x x_1 : ℕ) => 0) (PhysicalWaveSum.preterminal ∩ CutStageEstimates.physicalSublevel F.data.h qbig) ∧ CutStageEstimates.RawStageBounds (PhysicalWaveSum.physicalQ F.data.h) (LocalAngularDiagonal.rawSeries angular) (ActualIterationLedger.gain F.data.h) (PhysicalStageBounds.directLoss F.data.h 0) CB (fun (x x_1 : ℕ) => 0) (PhysicalWaveSum.preterminal ∩ CutStageEstimates.physicalSublevel F.data.h qbig) ∧ CutStageEstimates.RawStageBounds (PhysicalWaveSum.physicalQ F.data.h) (MixedCandidateAssembly.pressureStages H v upper bandFloor pInitial pStages) (ActualIterationLedger.gain F.data.h) (PhysicalStageBounds.pressureLoss F.data.h (2 * CoordinateAlgebra.A F.data.h) 0) CP (fun (x x_1 : ℕ) => 0) (PhysicalWaveSum.preterminal ∩ CutStageEstimates.physicalSublevel F.data.h qbig)

Quantitative bounds for the actual MCA/MAS indexing convention. The remaining representations concern the literal component fields.

Adapters for the constructed native mean families

noncomputable def NavierStokes.ActualPhysicalStageBounds.actualInitialTemporalInput (B N0 N : ℕ) (hN : 4 ≤ N) : MeanInput CorrectionInitialization.ActualPrimary.h (CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h - 1 / 2)

The constructed initialization families, with their proved native classes and common band choice. No native estimate is left as an input.

Equations

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

noncomputable def NavierStokes.ActualPhysicalStageBounds.actualInitialRankInput (B N0 N : ℕ) (hN : 4 ≤ N) : MeanInput CorrectionInitialization.ActualPrimary.h (CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h - 1 / 2)

Actual initial rank input, constructed using MeanInput.ofMoving.

Equations

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

noncomputable def NavierStokes.ActualPhysicalStageBounds.actualInitialAngularInput (B N0 N : ℕ) (hN : 4 ≤ N) : MeanInput CorrectionInitialization.ActualPrimary.h (CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h)

Actual initial angular input, constructed using MeanInput.ofMoving.

Equations

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

noncomputable def NavierStokes.ActualPhysicalStageBounds.actualInitialPressureInput (B N0 N : ℕ) (hN : 4 ≤ N) : MeanInput CorrectionInitialization.ActualPrimary.h (2 * CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h)

Actual initial pressure input, constructed using MeanInput.ofMoving.

Equations

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

@[simp]

theorem NavierStokes.ActualPhysicalStageBounds.actualInitialTemporalInput_family (B N0 N : ℕ) (hN : 4 ≤ N) : (actualInitialTemporalInput B N0 N hN).family = ActualMeanPhysicalData.initialTemporalFamily B N0 N

@[simp]

theorem NavierStokes.ActualPhysicalStageBounds.actualInitialRankInput_family (B N0 N : ℕ) (hN : 4 ≤ N) : (actualInitialRankInput B N0 N hN).family = ActualMeanPhysicalData.initialRankFamily B N0 N

@[simp]

theorem NavierStokes.ActualPhysicalStageBounds.actualInitialAngularInput_family (B N0 N : ℕ) (hN : 4 ≤ N) : (actualInitialAngularInput B N0 N hN).family = ActualMeanPhysicalData.initialAngularFamily B N0 N

@[simp]

theorem NavierStokes.ActualPhysicalStageBounds.actualInitialPressureInput_family (B N0 N : ℕ) (hN : 4 ≤ N) : (actualInitialPressureInput B N0 N hN).family = ActualMeanPhysicalData.initialPressureFamily B N0 N

theorem NavierStokes.ActualPhysicalStageBounds.actualInitialVelocity_rate {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (B N0 N : ℕ) (hN : 4 ≤ N) (WA : PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h D I K (Fin 3)) (m : ℕ) : DiagonalResidual.JetRate ActualBaseVelocityBounds.endpoint (PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h) (initialVelocity CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation CorrectionInitialization.ActualPrimary.upper B WA (actualInitialTemporalInput B N0 N hN) (actualInitialRankInput B N0 N hN) (actualInitialAngularInput B N0 N hN)) m (-InitializedPhysicalBackground.initialLoss CorrectionInitialization.ActualPrimary.h WA.alpha WA.shift (1 - ChartScales.kappa) (9 / 10) m)

The actual initialized velocity, with its actual initial temporal, rank, and direct angular families. Only the primary wave representation is supplied by the separate physical-copy construction.

noncomputable def NavierStokes.ActualPhysicalStageBounds.actualCycleTemporalInput {B N0 N : ℕ} {p : ℕ → CorrectionStep.CycleParameters (ActualInitialization.Index B N0)} (H : ActualMeanPhysicalData.InitialCycleInput B N0 N p) (j : ℕ) (hN : 4 ≤ N) {α : ℝ} (HC : WeightedClasses.MeanClass ActualInitialMean.strip α (((p j).afterSigned (CorrectionStep.CycleState.iterate p (CorrectionInitialization.ActualPrimary.commonContext B) (ActualInitialization.initialCycleState B N0) j).coefficients (CorrectionInitialization.ActualPrimary.commonContext B) (CorrectionStep.CycleState.iterate p (CorrectionInitialization.ActualPrimary.commonContext B) (ActualInitialization.initialCycleState B N0) j).state).axialResidual (CorrectionInitialization.ActualPrimary.commonContext B))) : MeanInput CorrectionInitialization.ActualPrimary.h (CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h - 1 / 2)

These four cycle adapters retain the literal families of the actual iterate. Their quantitative hypotheses are native source, debt, or mean classes; physical derivative bounds are conclusions of the earlier API.

Equations

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

noncomputable def NavierStokes.ActualPhysicalStageBounds.actualCycleRankInput {B N0 N : ℕ} {p : ℕ → CorrectionStep.CycleParameters (ActualInitialization.Index B N0)} (H : ActualMeanPhysicalData.InitialCycleInput B N0 N p) (j : ℕ) (hN : 4 ≤ N) {α : ℝ} (HC : WeightedClasses.UnweightedClass ActualInitialMean.slowStrip α (CorrectionState.debt (CorrectionInitialization.ActualPrimary.commonContext B) ((p j).afterTemporal (CorrectionStep.CycleState.iterate p (CorrectionInitialization.ActualPrimary.commonContext B) (ActualInitialization.initialCycleState B N0) j).coefficients (CorrectionInitialization.ActualPrimary.commonContext B) (CorrectionStep.CycleState.iterate p (CorrectionInitialization.ActualPrimary.commonContext B) (ActualInitialization.initialCycleState B N0) j).state))) : MeanInput CorrectionInitialization.ActualPrimary.h (CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h - 1 / 2)

Actual cycle rank input, constructed using MeanInput.ofMoving.

Equations

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

noncomputable def NavierStokes.ActualPhysicalStageBounds.actualCycleAngularInput {B N0 N : ℕ} {p : ℕ → CorrectionStep.CycleParameters (ActualInitialization.Index B N0)} (H : ActualMeanPhysicalData.InitialCycleInput B N0 N p) (j : ℕ) (hN : 4 ≤ N) {α : ℝ} (HT : MeanIncrementBounds.IncrementBounds ActualInitialMean.strip α ((p j).temporalIncrement (CorrectionStep.CycleState.iterate p (CorrectionInitialization.ActualPrimary.commonContext B) (ActualInitialization.initialCycleState B N0) j).coefficients (CorrectionInitialization.ActualPrimary.commonContext B) (CorrectionStep.CycleState.iterate p (CorrectionInitialization.ActualPrimary.commonContext B) (ActualInitialization.initialCycleState B N0) j).state)) (HR : MeanIncrementBounds.IncrementBounds ActualInitialMean.strip α ((p j).rankIncrement (CorrectionStep.CycleState.iterate p (CorrectionInitialization.ActualPrimary.commonContext B) (ActualInitialization.initialCycleState B N0) j).coefficients (CorrectionInitialization.ActualPrimary.commonContext B) (CorrectionStep.CycleState.iterate p (CorrectionInitialization.ActualPrimary.commonContext B) (ActualInitialization.initialCycleState B N0) j).state)) : MeanInput CorrectionInitialization.ActualPrimary.h (CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h)

Actual cycle angular input, constructed using MeanInput.ofMoving.

Equations

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

noncomputable def NavierStokes.ActualPhysicalStageBounds.actualCyclePressureInput {B N0 N : ℕ} {p : ℕ → CorrectionStep.CycleParameters (ActualInitialization.Index B N0)} (H : ActualMeanPhysicalData.InitialCycleInput B N0 N p) (j : ℕ) (hN : 4 ≤ N) {α : ℝ} (HC : WeightedClasses.MeanClass ActualInitialMean.strip α ((CorrectionStep.CycleState.iterate p (CorrectionInitialization.ActualPrimary.commonContext B) (ActualInitialization.initialCycleState B N0) (j + 1)).state.pressure - (CorrectionStep.CycleState.iterate p (CorrectionInitialization.ActualPrimary.commonContext B) (ActualInitialization.initialCycleState B N0) j).state.pressure)) : MeanInput CorrectionInitialization.ActualPrimary.h (2 * CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h)

Actual cycle pressure input as an element of MeanInput h (2 * CoordinateAlgebra.A h).

Equations

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