Regularity of the actual mean equations on a moving annulus

The inputs below are the individual mean, covariance, base, and virtual stress fields. Smoothness, moving support, and torus periodicity of their actual nonlinear fluxes and differential residuals are consequences. Base coefficients need smoothness and periodicity only at positive radii.

@[reducible, inline]

abbrev NavierStokes.MeanStateRegularity.Plane : Type

Plane: an abbreviation for PressureStream.Plane.

Equations

• NavierStokes.MeanStateRegularity.Plane = NavierStokes.PressureStream.Plane

@[reducible, inline]

abbrev NavierStokes.MeanStateRegularity.Point : Type

Point: an abbreviation for PressureStream.Lift Plane.

Equations

• NavierStokes.MeanStateRegularity.Point = NavierStokes.PressureStream.Lift NavierStokes.MeanStateRegularity.Plane

@[reducible, inline]

abbrev NavierStokes.MeanStateRegularity.Scalar : Type

Scalar: an abbreviation for MeanIncrementBounds.Field Point.

Equations

• NavierStokes.MeanStateRegularity.Scalar = NavierStokes.MeanIncrementBounds.Field NavierStokes.MeanStateRegularity.Point

@[reducible, inline]

abbrev NavierStokes.MeanStateRegularity.Tensor : Type

Tensor: an abbreviation for Fin 3 → Fin 3 → Scalar.

Equations

• NavierStokes.MeanStateRegularity.Tensor = (Fin 3 → Fin 3 → NavierStokes.MeanStateRegularity.Scalar)

noncomputable def NavierStokes.MeanStateRegularity.Periodic (U : Set Plane) (f : Scalar) : Prop

Periodicity on the entire fast torus at each allowed slow point.

Equations

• NavierStokes.MeanStateRegularity.Periodic U f = ∀ (n : ℕ), NavierStokes.PhysicalMeanDomain.PeriodicOn U (f n)

noncomputable def NavierStokes.MeanStateRegularity.PositivePeriodic (U : Set Plane) (f : Scalar) : Prop

A background coefficient is only used at positive physical radii.

Equations

• NavierStokes.MeanStateRegularity.PositivePeriodic U f = ∀ (n : ℕ) (R : ℝ), 0 < R → ∀ s ∈ U, NavierStokes.FourierAlias.TorusPeriodic fun (Y : NavierStokes.TorusInverse.Plane) => f n (R, s, Y)

theorem NavierStokes.MeanStateRegularity.Periodic.positive {U : Set Plane} {f : Scalar} (hf : Periodic U f) : PositivePeriodic U f

theorem NavierStokes.MeanStateRegularity.Periodic.zero {U : Set Plane} : Periodic U 0

theorem NavierStokes.MeanStateRegularity.Periodic.add {U : Set Plane} {f g : Scalar} (hf : Periodic U f) (hg : Periodic U g) : Periodic U (f + g)

theorem NavierStokes.MeanStateRegularity.Periodic.neg {U : Set Plane} {f : Scalar} (hf : Periodic U f) : Periodic U (-f)

theorem NavierStokes.MeanStateRegularity.Periodic.sub {U : Set Plane} {f g : Scalar} (hf : Periodic U f) (hg : Periodic U g) : Periodic U (f - g)

theorem NavierStokes.MeanStateRegularity.Periodic.mul {U : Set Plane} {f g : Scalar} (hf : Periodic U f) (hg : Periodic U g) : Periodic U (f * g)

theorem NavierStokes.MeanStateRegularity.Periodic.smul {U : Set Plane} {f : Scalar} (hf : Periodic U f) (c : ℝ) : Periodic U (c • f)

theorem NavierStokes.MeanStateRegularity.Periodic.band_mul {U : Set Plane} {f : Scalar} (hf : Periodic U f) (c : ℕ → ℝ) : Periodic U fun (n : ℕ) (x : Point) => c n * f n x

theorem NavierStokes.MeanStateRegularity.Periodic.directional {U : Set Plane} {f : Scalar} (hf : Periodic U f) (hU : IsOpen U) (v : Point) : Periodic U fun (n : ℕ) (x : Point) => (fderiv ℝ (f n) x) v

Translation invariance of the actual Fréchet derivative is local in the slow parameter. No global extension of the field is required.

structure NavierStokes.MeanStateRegularity.OperatorData (U : Set Plane) (o : MeanIncrementBounds.Operators Point) : Prop

The native graph coefficient is smooth and periodic where it can be multiplied by a supported mean field.

• regular : LocalRankDefect.LocalOperators U o
• profile_periodic : PositivePeriodic U fun (x : ℕ) => o.radialProfile

theorem NavierStokes.MeanStateRegularity.OperatorData.inv_periodic {U : Set Plane} {o : MeanIncrementBounds.Operators Point} (ho : OperatorData U o) : PositivePeriodic U o.invRadius

theorem NavierStokes.MeanStateRegularity.OperatorData.native (U : Set Plane) (r : CorrectionState.ReconstructionData) (ε fast : ℕ → ℝ) (z t v : Plane) : OperatorData U (StateMomentBalances.nativeOperators r ε fast z t v)

The actual reconstruction operators meet the primitive hypotheses.

theorem NavierStokes.MeanStateRegularity.MovingField.regular {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {f : Scalar} (hf : GaugeMomentBalances.MovingField U a b f) : GaugeDebtIncrement.Regular U a b f

theorem NavierStokes.MeanStateRegularity.MovingField.of_regular {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {f : Scalar} (hf : GaugeDebtIncrement.Regular U a b f) (hp : Periodic U.carrier f) : GaugeMomentBalances.MovingField U a b f

theorem NavierStokes.MeanStateRegularity.MovingField.zero {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} : GaugeMomentBalances.MovingField U a b 0

theorem NavierStokes.MeanStateRegularity.MovingField.add {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {f g : Scalar} (hf : GaugeMomentBalances.MovingField U a b f) (hg : GaugeMomentBalances.MovingField U a b g) : GaugeMomentBalances.MovingField U a b (f + g)

theorem NavierStokes.MeanStateRegularity.MovingField.neg {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {f : Scalar} (hf : GaugeMomentBalances.MovingField U a b f) : GaugeMomentBalances.MovingField U a b (-f)

theorem NavierStokes.MeanStateRegularity.MovingField.sub {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {f g : Scalar} (hf : GaugeMomentBalances.MovingField U a b f) (hg : GaugeMomentBalances.MovingField U a b g) : GaugeMomentBalances.MovingField U a b (f - g)

theorem NavierStokes.MeanStateRegularity.MovingField.mul {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {f g : Scalar} (hf : GaugeMomentBalances.MovingField U a b f) (hg : GaugeMomentBalances.MovingField U a b g) : GaugeMomentBalances.MovingField U a b (f * g)

theorem NavierStokes.MeanStateRegularity.MovingField.smul {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {f : Scalar} (hf : GaugeMomentBalances.MovingField U a b f) (c : ℝ) : GaugeMomentBalances.MovingField U a b (c • f)

theorem NavierStokes.MeanStateRegularity.MovingField.band_mul {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {f : Scalar} (hf : GaugeMomentBalances.MovingField U a b f) (c : ℕ → ℝ) : GaugeMomentBalances.MovingField U a b fun (n : ℕ) (x : GaugeMomentBalances.Point) => c n * f n x

theorem NavierStokes.MeanStateRegularity.MovingField.directional {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {f : Scalar} (hf : GaugeMomentBalances.MovingField U a b f) (v : Point) : GaugeMomentBalances.MovingField U a b fun (n : ℕ) (x : GaugeMomentBalances.Point) => (fderiv ℝ (f n) x) v

theorem NavierStokes.MeanStateRegularity.MovingField.coefficient_mul {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {f g : Scalar} (hf : GaugeMomentBalances.MovingField U a b f) (ha : 0 < a) (hab : a < b) (hg : MeanIncrementBounds.SmoothOn (LocalRankDefect.positiveDomain U.carrier) g) (hp : PositivePeriodic U.carrier g) : GaugeMomentBalances.MovingField U a b (g * f)

The base is not assumed smooth or periodic through the axis. The supported factor is identically zero there and below it.

theorem NavierStokes.MeanStateRegularity.MovingField.mul_coefficient {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {f g : Scalar} (hf : GaugeMomentBalances.MovingField U a b f) (ha : 0 < a) (hab : a < b) (hg : MeanIncrementBounds.SmoothOn (LocalRankDefect.positiveDomain U.carrier) g) (hp : PositivePeriodic U.carrier g) : GaugeMomentBalances.MovingField U a b (f * g)

theorem NavierStokes.MeanStateRegularity.MovingField.dr {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {f : Scalar} (hf : GaugeMomentBalances.MovingField U a b f) (ha : 0 < a) (hab : a < b) {o : MeanIncrementBounds.Operators Point} (ho : OperatorData U.carrier o) : GaugeMomentBalances.MovingField U a b (o.dr f)

theorem NavierStokes.MeanStateRegularity.MovingField.dz {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {f : Scalar} (hf : GaugeMomentBalances.MovingField U a b f) (o : MeanIncrementBounds.Operators Point) : GaugeMomentBalances.MovingField U a b (o.dz f)

theorem NavierStokes.MeanStateRegularity.MovingField.time {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {f : Scalar} (hf : GaugeMomentBalances.MovingField U a b f) (o : MeanIncrementBounds.Operators Point) : GaugeMomentBalances.MovingField U a b (o.time f)

theorem NavierStokes.MeanStateRegularity.MovingField.inv_mul {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {f : Scalar} (hf : GaugeMomentBalances.MovingField U a b f) (ha : 0 < a) (hab : a < b) {o : MeanIncrementBounds.Operators Point} (ho : OperatorData U.carrier o) : GaugeMomentBalances.MovingField U a b (o.invRadius * f)

theorem NavierStokes.MeanStateRegularity.MovingField.radialDiv {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {f : Scalar} (hf : GaugeMomentBalances.MovingField U a b f) (ha : 0 < a) (hab : a < b) {o : MeanIncrementBounds.Operators Point} (ho : OperatorData U.carrier o) (c : ℝ) : GaugeMomentBalances.MovingField U a b (o.radialDiv c f)

theorem NavierStokes.MeanStateRegularity.MovingField.viscosity {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {f : Scalar} (hf : GaugeMomentBalances.MovingField U a b f) (ha : 0 < a) (hab : a < b) {o : MeanIncrementBounds.Operators Point} (ho : OperatorData U.carrier o) (c : ℝ) : GaugeMomentBalances.MovingField U a b (o.viscosity c f)

theorem NavierStokes.MeanStateRegularity.MovingField.movingSupport {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {f : Scalar} (hf : GaugeMomentBalances.MovingField U a b f) (n : ℕ) : LocalSignedRequest.MovingSupport a b coord U.carrier (f n)

The moving physical interval is exactly the normalized support used by the signed-stress request.

structure NavierStokes.MeanStateRegularity.BaseData (U : Set Plane) (b : MeanIncrementBounds.Triple Point) : Prop

Primitive base regularity on the positive-radius domain.

• smooth : MeanIncrementBounds.SmoothTriple (LocalRankDefect.positiveDomain U) b
• radial_periodic : PositivePeriodic U b.radial
• angular_periodic : PositivePeriodic U b.angular
• axial_periodic : PositivePeriodic U b.axial

structure NavierStokes.MeanStateRegularity.PeriodicTriple (U : Set Plane) (m : MeanIncrementBounds.Triple Point) : Prop

Periodic triple data, collecting radial, angular, axial.

• radial : Periodic U m.radial
• angular : Periodic U m.angular
• axial : Periodic U m.axial

theorem NavierStokes.MeanStateRegularity.BaseData.of_periodic {U : Set Plane} {b : MeanIncrementBounds.Triple Point} (hb : MeanIncrementBounds.SmoothTriple (LocalRankDefect.positiveDomain U) b) (hp : PeriodicTriple U b) : BaseData U b

structure NavierStokes.MeanStateRegularity.MovingTriple {coord : ℝ} (U : LocalSignedRequest.SlowRegion coord) (a b : ℝ) (m : MeanIncrementBounds.Triple Point) : Prop

Moving triple data, collecting radial, angular, axial.

• radial : GaugeMomentBalances.MovingField U a b m.radial
• angular : GaugeMomentBalances.MovingField U a b m.angular
• axial : GaugeMomentBalances.MovingField U a b m.axial

theorem NavierStokes.MeanStateRegularity.MovingTriple.of_regular {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {m : MeanIncrementBounds.Triple Point} (hm : GaugeDebtIncrement.RegularTriple U a b m) (hp : PeriodicTriple U.carrier m) : MovingTriple U a b m

theorem NavierStokes.MeanStateRegularity.MovingTriple.regular {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {m : MeanIncrementBounds.Triple Point} (hm : MovingTriple U a b m) : GaugeDebtIncrement.RegularTriple U a b m

theorem NavierStokes.MeanStateRegularity.MovingTriple.periodic {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {m : MeanIncrementBounds.Triple Point} (hm : MovingTriple U a b m) : PeriodicTriple U.carrier m

theorem NavierStokes.MeanStateRegularity.MovingTriple.updated {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {m h : MeanIncrementBounds.Triple Point} (hm : MovingTriple U a b m) (hh : MovingTriple U a b h) : MovingTriple U a b (MeanIncrementBounds.updated m h)

theorem NavierStokes.MeanStateRegularity.MovingTriple.thetaRadial {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {m base : MeanIncrementBounds.Triple Point} (hm : MovingTriple U a b m) (ha : 0 < a) (hab : a < b) (hb : BaseData U.carrier base) : GaugeMomentBalances.MovingField U a b (MeanIncrementBounds.thetaRadial base m)

theorem NavierStokes.MeanStateRegularity.MovingTriple.thetaAxial {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {m base : MeanIncrementBounds.Triple Point} (hm : MovingTriple U a b m) (ha : 0 < a) (hab : a < b) (hb : BaseData U.carrier base) : GaugeMomentBalances.MovingField U a b (MeanIncrementBounds.thetaAxial base m)

theorem NavierStokes.MeanStateRegularity.MovingTriple.axialRadial {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {m base : MeanIncrementBounds.Triple Point} (hm : MovingTriple U a b m) (ha : 0 < a) (hab : a < b) (hb : BaseData U.carrier base) : GaugeMomentBalances.MovingField U a b (MeanIncrementBounds.axialRadial base m)

theorem NavierStokes.MeanStateRegularity.MovingTriple.axialAxial {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {m base : MeanIncrementBounds.Triple Point} (hm : MovingTriple U a b m) (ha : 0 < a) (hab : a < b) (hb : BaseData U.carrier base) : GaugeMomentBalances.MovingField U a b (MeanIncrementBounds.axialAxial base m)

theorem NavierStokes.MeanStateRegularity.MovingTriple.radialRadial {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {m base : MeanIncrementBounds.Triple Point} (hm : MovingTriple U a b m) (ha : 0 < a) (hab : a < b) (hb : BaseData U.carrier base) : GaugeMomentBalances.MovingField U a b (MeanIncrementBounds.radialRadial base m)

theorem NavierStokes.MeanStateRegularity.MovingTriple.radialAngular {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {m base : MeanIncrementBounds.Triple Point} (hm : MovingTriple U a b m) (ha : 0 < a) (hab : a < b) (hb : BaseData U.carrier base) : GaugeMomentBalances.MovingField U a b (MeanIncrementBounds.radialAngular base m)

theorem NavierStokes.MeanStateRegularity.MovingTriple.thetaResidual {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {m base : MeanIncrementBounds.Triple Point} (hm : MovingTriple U a b m) (ha : 0 < a) (hab : a < b) (hb : BaseData U.carrier base) {o : MeanIncrementBounds.Operators Point} (ho : OperatorData U.carrier o) {W : Tensor} (hW : ∀ (i j : Fin 3), GaugeMomentBalances.MovingField U a b (W i j)) {T : Scalar} (hT : GaugeMomentBalances.MovingField U a b T) : GaugeMomentBalances.MovingField U a b (MeanIncrementBounds.thetaResidual o base m W T)

theorem NavierStokes.MeanStateRegularity.MovingTriple.axialResidual {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {m base : MeanIncrementBounds.Triple Point} (hm : MovingTriple U a b m) (ha : 0 < a) (hab : a < b) (hb : BaseData U.carrier base) {o : MeanIncrementBounds.Operators Point} (ho : OperatorData U.carrier o) {W : Tensor} (hW : ∀ (i j : Fin 3), GaugeMomentBalances.MovingField U a b (W i j)) {p T : Scalar} (hp : GaugeMomentBalances.MovingField U a b p) (hT : GaugeMomentBalances.MovingField U a b T) : GaugeMomentBalances.MovingField U a b (MeanIncrementBounds.axialResidual o base m W p T)

theorem NavierStokes.MeanStateRegularity.MovingTriple.gr {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {m base : MeanIncrementBounds.Triple Point} (hm : MovingTriple U a b m) (ha : 0 < a) (hab : a < b) (hb : BaseData U.carrier base) {o : MeanIncrementBounds.Operators Point} (ho : OperatorData U.carrier o) {W : Tensor} (hW : ∀ (i j : Fin 3), GaugeMomentBalances.MovingField U a b (W i j)) : GaugeMomentBalances.MovingField U a b (MeanIncrementBounds.gr o base m W)

structure NavierStokes.MeanStateRegularity.PrimitiveData {coord : ℝ} (U : LocalSignedRequest.SlowRegion coord) (a b : ℝ) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) : Prop

Only the individual incoming fields are constrained. No residual, flux, pressure reconstruction, or quantitative class bound is an input.

• operators : OperatorData U.carrier c.operators
• base : BaseData U.carrier c.base
• mean : MovingTriple U a b u.mean
• covariance (i j : Fin 3) : GaugeMomentBalances.MovingField U a b (u.covariance i j)
• virtualTheta : GaugeMomentBalances.MovingField U a b c.virtualTheta
• virtualAxial : GaugeMomentBalances.MovingField U a b c.virtualAxial

theorem NavierStokes.MeanStateRegularity.PrimitiveData.of_regular {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {c : CorrectionState.Context Point} {u : CorrectionState.State Point} (ho : OperatorData U.carrier c.operators) (hb : BaseData U.carrier c.base) (hm : GaugeDebtIncrement.RegularTriple U a b u.mean) (hmp : PeriodicTriple U.carrier u.mean) (hW : ∀ (i j : Fin 3), GaugeDebtIncrement.Regular U a b (u.covariance i j)) (hWp : ∀ (i j : Fin 3), Periodic U.carrier (u.covariance i j)) (hT : GaugeMomentBalances.MovingField U a b c.virtualTheta) (hZ : GaugeMomentBalances.MovingField U a b c.virtualAxial) : PrimitiveData U a b c u

theorem NavierStokes.MeanStateRegularity.PrimitiveData.angular_flux {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {c : CorrectionState.Context Point} {u : CorrectionState.State Point} (H : PrimitiveData U a b c u) (ha : 0 < a) (hab : a < b) : GaugeMomentBalances.MovingAngularInputs U a b c u

theorem NavierStokes.MeanStateRegularity.PrimitiveData.axial_flux {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {c : CorrectionState.Context Point} {u : CorrectionState.State Point} (H : PrimitiveData U a b c u) (ha : 0 < a) (hab : a < b) : GaugeMomentBalances.MovingAxialInputs U a b c u

theorem NavierStokes.MeanStateRegularity.PrimitiveData.source {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {c : CorrectionState.Context Point} {u : CorrectionState.State Point} (H : PrimitiveData U a b c u) (ha : 0 < a) (hab : a < b) : GaugeMomentBalances.MovingField U a b (u.gr c)

theorem NavierStokes.MeanStateRegularity.PrimitiveData.theta {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {c : CorrectionState.Context Point} {u : CorrectionState.State Point} (H : PrimitiveData U a b c u) (ha : 0 < a) (hab : a < b) : GaugeMomentBalances.MovingField U a b (u.thetaResidual c)

theorem NavierStokes.MeanStateRegularity.PrimitiveData.axial {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {c : CorrectionState.Context Point} {u : CorrectionState.State Point} (H : PrimitiveData U a b c u) (ha : 0 < a) (hab : a < b) (hp : GaugeMomentBalances.MovingField U a b u.pressure) : GaugeMomentBalances.MovingField U a b (u.axialResidual c)

theorem NavierStokes.MeanStateRegularity.PrimitiveData.pressure {coord : ℝ} {U : LocalSignedRequest.SlowRegion coord} {c : CorrectionState.Context Point} {u : CorrectionState.State Point} {g : VariableGaugeMean.GaugeData Plane} (H : PrimitiveData U g.radial.inner g.radial.outer c u) (ha : 0 < g.radial.inner) (hd : 0 < g.radial.exponent) (hg : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength coord) (hfixed : (VariableGaugeMean.reconstructState g c u).pressure = u.pressure) : GaugeMomentBalances.MovingField U g.radial.inner g.radial.outer u.pressure

A reconstructed incoming state needs no separate regularity premise on its pressure.

theorem NavierStokes.MeanStateRegularity.PrimitiveData.axial_reconstructed {coord : ℝ} {U : LocalSignedRequest.SlowRegion coord} {c : CorrectionState.Context Point} {u : CorrectionState.State Point} {g : VariableGaugeMean.GaugeData Plane} (H : PrimitiveData U g.radial.inner g.radial.outer c u) (ha : 0 < g.radial.inner) (hd : 0 < g.radial.exponent) (hg : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength coord) (hfixed : (VariableGaugeMean.reconstructState g c u).pressure = u.pressure) : GaugeMomentBalances.MovingField U g.radial.inner g.radial.outer (u.axialResidual c)

theorem NavierStokes.MeanStateRegularity.PrimitiveData.waveStage {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {c : CorrectionState.Context Point} {u : CorrectionState.State Point} (H : PrimitiveData U a b c u) (g : VariableGaugeMean.GaugeData Plane) (w : CorrectionState.Oscillation Point) (q : CorrectionState.OscillatoryScalar Point) (gaussian : CorrectionState.Oscillation Point) (hX : ∀ (i j : Fin 3), GaugeMomentBalances.MovingField U a b (SignedMeanGain.covarianceIncrement u.oscillation w i j)) : PrimitiveData U a b c (SignedMeanGain.waveStage g c u w q gaussian)

The same primitive fields after adding the actual wave covariance increment. The pressure is still obtained by the genuine reconstruction.

theorem NavierStokes.MeanStateRegularity.PrimitiveData.waveStage_of_regular {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {c : CorrectionState.Context Point} {u : CorrectionState.State Point} (H : PrimitiveData U a b c u) (g : VariableGaugeMean.GaugeData Plane) (w : CorrectionState.Oscillation Point) (q : CorrectionState.OscillatoryScalar Point) (gaussian : CorrectionState.Oscillation Point) (hX : ∀ (i j : Fin 3), GaugeDebtIncrement.Regular U a b (SignedMeanGain.covarianceIncrement u.oscillation w i j)) (hXp : ∀ (i j : Fin 3), Periodic U.carrier (SignedMeanGain.covarianceIncrement u.oscillation w i j)) : PrimitiveData U a b c (SignedMeanGain.waveStage g c u w q gaussian)

Direct assembly of the signed mean-stage inputs

theorem NavierStokes.MeanStateRegularity.localData (G : SignedMeanGain.Geometry) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (w : CorrectionState.Oscillation Point) (q : CorrectionState.OscillatoryScalar Point) (gaussian : CorrectionState.Oscillation Point) (H : PrimitiveData G.region G.patch.a G.patch.b c u) (ho : c.operators = G.operators) (hX : ∀ (i j : Fin 3), GaugeMomentBalances.MovingField G.region G.patch.a G.patch.b (SignedMeanGain.covarianceIncrement u.oscillation w i j)) (hfixed : VariableGaugeMean.reconstructState G.gauge c u = u) (hmθ : ∀ (n : ℕ), ∀ s ∈ G.region.carrier, CorrectionState.radialMoment 2 u.mean.angular n s = 0) (hmz : ∀ (n : ℕ), ∀ s ∈ G.region.carrier, CorrectionState.radialMoment 1 u.mean.axial n s = 0) : SignedMeanGain.LocalData G c u w q gaussian

All residual, flux, and source regularity fields of LocalData follow from primitive data. Reconstruction and the two mass identities are the actual state invariants, not regularity premises.

theorem NavierStokes.MeanStateRegularity.localData_of_regular (G : SignedMeanGain.Geometry) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (w : CorrectionState.Oscillation Point) (q : CorrectionState.OscillatoryScalar Point) (gaussian : CorrectionState.Oscillation Point) (H : PrimitiveData G.region G.patch.a G.patch.b c u) (ho : c.operators = G.operators) (hX : ∀ (i j : Fin 3), GaugeDebtIncrement.Regular G.region G.patch.a G.patch.b (SignedMeanGain.covarianceIncrement u.oscillation w i j)) (hXp : ∀ (i j : Fin 3), Periodic G.region.carrier (SignedMeanGain.covarianceIncrement u.oscillation w i j)) (hfixed : VariableGaugeMean.reconstructState G.gauge c u = u) (hmθ : ∀ (n : ℕ), ∀ s ∈ G.region.carrier, CorrectionState.radialMoment 2 u.mean.angular n s = 0) (hmz : ∀ (n : ℕ), ∀ s ∈ G.region.carrier, CorrectionState.radialMoment 1 u.mean.axial n s = 0) : SignedMeanGain.LocalData G c u w q gaussian

The regularity endpoint for the actual covariance increment, including the one supplied by WaveStateRegularity, combines with primitive periodicity and supplies the complete signed-stage input record.