Coherence of the actual five-row rank correction

The debt is recomputed from the complete incoming state. Primitive chart data and the shared normalized inverse are transported before applying the actual variable-gauge stream and pressure constructors.

theorem NavierStokes.RankStateCoherence.sourceMoment_fiber {S : Type} (m : ℕ) (f g : PressureStream.Lift S → ℝ) (s : S) (he : ∀ (R : ℝ) (Y : PressureStream.Plane), f (R, s, Y) = g (R, s, Y)) : MeanChartCompatibility.sourceMoment m f s = MeanChartCompatibility.sourceMoment m g s

theorem NavierStokes.RankStateCoherence.sourceMoment_on {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] {l a : ℝ} (hl : 0 < l) (P : S ≃L[ℝ] T) (k m : ℕ) {V : Set S} {U : Set T} (hU : IsOpen U) (hmap : Set.MapsTo (⇑P) V U) {f : PressureStream.Lift S → ℝ} {g : PressureStream.Lift T → ℝ} (he : PhysicalResidualNaturality.ScalarOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.chartEquiv l ⋯ P k) a f g) (hg : ContDiffOn ℝ (↑⊤) g (PhysicalMeanDomain.slowDomain U)) (hp : PhysicalMeanDomain.PeriodicOn U g) {s : S} (hs : s ∈ V) : MeanChartCompatibility.sourceMoment m f s = a / l ^ (m + 1) * MeanChartCompatibility.sourceMoment m g (P s)

The whole-fiber moment of a compatible field, using only local slow regularity and the actual torus covering.

structure NavierStokes.RankStateCoherence.DebtRegular {T : Type} [NormedAddCommGroup T] [NormedSpace ℝ T] (U : Set T) (C : CorrectionState.Context (PressureStream.Lift T)) (u : CorrectionState.State (PressureStream.Lift T)) (n : ℕ) : Prop

Reference fields needed for the actual three measured debts.

• radial : ContDiffOn ℝ (↑⊤) (u.gr C n) (PhysicalMeanDomain.slowDomain U)
• angular : ContDiffOn ℝ (↑⊤) ((MeanIncrementBounds.thetaAxial C.base u.mean + u.covariance 2 1) n) (PhysicalMeanDomain.slowDomain U)
• axial : ContDiffOn ℝ (↑⊤) ((MeanIncrementBounds.axialAxial C.base u.mean + u.covariance 2 2) n) (PhysicalMeanDomain.slowDomain U)
• radial_periodic : PhysicalMeanDomain.PeriodicOn U (u.gr C n)
• angular_periodic : PhysicalMeanDomain.PeriodicOn U ((MeanIncrementBounds.thetaAxial C.base u.mean + u.covariance 2 1) n)
• axial_periodic : PhysicalMeanDomain.PeriodicOn U ((MeanIncrementBounds.axialAxial C.base u.mean + u.covariance 2 2) n)

theorem NavierStokes.RankStateCoherence.measured_debt_on {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] {l c : ℝ} (hl : 0 < l) (P : S ≃L[ℝ] T) (k : ℕ) {V : Set S} {U : Set T} (hV : IsOpen V) (hU : IsOpen U) (hmap : Set.MapsTo (⇑P) V U) {C : CorrectionState.Context (PressureStream.Lift S)} {Cr : CorrectionState.Context (PressureStream.Lift T)} {u : CorrectionState.State (PressureStream.Lift S)} {ur : CorrectionState.State (PressureStream.Lift T)} {n nr : ℕ} (H : PhysicalResidualNaturality.StateOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.chartEquiv l ⋯ P k) c l u ur n nr) (G : PhysicalResidualNaturality.ContextOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.chartEquiv l ⋯ P k) c l C Cr n nr) (R : DebtRegular U Cr ur nr) {s : S} (hs : s ∈ V) : CorrectionState.debt C u n s = MeanRankUpdate.scaleDebt l⁻¹ c (CorrectionState.debt Cr ur nr (P s))

All three debts are measured from the full base and state. The powers are pressure c², angular c²/l³, and axial c²/l².

structure NavierStokes.RankStateCoherence.RankOn {S T : Type} (V : Set S) (P : S → T) (l c : ℝ) (r : CorrectionState.RankData S) (rr : CorrectionState.RankData T) (n nr : ℕ) : Prop

Primitive rank data use one dimensionless kernel. No rank-output or debt equality is a field of this structure.

• lambda : r.lambda = rr.lambda
• inner : r.inner = rr.inner
• outer : r.outer = rr.outer
• length (s : S) : s ∈ V → r.length n s = l⁻¹ * rr.length nr (P s)
• velocity (s : S) : s ∈ V → r.velocity n s = c * rr.velocity nr (P s)
• coefficient (s : S) : s ∈ V → r.coefficient n s = rr.coefficient nr (P s)
• reference_length (s : S) : s ∈ V → rr.length nr (P s) ≠ 0
• reference_velocity (s : S) : s ∈ V → rr.velocity nr (P s) ≠ 0

theorem NavierStokes.RankStateCoherence.RankOn.angular {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] {V : Set S} {P : S → T} {l c : ℝ} (hl : l ≠ 0) (hc : c ≠ 0) {r : CorrectionState.RankData S} {rr : CorrectionState.RankData T} {n nr : ℕ} (H : RankOn V P l c r rr n nr) {C : CorrectionState.Context (PressureStream.Lift S)} {Cr : CorrectionState.Context (PressureStream.Lift T)} {u : CorrectionState.State (PressureStream.Lift S)} {ur : CorrectionState.State (PressureStream.Lift T)} {s : S} (hs : s ∈ V) (hd : CorrectionState.debt C u n s = MeanRankUpdate.scaleDebt l⁻¹ c (CorrectionState.debt Cr ur nr (P s))) (R : ℝ) : CorrectionState.rankAngular r C u n (R, s) = c * CorrectionState.rankAngular rr Cr ur nr (l * R, P s)

theorem NavierStokes.RankStateCoherence.RankOn.desiredAxial {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] {V : Set S} {P : S → T} {l c : ℝ} (hl : l ≠ 0) (hc : c ≠ 0) {r : CorrectionState.RankData S} {rr : CorrectionState.RankData T} {n nr : ℕ} (H : RankOn V P l c r rr n nr) {C : CorrectionState.Context (PressureStream.Lift S)} {Cr : CorrectionState.Context (PressureStream.Lift T)} {u : CorrectionState.State (PressureStream.Lift S)} {ur : CorrectionState.State (PressureStream.Lift T)} {s : S} (hs : s ∈ V) (hd : CorrectionState.debt C u n s = MeanRankUpdate.scaleDebt l⁻¹ c (CorrectionState.debt Cr ur nr (P s))) (R : ℝ) : CorrectionState.rankDesiredAxial r C u n (R, s) = c * CorrectionState.rankDesiredAxial rr Cr ur nr (l * R, P s)

theorem NavierStokes.RankStateCoherence.rankAngular_on {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] {l c : ℝ} (hl : 0 < l) (hc : c ≠ 0) (P : S ≃L[ℝ] T) (k : ℕ) {V : Set S} {U : Set T} (hV : IsOpen V) (hU : IsOpen U) (hmap : Set.MapsTo (⇑P) V U) {C : CorrectionState.Context (PressureStream.Lift S)} {Cr : CorrectionState.Context (PressureStream.Lift T)} {u : CorrectionState.State (PressureStream.Lift S)} {ur : CorrectionState.State (PressureStream.Lift T)} {n nr : ℕ} (H : PhysicalResidualNaturality.StateOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.chartEquiv l ⋯ P k) c l u ur n nr) (G : PhysicalResidualNaturality.ContextOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.chartEquiv l ⋯ P k) c l C Cr n nr) (R : DebtRegular U Cr ur nr) {r : CorrectionState.RankData S} {rr : CorrectionState.RankData T} (K : RankOn V (⇑P) l c r rr n nr) : PhysicalResidualNaturality.ScalarOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.chartEquiv l ⋯ P k) c (MeanRankUpdate.slowLift (CorrectionState.rankAngular r C u n)) (MeanRankUpdate.slowLift (CorrectionState.rankAngular rr Cr ur nr))

theorem NavierStokes.RankStateCoherence.rankDesiredAxial_on {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] {l c : ℝ} (hl : 0 < l) (hc : c ≠ 0) (P : S ≃L[ℝ] T) (k : ℕ) {V : Set S} {U : Set T} (hV : IsOpen V) (hU : IsOpen U) (hmap : Set.MapsTo (⇑P) V U) {C : CorrectionState.Context (PressureStream.Lift S)} {Cr : CorrectionState.Context (PressureStream.Lift T)} {u : CorrectionState.State (PressureStream.Lift S)} {ur : CorrectionState.State (PressureStream.Lift T)} {n nr : ℕ} (H : PhysicalResidualNaturality.StateOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.chartEquiv l ⋯ P k) c l u ur n nr) (G : PhysicalResidualNaturality.ContextOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.chartEquiv l ⋯ P k) c l C Cr n nr) (R : DebtRegular U Cr ur nr) {r : CorrectionState.RankData S} {rr : CorrectionState.RankData T} (K : RankOn V (⇑P) l c r rr n nr) : PhysicalResidualNaturality.ScalarOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.chartEquiv l ⋯ P k) c (MeanRankUpdate.slowLift (CorrectionState.rankDesiredAxial r C u n)) (MeanRankUpdate.slowLift (CorrectionState.rankDesiredAxial rr Cr ur nr))

theorem NavierStokes.RankStateCoherence.rankPotential_on {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] {l c : ℝ} (hl : 0 < l) (hc : c ≠ 0) (P : S ≃L[ℝ] T) (k : ℕ) {V : Set S} {U : Set T} (hV : IsOpen V) (hU : IsOpen U) (hmap : Set.MapsTo (⇑P) V U) {C : CorrectionState.Context (PressureStream.Lift S)} {Cr : CorrectionState.Context (PressureStream.Lift T)} {u : CorrectionState.State (PressureStream.Lift S)} {ur : CorrectionState.State (PressureStream.Lift T)} {n nr : ℕ} (H : PhysicalResidualNaturality.StateOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.chartEquiv l ⋯ P k) c l u ur n nr) (G : PhysicalResidualNaturality.ContextOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.chartEquiv l ⋯ P k) c l C Cr n nr) (R : DebtRegular U Cr ur nr) {r : CorrectionState.RankData S} {rr : CorrectionState.RankData T} (K : RankOn V (⇑P) l c r rr n nr) {g : VariableGaugeMean.GaugeData S} {gr : VariableGaugeMean.GaugeData T} (J : GaugeStateCoherence.GaugeOn V l (↑P) k g gr n nr) (F : LocalRankDefect.RankGeometry gr rr U Cr ur) : PhysicalResidualNaturality.ScalarOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.chartEquiv l ⋯ P k) (c / l) (VariableGaugeMean.rankPotential g r C u n) (VariableGaugeMean.rankPotential gr rr Cr ur nr)

Naturality of the literal moving-gauge rank potential. Its source is the already constructed five-row inverse of the measured debt.

theorem NavierStokes.RankStateCoherence.rankIncrementState_on {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] {l c : ℝ} (hl : 0 < l) (hc : c ≠ 0) (P : S ≃L[ℝ] T) (k : ℕ) {V : Set S} {U : Set T} (hV : IsOpen V) (hU : IsOpen U) (hmap : Set.MapsTo (⇑P) V U) {C : CorrectionState.Context (PressureStream.Lift S)} {Cr : CorrectionState.Context (PressureStream.Lift T)} {u : CorrectionState.State (PressureStream.Lift S)} {ur : CorrectionState.State (PressureStream.Lift T)} {n nr : ℕ} (H : PhysicalResidualNaturality.StateOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.chartEquiv l ⋯ P k) c l u ur n nr) (G : PhysicalResidualNaturality.ContextOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.chartEquiv l ⋯ P k) c l C Cr n nr) (R : DebtRegular U Cr ur nr) {r : CorrectionState.RankData S} {rr : CorrectionState.RankData T} (K : RankOn V (⇑P) l c r rr n nr) {g : VariableGaugeMean.GaugeData S} {gr : VariableGaugeMean.GaugeData T} (J : GaugeStateCoherence.GaugeOn V l (↑P) k g gr n nr) (F : LocalRankDefect.RankGeometry gr rr U Cr ur) (axial : S × PressureStream.Plane) (axialr : T × PressureStream.Plane) (ha : ((↑P).prodMap (TemporalMeanUpdate.coverMap k)) (C.operators.epsilon n • axial) = l • Cr.operators.epsilon nr • axialr) : PhysicalResidualNaturality.TripleOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.chartEquiv l ⋯ P k) c (VariableGaugeMean.rankIncrementState g r axial C u) (VariableGaugeMean.rankIncrementState gr rr axialr Cr ur) n nr

All three components are the actual stream reconstruction of the rank correction. No output-increment coherence is assumed.

noncomputable def NavierStokes.RankStateCoherence.rankAddedState {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (g : VariableGaugeMean.GaugeData S) (r : CorrectionState.RankData S) (axial : S × PressureStream.Plane) (C : CorrectionState.Context (PressureStream.Lift S)) (u : CorrectionState.State (PressureStream.Lift S)) : CorrectionState.State (PressureStream.Lift S)

The actual state before the rank step's pressure is reconstructed.

Equations

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

theorem NavierStokes.RankStateCoherence.add_mean_on {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {V : Set D} {e : D ≃L[ℝ] E} {c l : ℝ} {u : CorrectionState.State D} {ur : CorrectionState.State E} {n nr : ℕ} (H : PhysicalResidualNaturality.StateOn V e c l u ur n nr) {m : MeanIncrementBounds.Triple D} {mr : MeanIncrementBounds.Triple E} (hm : PhysicalResidualNaturality.TripleOn V e c m mr n nr) : PhysicalResidualNaturality.StateOn V e c l (u.addIncrement m 0 0 0 CorrectionState.ExcludedErrors.zero) (ur.addIncrement mr 0 0 0 CorrectionState.ExcludedErrors.zero) n nr

theorem NavierStokes.RankStateCoherence.rankStageState_on {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] {l c : ℝ} (hl : 0 < l) (hc : c ≠ 0) (P : S ≃L[ℝ] T) (k : ℕ) {V : Set S} {U : Set T} (hV : IsOpen V) (hU : IsOpen U) (hmap : Set.MapsTo (⇑P) V U) {C : CorrectionState.Context (PressureStream.Lift S)} {Cr : CorrectionState.Context (PressureStream.Lift T)} {u : CorrectionState.State (PressureStream.Lift S)} {ur : CorrectionState.State (PressureStream.Lift T)} {n nr : ℕ} (H : PhysicalResidualNaturality.StateOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.chartEquiv l ⋯ P k) c l u ur n nr) (G : PhysicalResidualNaturality.ContextOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.chartEquiv l ⋯ P k) c l C Cr n nr) (R : DebtRegular U Cr ur nr) {r : CorrectionState.RankData S} {rr : CorrectionState.RankData T} (K : RankOn V (⇑P) l c r rr n nr) {g : VariableGaugeMean.GaugeData S} {gr : VariableGaugeMean.GaugeData T} (J : GaugeStateCoherence.GaugeOn V l (↑P) k g gr n nr) (F : LocalRankDefect.RankGeometry gr rr U Cr ur) (axial : S × PressureStream.Plane) (axialr : T × PressureStream.Plane) (ha : ((↑P).prodMap (TemporalMeanUpdate.coverMap k)) (C.operators.epsilon n • axial) = l • Cr.operators.epsilon nr • axialr) (hf : ContDiffOn ℝ (↑⊤) ((rankAddedState gr rr axialr Cr ur).gr Cr nr) (PhysicalMeanDomain.slowDomain U)) (hp : PhysicalMeanDomain.PeriodicOn U ((rankAddedState gr rr axialr Cr ur).gr Cr nr)) (hs : VariableGaugeMean.SupportedGauge gr.radial.inner gr.radial.outer (gr.length nr) U ((rankAddedState gr rr axialr Cr ur).gr Cr nr)) : PhysicalResidualNaturality.StateOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.chartEquiv l ⋯ P k) c l (VariableGaugeMean.rankStageState g r axial C u) (VariableGaugeMean.rankStageState gr rr axialr Cr ur) n nr

Coherence survives the complete rank step, including the pressure recomputed from the new actual radial residual.

The actual normalized data used by the recurrence

theorem NavierStokes.RankStateCoherence.normalized_rank_on {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (B lam a b : ℝ) (n m : ℕ) {V : Set PressureStream.Plane} (hV : ∀ s ∈ V, 0 < s.1) : RankOn V (⇑(GaugeStateCoherence.bandSlowEquiv h n m)) (GaugeStateCoherence.bandScale n m) (GaugeStateCoherence.bandVelocityScale h n m) (RankStateBounds.normalizedData (2 * h) (CoordinateAlgebra.A h) B lam a b) (RankStateBounds.normalizedData (2 * h) (CoordinateAlgebra.A h) B lam a b) n m

theorem NavierStokes.RankStateCoherence.normalized_rank_on_of_parameters {h B : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (n m : ℕ) {V U : Set PressureStream.Plane} (htime : ∀ s ∈ V, 0 < s.1) (hmap : Set.MapsTo (⇑(GaugeStateCoherence.bandSlowEquiv h n m)) V U) {r rr : CorrectionState.RankData PressureStream.Plane} (hr : RankStateBounds.NormalizedParameters (2 * h) (CoordinateAlgebra.A h) B r V) (hrr : RankStateBounds.NormalizedParameters (2 * h) (CoordinateAlgebra.A h) B rr U) (hlam : r.lambda = rr.lambda) (ha : r.inner = rr.inner) (hb : r.outer = rr.outer) : RankOn V (⇑(GaugeStateCoherence.bandSlowEquiv h n m)) (GaugeStateCoherence.bandScale n m) (GaugeStateCoherence.bandVelocityScale h n m) r rr n m

All five rows, against the full base

theorem NavierStokes.RankStateCoherence.fiveRows_chart {l c : ℝ} (hl : 0 < l) {v g f z vr gr fr zr : ℝ → ℝ} {d dr : MeanRankUpdate.Debt} (H : FiveRowRank.FiveRows vr gr dr fr zr) (hv : ∀ (R : ℝ), v R = c * vr (l * R)) (hg : ∀ (R : ℝ), g R = c * gr (l * R)) (hf : ∀ (R : ℝ), f R = c * fr (l * R)) (hz : ∀ (R : ℝ), z R = c * zr (l * R)) (hd : d = MeanRankUpdate.scaleDebt l⁻¹ c dr) : FiveRowRank.FiveRows v g d f z

theorem NavierStokes.RankStateCoherence.scalarOn_slice {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] {l c : ℝ} (hl : 0 < l) (P : S ≃L[ℝ] T) (k : ℕ) {V : Set S} {f : PressureStream.Lift S → ℝ} {g : PressureStream.Lift T → ℝ} (H : PhysicalResidualNaturality.ScalarOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.chartEquiv l ⋯ P k) c f g) {s : S} (hs : s ∈ V) (R : ℝ) : f (R, s, 0) = c * g (l * R, P s, 0)

theorem NavierStokes.RankStateCoherence.rankIncrementState_fiveRows_on {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] [FiniteDimensional ℝ T] {l c : ℝ} (hl : 0 < l) (hc : c ≠ 0) (P : S ≃L[ℝ] T) (k : ℕ) {V : Set S} {U : Set T} (hV : IsOpen V) (hU : IsOpen U) (hmap : Set.MapsTo (⇑P) V U) {C : CorrectionState.Context (PressureStream.Lift S)} {Cr : CorrectionState.Context (PressureStream.Lift T)} {u : CorrectionState.State (PressureStream.Lift S)} {ur : CorrectionState.State (PressureStream.Lift T)} {n nr : ℕ} (H : PhysicalResidualNaturality.StateOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.chartEquiv l ⋯ P k) c l u ur n nr) (G : PhysicalResidualNaturality.ContextOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.chartEquiv l ⋯ P k) c l C Cr n nr) (R : DebtRegular U Cr ur nr) {r : CorrectionState.RankData S} {rr : CorrectionState.RankData T} (K : RankOn V (⇑P) l c r rr n nr) {g : VariableGaugeMean.GaugeData S} {gr : VariableGaugeMean.GaugeData T} (J : GaugeStateCoherence.GaugeOn V l (↑P) k g gr n nr) (F : LocalRankDefect.RankGeometry gr rr U Cr ur) (axial : S × PressureStream.Plane) (axialr : T × PressureStream.Plane) (ha : ((↑P).prodMap (TemporalMeanUpdate.coverMap k)) (C.operators.epsilon n • axial) = l • Cr.operators.epsilon nr • axialr) {lo hi : ℝ} (hlo : 0 < lo) (hlohi : lo < hi) (hleft : ∀ (m : ℕ), ∀ t ∈ U, lo ≤ rr.length m t * rr.inner) (hright : ∀ (m : ℕ), ∀ t ∈ U, rr.length m t * rr.outer ≤ hi) {s : S} (hs : s ∈ V) : FiveRowRank.FiveRows (DefectIncrementBounds.slowSlice C.base.angular n s) (DefectIncrementBounds.slowSlice C.base.axial n s) (CorrectionState.debt C u n s) (DefectIncrementBounds.slowSlice (VariableGaugeMean.rankIncrementState g r axial C u).angular n s) (DefectIncrementBounds.slowSlice (VariableGaugeMean.rankIncrementState g r axial C u).axial n s)

The five-row conclusion is transported from the actual reference rank solve. Both background slices here are the complete stored base.

theorem NavierStokes.RankStateCoherence.band_axial_vector (h : ℝ) (n m k : ℕ) : ((↑(GaugeStateCoherence.bandSlowEquiv h n m)).prodMap (TemporalMeanUpdate.coverMap k)) (ChartScales.Q n ^ h • ((0, 1), 0)) = GaugeStateCoherence.bandScale n m • ChartScales.Q m ^ h • ((0, 1), 0)

The physical axial unit has the required chart differential, with the actual viscosity/axial coefficient Q^h.

theorem NavierStokes.RankStateCoherence.normalized_rankStageState_on {h d a b M B lam ra rb : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hab : a < b) (index : ℕ → ℕ) (n m k : ℕ) (hi : index n + k = index m) {V U : Set PressureStream.Plane} (hV : IsOpen V) (hU : IsOpen U) (htime : ∀ s ∈ V, 0 < s.1) (hmap : Set.MapsTo (⇑(GaugeStateCoherence.bandSlowEquiv h n m)) V U) (C Cr : CorrectionState.Context (PressureStream.Lift PressureStream.Plane)) (u ur : CorrectionState.State (PressureStream.Lift PressureStream.Plane)) (H : PhysicalResidualNaturality.StateOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.bandChartEquiv h n m k) (GaugeStateCoherence.bandVelocityScale h n m) (GaugeStateCoherence.bandScale n m) u ur n m) (G : PhysicalResidualNaturality.ContextOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.bandChartEquiv h n m k) (GaugeStateCoherence.bandVelocityScale h n m) (GaugeStateCoherence.bandScale n m) C Cr n m) (R : DebtRegular U Cr ur m) (F : LocalRankDefect.RankGeometry (VariableGaugeMean.similarityGauge h d a b M hab index) (RankStateBounds.normalizedData (2 * h) (CoordinateAlgebra.A h) B lam ra rb) U Cr ur) (heps : C.operators.epsilon n = ChartScales.Q n ^ h) (hepsr : Cr.operators.epsilon m = ChartScales.Q m ^ h) (hf : ContDiffOn ℝ (↑⊤) ((rankAddedState (VariableGaugeMean.similarityGauge h d a b M hab index) (RankStateBounds.normalizedData (2 * h) (CoordinateAlgebra.A h) B lam ra rb) ((0, 1), 0) Cr ur).gr Cr m) (PhysicalMeanDomain.slowDomain U)) (hp : PhysicalMeanDomain.PeriodicOn U ((rankAddedState (VariableGaugeMean.similarityGauge h d a b M hab index) (RankStateBounds.normalizedData (2 * h) (CoordinateAlgebra.A h) B lam ra rb) ((0, 1), 0) Cr ur).gr Cr m)) (hs : VariableGaugeMean.SupportedGauge a b (VariableGaugeMean.qLength (2 * h)) U ((rankAddedState (VariableGaugeMean.similarityGauge h d a b M hab index) (RankStateBounds.normalizedData (2 * h) (CoordinateAlgebra.A h) B lam ra rb) ((0, 1), 0) Cr ur).gr Cr m)) : PhysicalResidualNaturality.StateOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.bandChartEquiv h n m k) (GaugeStateCoherence.bandVelocityScale h n m) (GaugeStateCoherence.bandScale n m) (VariableGaugeMean.rankStageState (VariableGaugeMean.similarityGauge h d a b M hab index) (RankStateBounds.normalizedData (2 * h) (CoordinateAlgebra.A h) B lam ra rb) ((0, 1), 0) C u) (VariableGaugeMean.rankStageState (VariableGaugeMean.similarityGauge h d a b M hab index) (RankStateBounds.normalizedData (2 * h) (CoordinateAlgebra.A h) B lam ra rb) ((0, 1), 0) Cr ur) n m

Concrete normalized rank stage at the common cover. Every rank parameter and axial scaling law is derived from the shared data.