Primitive regularity under the actual mean stages #
The temporal and rank increments below are the literal variable-gauge stream constructions. Their smoothness, moving support, and periodicity are derived before updating the state. No new residual regularity or quantitative estimate is an input to preservation.
theorem
NavierStokes.MeanStageRegularity.MovingField.temporalAtIndex
{coord a b : ℝ}
{U : LocalSignedRequest.SlowRegion coord}
{f : Scalar}
(hf : GaugeMomentBalances.MovingField U a b f)
(h : ℝ)
(index : ℕ → ℕ)
:
GaugeMomentBalances.MovingField U a b fun (n : ℕ) => MeanChartCompatibility.temporalAtIndex h n (index n) (f n)
theorem
NavierStokes.MeanStageRegularity.MovingField.streamPotential
{coord a b : ℝ}
{U : LocalSignedRequest.SlowRegion coord}
{f : Scalar}
(hf : GaugeMomentBalances.MovingField U a b f)
(ha : 0 < a)
(hab : a < b)
{d : ℝ}
(hd : 0 < d)
(M : ℕ → ℝ)
(v : Plane)
:
GaugeMomentBalances.MovingField U a b fun (n : ℕ) =>
VariableGaugeMean.streamPotential d a b (M n) (VariableGaugeMean.qLength coord) v (f n)
theorem
NavierStokes.MeanStageRegularity.MovingField.divideRadius
{coord a b : ℝ}
{U : LocalSignedRequest.SlowRegion coord}
{f : Scalar}
(hf : GaugeMomentBalances.MovingField U a b f)
(ha : 0 < a)
(hab : a < b)
:
GaugeMomentBalances.MovingField U a b fun (n : ℕ) => PressureStream.divideRadius (f n)
theorem
NavierStokes.MeanStageRegularity.MovingField.streamBeta
{coord a b : ℝ}
{U : LocalSignedRequest.SlowRegion coord}
{f : Scalar}
(hf : GaugeMomentBalances.MovingField U a b f)
(ε : ℕ → ℝ)
(w : Plane × Plane)
:
GaugeMomentBalances.MovingField U a b fun (n : ℕ) => PressureStream.streamBeta (ε n • w) (f n)
theorem
NavierStokes.MeanStageRegularity.MovingField.streamGamma
{coord a b : ℝ}
{U : LocalSignedRequest.SlowRegion coord}
{f : Scalar}
(hf : GaugeMomentBalances.MovingField U a b f)
(ha : 0 < a)
(hab : a < b)
(d : ℝ)
(M : ℕ → ℝ)
(v : Plane)
:
GaugeMomentBalances.MovingField U a b fun (n : ℕ) =>
PressureStream.streamGamma (PressureStream.physicalSpeed d (M n)) (0, v) (f n)
theorem
NavierStokes.MeanStageRegularity.temporalIncrement_moving
{coord : ℝ}
{U : LocalSignedRequest.SlowRegion coord}
{g : VariableGaugeMean.GaugeData Plane}
{c : CorrectionState.Context Point}
{u : CorrectionState.State Point}
(H : MeanStateRegularity.PrimitiveData U g.radial.inner g.radial.outer c u)
(ha : 0 < g.radial.inner)
(hd : 0 < g.radial.exponent)
(hell : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength coord)
(hfixed : (VariableGaugeMean.reconstructState g c u).pressure = u.pressure)
(h : ℝ)
(index : ℕ → ℕ)
(axial : Plane × Plane)
:
MeanStateRegularity.MovingTriple U g.radial.inner g.radial.outer
(VariableGaugeMean.temporalIncrementState g h index axial c u)
Actual stream-based temporal coefficients, including the radial component and all radii.
theorem
NavierStokes.MeanStageRegularity.temporalStage_primitive
{coord : ℝ}
{U : LocalSignedRequest.SlowRegion coord}
{g : VariableGaugeMean.GaugeData Plane}
{c : CorrectionState.Context Point}
{u : CorrectionState.State Point}
(H : MeanStateRegularity.PrimitiveData U g.radial.inner g.radial.outer c u)
(ha : 0 < g.radial.inner)
(hd : 0 < g.radial.exponent)
(hell : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength coord)
(hfixed : (VariableGaugeMean.reconstructState g c u).pressure = u.pressure)
(h : ℝ)
(index : ℕ → ℕ)
(axial : Plane × Plane)
:
MeanStateRegularity.PrimitiveData U g.radial.inner g.radial.outer c
(VariableGaugeMean.temporalStageState g h index axial c u)
theorem
NavierStokes.MeanStageRegularity.temporalStage_reconstructed
(g : VariableGaugeMean.GaugeData Plane)
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
(h : ℝ)
(index : ℕ → ℕ)
(axial : Plane × Plane)
:
VariableGaugeMean.reconstructState g c (VariableGaugeMean.temporalStageState g h index axial c u) = VariableGaugeMean.temporalStageState g h index axial c u
theorem
NavierStokes.MeanStageRegularity.temporalStage_preserves
{coord : ℝ}
{U : LocalSignedRequest.SlowRegion coord}
{g : VariableGaugeMean.GaugeData Plane}
{c : CorrectionState.Context Point}
{u : CorrectionState.State Point}
(H : MeanStateRegularity.PrimitiveData U g.radial.inner g.radial.outer c u)
(ha : 0 < g.radial.inner)
(hd : 0 < g.radial.exponent)
(hell : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength coord)
(hfixed : (VariableGaugeMean.reconstructState g c u).pressure = u.pressure)
(h : ℝ)
(index : ℕ → ℕ)
(axial : Plane × Plane)
:
MeanStateRegularity.PrimitiveData U g.radial.inner g.radial.outer c
(VariableGaugeMean.temporalStageState g h index axial c u) ∧ VariableGaugeMean.reconstructState g c (VariableGaugeMean.temporalStageState g h index axial c u) = VariableGaugeMean.temporalStageState g h index axial c u
The primitive invariant and actual pressure reconstruction are both available for the next stage.
The measured debt remains an actual smooth input to rank repair #
theorem
NavierStokes.MeanStageRegularity.debt_smooth
{coord a b : ℝ}
{U : LocalSignedRequest.SlowRegion coord}
{c : CorrectionState.Context Point}
{u : CorrectionState.State Point}
(H : MeanStateRegularity.PrimitiveData U a b c u)
(ha : 0 < a)
(hab : a < b)
(n : ℕ)
:
ContDiffOn ℝ (↑⊤) (CorrectionState.debt c u n) U.carrier
theorem
NavierStokes.MeanStageRegularity.rankGeometry_for_state
{coord a b : ℝ}
{U : LocalSignedRequest.SlowRegion coord}
{g : VariableGaugeMean.GaugeData Plane}
{r : CorrectionState.RankData Plane}
{c : CorrectionState.Context Point}
{u v : CorrectionState.State Point}
(H : MeanStateRegularity.PrimitiveData U a b c u)
(ha : 0 < a)
(hab : a < b)
(hg : LocalRankDefect.RankGeometry g r U.carrier c v)
:
LocalRankDefect.RankGeometry g r U.carrier c u
The fixed rank geometry can be reused at a new state. Its only state-dependent analytic field, smoothness of the measured debt, is reproved from that state's primitive invariant.
theorem
NavierStokes.MeanStageRegularity.rankDesired_moving
{coord : ℝ}
{U : LocalSignedRequest.SlowRegion coord}
{g : VariableGaugeMean.GaugeData Plane}
{r : CorrectionState.RankData Plane}
{c : CorrectionState.Context Point}
{u : CorrectionState.State Point}
(hg : LocalRankDefect.RankGeometry g r U.carrier c u)
(hell : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength coord)
:
GaugeMomentBalances.MovingField U g.radial.inner g.radial.outer fun (n : ℕ) =>
MeanRankUpdate.slowLift (CorrectionState.rankDesiredAxial r c u n)
The actual desired rank source has support inside the original moving gauge, using its proved reserved-patch support and enclosure.
theorem
NavierStokes.MeanStageRegularity.rankAngular_moving
{coord : ℝ}
{U : LocalSignedRequest.SlowRegion coord}
{g : VariableGaugeMean.GaugeData Plane}
{r : CorrectionState.RankData Plane}
{c : CorrectionState.Context Point}
{u : CorrectionState.State Point}
(hg : LocalRankDefect.RankGeometry g r U.carrier c u)
(hell : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength coord)
(axial : Plane × Plane)
:
GaugeMomentBalances.MovingField U g.radial.inner g.radial.outer
(VariableGaugeMean.rankIncrementState g r axial c u).angular
theorem
NavierStokes.MeanStageRegularity.rankIncrement_moving
{coord : ℝ}
{U : LocalSignedRequest.SlowRegion coord}
{g : VariableGaugeMean.GaugeData Plane}
{r : CorrectionState.RankData Plane}
{c : CorrectionState.Context Point}
{u : CorrectionState.State Point}
(hg : LocalRankDefect.RankGeometry g r U.carrier c u)
(hell : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength coord)
(axial : Plane × Plane)
:
MeanStateRegularity.MovingTriple U g.radial.inner g.radial.outer (VariableGaugeMean.rankIncrementState g r axial c u)
theorem
NavierStokes.MeanStageRegularity.rankStage_primitive
{coord : ℝ}
{U : LocalSignedRequest.SlowRegion coord}
{g : VariableGaugeMean.GaugeData Plane}
{r : CorrectionState.RankData Plane}
{c : CorrectionState.Context Point}
{u : CorrectionState.State Point}
(H : MeanStateRegularity.PrimitiveData U g.radial.inner g.radial.outer c u)
(hg : LocalRankDefect.RankGeometry g r U.carrier c u)
(hell : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength coord)
(axial : Plane × Plane)
:
MeanStateRegularity.PrimitiveData U g.radial.inner g.radial.outer c (VariableGaugeMean.rankStageState g r axial c u)
theorem
NavierStokes.MeanStageRegularity.rankStage_reconstructed
(g : VariableGaugeMean.GaugeData Plane)
(r : CorrectionState.RankData Plane)
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
(axial : Plane × Plane)
:
VariableGaugeMean.reconstructState g c (VariableGaugeMean.rankStageState g r axial c u) = VariableGaugeMean.rankStageState g r axial c u
theorem
NavierStokes.MeanStageRegularity.rankStage_preserves
{coord : ℝ}
{U : LocalSignedRequest.SlowRegion coord}
{g : VariableGaugeMean.GaugeData Plane}
{r : CorrectionState.RankData Plane}
{c : CorrectionState.Context Point}
{u : CorrectionState.State Point}
(H : MeanStateRegularity.PrimitiveData U g.radial.inner g.radial.outer c u)
(hg : LocalRankDefect.RankGeometry g r U.carrier c u)
(hell : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength coord)
(axial : Plane × Plane)
:
MeanStateRegularity.PrimitiveData U g.radial.inner g.radial.outer c (VariableGaugeMean.rankStageState g r axial c u) ∧ VariableGaugeMean.reconstructState g c (VariableGaugeMean.rankStageState g r axial c u) = VariableGaugeMean.rankStageState g r axial c u
theorem
NavierStokes.MeanStageRegularity.rankStage_from_geometry
{coord : ℝ}
{U : LocalSignedRequest.SlowRegion coord}
{g : VariableGaugeMean.GaugeData Plane}
{r : CorrectionState.RankData Plane}
{c : CorrectionState.Context Point}
{u v : CorrectionState.State Point}
(H : MeanStateRegularity.PrimitiveData U g.radial.inner g.radial.outer c u)
(hg : LocalRankDefect.RankGeometry g r U.carrier c v)
(hell : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength coord)
(axial : Plane × Plane)
:
MeanStateRegularity.PrimitiveData U g.radial.inner g.radial.outer c (VariableGaugeMean.rankStageState g r axial c u) ∧ VariableGaugeMean.reconstructState g c (VariableGaugeMean.rankStageState g r axial c u) = VariableGaugeMean.rankStageState g r axial c u
An earlier geometric certificate suffices. The new state's debt is computed and its smoothness is derived before performing rank repair.
theorem
NavierStokes.MeanStageRegularity.temporal_rank_preserves
{coord : ℝ}
{U : LocalSignedRequest.SlowRegion coord}
{g : VariableGaugeMean.GaugeData Plane}
{r : CorrectionState.RankData Plane}
{c : CorrectionState.Context Point}
{u v : CorrectionState.State Point}
(H : MeanStateRegularity.PrimitiveData U g.radial.inner g.radial.outer c u)
(hg : LocalRankDefect.RankGeometry g r U.carrier c v)
(hell : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength coord)
(hfixed : (VariableGaugeMean.reconstructState g c u).pressure = u.pressure)
(h : ℝ)
(index : ℕ → ℕ)
(axialTime axialRank : Plane × Plane)
:
have next :=
VariableGaugeMean.rankStageState g r axialRank c (VariableGaugeMean.temporalStageState g h index axialTime c u);
MeanStateRegularity.PrimitiveData U g.radial.inner g.radial.outer c next ∧ VariableGaugeMean.reconstructState g c next = next
The two literal mean stages preserve the same primitive invariant. The rank geometry is refreshed from the actual temporal output before the rank correction is formed.