Actual defect changes under the slow rank update

The pressure, angular flux, and axial flux defects are actual torus/radial moments. Their linear changes are precisely the last three rows of (35). The remaining terms include the complete radial-source remainder of (32).

@[reducible, inline]

abbrev NavierStokes.DefectIncrementBounds.Point (P : Type) : Type

Point: an abbreviation for PressureStream.Lift P.

Equations

• NavierStokes.DefectIncrementBounds.Point P = NavierStokes.PressureStream.Lift P

@[reducible, inline]

abbrev NavierStokes.DefectIncrementBounds.ScalarField (D : Type) : Type

Scalar field: an abbreviation for MeanIncrementBounds.Field D.

Equations

• NavierStokes.DefectIncrementBounds.ScalarField D = NavierStokes.MeanIncrementBounds.Field D

noncomputable def NavierStokes.DefectIncrementBounds.positiveDomain {P : Type} : Set (Point P)

Positive domain, given by {x | 0 < x.1}.

Equations

• NavierStokes.DefectIncrementBounds.positiveDomain = {x : NavierStokes.DefectIncrementBounds.Point P | 0 < x.1}

theorem NavierStokes.DefectIncrementBounds.positiveDomain_open {P : Type} [NormedAddCommGroup P] : IsOpen positiveDomain

structure NavierStokes.DefectIncrementBounds.Shell {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (a b : ℝ) (f : ScalarField (Point P)) : Prop

Global smooth zero extension with a fixed radial support shell.

• smooth (n : ℕ) : ContDiff ℝ (↑⊤) (f n)
• supported (n : ℕ) : RadialAlias.RadiallySupported a b (f n)

theorem NavierStokes.DefectIncrementBounds.Shell.zero_of_not_mem {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b : ℝ} {f : ScalarField (Point P)} (hf : Shell a b f) (n : ℕ) (x : Point P) (hx : x.1 ∉ Set.Icc a b) : f n x = 0

theorem NavierStokes.DefectIncrementBounds.Shell.zero {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b : ℝ} : Shell a b 0

theorem NavierStokes.DefectIncrementBounds.Shell.add {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b : ℝ} {f g : ScalarField (Point P)} (hf : Shell a b f) (hg : Shell a b g) : Shell a b (f + g)

theorem NavierStokes.DefectIncrementBounds.Shell.neg {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b : ℝ} {f : ScalarField (Point P)} (hf : Shell a b f) : Shell a b (-f)

theorem NavierStokes.DefectIncrementBounds.Shell.sub {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b : ℝ} {f g : ScalarField (Point P)} (hf : Shell a b f) (hg : Shell a b g) : Shell a b (f - g)

theorem NavierStokes.DefectIncrementBounds.Shell.mul {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b : ℝ} {f g : ScalarField (Point P)} (hf : Shell a b f) (hg : Shell a b g) : Shell a b (f * g)

theorem NavierStokes.DefectIncrementBounds.Shell.band_mul {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b : ℝ} {f : ScalarField (Point P)} (hf : Shell a b f) (c : ℕ → ℝ) : Shell a b fun (n : ℕ) (x : Point P) => c n * f n x

theorem NavierStokes.DefectIncrementBounds.Shell.smul {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b : ℝ} {f : ScalarField (Point P)} (hf : Shell a b f) (c : ℝ) : Shell a b (c • f)

theorem NavierStokes.DefectIncrementBounds.Shell.directional {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b : ℝ} {f : ScalarField (Point P)} (hf : Shell a b f) (v : Point P) : Shell a b fun (n : ℕ) (x : Point P) => (fderiv ℝ (f n) x) v

theorem NavierStokes.DefectIncrementBounds.Shell.coefficient_mul {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b : ℝ} {f g : ScalarField (Point P)} (hf : Shell a b f) (ha : 0 < a) (hg : MeanIncrementBounds.SmoothOn positiveDomain g) : Shell a b (g * f)

Coefficients need smoothness only on the physical region R > 0. Near the axis the actual product vanishes because the other factor is supported away from it.

theorem NavierStokes.DefectIncrementBounds.Shell.mul_coefficient {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b : ℝ} {f g : ScalarField (Point P)} (hf : Shell a b f) (ha : 0 < a) (hg : MeanIncrementBounds.SmoothOn positiveDomain g) : Shell a b (f * g)

theorem NavierStokes.DefectIncrementBounds.Shell.smoothOn {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b : ℝ} {f : ScalarField (Point P)} (hf : Shell a b f) (U : Set (Point P)) : MeanIncrementBounds.SmoothOn U f

structure NavierStokes.DefectIncrementBounds.ShellTriple {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (a b : ℝ) (m : MeanIncrementBounds.Triple (Point P)) : Prop

Shell triple data, collecting radial, angular, axial.

• radial : Shell a b m.radial
• angular : Shell a b m.angular
• axial : Shell a b m.axial

theorem NavierStokes.DefectIncrementBounds.ShellTriple.updated {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b : ℝ} {m h : MeanIncrementBounds.Triple (Point P)} (hm : ShellTriple a b m) (hh : ShellTriple a b h) : ShellTriple a b (MeanIncrementBounds.updated m h)

theorem NavierStokes.DefectIncrementBounds.ShellTriple.smooth {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b : ℝ} {m : MeanIncrementBounds.Triple (Point P)} (hm : ShellTriple a b m) (U : Set (Point P)) : MeanIncrementBounds.SmoothTriple U m

structure NavierStokes.DefectIncrementBounds.PositiveOperators {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (o : MeanIncrementBounds.Operators (Point P)) : Prop

The radial chart has its actual radius and a coefficient smooth on the physical positive radial region. No estimate on a residual is assumed.

• radius_eq : o.radius = Prod.fst
• radialProfile : ContDiffOn ℝ (↑⊤) o.radialProfile positiveDomain

theorem NavierStokes.DefectIncrementBounds.PositiveOperators.invRadius_smooth {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {o : MeanIncrementBounds.Operators (Point P)} (ho : PositiveOperators o) : MeanIncrementBounds.SmoothOn positiveDomain o.invRadius

theorem NavierStokes.DefectIncrementBounds.Shell.dr {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b : ℝ} {f : ScalarField (Point P)} {o : MeanIncrementBounds.Operators (Point P)} (hf : Shell a b f) (ha : 0 < a) (ho : PositiveOperators o) : Shell a b (o.dr f)

theorem NavierStokes.DefectIncrementBounds.Shell.dz {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b : ℝ} {f : ScalarField (Point P)} (hf : Shell a b f) (o : MeanIncrementBounds.Operators (Point P)) : Shell a b (o.dz f)

theorem NavierStokes.DefectIncrementBounds.Shell.time {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b : ℝ} {f : ScalarField (Point P)} (hf : Shell a b f) (o : MeanIncrementBounds.Operators (Point P)) : Shell a b (o.time f)

theorem NavierStokes.DefectIncrementBounds.Shell.inv_mul {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b : ℝ} {f : ScalarField (Point P)} {o : MeanIncrementBounds.Operators (Point P)} (hf : Shell a b f) (ha : 0 < a) (ho : PositiveOperators o) : Shell a b (o.invRadius * f)

theorem NavierStokes.DefectIncrementBounds.Shell.radialDiv {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b : ℝ} {f : ScalarField (Point P)} {o : MeanIncrementBounds.Operators (Point P)} (hf : Shell a b f) (ha : 0 < a) (ho : PositiveOperators o) (c : ℝ) : Shell a b (o.radialDiv c f)

theorem NavierStokes.DefectIncrementBounds.Shell.viscosity {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b : ℝ} {f : ScalarField (Point P)} {o : MeanIncrementBounds.Operators (Point P)} (hf : Shell a b f) (ha : 0 < a) (ho : PositiveOperators o) (c : ℝ) : Shell a b (o.viscosity c f)

theorem NavierStokes.DefectIncrementBounds.thetaAxial_shell {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b : ℝ} (ha : 0 < a) {base m : MeanIncrementBounds.Triple (Point P)} (hb : MeanIncrementBounds.SmoothTriple positiveDomain base) (hm : ShellTriple a b m) : Shell a b (MeanIncrementBounds.thetaAxial base m)

theorem NavierStokes.DefectIncrementBounds.axialAxial_shell {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b : ℝ} (ha : 0 < a) {base m : MeanIncrementBounds.Triple (Point P)} (hb : MeanIncrementBounds.SmoothTriple positiveDomain base) (hm : ShellTriple a b m) : Shell a b (MeanIncrementBounds.axialAxial base m)

theorem NavierStokes.DefectIncrementBounds.axialRadial_shell {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b : ℝ} (ha : 0 < a) {base m : MeanIncrementBounds.Triple (Point P)} (hb : MeanIncrementBounds.SmoothTriple positiveDomain base) (hm : ShellTriple a b m) : Shell a b (MeanIncrementBounds.axialRadial base m)

theorem NavierStokes.DefectIncrementBounds.radialRadial_shell {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b : ℝ} (ha : 0 < a) {base m : MeanIncrementBounds.Triple (Point P)} (hb : MeanIncrementBounds.SmoothTriple positiveDomain base) (hm : ShellTriple a b m) : Shell a b (MeanIncrementBounds.radialRadial base m)

theorem NavierStokes.DefectIncrementBounds.radialAngular_shell {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b : ℝ} (ha : 0 < a) {base m : MeanIncrementBounds.Triple (Point P)} (hb : MeanIncrementBounds.SmoothTriple positiveDomain base) (hm : ShellTriple a b m) : Shell a b (MeanIncrementBounds.radialAngular base m)

theorem NavierStokes.DefectIncrementBounds.gr_shell {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b : ℝ} (ha : 0 < a) {base m : MeanIncrementBounds.Triple (Point P)} (hb : MeanIncrementBounds.SmoothTriple positiveDomain base) (hm : ShellTriple a b m) {o : MeanIncrementBounds.Operators (Point P)} (ho : PositiveOperators o) (W : Fin 3 → Fin 3 → ScalarField (Point P)) (hW : ∀ (i j : Fin 3), Shell a b (W i j)) : Shell a b (MeanIncrementBounds.gr o base m W)

theorem NavierStokes.DefectIncrementBounds.leadingRadial_shell {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b : ℝ} (ha : 0 < a) {base h : MeanIncrementBounds.Triple (Point P)} (hb : MeanIncrementBounds.SmoothTriple positiveDomain base) (hh : ShellTriple a b h) {o : MeanIncrementBounds.Operators (Point P)} (ho : PositiveOperators o) : Shell a b (MeanIncrementBounds.leadingRadial o base h)

The actual three moments and their linearity

noncomputable def NavierStokes.DefectIncrementBounds.barMoment {P : Type} (k : ℕ) (f : ScalarField (Point P)) : ScalarField P

Bar moment, given by CorrectionState.radialMoment k f.

Equations

• NavierStokes.DefectIncrementBounds.barMoment k f = NavierStokes.CorrectionState.radialMoment k f

theorem NavierStokes.DefectIncrementBounds.barMoment_apply {P : Type} (k : ℕ) (f : ScalarField (Point P)) (n : ℕ) (p : P) : barMoment k f n p = ∫ (r : ℝ), r ^ k * PressureStream.torusAverage (f n) (r, p)

theorem NavierStokes.DefectIncrementBounds.torusAverage_add {P : Type} [NormedAddCommGroup P] {f g : Point P → ℝ} (hf : Continuous f) (hg : Continuous g) (p : ℝ × P) : PressureStream.torusAverage (fun (x : PressureStream.Lift P) => f x + g x) p = PressureStream.torusAverage f p + PressureStream.torusAverage g p

theorem NavierStokes.DefectIncrementBounds.Shell.barIntegrable {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b : ℝ} {f : ScalarField (Point P)} (hf : Shell a b f) (k n : ℕ) (p : P) : MeasureTheory.Integrable (fun (r : ℝ) => r ^ k * PressureStream.torusAverage (f n) (r, p)) MeasureTheory.volume

theorem NavierStokes.DefectIncrementBounds.barMoment_add {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b : ℝ} {f g : ScalarField (Point P)} (hf : Shell a b f) (hg : Shell a b g) (k : ℕ) : barMoment k (f + g) = barMoment k f + barMoment k g

theorem NavierStokes.DefectIncrementBounds.barMoment_sub {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b : ℝ} {f g : ScalarField (Point P)} (hf : Shell a b f) (hg : Shell a b g) (k : ℕ) : barMoment k (f - g) = barMoment k f - barMoment k g

theorem NavierStokes.DefectIncrementBounds.barMoment_smul {P : Type} (c : ℝ) (f : ScalarField (Point P)) (k : ℕ) : barMoment k (c • f) = c • barMoment k f

@[simp]

theorem NavierStokes.DefectIncrementBounds.barMoment_zero {P : Type} (k : ℕ) : barMoment k 0 = 0

theorem NavierStokes.DefectIncrementBounds.barMoment_mem {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b cL cR : ℝ} (ha : 0 < a) (hab : a < b) (hcL : 0 < cL) (hcR : 0 < cR) (ε S : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hS : ∀ (n : ℕ), 1 ≤ S n) {α : ℝ} {f : ScalarField (Point P)} (hf : Shell a b f) (hclass : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) α f) (k : ℕ) : WeightedClasses.UnweightedClass (MeanMomentBounds.slowStripData ε S hε hεone hS) α (barMoment k f)

Literal changes, linear rows, and explicit nonlinear remainders

noncomputable def NavierStokes.DefectIncrementBounds.thetaLeading {P : Type} (base h : MeanIncrementBounds.Triple (Point P)) : ScalarField (Point P)

Theta leading, given by base.axial * h.angular + base.angular * h.axial.

Equations

• NavierStokes.DefectIncrementBounds.thetaLeading base h = base.axial * h.angular + base.angular * h.axial

noncomputable def NavierStokes.DefectIncrementBounds.axialLeading {P : Type} (base h : MeanIncrementBounds.Triple (Point P)) : ScalarField (Point P)

Axial leading, given by (2 : ℝ) • (base.axial * h.axial).

Equations

• NavierStokes.DefectIncrementBounds.axialLeading base h = 2 • (base.axial * h.axial)

noncomputable def NavierStokes.DefectIncrementBounds.thetaQuadratic {P : Type} (m h : MeanIncrementBounds.Triple (Point P)) : ScalarField (Point P)

Theta quadratic, given by m.axial * h.angular + h.axial * m.angular + h.axial * h.angular.

Equations

• NavierStokes.DefectIncrementBounds.thetaQuadratic m h = m.axial * h.angular + h.axial * m.angular + h.axial * h.angular

noncomputable def NavierStokes.DefectIncrementBounds.axialQuadratic {P : Type} (m h : MeanIncrementBounds.Triple (Point P)) : ScalarField (Point P)

Axial quadratic, given by (2 : ℝ) • (m.axial * h.axial) + h.axial * h.axial.

Equations

• NavierStokes.DefectIncrementBounds.axialQuadratic m h = 2 • (m.axial * h.axial) + h.axial * h.axial

noncomputable def NavierStokes.DefectIncrementBounds.actualRadialError {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (o : MeanIncrementBounds.Operators (Point P)) (base m h : MeanIncrementBounds.Triple (Point P)) (W : Fin 3 → Fin 3 → ScalarField (Point P)) : ScalarField (Point P)

This is the actual source difference minus the centrifugal linear row; its formula and class are proved from equation (32).

Equations

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

noncomputable def NavierStokes.DefectIncrementBounds.pressureDefect {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (o : MeanIncrementBounds.Operators (Point P)) (base m : MeanIncrementBounds.Triple (Point P)) (W : Fin 3 → Fin 3 → ScalarField (Point P)) : ScalarField P

Pressure defect, given by barMoment 0 (gr o base m W).

Equations

• NavierStokes.DefectIncrementBounds.pressureDefect o base m W = NavierStokes.DefectIncrementBounds.barMoment 0 (NavierStokes.MeanIncrementBounds.gr o base m W)

noncomputable def NavierStokes.DefectIncrementBounds.thetaDefect {P : Type} (base m : MeanIncrementBounds.Triple (Point P)) (W : Fin 3 → Fin 3 → ScalarField (Point P)) : ScalarField P

Theta defect, given by barMoment 2 (thetaAxial base m + W 2 1).

Equations

• NavierStokes.DefectIncrementBounds.thetaDefect base m W = NavierStokes.DefectIncrementBounds.barMoment 2 (NavierStokes.MeanIncrementBounds.thetaAxial base m + W 2 1)

noncomputable def NavierStokes.DefectIncrementBounds.axialDefect {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (o : MeanIncrementBounds.Operators (Point P)) (base m : MeanIncrementBounds.Triple (Point P)) (W : Fin 3 → Fin 3 → ScalarField (Point P)) : ScalarField P

Axial defect, given by barMoment 1 (axialAxial base m + W 2 2) - (1 / 2 : ℝ) • barMoment 2 (gr o base m W).

Equations

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

noncomputable def NavierStokes.DefectIncrementBounds.defects {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (o : MeanIncrementBounds.Operators (Point P)) (base m : MeanIncrementBounds.Triple (Point P)) (W : Fin 3 → Fin 3 → ScalarField (Point P)) : ℕ → P → Fin 3 → ℝ

Defects, defined pointwise by ![pressureDefect o base m W n p, thetaDefect base m W n p, axialDefect o base m W n p].

Equations

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

noncomputable def NavierStokes.DefectIncrementBounds.linearRows {P : Type} (o : MeanIncrementBounds.Operators (Point P)) (base h : MeanIncrementBounds.Triple (Point P)) : ℕ → P → Fin 3 → ℝ

Linear rows as an element of ℕ → P → Fin 3 → ℝ.

Equations

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

noncomputable def NavierStokes.DefectIncrementBounds.remainders {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (o : MeanIncrementBounds.Operators (Point P)) (base m h : MeanIncrementBounds.Triple (Point P)) (W : Fin 3 → Fin 3 → ScalarField (Point P)) : ℕ → P → Fin 3 → ℝ

Remainders as an element of ℕ → P → Fin 3 → ℝ.

Equations

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

theorem NavierStokes.DefectIncrementBounds.thetaQuadratic_shell {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b : ℝ} {m h : MeanIncrementBounds.Triple (Point P)} (hm : ShellTriple a b m) (hh : ShellTriple a b h) : Shell a b (thetaQuadratic m h)

theorem NavierStokes.DefectIncrementBounds.axialQuadratic_shell {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b : ℝ} {m h : MeanIncrementBounds.Triple (Point P)} (hm : ShellTriple a b m) (hh : ShellTriple a b h) : Shell a b (axialQuadratic m h)

theorem NavierStokes.DefectIncrementBounds.thetaLeading_shell {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b : ℝ} (ha : 0 < a) {base h : MeanIncrementBounds.Triple (Point P)} (hb : MeanIncrementBounds.SmoothTriple positiveDomain base) (hh : ShellTriple a b h) : Shell a b (thetaLeading base h)

theorem NavierStokes.DefectIncrementBounds.axialLeading_shell {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b : ℝ} (ha : 0 < a) {base h : MeanIncrementBounds.Triple (Point P)} (hb : MeanIncrementBounds.SmoothTriple positiveDomain base) (hh : ShellTriple a b h) : Shell a b (axialLeading base h)

theorem NavierStokes.DefectIncrementBounds.actualRadialError_shell {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b : ℝ} (ha : 0 < a) {o : MeanIncrementBounds.Operators (Point P)} (ho : PositiveOperators o) {base m h : MeanIncrementBounds.Triple (Point P)} (hb : MeanIncrementBounds.SmoothTriple positiveDomain base) (hm : ShellTriple a b m) (hh : ShellTriple a b h) (W : Fin 3 → Fin 3 → ScalarField (Point P)) (hW : ∀ (i j : Fin 3), Shell a b (W i j)) : Shell a b (actualRadialError o base m h W)

theorem NavierStokes.DefectIncrementBounds.thetaAxial_update_split {P : Type} (base m h : MeanIncrementBounds.Triple (Point P)) (W : Fin 3 → Fin 3 → ScalarField (Point P)) : MeanIncrementBounds.thetaAxial base (MeanIncrementBounds.updated m h) + W 2 1 = MeanIncrementBounds.thetaAxial base m + W 2 1 + thetaLeading base h + thetaQuadratic m h

theorem NavierStokes.DefectIncrementBounds.axialAxial_update_split {P : Type} (base m h : MeanIncrementBounds.Triple (Point P)) (W : Fin 3 → Fin 3 → ScalarField (Point P)) : MeanIncrementBounds.axialAxial base (MeanIncrementBounds.updated m h) + W 2 2 = MeanIncrementBounds.axialAxial base m + W 2 2 + axialLeading base h + axialQuadratic m h

theorem NavierStokes.DefectIncrementBounds.radial_update_split {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (o : MeanIncrementBounds.Operators (Point P)) (base m h : MeanIncrementBounds.Triple (Point P)) (W : Fin 3 → Fin 3 → ScalarField (Point P)) : MeanIncrementBounds.gr o base (MeanIncrementBounds.updated m h) W = MeanIncrementBounds.gr o base m W + MeanIncrementBounds.leadingRadial o base h + actualRadialError o base m h W

theorem NavierStokes.DefectIncrementBounds.actualRadialError_eq_formula {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {U : Set (Point P)} (hU : IsOpen U) (o : MeanIncrementBounds.Operators (Point P)) (ha : ContDiffOn ℝ (↑⊤) o.radialProfile U) {base m h : MeanIncrementBounds.Triple (Point P)} (hb : MeanIncrementBounds.SmoothTriple U base) (hm : MeanIncrementBounds.SmoothTriple U m) (hh : MeanIncrementBounds.SmoothTriple U h) (W : Fin 3 → Fin 3 → ScalarField (Point P)) (hW : ∀ (i j : Fin 3), MeanIncrementBounds.SmoothOn U (W i j)) : MeanIncrementBounds.Agree U (actualRadialError o base m h W) (MeanIncrementBounds.radialRemainder o base m h)

The complete equation-(32) remainder: slow/fast time, radial transport, axial transport, old/new angular products, and viscosity are retained.

theorem NavierStokes.DefectIncrementBounds.thetaQuadratic_mem {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {s : WeightedClasses.StripData (Point P)} {o : MeanIncrementBounds.Operators (Point P)} {κ H : ℝ} {m h : MeanIncrementBounds.Triple (Point P)} (ho : MeanIncrementBounds.OperatorBounds s o κ) (hm : MeanIncrementBounds.CumulativeBounds s m) (hh : MeanIncrementBounds.IncrementBounds s H h) (hH : 9 / 10 ≤ H) : WeightedClasses.MeanClass s (H + 9 / 10 - 2 * κ) (thetaQuadratic m h)

theorem NavierStokes.DefectIncrementBounds.axialQuadratic_mem {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {s : WeightedClasses.StripData (Point P)} {o : MeanIncrementBounds.Operators (Point P)} {κ H : ℝ} {m h : MeanIncrementBounds.Triple (Point P)} (ho : MeanIncrementBounds.OperatorBounds s o κ) (hm : MeanIncrementBounds.CumulativeBounds s m) (hh : MeanIncrementBounds.IncrementBounds s H h) (hH : 9 / 10 ≤ H) : WeightedClasses.MeanClass s (H + 9 / 10 - 2 * κ) (axialQuadratic m h)

theorem NavierStokes.DefectIncrementBounds.actualRadialError_mem {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {s : WeightedClasses.StripData (Point P)} {o : MeanIncrementBounds.Operators (Point P)} {κ H : ℝ} {base m h : MeanIncrementBounds.Triple (Point P)} (ho : MeanIncrementBounds.OperatorBounds s o κ) (hb : MeanIncrementBounds.BaseBounds s base) (hm : MeanIncrementBounds.CumulativeBounds s m) (hh : MeanIncrementBounds.IncrementBounds s H h) (hH : 9 / 10 ≤ H) (W : Fin 3 → Fin 3 → ScalarField (Point P)) (hW : ∀ (i j : Fin 3), MeanIncrementBounds.SmoothOn s.domain (W i j)) : WeightedClasses.MeanClass s (H + 9 / 10 - 2 * κ) (actualRadialError o base m h W)

theorem NavierStokes.DefectIncrementBounds.pressureDefect_update {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b : ℝ} (ha : 0 < a) {o : MeanIncrementBounds.Operators (Point P)} (hop : PositiveOperators o) {base m h : MeanIncrementBounds.Triple (Point P)} (hb : MeanIncrementBounds.SmoothTriple positiveDomain base) (hm : ShellTriple a b m) (hh : ShellTriple a b h) (W : Fin 3 → Fin 3 → ScalarField (Point P)) (hW : ∀ (i j : Fin 3), Shell a b (W i j)) : pressureDefect o base (MeanIncrementBounds.updated m h) W = pressureDefect o base m W + barMoment 0 (MeanIncrementBounds.leadingRadial o base h) + barMoment 0 (actualRadialError o base m h W)

theorem NavierStokes.DefectIncrementBounds.thetaDefect_update {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b : ℝ} (ha : 0 < a) {base m h : MeanIncrementBounds.Triple (Point P)} (hb : MeanIncrementBounds.SmoothTriple positiveDomain base) (hm : ShellTriple a b m) (hh : ShellTriple a b h) (W : Fin 3 → Fin 3 → ScalarField (Point P)) (hW : ∀ (i j : Fin 3), Shell a b (W i j)) : thetaDefect base (MeanIncrementBounds.updated m h) W = thetaDefect base m W + barMoment 2 (thetaLeading base h) + barMoment 2 (thetaQuadratic m h)

theorem NavierStokes.DefectIncrementBounds.axialDefect_update {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b : ℝ} (ha : 0 < a) {o : MeanIncrementBounds.Operators (Point P)} (hop : PositiveOperators o) {base m h : MeanIncrementBounds.Triple (Point P)} (hb : MeanIncrementBounds.SmoothTriple positiveDomain base) (hm : ShellTriple a b m) (hh : ShellTriple a b h) (W : Fin 3 → Fin 3 → ScalarField (Point P)) (hW : ∀ (i j : Fin 3), Shell a b (W i j)) : axialDefect o base (MeanIncrementBounds.updated m h) W = axialDefect o base m W + (barMoment 1 (axialLeading base h) - (1 / 2) • barMoment 2 (MeanIncrementBounds.leadingRadial o base h)) + (barMoment 1 (axialQuadratic m h) - (1 / 2) • barMoment 2 (actualRadialError o base m h W))

theorem NavierStokes.DefectIncrementBounds.defects_update {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b : ℝ} (ha : 0 < a) {o : MeanIncrementBounds.Operators (Point P)} (hop : PositiveOperators o) {base m h : MeanIncrementBounds.Triple (Point P)} (hb : MeanIncrementBounds.SmoothTriple positiveDomain base) (hm : ShellTriple a b m) (hh : ShellTriple a b h) (W : Fin 3 → Fin 3 → ScalarField (Point P)) (hW : ∀ (i j : Fin 3), Shell a b (W i j)) : defects o base (MeanIncrementBounds.updated m h) W = defects o base m W + linearRows o base h + remainders o base m h W

Every defect changes by the exact row (35) and its explicitly computed remainder. No estimate or cancellation is a premise of this identity.

theorem NavierStokes.DefectIncrementBounds.defects_after_solved_rows {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b : ℝ} (ha : 0 < a) {o : MeanIncrementBounds.Operators (Point P)} (hop : PositiveOperators o) {base m h : MeanIncrementBounds.Triple (Point P)} (hb : MeanIncrementBounds.SmoothTriple positiveDomain base) (hm : ShellTriple a b m) (hh : ShellTriple a b h) (W : Fin 3 → Fin 3 → ScalarField (Point P)) (hW : ∀ (i j : Fin 3), Shell a b (W i j)) (hrows : linearRows o base h = -defects o base m W) : defects o base (MeanIncrementBounds.updated m h) W = remainders o base m h W

theorem NavierStokes.DefectIncrementBounds.unweighted_sub {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {α : ℝ} {f g : ScalarField D} (hf : WeightedClasses.UnweightedClass s α f) (hg : WeightedClasses.UnweightedClass s α g) : WeightedClasses.UnweightedClass s α (f - g)

theorem NavierStokes.DefectIncrementBounds.unweighted_smul {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {α : ℝ} {f : ScalarField D} (hf : WeightedClasses.UnweightedClass s α f) (c : ℝ) : WeightedClasses.UnweightedClass s α (c • f)

theorem NavierStokes.DefectIncrementBounds.remainders_mem {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b cL cR : ℝ} (ha : 0 < a) (hab : a < b) (hcL : 0 < cL) (hcR : 0 < cR) (ε S : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hS : ∀ (n : ℕ), 1 ≤ S n) {o : MeanIncrementBounds.Operators (Point P)} {κ H : ℝ} {base m h : MeanIncrementBounds.Triple (Point P)} (hop : PositiveOperators o) (hbs : MeanIncrementBounds.SmoothTriple positiveDomain base) (hms : ShellTriple a b m) (hhs : ShellTriple a b h) (W : Fin 3 → Fin 3 → ScalarField (Point P)) (hW : ∀ (i j : Fin 3), Shell a b (W i j)) (ho : MeanIncrementBounds.OperatorBounds (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) o κ) (hb : MeanIncrementBounds.BaseBounds (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) base) (hm : MeanIncrementBounds.CumulativeBounds (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) m) (hh : MeanIncrementBounds.IncrementBounds (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) H h) (hH : 9 / 10 ≤ H) (i : Fin 3) : WeightedClasses.UnweightedClass (MeanMomentBounds.slowStripData ε S hε hεone hS) (H + 9 / 10 - 2 * κ) fun (n : ℕ) (p : P) => remainders o base m h W n p i

The remainder bound is derived from the primitive mean classes and the literal equation-(32) source, then integrated by the actual moment map.

theorem NavierStokes.DefectIncrementBounds.defects_after_rank_mem {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b cL cR : ℝ} (ha : 0 < a) (hab : a < b) (hcL : 0 < cL) (hcR : 0 < cR) (ε S : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hS : ∀ (n : ℕ), 1 ≤ S n) {o : MeanIncrementBounds.Operators (Point P)} {κ H : ℝ} {base m h : MeanIncrementBounds.Triple (Point P)} (hop : PositiveOperators o) (hbs : MeanIncrementBounds.SmoothTriple positiveDomain base) (hms : ShellTriple a b m) (hhs : ShellTriple a b h) (W : Fin 3 → Fin 3 → ScalarField (Point P)) (hW : ∀ (i j : Fin 3), Shell a b (W i j)) (ho : MeanIncrementBounds.OperatorBounds (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) o κ) (hb : MeanIncrementBounds.BaseBounds (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) base) (hm : MeanIncrementBounds.CumulativeBounds (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) m) (hh : MeanIncrementBounds.IncrementBounds (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) H h) (hH : 9 / 10 ≤ H) (hrows : linearRows o base h = -defects o base m W) (i : Fin 3) : WeightedClasses.UnweightedClass (MeanMomentBounds.slowStripData ε S hε hεone hS) (H + 9 / 10 - 2 * κ) fun (n : ℕ) (p : P) => defects o base (MeanIncrementBounds.updated m h) W n p i

Identification with the five solved rows and both exact masses

noncomputable def NavierStokes.DefectIncrementBounds.slowSlice {P : Type} (f : ScalarField (Point P)) (n : ℕ) (p : P) (r : ℝ) : ℝ

Slow slice, given by f n (r, (p, 0)).

Equations

• NavierStokes.DefectIncrementBounds.slowSlice f n p r = f n (r, p, 0)

noncomputable def NavierStokes.DefectIncrementBounds.IsSlow {P : Type} (f : ScalarField (Point P)) : Prop

Is slow, given by ∀ n r p Y, f n (r, (p, Y)) = slowSlice f n p r.

Equations

• NavierStokes.DefectIncrementBounds.IsSlow f = ∀ (n : ℕ) (r : ℝ) (p : P) (Y : NavierStokes.PressureStream.Plane), f n (r, p, Y) = NavierStokes.DefectIncrementBounds.slowSlice f n p r

theorem NavierStokes.DefectIncrementBounds.IsSlow.add {P : Type} {f g : ScalarField (Point P)} (hf : IsSlow f) (hg : IsSlow g) : IsSlow (f + g)

theorem NavierStokes.DefectIncrementBounds.IsSlow.mul {P : Type} {f g : ScalarField (Point P)} (hf : IsSlow f) (hg : IsSlow g) : IsSlow (f * g)

theorem NavierStokes.DefectIncrementBounds.IsSlow.smul {P : Type} {f : ScalarField (Point P)} (hf : IsSlow f) (c : ℝ) : IsSlow (c • f)

theorem NavierStokes.DefectIncrementBounds.PositiveOperators.invRadius_slow {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {o : MeanIncrementBounds.Operators (Point P)} (ho : PositiveOperators o) : IsSlow o.invRadius

theorem NavierStokes.DefectIncrementBounds.barMoment_slow {P : Type} {f : ScalarField (Point P)} (hf : IsSlow f) (k n : ℕ) (p : P) : barMoment k f n p = ∫ (r : ℝ), r ^ k * slowSlice f n p r

theorem NavierStokes.DefectIncrementBounds.Shell.sliceIntegrable {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b : ℝ} {f : ScalarField (Point P)} (hf : Shell a b f) (k n : ℕ) (p : P) : MeasureTheory.Integrable (fun (r : ℝ) => r ^ k * slowSlice f n p r) MeasureTheory.volume

theorem NavierStokes.DefectIncrementBounds.fiveRows_mass_zero {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {o : MeanIncrementBounds.Operators (Point P)} {base m h : MeanIncrementBounds.Triple (Point P)} {W : Fin 3 → Fin 3 → ScalarField (Point P)} (hv : IsSlow h.angular) (hg : IsSlow h.axial) (hrows : ∀ (n : ℕ) (p : P), FiveRowRank.FiveRows (slowSlice base.angular n p) (slowSlice base.axial n p) (defects o base m W n p) (slowSlice h.angular n p) (slowSlice h.axial n p)) : barMoment 2 h.angular = 0 ∧ barMoment 1 h.axial = 0

theorem NavierStokes.DefectIncrementBounds.fiveRows_preserve_masses {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b : ℝ} {o : MeanIncrementBounds.Operators (Point P)} {base m h : MeanIncrementBounds.Triple (Point P)} {W : Fin 3 → Fin 3 → ScalarField (Point P)} (hm : ShellTriple a b m) (hh : ShellTriple a b h) (hv : IsSlow h.angular) (hg : IsSlow h.axial) (hrows : ∀ (n : ℕ) (p : P), FiveRowRank.FiveRows (slowSlice base.angular n p) (slowSlice base.axial n p) (defects o base m W n p) (slowSlice h.angular n p) (slowSlice h.axial n p)) : barMoment 2 (MeanIncrementBounds.updated m h).angular = barMoment 2 m.angular ∧ barMoment 1 (MeanIncrementBounds.updated m h).axial = barMoment 1 m.axial

theorem NavierStokes.DefectIncrementBounds.linearRows_eq_neg_of_fiveRows {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b : ℝ} (ha : 0 < a) {o : MeanIncrementBounds.Operators (Point P)} (hop : PositiveOperators o) {base m h : MeanIncrementBounds.Triple (Point P)} (hb : MeanIncrementBounds.SmoothTriple positiveDomain base) (hh : ShellTriple a b h) (hV : IsSlow base.angular) (hG : IsSlow base.axial) (hv : IsSlow h.angular) (hg : IsSlow h.axial) (W : Fin 3 → Fin 3 → ScalarField (Point P)) (hrows : ∀ (n : ℕ) (p : P), FiveRowRank.FiveRows (slowSlice base.angular n p) (slowSlice base.axial n p) (defects o base m W n p) (slowSlice h.angular n p) (slowSlice h.axial n p)) : linearRows o base h = -defects o base m W

The three moment rows are exactly those solved in (35), including the minus sign and factor one half in the axial pressure moment.

The actual constructed CorrectionState.rankStage

theorem NavierStokes.DefectIncrementBounds.defects_eq_stateDebt {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (c : CorrectionState.Context (Point P)) (u : CorrectionState.State (Point P)) : defects c.operators c.base u.mean u.covariance = CorrectionState.debt c u

theorem NavierStokes.DefectIncrementBounds.rankStage_covariance {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (p : CorrectionState.ReconstructionData) (r : CorrectionState.RankData P) (axial : P × PressureStream.Plane) (c : CorrectionState.Context (Point P)) (u : CorrectionState.State (Point P)) : (CorrectionState.rankStage p r axial c u).covariance = u.covariance

theorem NavierStokes.DefectIncrementBounds.rankStage_debt_eq {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (p : CorrectionState.ReconstructionData) (r : CorrectionState.RankData P) (axial : P × PressureStream.Plane) (c : CorrectionState.Context (Point P)) (u : CorrectionState.State (Point P)) : CorrectionState.debt c (CorrectionState.rankStage p r axial c u) = defects c.operators c.base (MeanIncrementBounds.updated u.mean (CorrectionState.rankIncrement p r axial c u)) u.covariance

structure NavierStokes.DefectIncrementBounds.RankGeometry {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (p : CorrectionState.ReconstructionData) (r : CorrectionState.RankData P) (c : CorrectionState.Context (Point P)) (u : CorrectionState.State (Point P)) : Prop

Geometric and primitive regularity hypotheses for the constructed rank patch. The conclusion is not among the fields: the inverse, actual stream, five rows, and their cancellation are supplied by proved theorems.

• primitive_inner_pos : 0 < p.inner
• exponent_pos : 0 < p.exponent
• lambda_pos : 0 < r.lambda
• coefficient_ne (n : ℕ) (x : P) : r.coefficient n x ≠ 0
• inner_pos : 0 < r.inner
• inner_lt_outer : r.inner < r.outer
• length_pos (n : ℕ) (x : P) : 0 < r.length n x
• velocity_ne (n : ℕ) (x : P) : r.velocity n x ≠ 0
• desired_smooth (n : ℕ) : ContDiff ℝ (↑⊤) (CorrectionState.rankDesiredAxial r c u n)
• desired_supported (n : ℕ) : RadialAlias.RadiallySupported p.inner p.outer (CorrectionState.rankDesiredAxial r c u n)
• angular_model (n : ℕ) (x : P) (R : ℝ) : R ∈ Set.Ioo (r.length n x * r.inner) (r.length n x * r.outer) → c.base.angular n (R, x, 0) = MeanRankUpdate.background r.lambda (r.coefficient n x) (r.length n x) (r.velocity n x) R
• axial_model (n : ℕ) (x : P) (R : ℝ) : R ∈ Set.Ioo (r.length n x * r.inner) (r.length n x * r.outer) → c.base.axial n (R, x, 0) = 0

theorem NavierStokes.DefectIncrementBounds.rankIncrement_angular_slow {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (p : CorrectionState.ReconstructionData) (r : CorrectionState.RankData P) (axial : P × PressureStream.Plane) (c : CorrectionState.Context (Point P)) (u : CorrectionState.State (Point P)) : IsSlow (CorrectionState.rankIncrement p r axial c u).angular

theorem NavierStokes.DefectIncrementBounds.RankGeometry.axial_exact {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {p : CorrectionState.ReconstructionData} {r : CorrectionState.RankData P} {c : CorrectionState.Context (Point P)} {u : CorrectionState.State (Point P)} (hg : RankGeometry p r c u) (axial : P × PressureStream.Plane) (n : ℕ) (x : Point P) : (CorrectionState.rankIncrement p r axial c u).axial n x = CorrectionState.rankDesiredAxial r c u n (x.1, x.2.1)

theorem NavierStokes.DefectIncrementBounds.RankGeometry.axial_slow {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {p : CorrectionState.ReconstructionData} {r : CorrectionState.RankData P} {c : CorrectionState.Context (Point P)} {u : CorrectionState.State (Point P)} (hg : RankGeometry p r c u) (axial : P × PressureStream.Plane) : IsSlow (CorrectionState.rankIncrement p r axial c u).axial

theorem NavierStokes.DefectIncrementBounds.RankGeometry.fiveRows {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {p : CorrectionState.ReconstructionData} {r : CorrectionState.RankData P} {c : CorrectionState.Context (Point P)} {u : CorrectionState.State (Point P)} (hg : RankGeometry p r c u) (axial : P × PressureStream.Plane) (n : ℕ) (x : P) : FiveRowRank.FiveRows (slowSlice c.base.angular n x) (slowSlice c.base.axial n x) (defects c.operators c.base u.mean u.covariance n x) (slowSlice (CorrectionState.rankIncrement p r axial c u).angular n x) (slowSlice (CorrectionState.rankIncrement p r axial c u).axial n x)

These are the solved rows for the actual axial stream, not for an unrealized desired increment.

theorem NavierStokes.DefectIncrementBounds.RankGeometry.solved_rows {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {p : CorrectionState.ReconstructionData} {r : CorrectionState.RankData P} {c : CorrectionState.Context (Point P)} {u : CorrectionState.State (Point P)} (hg : RankGeometry p r c u) (axial : P × PressureStream.Plane) {a b : ℝ} (ha : 0 < a) (hop : PositiveOperators c.operators) (hb : MeanIncrementBounds.SmoothTriple positiveDomain c.base) (hh : ShellTriple a b (CorrectionState.rankIncrement p r axial c u)) (hV : IsSlow c.base.angular) (hG : IsSlow c.base.axial) : linearRows c.operators c.base (CorrectionState.rankIncrement p r axial c u) = -defects c.operators c.base u.mean u.covariance

theorem NavierStokes.DefectIncrementBounds.RankGeometry.preserve_masses {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {p : CorrectionState.ReconstructionData} {r : CorrectionState.RankData P} {c : CorrectionState.Context (Point P)} {u : CorrectionState.State (Point P)} (hg : RankGeometry p r c u) (axial : P × PressureStream.Plane) {a b : ℝ} (hm : ShellTriple a b u.mean) (hh : ShellTriple a b (CorrectionState.rankIncrement p r axial c u)) : CorrectionState.radialMoment 2 (CorrectionState.rankStage p r axial c u).mean.angular = CorrectionState.radialMoment 2 u.mean.angular ∧ CorrectionState.radialMoment 1 (CorrectionState.rankStage p r axial c u).mean.axial = CorrectionState.radialMoment 1 u.mean.axial

theorem NavierStokes.DefectIncrementBounds.RankGeometry.zeroMasses {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {p : CorrectionState.ReconstructionData} {r : CorrectionState.RankData P} {c : CorrectionState.Context (Point P)} {u : CorrectionState.State (Point P)} (hg : RankGeometry p r c u) (axial : P × PressureStream.Plane) {a b : ℝ} (hm : ShellTriple a b u.mean) (hh : ShellTriple a b (CorrectionState.rankIncrement p r axial c u)) (hzero : CorrectionState.ZeroMasses u) : CorrectionState.ZeroMasses (CorrectionState.rankStage p r axial c u)

theorem NavierStokes.DefectIncrementBounds.RankGeometry.debt_eq_remainders {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {p : CorrectionState.ReconstructionData} {r : CorrectionState.RankData P} {c : CorrectionState.Context (Point P)} {u : CorrectionState.State (Point P)} (hg : RankGeometry p r c u) (axial : P × PressureStream.Plane) {a b : ℝ} (ha : 0 < a) (hop : PositiveOperators c.operators) (hb : MeanIncrementBounds.SmoothTriple positiveDomain c.base) (hm : ShellTriple a b u.mean) (hh : ShellTriple a b (CorrectionState.rankIncrement p r axial c u)) (hW : ∀ (i j : Fin 3), Shell a b (u.covariance i j)) (hV : IsSlow c.base.angular) (hG : IsSlow c.base.axial) : CorrectionState.debt c (CorrectionState.rankStage p r axial c u) = remainders c.operators c.base u.mean (CorrectionState.rankIncrement p r axial c u) u.covariance

theorem NavierStokes.DefectIncrementBounds.rankStage_defect_class {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b cL cR : ℝ} (ha : 0 < a) (hab : a < b) (hcL : 0 < cL) (hcR : 0 < cR) (ε S : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hS : ∀ (n : ℕ), 1 ≤ S n) {p : CorrectionState.ReconstructionData} {r : CorrectionState.RankData P} {c : CorrectionState.Context (Point P)} {u : CorrectionState.State (Point P)} (axial : P × PressureStream.Plane) (hg : RankGeometry p r c u) (hop : PositiveOperators c.operators) (hbs : MeanIncrementBounds.SmoothTriple positiveDomain c.base) (hms : ShellTriple a b u.mean) (hhs : ShellTriple a b (CorrectionState.rankIncrement p r axial c u)) (hW : ∀ (i j : Fin 3), Shell a b (u.covariance i j)) (hV : IsSlow c.base.angular) (hG : IsSlow c.base.axial) {κ H : ℝ} (ho : MeanIncrementBounds.OperatorBounds (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) c.operators κ) (hb : MeanIncrementBounds.BaseBounds (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) c.base) (hm : MeanIncrementBounds.CumulativeBounds (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) u.mean) (hh : MeanIncrementBounds.IncrementBounds (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) H (CorrectionState.rankIncrement p r axial c u)) (hH : 9 / 10 ≤ H) (i : Fin 3) : WeightedClasses.UnweightedClass (MeanMomentBounds.slowStripData ε S hε hεone hS) (H + 9 / 10 - 2 * κ) fun (n : ℕ) (x : P) => CorrectionState.debt c (CorrectionState.rankStage p r axial c u) n x i

The constructed rank solve followed by actual pressure recomputation has the claimed stronger defects. The inputs are primitive fields and their classes; no solved-row, defect-remainder, or pressure-error estimate is assumed.

theorem NavierStokes.DefectIncrementBounds.rankStage_defectBounds {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b cL cR : ℝ} (ha : 0 < a) (hab : a < b) (hcL : 0 < cL) (hcR : 0 < cR) (ε S : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hS : ∀ (n : ℕ), 1 ≤ S n) {p : CorrectionState.ReconstructionData} {r : CorrectionState.RankData P} {c : CorrectionState.Context (Point P)} {u : CorrectionState.State (Point P)} (axial : P × PressureStream.Plane) (hg : RankGeometry p r c u) (hop : PositiveOperators c.operators) (hbs : MeanIncrementBounds.SmoothTriple positiveDomain c.base) (hms : ShellTriple a b u.mean) (hhs : ShellTriple a b (CorrectionState.rankIncrement p r axial c u)) (hW : ∀ (i j : Fin 3), Shell a b (u.covariance i j)) (hV : IsSlow c.base.angular) (hG : IsSlow c.base.axial) {κ H : ℝ} (ho : MeanIncrementBounds.OperatorBounds (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) c.operators κ) (hb : MeanIncrementBounds.BaseBounds (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) c.base) (hm : MeanIncrementBounds.CumulativeBounds (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) u.mean) (hh : MeanIncrementBounds.IncrementBounds (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) H (CorrectionState.rankIncrement p r axial c u)) (hH : 9 / 10 ≤ H) {σ : ℝ} (hσ : 1 + σ ≤ H + 9 / 10 - 2 * κ) : CorrectionState.DefectBounds (MeanMomentBounds.slowStripData ε S hε hεone hS) σ c (CorrectionState.rankStage p r axial c u)