Full-vector bounds for the actual moving-gauge excluded aliases

The pressure source class is derived from the primitive base, operators, mean, and covariance. Scalar alias estimates are then applied to that actual source and lifted through fixed linear component maps. All regularity is supplied by the incoming primitive fields and the genuine pressure reconstruction, not by a hypothesis on an alias output.

theorem NavierStokes.GaugeExcludedBounds.radialSource_mem {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {o : MeanIncrementBounds.Operators D} {base mean : MeanIncrementBounds.Triple D} {κ γ : ℝ} (ho : MeanIncrementBounds.OperatorBounds s o κ) (hb : MeanIncrementBounds.BaseBounds s base) (hm : MeanIncrementBounds.CumulativeBounds s mean) (W : Fin 3 → Fin 3 → MeanIncrementBounds.Field D) (hW : ∀ (i j : Fin 3), WeightedClasses.MeanClass s γ (W i j)) : WeightedClasses.MeanClass s (min (9 / 10) γ - 2 * κ) (MeanIncrementBounds.gr o base mean W)

An ordinary class for the literal radial forcing, before pressure reconstruction. No class of gr is an input.

theorem NavierStokes.GaugeExcludedBounds.state_gr_mem {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {c : CorrectionState.Context D} {u : CorrectionState.State D} {κ γ : ℝ} (ho : MeanIncrementBounds.OperatorBounds s c.operators κ) (hb : MeanIncrementBounds.BaseBounds s c.base) (hu : CorrectionState.CumulativeBounds s u) (hW : ∀ (i j : Fin 3), WeightedClasses.MeanClass s γ (u.covariance i j)) : WeightedClasses.MeanClass s (min (9 / 10) γ - 2 * κ) (u.gr c)

theorem NavierStokes.GaugeExcludedBounds.meanClass_unweighted {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {β : ℝ} {f : ℕ → D → E} (hf : WeightedClasses.MeanClass s β f) (hζ : ∀ x ∈ s.domain, s.zeta x ≤ 1) : WeightedClasses.UnweightedClass s β f

theorem NavierStokes.GaugeExcludedBounds.pressureAlias_axisymmetric {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (g : VariableGaugeMean.GaugeData S) (c : CorrectionState.Context (PressureStream.Lift S)) (u : CorrectionState.State (PressureStream.Lift S)) (n : ℕ) (z : PressureStream.Lift S) (θ : ℝ) : VariableGaugeMean.pressureAliasState g c u n (z, θ) = VariableGaugeMean.pressureAliasState g c u n (z, 0)

theorem NavierStokes.GaugeExcludedBounds.temporalAlias_axisymmetric {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (g : VariableGaugeMean.GaugeData S) (h : ℝ) (index : ℕ → ℕ) (c : CorrectionState.Context (PressureStream.Lift S)) (u : CorrectionState.State (PressureStream.Lift S)) (n : ℕ) (z : PressureStream.Lift S) (θ : ℝ) : VariableGaugeMean.temporalAliasState g h index c u n (z, θ) = VariableGaugeMean.temporalAliasState g h index c u n (z, 0)

theorem NavierStokes.GaugeExcludedBounds.pressureAlias_vector_mem {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {s : WeightedClasses.StripData (PressureStream.Lift S)} {β : ℝ} (g : VariableGaugeMean.GaugeData S) (c : CorrectionState.Context (PressureStream.Lift S)) (u : CorrectionState.State (PressureStream.Lift S)) (hf : WeightedClasses.MeanClass s β fun (n : ℕ) (z : PressureStream.Lift S) => VariableGaugeMean.pressureAliasState g c u n (z, 0) 0) : WeightedClasses.MeanClass s β fun (n : ℕ) (z : PressureStream.Lift S) => VariableGaugeMean.pressureAliasState g c u n (z, 0)

theorem NavierStokes.GaugeExcludedBounds.temporalAlias_vector_mem {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {s : WeightedClasses.StripData (PressureStream.Lift S)} {β : ℝ} (g : VariableGaugeMean.GaugeData S) (h : ℝ) (index : ℕ → ℕ) (c : CorrectionState.Context (PressureStream.Lift S)) (u : CorrectionState.State (PressureStream.Lift S)) (hf : WeightedClasses.MeanClass s β fun (n : ℕ) (z : PressureStream.Lift S) => VariableGaugeMean.temporalAliasState g h index c u n (z, 0) 2) : WeightedClasses.MeanClass s β fun (n : ℕ) (z : PressureStream.Lift S) => VariableGaugeMean.temporalAliasState g h index c u n (z, 0)

theorem NavierStokes.GaugeExcludedBounds.pressureAlias_angle_mem {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {s : WeightedClasses.StripData (PressureStream.Lift S)} {β : ℝ} (g : VariableGaugeMean.GaugeData S) (c : CorrectionState.Context (PressureStream.Lift S)) (u : CorrectionState.State (PressureStream.Lift S)) (hf : WeightedClasses.MeanClass s β fun (n : ℕ) (z : PressureStream.Lift S) => VariableGaugeMean.pressureAliasState g c u n (z, 0) 0) : WeightedClasses.MeanClass (HarmonicWaveInteraction.productStrip s) β (VariableGaugeMean.pressureAliasState g c u)

theorem NavierStokes.GaugeExcludedBounds.temporalAlias_angle_mem {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {s : WeightedClasses.StripData (PressureStream.Lift S)} {β : ℝ} (g : VariableGaugeMean.GaugeData S) (h : ℝ) (index : ℕ → ℕ) (c : CorrectionState.Context (PressureStream.Lift S)) (u : CorrectionState.State (PressureStream.Lift S)) (hf : WeightedClasses.MeanClass s β fun (n : ℕ) (z : PressureStream.Lift S) => VariableGaugeMean.temporalAliasState g h index c u n (z, 0) 2) : WeightedClasses.MeanClass (HarmonicWaveInteraction.productStrip s) β (VariableGaugeMean.temporalAliasState g h index c u)

theorem NavierStokes.GaugeExcludedBounds.movingStrip_zeta_le_one {coord a b cL cR : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (x : MeanStateRegularity.Point) : (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL).zeta x ≤ 1

@[reducible, inline]

noncomputable abbrev NavierStokes.GaugeExcludedBounds.actualStrip {a b h cL cR : ℝ} (U : LocalSignedRequest.SlowRegion (2 * h)) (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (hh : 0 < h) (L : ℕ → ℝ) (hL : ∀ (n : ℕ), 1 ≤ L n) : WeightedClasses.StripData MeanStateRegularity.Point

The actual moving strip, with the manuscript's band scale.

Equations

• NavierStokes.GaugeExcludedBounds.actualStrip U ha hcL hcR hh L hL = NavierStokes.LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR (NavierStokes.ChartScales.epsilon h) L ⋯ ⋯ hL

@[reducible, inline]

noncomputable abbrev NavierStokes.GaugeExcludedBounds.actualGauge (h a b Mbase : ℝ) (hab : a < b) (index : ℕ → ℕ) : VariableGaugeMean.GaugeData PressureStream.Plane

The actual moving pressure/stream gauge.

Equations

• NavierStokes.GaugeExcludedBounds.actualGauge h a b Mbase hab index = NavierStokes.VariableGaugeMean.similarityGauge h (NavierStokes.ChartScales.radialExponent h) a b Mbase hab index

@[reducible, inline]

abbrev NavierStokes.GaugeExcludedBounds.Point : Type

Point: an abbreviation for MeanStateRegularity.Point.

Equations

• NavierStokes.GaugeExcludedBounds.Point = NavierStokes.MeanStateRegularity.Point

theorem NavierStokes.GaugeExcludedBounds.pressureAliasState_mean_bounds {a b h Mbase cL cR : ℝ} (U : LocalSignedRequest.SlowRegion (2 * h)) (ha : 0 < a) (hab : a < b) (hcL : 0 < cL) (hcR : 0 < cR) (hh : 0 < h) (hM : Mbase ≠ 0) (index : ℕ → ℕ) (D : ℕ) (hgapLower : ∀ (n : ℕ), ChartScales.nativeIndex h n ≤ index n + D) (L : ℕ → ℝ) (hL : ∀ (n : ℕ), 1 ≤ L n) (hS : ∀ (n : ℕ), ChartScales.S n ≤ L n) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) {κ γ : ℝ} (H : MeanStateRegularity.PrimitiveData U a b c u) (ho : MeanIncrementBounds.OperatorBounds (actualStrip U ha hcL hcR hh L hL) c.operators κ) (hb : MeanIncrementBounds.BaseBounds (actualStrip U ha hcL hcR hh L hL) c.base) (hu : CorrectionState.CumulativeBounds (actualStrip U ha hcL hcR hh L hL) u) (hW : ∀ (i j : Fin 3), WeightedClasses.MeanClass (actualStrip U ha hcL hcR hh L hL) γ (u.covariance i j)) (β : ℝ) : (WeightedClasses.MeanClass (actualStrip U ha hcL hcR hh L hL) β fun (n : ℕ) (z : MeanStateRegularity.Point) => VariableGaugeMean.pressureAliasState (actualGauge h a b Mbase hab index) c u n (z, 0)) ∧ WeightedClasses.MeanClass (HarmonicWaveInteraction.productStrip (actualStrip U ha hcL hcR hh L hL)) β (VariableGaugeMean.pressureAliasState (actualGauge h a b Mbase hab index) c u)

The actual pressure alias as a full vector, both on the stripped domain and on its angular lift. Its source class is derived internally.

theorem NavierStokes.GaugeExcludedBounds.pressureAliasState_bounds {a b h Mbase cL cR : ℝ} (U : LocalSignedRequest.SlowRegion (2 * h)) (ha : 0 < a) (hab : a < b) (hcL : 0 < cL) (hcR : 0 < cR) (hh : 0 < h) (hM : Mbase ≠ 0) (index : ℕ → ℕ) (D : ℕ) (hgapLower : ∀ (n : ℕ), ChartScales.nativeIndex h n ≤ index n + D) (L : ℕ → ℝ) (hL : ∀ (n : ℕ), 1 ≤ L n) (hS : ∀ (n : ℕ), ChartScales.S n ≤ L n) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) {κ γ : ℝ} (H : MeanStateRegularity.PrimitiveData U a b c u) (ho : MeanIncrementBounds.OperatorBounds (actualStrip U ha hcL hcR hh L hL) c.operators κ) (hb : MeanIncrementBounds.BaseBounds (actualStrip U ha hcL hcR hh L hL) c.base) (hu : CorrectionState.CumulativeBounds (actualStrip U ha hcL hcR hh L hL) u) (hW : ∀ (i j : Fin 3), WeightedClasses.MeanClass (actualStrip U ha hcL hcR hh L hL) γ (u.covariance i j)) (β : ℝ) : (WeightedClasses.UnweightedClass (actualStrip U ha hcL hcR hh L hL) β fun (n : ℕ) (z : MeanStateRegularity.Point) => VariableGaugeMean.pressureAliasState (actualGauge h a b Mbase hab index) c u n (z, 0)) ∧ WeightedClasses.UnweightedClass (HarmonicWaveInteraction.productStrip (actualStrip U ha hcL hcR hh L hL)) β (VariableGaugeMean.pressureAliasState (actualGauge h a b Mbase hab index) c u)

Every real target power is available, hence every positive one. The vector signs are those of the literal pressureAliasState.

theorem NavierStokes.GaugeExcludedBounds.temporalAliasState_mean_bounds {a b h Mbase cL cR : ℝ} (U : LocalSignedRequest.SlowRegion (2 * h)) (ha : 0 < a) (hab : a < b) (hcL : 0 < cL) (hcR : 0 < cR) (hh : 0 < h) (hM : Mbase ≠ 0) (index : ℕ → ℕ) (D : ℕ) (hgapLower : ∀ (n : ℕ), ChartScales.nativeIndex h n ≤ index n + D) (hgapUpper : ∀ (n : ℕ), index n ≤ ChartScales.nativeIndex h n + D) (L : ℕ → ℝ) (hL : ∀ (n : ℕ), 1 ≤ L n) (hS : ∀ (n : ℕ), ChartScales.S n ≤ L n) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) {α : ℝ} (H : MeanStateRegularity.PrimitiveData U a b c u) (hfixed : (VariableGaugeMean.reconstructState (actualGauge h a b Mbase hab index) c u).pressure = u.pressure) (hfast : c.operators.fastCoefficient = fun (n : ℕ) => ChartScales.Tg ^ index n * ChartScales.Q n ^ (1 + h)) (hv : c.operators.vT = (0, 0, TorusInverse.vector TorusInverse.Direction.temporal)) (hraw : WeightedClasses.MeanClass (actualStrip U ha hcL hcR hh L hL) α (u.axialResidual c)) (β : ℝ) : (WeightedClasses.MeanClass (actualStrip U ha hcL hcR hh L hL) β fun (n : ℕ) (z : MeanStateRegularity.Point) => VariableGaugeMean.temporalAliasState (actualGauge h a b Mbase hab index) h index c u n (z, 0)) ∧ WeightedClasses.MeanClass (HarmonicWaveInteraction.productStrip (actualStrip U ha hcL hcR hh L hL)) β (VariableGaugeMean.temporalAliasState (actualGauge h a b Mbase hab index) h index c u)

Regularity of the actual raw axial residual follows from the primitive fields and the pressure reconstruction invariant. Only its ordinary incoming class is an induction input.

theorem NavierStokes.GaugeExcludedBounds.temporalAliasState_bounds {a b h Mbase cL cR : ℝ} (U : LocalSignedRequest.SlowRegion (2 * h)) (ha : 0 < a) (hab : a < b) (hcL : 0 < cL) (hcR : 0 < cR) (hh : 0 < h) (hM : Mbase ≠ 0) (index : ℕ → ℕ) (D : ℕ) (hgapLower : ∀ (n : ℕ), ChartScales.nativeIndex h n ≤ index n + D) (hgapUpper : ∀ (n : ℕ), index n ≤ ChartScales.nativeIndex h n + D) (L : ℕ → ℝ) (hL : ∀ (n : ℕ), 1 ≤ L n) (hS : ∀ (n : ℕ), ChartScales.S n ≤ L n) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) {α : ℝ} (H : MeanStateRegularity.PrimitiveData U a b c u) (hfixed : (VariableGaugeMean.reconstructState (actualGauge h a b Mbase hab index) c u).pressure = u.pressure) (hfast : c.operators.fastCoefficient = fun (n : ℕ) => ChartScales.Tg ^ index n * ChartScales.Q n ^ (1 + h)) (hv : c.operators.vT = (0, 0, TorusInverse.vector TorusInverse.Direction.temporal)) (hraw : WeightedClasses.MeanClass (actualStrip U ha hcL hcR hh L hL) α (u.axialResidual c)) (β : ℝ) : (WeightedClasses.UnweightedClass (actualStrip U ha hcL hcR hh L hL) β fun (n : ℕ) (z : MeanStateRegularity.Point) => VariableGaugeMean.temporalAliasState (actualGauge h a b Mbase hab index) h index c u n (z, 0)) ∧ WeightedClasses.UnweightedClass (HarmonicWaveInteraction.productStrip (actualStrip U ha hcL hcR hh L hL)) β (VariableGaugeMean.temporalAliasState (actualGauge h a b Mbase hab index) h index c u)

theorem NavierStokes.GaugeExcludedBounds.primitiveData_reconstruct {coord a b : ℝ} {U : LocalSignedRequest.SlowRegion coord} {c : CorrectionState.Context Point} {u : CorrectionState.State Point} (H : MeanStateRegularity.PrimitiveData U a b c u) (g : VariableGaugeMean.GaugeData TorusInverse.Plane) : MeanStateRegularity.PrimitiveData U a b c (VariableGaugeMean.reconstructState g c u)

theorem NavierStokes.GaugeExcludedBounds.reconstructed_pressure_fixed (g : VariableGaugeMean.GaugeData TorusInverse.Plane) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) : (VariableGaugeMean.reconstructState g c (VariableGaugeMean.reconstructState g c u)).pressure = (VariableGaugeMean.reconstructState g c u).pressure

theorem NavierStokes.GaugeExcludedBounds.temporalAliasState_reconstructed_bounds {a b h Mbase cL cR α : ℝ} (U : LocalSignedRequest.SlowRegion (2 * h)) (ha : 0 < a) (hab : a < b) (hcL : 0 < cL) (hcR : 0 < cR) (hh : 0 < h) (hM : Mbase ≠ 0) (index : ℕ → ℕ) (D : ℕ) (hgapLower : ∀ (n : ℕ), ChartScales.nativeIndex h n ≤ index n + D) (hgapUpper : ∀ (n : ℕ), index n ≤ ChartScales.nativeIndex h n + D) (L : ℕ → ℝ) (hL : ∀ (n : ℕ), 1 ≤ L n) (hS : ∀ (n : ℕ), ChartScales.S n ≤ L n) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData U a b c u) (hfast : c.operators.fastCoefficient = fun (n : ℕ) => ChartScales.Tg ^ index n * ChartScales.Q n ^ (1 + h)) (hv : c.operators.vT = (0, 0, TorusInverse.vector TorusInverse.Direction.temporal)) (hraw : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR (ChartScales.epsilon h) L ⋯ ⋯ hL) α ((VariableGaugeMean.reconstructState (VariableGaugeMean.similarityGauge h (ChartScales.radialExponent h) a b Mbase hab index) c u).axialResidual c)) (β : ℝ) : have g := VariableGaugeMean.similarityGauge h (ChartScales.radialExponent h) a b Mbase hab index; have s := LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR (ChartScales.epsilon h) L ⋯ ⋯ hL; (WeightedClasses.UnweightedClass s β fun (n : ℕ) (z : LocalSignedRequest.Point) => VariableGaugeMean.temporalAliasState g h index c (VariableGaugeMean.reconstructState g c u) n (z, 0)) ∧ WeightedClasses.UnweightedClass (HarmonicWaveInteraction.productStrip s) β (VariableGaugeMean.temporalAliasState g h index c (VariableGaugeMean.reconstructState g c u))

For a literally reconstructed incoming state the fixed-pressure invariant is discharged by the construction itself.