Stage estimates with the current-band particular fields

The signed waves and mean increments retain their actual native inputs. The particular contribution is an independently constructed physical field, with no physical copy-family representation imposed on it.

The actual particular waves on valid physical charts

The physical representative uses only the literal current-band solve. Its compatibility is obtained from the corresponding current-source transport laws. No value of a reference solve on an excluded face is used to define the physical representative.

Coherence of the actual current-band particular potential

The common copy coefficient is retained, including its cutoffs. Its vector potential is transported before taking the physical curl. The derivative identity uses an invertible linear chart and does not require an additional smoothness assumption on the phase.

theorem NavierStokes.ActualParticularPotentialCoherence.vectorPotential_equiv {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (e : E ≃L[ℝ] F) {s b K L : ℝ} (hs : s ≠ 0) (hb : b ≠ 0) (hK : K ≠ 0) (hKL : K * b = L) (r : E → ℝ) (R : F → ℝ) (Sr St Sz : E → E) (Vr Vt Vz : F → F) (hr : ∀ (x : E), R (e x) = s * r x) (hDr : ∀ (x : E), e (Sr x) = s • Vr (e x)) (hDt : ∀ (x : E), e (St x) = Vt (e x)) (hDz : ∀ (x : E), e (Sz x) = s • Vz (e x)) (c : ℝ) (Φ : F → ℝ) (a : F → HarmonicCalculus.ComplexVector) (x : E) : CurlClassBounds.vectorPotential K r Sr St Sz (fun (y : E) => b * Φ (e y)) (fun (y : E) => c • a (e y)) x = (c / s) • CurlClassBounds.vectorPotential L R Vr Vt Vz Φ a (e x)

The phase scale cancels the inverse carrier in the literal potential. An invertible chart also handles the convention for a nonexistent derivative.

theorem NavierStokes.ActualParticularPotentialCoherence.potential_weight {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (h : ℝ) : PhysicalParticularWave.velocityWeight h Q Qr / PhysicalParticularWave.ratioPower Q Qr (1 / 2) = PhysicalParticularWave.ratioPower Q Qr h

The physical potential has the scale exponent h, one half below the velocity exponent.

theorem NavierStokes.ActualParticularPotentialCoherence.pressure_weight {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (h : ℝ) : PhysicalParticularWave.pressureWeight h Q Qr = PhysicalParticularWave.velocityWeight h Q Qr ^ 2

@[reducible, inline]

abbrev NavierStokes.ActualParticularPotentialCoherence.Label (B N0 : ℕ) : Type

Label: an abbreviation for ActualParticularStageControls.Label.

Equations

• NavierStokes.ActualParticularPotentialCoherence.Label = NavierStokes.ActualParticularStageControls.Label

noncomputable def NavierStokes.ActualParticularPotentialCoherence.potential {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (j : ℤ) (n : ℕ) : PhysicalParticularWave.WaveSpace → HarmonicCalculus.ComplexVector

The potential of the actual current common coefficient.

Equations

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

noncomputable def NavierStokes.ActualParticularPotentialCoherence.pressureMode {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (j : ℤ) (n : ℕ) : PhysicalParticularWave.WaveSpace → ℂ

The complete harmonic pressure, with the actual current common pressure coefficient and the same carrier.

Equations

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

theorem NavierStokes.ActualParticularPotentialCoherence.potential_eq_copyData {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (j : ℤ) (n : ℕ) : potential x l j n = (ActualParticularCoherence.copyData x l j).common.curlPotential (CorrectionStep.ParticularParameters.nativeStrip ActualParticularStageControls.associatedStrip) ActualParticularStageControls.directions n

theorem NavierStokes.ActualParticularPotentialCoherence.pressureMode_eq_copyData {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (j : ℤ) (n : ℕ) : pressureMode x l j n = HarmonicCalculus.mode ((ActualParticularCoherence.copyData x l j).background.frequency n) ((ActualParticularCoherence.copyData x l j).background.phase n) ((ActualParticularCoherence.copyData x l j).common.pressure n)

theorem NavierStokes.ActualParticularPotentialCoherence.potential_eq {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (j : ℤ) (n : ℕ) : potential x l j n = CurlClassBounds.vectorPotential (↑j * (x.coefficients.blocks l).frequency n) (fun (y : PhysicalParticularWave.WaveSpace) => y.1.1.1) (ActualParticularStageControls.directions.radialField n) (fun (x : PhysicalParticularWave.WaveSpace) => ActualParticularStageControls.directions.angular) (ActualParticularStageControls.directions.axialField (CorrectionStep.ParticularParameters.nativeStrip ActualParticularStageControls.associatedStrip) n) ((ActualReferenceRebase.actualCoefficients x l j).phase n) ((ActualReferenceRebase.actualCoefficients x l j).amplitude n)

theorem NavierStokes.ActualParticularPotentialCoherence.pressureMode_eq {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (j : ℤ) (n : ℕ) : pressureMode x l j n = HarmonicCalculus.mode (↑j * (x.coefficients.blocks l).frequency n) ((ActualReferenceRebase.actualCoefficients x l j).phase n) ((ActualReferenceRebase.actualCoefficients x l j).pressure n)

theorem NavierStokes.ActualParticularPotentialCoherence.potential_band_of_germ {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (j : ℤ) (n m : ℕ) (hKn : ↑j * (x.coefficients.blocks l).frequency n ≠ 0) (hKm : ↑j * (x.coefficients.blocks l).frequency m ≠ 0) (z : PhysicalParticularWave.WaveSpace) (ha : (ActualReferenceRebase.actualCoefficients x l j).amplitude n z = PhysicalParticularWave.velocityWeight CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (ChartScales.Q m) • (ActualReferenceRebase.actualCoefficients x l j).amplitude m ((ActualParticularCoherence.bandMap n m) z)) (hp : (ActualReferenceRebase.actualCoefficients x l j).phase n =ᶠ[nhds z] fun (y : PhysicalParticularWave.WaveSpace) => ↑j * (x.coefficients.blocks l).frequency m / (↑j * (x.coefficients.blocks l).frequency n) * (ActualReferenceRebase.actualCoefficients x l j).phase m ((ActualParticularCoherence.bandMap n m) y)) : potential x l j n z = PhysicalParticularWave.ratioPower (ChartScales.Q n) (ChartScales.Q m) CorrectionInitialization.ActualPrimary.h • potential x l j m ((ActualParticularCoherence.bandMap n m) z)

Only the phase needs a germ: the undifferentiated raw amplitude is evaluated at the point.

theorem NavierStokes.ActualParticularPotentialCoherence.pressureMode_band_of_values {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (j : ℤ) (n m : ℕ) (hKn : ↑j * (x.coefficients.blocks l).frequency n ≠ 0) (z : PhysicalParticularWave.WaveSpace) (ha : (ActualReferenceRebase.actualCoefficients x l j).pressure n z = PhysicalParticularWave.pressureWeight CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (ChartScales.Q m) • (ActualReferenceRebase.actualCoefficients x l j).pressure m ((ActualParticularCoherence.bandMap n m) z)) (hp : (ActualReferenceRebase.actualCoefficients x l j).phase n z = ↑j * (x.coefficients.blocks l).frequency m / (↑j * (x.coefficients.blocks l).frequency n) * (ActualReferenceRebase.actualCoefficients x l j).phase m ((ActualParticularCoherence.bandMap n m) z)) : pressureMode x l j n z = PhysicalParticularWave.pressureWeight CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (ChartScales.Q m) • pressureMode x l j m ((ActualParticularCoherence.bandMap n m) z)

The pressure carrier is transported exactly together with its scalar coefficient.

theorem NavierStokes.ActualParticularPotentialCoherence.potential_band {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (I : ActualParticularCoherence.SourceInputs x l) (hfrequency : ∀ (n : ℕ), (x.coefficients.blocks l).frequency n = ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n)) {V : Set TorusInverse.Plane} (hV : IsOpen V) (htime : ∀ s ∈ V, 0 < s.1) (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) (hmap : Set.MapsTo (⇑(GaugeStateCoherence.bandSlowEquiv CorrectionInitialization.ActualPrimary.h n m)) V CorrectionInitialization.ActualPrimary.standardRegion.carrier) (HS : ActualReferenceRebase.StateComparison x V n m k) (HB : ActualReferenceRebase.BlockComparison x l V n m k) (j : ℤ) (hj : j ≠ 0) (z : PhysicalParticularWave.WaveSpace) (hz : z ∈ ActualParticularCoherence.waveDomain V) : potential x l j n z = PhysicalParticularWave.ratioPower (ChartScales.Q n) (ChartScales.Q m) CorrectionInitialization.ActualPrimary.h • potential x l j m ((ActualParticularCoherence.bandMap n m) z)

Current-copy potential covariance is a consequence of actual source continuity, support/order, and incoming state/block coherence.

theorem NavierStokes.ActualParticularPotentialCoherence.pressureMode_band {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (I : ActualParticularCoherence.SourceInputs x l) (hfrequency : ∀ (n : ℕ), (x.coefficients.blocks l).frequency n = ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n)) {V : Set TorusInverse.Plane} (hV : IsOpen V) (htime : ∀ s ∈ V, 0 < s.1) (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) (hmap : Set.MapsTo (⇑(GaugeStateCoherence.bandSlowEquiv CorrectionInitialization.ActualPrimary.h n m)) V CorrectionInitialization.ActualPrimary.standardRegion.carrier) (HS : ActualReferenceRebase.StateComparison x V n m k) (HB : ActualReferenceRebase.BlockComparison x l V n m k) (j : ℤ) (hj : j ≠ 0) (z : PhysicalParticularWave.WaveSpace) (hz : z ∈ ActualParticularCoherence.waveDomain V) : pressureMode x l j n z = PhysicalParticularWave.pressureWeight CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (ChartScales.Q m) • pressureMode x l j m ((ActualParticularCoherence.bandMap n m) z)

The full current harmonic pressure has the square velocity scale.

theorem NavierStokes.ActualParticularPotentialCoherence.pressureMode_band_sq {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (I : ActualParticularCoherence.SourceInputs x l) (hfrequency : ∀ (n : ℕ), (x.coefficients.blocks l).frequency n = ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n)) {V : Set TorusInverse.Plane} (hV : IsOpen V) (htime : ∀ s ∈ V, 0 < s.1) (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) (hmap : Set.MapsTo (⇑(GaugeStateCoherence.bandSlowEquiv CorrectionInitialization.ActualPrimary.h n m)) V CorrectionInitialization.ActualPrimary.standardRegion.carrier) (HS : ActualReferenceRebase.StateComparison x V n m k) (HB : ActualReferenceRebase.BlockComparison x l V n m k) (j : ℤ) (hj : j ≠ 0) (z : PhysicalParticularWave.WaveSpace) (hz : z ∈ ActualParticularCoherence.waveDomain V) : pressureMode x l j n z = PhysicalParticularWave.velocityWeight CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (ChartScales.Q m) ^ 2 • pressureMode x l j m ((ActualParticularCoherence.bandMap n m) z)

theorem NavierStokes.ActualParticularPotentialCoherence.potential_band_germ {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (I : ActualParticularCoherence.SourceInputs x l) (hfrequency : ∀ (n : ℕ), (x.coefficients.blocks l).frequency n = ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n)) {V : Set TorusInverse.Plane} (hV : IsOpen V) (htime : ∀ s ∈ V, 0 < s.1) (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) (hmap : Set.MapsTo (⇑(GaugeStateCoherence.bandSlowEquiv CorrectionInitialization.ActualPrimary.h n m)) V CorrectionInitialization.ActualPrimary.standardRegion.carrier) (HS : ActualReferenceRebase.StateComparison x V n m k) (HB : ActualReferenceRebase.BlockComparison x l V n m k) (j : ℤ) (hj : j ≠ 0) (z : PhysicalParticularWave.WaveSpace) (hz : z ∈ ActualParticularCoherence.waveDomain V) : potential x l j n =ᶠ[nhds z] fun (y : PhysicalParticularWave.WaveSpace) => PhysicalParticularWave.ratioPower (ChartScales.Q n) (ChartScales.Q m) CorrectionInitialization.ActualPrimary.h • potential x l j m ((ActualParticularCoherence.bandMap n m) y)

Equality holds as an ambient germ at every point of the open slow overlap, including all free radial, angular, and fast coordinates.

theorem NavierStokes.ActualParticularPotentialCoherence.pressureMode_band_germ {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (I : ActualParticularCoherence.SourceInputs x l) (hfrequency : ∀ (n : ℕ), (x.coefficients.blocks l).frequency n = ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n)) {V : Set TorusInverse.Plane} (hV : IsOpen V) (htime : ∀ s ∈ V, 0 < s.1) (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) (hmap : Set.MapsTo (⇑(GaugeStateCoherence.bandSlowEquiv CorrectionInitialization.ActualPrimary.h n m)) V CorrectionInitialization.ActualPrimary.standardRegion.carrier) (HS : ActualReferenceRebase.StateComparison x V n m k) (HB : ActualReferenceRebase.BlockComparison x l V n m k) (j : ℤ) (hj : j ≠ 0) (z : PhysicalParticularWave.WaveSpace) (hz : z ∈ ActualParticularCoherence.waveDomain V) : pressureMode x l j n =ᶠ[nhds z] fun (y : PhysicalParticularWave.WaveSpace) => PhysicalParticularWave.pressureWeight CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (ChartScales.Q m) • pressureMode x l j m ((ActualParticularCoherence.bandMap n m) y)

Removing the native scales from the current particular modes

The native potential and pressure transformation laws imply equality of their actual physical modes. The angle and Cartesian rotation are the same at both bands, so the native scale cancels before applying either map.

theorem NavierStokes.CurrentParticularPhysicalCoherence.unscale_of_ratioPower {E : Type u_1} [MulAction ℝ E] {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (a : ℝ) {v vr : E} (hv : v = PhysicalParticularWave.ratioPower Q Qr a • vr) : Q ^ (-a) • v = Qr ^ (-a) • vr

Cancel a positive native scale before applying a physical coordinate map. No regularity or linearity of that later map is required.

theorem NavierStokes.CurrentParticularPhysicalCoherence.localPotentialMode_eq_of_native {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualCurrentParticularPhysical.Label B N0)) (l : ActualCurrentParticularPhysical.Label B N0) (j : ℤ) (n m : ℕ) (w : ProblemStatement.SpaceTime) (hpot : ActualCurrentParticularPhysical.nativePotential x l j n (ActualCurrentParticularPhysical.nativePoint n w) = PhysicalParticularWave.ratioPower (ChartScales.Q n) (ChartScales.Q m) CorrectionInitialization.ActualPrimary.h • ActualCurrentParticularPhysical.nativePotential x l j m (ActualCurrentParticularPhysical.nativePoint m w)) : ActualCurrentParticularPhysical.localPotentialMode x l j n w = ActualCurrentParticularPhysical.localPotentialMode x l j m w

The actual current-band vector potential becomes independent of the band once its native transformation law is supplied.

theorem NavierStokes.CurrentParticularPhysicalCoherence.localPressureMode_eq_of_native {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualCurrentParticularPhysical.Label B N0)) (l : ActualCurrentParticularPhysical.Label B N0) (j : ℤ) (n m : ℕ) (w : ProblemStatement.SpaceTime) (hp : ActualCurrentParticularPhysical.nativePressure x l j n (ActualCurrentParticularPhysical.nativePoint n w) = PhysicalParticularWave.pressureWeight CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (ChartScales.Q m) • ActualCurrentParticularPhysical.nativePressure x l j m (ActualCurrentParticularPhysical.nativePoint m w)) : ActualCurrentParticularPhysical.localPressureMode x l j n w = ActualCurrentParticularPhysical.localPressureMode x l j m w

The pressure weight cancels the physical factor with exponent -2A. The real part is taken only after cancelling the complex native modes.

noncomputable def NavierStokes.ActualValidBandWaves.localPotential {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualInitialization.Index B N0)) (n : ℕ) : ProblemStatement.VelocityField

The actual finite current-band potential, in the initializer's label order.

Equations

• NavierStokes.ActualValidBandWaves.localPotential x n = NavierStokes.ActualCurrentParticularPhysical.localPotential (NavierStokes.ActualCycleParameters.particularState x) n

noncomputable def NavierStokes.ActualValidBandWaves.localPressure {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualInitialization.Index B N0)) (n : ℕ) : ProblemStatement.PressureField

Local pressure, given by ActualCurrentParticularPhysical.localPressure (ActualCycleParameters.particularState x) n.

Equations

• NavierStokes.ActualValidBandWaves.localPressure x n = NavierStokes.ActualCurrentParticularPhysical.localPressure (NavierStokes.ActualCycleParameters.particularState x) n

noncomputable def NavierStokes.ActualValidBandWaves.potential {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualInitialization.Index B N0)) (N : ℕ) : ProblemStatement.VelocityField

One representative of the actual current-band potential formulas.

Equations

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

noncomputable def NavierStokes.ActualValidBandWaves.pressure {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualInitialization.Index B N0)) (N : ℕ) : ProblemStatement.PressureField

Pressure, given by ValidDyadicBandCover.field h N (localPressure x).

Equations

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

@[reducible, inline]

noncomputable abbrev NavierStokes.ActualValidBandWaves.gluedPotential {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualInitialization.Index B N0)) (N : ℕ) : ProblemStatement.VelocityField

Glued potential: an abbreviation for @potential.

Equations

• @NavierStokes.ActualValidBandWaves.gluedPotential = @NavierStokes.ActualValidBandWaves.potential

@[reducible, inline]

noncomputable abbrev NavierStokes.ActualValidBandWaves.gluedPressure {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualInitialization.Index B N0)) (N : ℕ) : ProblemStatement.PressureField

Glued pressure: an abbreviation for @pressure.

Equations

• @NavierStokes.ActualValidBandWaves.gluedPressure = @NavierStokes.ActualValidBandWaves.pressure

theorem NavierStokes.ActualValidBandWaves.nativePoint_bandMap (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) (w : ProblemStatement.SpaceTime) (hr : 0 < PolarCharts.radius (PhysicalGraphBounds.radialProjection w)) : (ActualParticularCoherence.bandMap n m) (ActualCurrentParticularPhysical.nativePoint n w) = ActualCurrentParticularPhysical.nativePoint m w

The same physical polar angle is used in both bands. The comparison therefore retains the complete fast fiber instead of choosing new angles.

theorem NavierStokes.ActualValidBandWaves.nativePoint_parameterChange (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) (w : ProblemStatement.SpaceTime) (hr : 0 < PolarCharts.radius (PhysicalGraphBounds.radialProjection w)) : PhysicalParticularWave.parameterChange CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (ChartScales.Q m) (ActualCurrentParticularPhysical.nativePoint n w).1.1 = (ActualCurrentParticularPhysical.nativePoint m w).1.1

theorem NavierStokes.ActualValidBandWaves.nativePoint_slowChange (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) (w : ProblemStatement.SpaceTime) (hr : 0 < PolarCharts.radius (PhysicalGraphBounds.radialProjection w)) : (GaugeStateCoherence.bandSlowEquiv CorrectionInitialization.ActualPrimary.h n m) (ActualCurrentParticularPhysical.nativePoint n w).1.1.2 = (ActualCurrentParticularPhysical.nativePoint m w).1.1.2

theorem NavierStokes.ActualValidBandWaves.nativePoint_overlap (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) {w : ProblemStatement.SpaceTime} (hn : w ∈ ValidDyadicBandCover.band CorrectionInitialization.ActualPrimary.h n) (hm : w ∈ ValidDyadicBandCover.band CorrectionInitialization.ActualPrimary.h m) (hr : 0 < PolarCharts.radius (PhysicalGraphBounds.radialProjection w)) : (ActualCurrentParticularPhysical.nativePoint n w).1.1.2 ∈ ActualInitialCoherence.overlap n m

theorem NavierStokes.ActualValidBandWaves.current_frequency {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (ActualInitialization.Index B N0)} {S : ActualInitialization.Index B N0 → ℕ → Set LocalSignedRequest.Point} (H : CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry (CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock ActualInitialization.envelope S σ x) (l : ActualParticularStageControls.Label B N0) (n : ℕ) : ((ActualCycleParameters.particularState x).coefficients.blocks l).frequency n = ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n)

theorem NavierStokes.ActualValidBandWaves.refined_support {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (ActualInitialization.Index B N0)} {S : ActualInitialization.Index B N0 → ℕ → Set LocalSignedRequest.Point} (H : CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry (CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock ActualInitialization.envelope S σ x) (hcore : ∀ (l : ActualInitialization.Index B N0) (n : ℕ), S l n ⊆ ActualCoreSupport.refinedCarrier l n) (l : ActualParticularStageControls.Label B N0) : HarmonicSourceSupport.InputSupportOn ActualInitialization.geometry.domain (ActualCoreSupport.refinedCarrier (l.2, l.1)) ((ActualCycleParameters.particularState x).coefficients.blocks l) ((ActualCycleParameters.particularState x).coefficients.gaussian l) ((ActualCycleParameters.particularState x).coefficients.aliasCoefficients l)

theorem NavierStokes.ActualValidBandWaves.nativePotential_eq_actual {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (ActualInitialization.Index B N0)} {S : ActualInitialization.Index B N0 → ℕ → Set LocalSignedRequest.Point} (H : CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry (CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock ActualInitialization.envelope S σ x) (l : ActualParticularStageControls.Label B N0) (j : ℤ) (n : ℕ) : ActualCurrentParticularPhysical.nativePotential (ActualCycleParameters.particularState x) l j n = ActualParticularPotentialCoherence.potential (ActualCycleParameters.particularState x) l j n

theorem NavierStokes.ActualValidBandWaves.nativePressure_eq_actual {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (ActualInitialization.Index B N0)} {S : ActualInitialization.Index B N0 → ℕ → Set LocalSignedRequest.Point} (H : CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry (CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock ActualInitialization.envelope S σ x) (l : ActualParticularStageControls.Label B N0) (j : ℤ) (n : ℕ) : ActualCurrentParticularPhysical.nativePressure (ActualCycleParameters.particularState x) l j n = ActualParticularPotentialCoherence.pressureMode (ActualCycleParameters.particularState x) l j n

theorem NavierStokes.ActualValidBandWaves.modes_zero_of_inactive {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (ActualInitialization.Index B N0)} {S : ActualInitialization.Index B N0 → ℕ → Set LocalSignedRequest.Point} (H : CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry (CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock ActualInitialization.envelope S σ x) (C : ActualCycleCoherence.Coherent x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (hcore : ∀ (l : ActualInitialization.Index B N0) (n : ℕ), S l n ⊆ ActualCoreSupport.refinedCarrier l n) (l : ActualParticularStageControls.Label B N0) (j : ℤ) (n : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ ValidDyadicBandCover.band CorrectionInitialization.ActualPrimary.h n) (hl : l ∉ (ActualCycleParameters.particularState x).coefficients.labels n) : ActualCurrentParticularPhysical.localPotentialMode (ActualCycleParameters.particularState x) l j n w = 0 ∧ ActualCurrentParticularPhysical.localPressureMode (ActualCycleParameters.particularState x) l j n w = 0

theorem NavierStokes.ActualValidBandWaves.modes_eq_ordered {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (ActualInitialization.Index B N0)} {S : ActualInitialization.Index B N0 → ℕ → Set LocalSignedRequest.Point} (H : CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry (CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock ActualInitialization.envelope S σ x) (C : ActualCycleCoherence.Coherent x) (hS : ∀ (l : ActualInitialization.Index B N0) (n : ℕ), IsClosed (S l n)) (hcore : ∀ (l : ActualInitialization.Index B N0) (n : ℕ), S l n ⊆ ActualCoreSupport.refinedCarrier l n) (l : ActualParticularStageControls.Label B N0) (j : ℤ) (hj : j ≠ 0) (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) {w : ProblemStatement.SpaceTime} (hn : w ∈ ValidDyadicBandCover.band CorrectionInitialization.ActualPrimary.h n) (hm : w ∈ ValidDyadicBandCover.band CorrectionInitialization.ActualPrimary.h m) (hr : 0 < PolarCharts.radius (PhysicalGraphBounds.radialProjection w)) : ActualCurrentParticularPhysical.localPotentialMode (ActualCycleParameters.particularState x) l j n w = ActualCurrentParticularPhysical.localPotentialMode (ActualCycleParameters.particularState x) l j m w ∧ ActualCurrentParticularPhysical.localPressureMode (ActualCycleParameters.particularState x) l j n w = ActualCurrentParticularPhysical.localPressureMode (ActualCycleParameters.particularState x) l j m w

theorem NavierStokes.ActualValidBandWaves.local_fields_eq_ordered {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (ActualInitialization.Index B N0)} {S : ActualInitialization.Index B N0 → ℕ → Set LocalSignedRequest.Point} (H : CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry (CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock ActualInitialization.envelope S σ x) (C : ActualCycleCoherence.Coherent x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (hS : ∀ (l : ActualInitialization.Index B N0) (n : ℕ), IsClosed (S l n)) (hcore : ∀ (l : ActualInitialization.Index B N0) (n : ℕ), S l n ⊆ ActualCoreSupport.refinedCarrier l n) (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) {w : ProblemStatement.SpaceTime} (hn : w ∈ ValidDyadicBandCover.band CorrectionInitialization.ActualPrimary.h n) (hm : w ∈ ValidDyadicBandCover.band CorrectionInitialization.ActualPrimary.h m) (hr : 0 < PolarCharts.radius (PhysicalGraphBounds.radialProjection w)) : localPotential x n w = localPotential x m w ∧ localPressure x n w = localPressure x m w

theorem NavierStokes.ActualValidBandWaves.local_fields_eq {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (ActualInitialization.Index B N0)} {S : ActualInitialization.Index B N0 → ℕ → Set LocalSignedRequest.Point} (H : CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry (CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock ActualInitialization.envelope S σ x) (C : ActualCycleCoherence.Coherent x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (hS : ∀ (l : ActualInitialization.Index B N0) (n : ℕ), IsClosed (S l n)) (hcore : ∀ (l : ActualInitialization.Index B N0) (n : ℕ), S l n ⊆ ActualCoreSupport.refinedCarrier l n) (n m : ℕ) {w : ProblemStatement.SpaceTime} (hn : w ∈ ValidDyadicBandCover.band CorrectionInitialization.ActualPrimary.h n) (hm : w ∈ ValidDyadicBandCover.band CorrectionInitialization.ActualPrimary.h m) : localPotential x n w = localPotential x m w ∧ localPressure x n w = localPressure x m w

theorem NavierStokes.ActualValidBandWaves.compatible {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (ActualInitialization.Index B N0)} {S : ActualInitialization.Index B N0 → ℕ → Set LocalSignedRequest.Point} (H : CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry (CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock ActualInitialization.envelope S σ x) (C : ActualCycleCoherence.Coherent x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (hS : ∀ (l : ActualInitialization.Index B N0) (n : ℕ), IsClosed (S l n)) (hcore : ∀ (l : ActualInitialization.Index B N0) (n : ℕ), S l n ⊆ ActualCoreSupport.refinedCarrier l n) (N : ℕ) : ValidDyadicBandCover.Compatible CorrectionInitialization.ActualPrimary.h N (localPotential x) ∧ ValidDyadicBandCover.Compatible CorrectionInitialization.ActualPrimary.h N (localPressure x)

theorem NavierStokes.ActualValidBandWaves.potential_germ {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (ActualInitialization.Index B N0)} {S : ActualInitialization.Index B N0 → ℕ → Set LocalSignedRequest.Point} (H : CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry (CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock ActualInitialization.envelope S σ x) (C : ActualCycleCoherence.Coherent x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (hS : ∀ (l : ActualInitialization.Index B N0) (n : ℕ), IsClosed (S l n)) (hcore : ∀ (l : ActualInitialization.Index B N0) (n : ℕ), S l n ⊆ ActualCoreSupport.refinedCarrier l n) (N n : ℕ) (hn : N ≤ n) {w : ProblemStatement.SpaceTime} (hw : w ∈ ValidDyadicBandCover.band CorrectionInitialization.ActualPrimary.h n) : potential x N =ᶠ[nhds w] localPotential x n

theorem NavierStokes.ActualValidBandWaves.pressure_germ {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (ActualInitialization.Index B N0)} {S : ActualInitialization.Index B N0 → ℕ → Set LocalSignedRequest.Point} (H : CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry (CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock ActualInitialization.envelope S σ x) (C : ActualCycleCoherence.Coherent x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (hS : ∀ (l : ActualInitialization.Index B N0) (n : ℕ), IsClosed (S l n)) (hcore : ∀ (l : ActualInitialization.Index B N0) (n : ℕ), S l n ⊆ ActualCoreSupport.refinedCarrier l n) (N n : ℕ) (hn : N ≤ n) {w : ProblemStatement.SpaceTime} (hw : w ∈ ValidDyadicBandCover.band CorrectionInitialization.ActualPrimary.h n) : pressure x N =ᶠ[nhds w] localPressure x n

theorem NavierStokes.ActualValidBandWaves.fields_eq {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (ActualInitialization.Index B N0)} {S : ActualInitialization.Index B N0 → ℕ → Set LocalSignedRequest.Point} (H : CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry (CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock ActualInitialization.envelope S σ x) (C : ActualCycleCoherence.Coherent x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (hS : ∀ (l : ActualInitialization.Index B N0) (n : ℕ), IsClosed (S l n)) (hcore : ∀ (l : ActualInitialization.Index B N0) (n : ℕ), S l n ⊆ ActualCoreSupport.refinedCarrier l n) (N n : ℕ) (hn : N ≤ n) {w : ProblemStatement.SpaceTime} (hw : w ∈ ValidDyadicBandCover.band CorrectionInitialization.ActualPrimary.h n) : potential x N w = localPotential x n w ∧ pressure x N w = localPressure x n w

theorem NavierStokes.ActualValidBandWaves.potential_curl_germ {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (ActualInitialization.Index B N0)} {S : ActualInitialization.Index B N0 → ℕ → Set LocalSignedRequest.Point} (H : CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry (CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock ActualInitialization.envelope S σ x) (C : ActualCycleCoherence.Coherent x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (hS : ∀ (l : ActualInitialization.Index B N0) (n : ℕ), IsClosed (S l n)) (hcore : ∀ (l : ActualInitialization.Index B N0) (n : ℕ), S l n ⊆ ActualCoreSupport.refinedCarrier l n) (N n : ℕ) (hn : N ≤ n) {w : ProblemStatement.SpaceTime} (hw : w ∈ ValidDyadicBandCover.band CorrectionInitialization.ActualPrimary.h n) : SpatialCurl.spatialCurl (potential x N) =ᶠ[nhds w] SpatialCurl.spatialCurl (localPotential x n)

theorem NavierStokes.ActualValidBandWaves.jets_eq {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (ActualInitialization.Index B N0)} {S : ActualInitialization.Index B N0 → ℕ → Set LocalSignedRequest.Point} (H : CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry (CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock ActualInitialization.envelope S σ x) (C : ActualCycleCoherence.Coherent x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (hS : ∀ (l : ActualInitialization.Index B N0) (n : ℕ), IsClosed (S l n)) (hcore : ∀ (l : ActualInitialization.Index B N0) (n : ℕ), S l n ⊆ ActualCoreSupport.refinedCarrier l n) (N n : ℕ) (hn : N ≤ n) {w : ProblemStatement.SpaceTime} (hw : w ∈ ValidDyadicBandCover.band CorrectionInitialization.ActualPrimary.h n) (m : ℕ) : iteratedFDeriv ℝ m (potential x N) w = iteratedFDeriv ℝ m (localPotential x n) w ∧ iteratedFDeriv ℝ m (pressure x N) w = iteratedFDeriv ℝ m (localPressure x n) w

theorem NavierStokes.ActualValidBandWaves.active_zero_germs {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (ActualInitialization.Index B N0)} {S : ActualInitialization.Index B N0 → ℕ → Set LocalSignedRequest.Point} (H : CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry (CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock ActualInitialization.envelope S σ x) (C : ActualCycleCoherence.Coherent x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (hS : ∀ (l : ActualInitialization.Index B N0) (n : ℕ), IsClosed (S l n)) (hcore : ∀ (l : ActualInitialization.Index B N0) (n : ℕ), S l n ⊆ ActualCoreSupport.refinedCarrier l n) {N : ℕ} {qbig : ℝ} (hqbig : qbig ≤ ChartScales.Q N) {w : ProblemStatement.SpaceTime} (hw : w ∈ CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig) (hX : (SlowBorelBase.cartesianChart CorrectionInitialization.ActualPrimary.h w).2.1 ∉ Set.Icc (NominalConeAssembly.activeLeft CorrectionInitialization.ActualPrimary.nominal) (NominalConeAssembly.activeRight CorrectionInitialization.ActualPrimary.nominal)) : (potential x N =ᶠ[nhds w] fun (x : ProblemStatement.SpaceTime) => 0) ∧ pressure x N =ᶠ[nhds w] fun (x : ProblemStatement.SpaceTime) => 0

theorem NavierStokes.ActualValidBandWaves.shrinking_support {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (ActualInitialization.Index B N0)} {S : ActualInitialization.Index B N0 → ℕ → Set LocalSignedRequest.Point} (H : CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry (CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock ActualInitialization.envelope S σ x) (C : ActualCycleCoherence.Coherent x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (hS : ∀ (l : ActualInitialization.Index B N0) (n : ℕ), IsClosed (S l n)) (hcore : ∀ (l : ActualInitialization.Index B N0) (n : ℕ), S l n ⊆ ActualCoreSupport.refinedCarrier l n) {N : ℕ} {qbig : ℝ} (hqbig : qbig ≤ ChartScales.Q N) : MixedDiagonalExtensions.SublevelShrinkingSupport CorrectionInitialization.ActualPrimary.h PhysicalStageSupport.actualOuterConstant qbig (potential x N) ∧ MixedDiagonalExtensions.SublevelShrinkingSupport CorrectionInitialization.ActualPrimary.h PhysicalStageSupport.actualOuterConstant qbig (pressure x N)

theorem NavierStokes.ActualValidBandWaves.axis_zero {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (ActualInitialization.Index B N0)} {S : ActualInitialization.Index B N0 → ℕ → Set LocalSignedRequest.Point} (H : CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry (CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock ActualInitialization.envelope S σ x) (C : ActualCycleCoherence.Coherent x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (hS : ∀ (l : ActualInitialization.Index B N0) (n : ℕ), IsClosed (S l n)) (hcore : ∀ (l : ActualInitialization.Index B N0) (n : ℕ), S l n ⊆ ActualCoreSupport.refinedCarrier l n) {N : ℕ} {qbig : ℝ} (hqbig : qbig ≤ ChartScales.Q N) : GermCandidateAssembly.AxisZeroOn (MixedAxisPreservation.localDomain CorrectionInitialization.ActualPrimary.h qbig) (potential x N)

theorem NavierStokes.ActualValidBandWaves.refined_invariant {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (ActualInitialization.Index B N0)} {S : ActualInitialization.Index B N0 → ℕ → Set LocalSignedRequest.Point} (H : CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry (CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock ActualInitialization.envelope S σ x) (hcore : ∀ (l : ActualInitialization.Index B N0) (n : ℕ), S l n ⊆ ActualCoreSupport.refinedCarrier l n) : ActualParticularCycleData.Invariant σ x

theorem NavierStokes.ActualValidBandWaves.local_fields_smooth {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (ActualInitialization.Index B N0)} {S : ActualInitialization.Index B N0 → ℕ → Set LocalSignedRequest.Point} (H : CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry (CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock ActualInitialization.envelope S σ x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (hcore : ∀ (l : ActualInitialization.Index B N0) (n : ℕ), S l n ⊆ ActualCoreSupport.refinedCarrier l n) (n : ℕ) : ContDiffOn ℝ (↑⊤) (localPotential x n) (ValidDyadicBandCover.band CorrectionInitialization.ActualPrimary.h n) ∧ ContDiffOn ℝ (↑⊤) (localPressure x n) (ValidDyadicBandCover.band CorrectionInitialization.ActualPrimary.h n)

theorem NavierStokes.ActualValidBandWaves.fields_smooth {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (ActualInitialization.Index B N0)} {S : ActualInitialization.Index B N0 → ℕ → Set LocalSignedRequest.Point} (H : CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry (CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock ActualInitialization.envelope S σ x) (C : ActualCycleCoherence.Coherent x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (hS : ∀ (l : ActualInitialization.Index B N0) (n : ℕ), IsClosed (S l n)) (hcore : ∀ (l : ActualInitialization.Index B N0) (n : ℕ), S l n ⊆ ActualCoreSupport.refinedCarrier l n) {N : ℕ} {qbig : ℝ} (hqbig : qbig ≤ ChartScales.Q N) : ContDiffOn ℝ (↑⊤) (potential x N) (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig) ∧ ContDiffOn ℝ (↑⊤) (pressure x N) (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig)

Physical jet bounds for the actual current particular label sum

The closed label windows bound the number of contributing spatial labels. The two column choices are retained by the signed-label map and are already included in the 2250-color palette. The finite harmonic sum remains explicit.

@[reducible, inline]

abbrev NavierStokes.CurrentParticularLabelBounds.Label (B N0 : ℕ) : Type

Label: an abbreviation for ActualCurrentParticularPhysical.Label B N0.

Equations

• NavierStokes.CurrentParticularLabelBounds.Label B N0 = NavierStokes.ActualCurrentParticularPhysical.Label B N0

noncomputable def NavierStokes.CurrentParticularLabelBounds.signedLabel {B N0 : ℕ} (l : Label B N0) : SlotColoring.Label

Signed label, given by ActualPrimaryCovariance.signedLabelOf (l.2, l.1).

Equations

• NavierStokes.CurrentParticularLabelBounds.signedLabel l = NavierStokes.ActualPrimaryCovariance.signedLabelOf (l.2, l.1)

theorem NavierStokes.CurrentParticularLabelBounds.signedLabel_injective {B N0 : ℕ} : Function.Injective signedLabel

theorem NavierStokes.CurrentParticularLabelBounds.signedLabel_level {B N0 : ℕ} (l : Label B N0) : 1 ≤ (signedLabel l).1

noncomputable def NavierStokes.CurrentParticularLabelBounds.windowPosition (w : ProblemStatement.SpaceTime) : SlotColoring.Position

Window position, given by ![AnnularEndpoint.radius w, w.2 2, 1 - w.1].

Equations

• NavierStokes.CurrentParticularLabelBounds.windowPosition w = ![NavierStokes.AnnularEndpoint.radius w, w.2.ofLp 2, 1 - w.1]

noncomputable def NavierStokes.CurrentParticularLabelBounds.window (w : ProblemStatement.SpaceTime) : LabelSumBounds.WindowPoint

Window, given by (SquaredPartition.logCoordinate (PhysicalWaveSum.physicalQ h w), windowPosition w).

Equations

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

theorem NavierStokes.CurrentParticularLabelBounds.windowPosition_continuous : Continuous windowPosition

theorem NavierStokes.CurrentParticularLabelBounds.window_continuousAt {w : ProblemStatement.SpaceTime} (ht : w ∈ PhysicalWaveSum.preterminal) : ContinuousAt window w

noncomputable def NavierStokes.CurrentParticularLabelBounds.chartPoint (n : ℕ) (w : ProblemStatement.SpaceTime) : LocalSignedRequest.Point

Chart point, constructed using ActualCarrierTransport.associatedPoint.

Equations

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

theorem NavierStokes.CurrentParticularLabelBounds.chartPoint_time_pos (n : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ ValidDyadicBandCover.band CorrectionInitialization.ActualPrimary.h n) : 0 < (chartPoint n w).2.1.1

theorem NavierStokes.CurrentParticularLabelBounds.chartPoint_scale (n : ℕ) {w : ProblemStatement.SpaceTime} (ht : w ∈ PhysicalWaveSum.preterminal) : CorrectionInitialization.ActualPrimary.physicalScale n (chartPoint n w) = PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w

theorem NavierStokes.CurrentParticularLabelBounds.chartPoint_position (n : ℕ) (w : ProblemStatement.SpaceTime) : CorrectionInitialization.ActualPrimary.physicalPosition n (chartPoint n w) = windowPosition w

theorem NavierStokes.CurrentParticularLabelBounds.nativeMask_physicalBox {B N0 : ℕ} (L : CorrectionInitialization.ActualPrimary.Label B N0) (j : Fin 2) {p : PhaseCalculus.Slow} (hp : p ∈ tsupport (PrimaryRepresentatives.nativeMask (BaseChartJets.cellBand L) (PrimaryGeometryAssembly.label CorrectionInitialization.ActualPrimary.nominal L).2)) : CorrectionInitialization.ActualPrimary.position L p ∈ SlotColoring.physicalBox (CoordinateAlgebra.D CorrectionInitialization.ActualPrimary.h) (signedLabel (j, L))

The genuine one-mesh native support is contained in the two-mesh physical box. The column sign does not change the physical box.

theorem NavierStokes.CurrentParticularLabelBounds.refinedCarrier_window {B N0 : ℕ} (l : Label B N0) (n : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ ValidDyadicBandCover.band CorrectionInitialization.ActualPrimary.h n) (hs : chartPoint n w ∈ ActualCoreSupport.refinedCarrier (l.2, l.1) n) : window w ∈ LabelSumBounds.closedWindow (CoordinateAlgebra.D CorrectionInitialization.ActualPrimary.h) (signedLabel l)

Full refined support, including the native dyadic factor and the slow mask, puts a physical point in its actual signed label's closed window.

theorem NavierStokes.CurrentParticularLabelBounds.current_modes_window {B N0 : ℕ} (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (hs : HarmonicSourceSupport.InputSupportOn ActualInitialization.geometry.domain (ActualCoreSupport.refinedCarrier (l.2, l.1)) (x.coefficients.blocks l) (x.coefficients.gaussian l) (x.coefficients.aliasCoefficients l)) (j : ℤ) (n : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ ValidDyadicBandCover.band CorrectionInitialization.ActualPrimary.h n) : (ActualCurrentParticularPhysical.localPotentialMode x l j n w ≠ 0 → window w ∈ LabelSumBounds.closedWindow (CoordinateAlgebra.D CorrectionInitialization.ActualPrimary.h) (signedLabel l)) ∧ (ActualCurrentParticularPhysical.localPressureMode x l j n w ≠ 0 → window w ∈ LabelSumBounds.closedWindow (CoordinateAlgebra.D CorrectionInitialization.ActualPrimary.h) (signedLabel l))

Finite harmonic sums with uniform spatial multiplicity

theorem NavierStokes.CurrentParticularLabelBounds.finite_modes_jet_bound {B N0 : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (n : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ ValidDyadicBandCover.band CorrectionInitialization.ActualPrimary.h n) (F : Finset (Label B N0)) (J : Finset ℤ) (f : Label B N0 → ℤ → ProblemStatement.SpaceTime → E) (m : ℕ) (hf : ∀ l ∈ F, ∀ j ∈ J, ContDiffAt ℝ (↑m) (f l j) w) (hs : ∀ l ∈ F, ∀ j ∈ J, ∀ y ∈ ValidDyadicBandCover.band CorrectionInitialization.ActualPrimary.h n, f l j y ≠ 0 → window y ∈ LabelSumBounds.closedWindow (CoordinateAlgebra.D CorrectionInitialization.ActualPrimary.h) (signedLabel l)) (C : ℤ → ℝ) (hC : ∀ j ∈ J, 0 ≤ C j) (hb : ∀ l ∈ F, ∀ j ∈ J, window w ∈ LabelSumBounds.closedWindow (CoordinateAlgebra.D CorrectionInitialization.ActualPrimary.h) (signedLabel l) → ‖iteratedFDeriv ℝ m (f l j) w‖ ≤ C j) : ‖iteratedFDeriv ℝ m (fun (y : ProblemStatement.SpaceTime) => ∑ l ∈ F, ∑ j ∈ J, f l j y) w‖ ≤ 2250 * ∑ j ∈ J, C j

The spatial factor is 2250, independently of the number of labels. Different harmonics may retain different constants. All jet hypotheses are pointwise at w; the open band is used only for support and germs.

theorem NavierStokes.CurrentParticularLabelBounds.modes_card (N : ℕ) : (ParticularWaveAssembly.modes N).card = 2 * N

theorem NavierStokes.CurrentParticularLabelBounds.localPotential_jet_bound {B N0 : ℕ} (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (x : CorrectionStep.CycleState (Label B N0)) (hs : ∀ (l : Label B N0), HarmonicSourceSupport.InputSupportOn ActualInitialization.geometry.domain (ActualCoreSupport.refinedCarrier (l.2, l.1)) (x.coefficients.blocks l) (x.coefficients.gaussian l) (x.coefficients.aliasCoefficients l)) (n m : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ ValidDyadicBandCover.band CorrectionInitialization.ActualPrimary.h n) (C : ℤ → ℝ) (hC : ∀ j ∈ ParticularWaveAssembly.modes x.coefficients.residualBand, 0 ≤ C j) (hf : ∀ l ∈ x.coefficients.labels n, ∀ j ∈ ParticularWaveAssembly.modes x.coefficients.residualBand, ContDiffAt ℝ (↑m) (ActualCurrentParticularPhysical.localPotentialMode x l j n) w) (hb : ∀ l ∈ x.coefficients.labels n, ∀ j ∈ ParticularWaveAssembly.modes x.coefficients.residualBand, window w ∈ LabelSumBounds.closedWindow (CoordinateAlgebra.D CorrectionInitialization.ActualPrimary.h) (signedLabel l) → ‖iteratedFDeriv ℝ m (ActualCurrentParticularPhysical.localPotentialMode x l j n) w‖ ≤ C j) : ‖iteratedFDeriv ℝ m (ActualCurrentParticularPhysical.localPotential x n) w‖ ≤ 2250 * ∑ j ∈ ParticularWaveAssembly.modes x.coefficients.residualBand, C j

theorem NavierStokes.CurrentParticularLabelBounds.localPressure_jet_bound {B N0 : ℕ} (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (x : CorrectionStep.CycleState (Label B N0)) (hs : ∀ (l : Label B N0), HarmonicSourceSupport.InputSupportOn ActualInitialization.geometry.domain (ActualCoreSupport.refinedCarrier (l.2, l.1)) (x.coefficients.blocks l) (x.coefficients.gaussian l) (x.coefficients.aliasCoefficients l)) (n m : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ ValidDyadicBandCover.band CorrectionInitialization.ActualPrimary.h n) (C : ℤ → ℝ) (hC : ∀ j ∈ ParticularWaveAssembly.modes x.coefficients.residualBand, 0 ≤ C j) (hf : ∀ l ∈ x.coefficients.labels n, ∀ j ∈ ParticularWaveAssembly.modes x.coefficients.residualBand, ContDiffAt ℝ (↑m) (ActualCurrentParticularPhysical.localPressureMode x l j n) w) (hb : ∀ l ∈ x.coefficients.labels n, ∀ j ∈ ParticularWaveAssembly.modes x.coefficients.residualBand, window w ∈ LabelSumBounds.closedWindow (CoordinateAlgebra.D CorrectionInitialization.ActualPrimary.h) (signedLabel l) → ‖iteratedFDeriv ℝ m (ActualCurrentParticularPhysical.localPressureMode x l j n) w‖ ≤ C j) : ‖iteratedFDeriv ℝ m (ActualCurrentParticularPhysical.localPressure x n) w‖ ≤ 2250 * ∑ j ∈ ParticularWaveAssembly.modes x.coefficients.residualBand, C j

theorem NavierStokes.CurrentParticularLabelBounds.localPotential_jet_bound_uniform {B N0 : ℕ} (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (x : CorrectionStep.CycleState (Label B N0)) (hs : ∀ (l : Label B N0), HarmonicSourceSupport.InputSupportOn ActualInitialization.geometry.domain (ActualCoreSupport.refinedCarrier (l.2, l.1)) (x.coefficients.blocks l) (x.coefficients.gaussian l) (x.coefficients.aliasCoefficients l)) (n m : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ ValidDyadicBandCover.band CorrectionInitialization.ActualPrimary.h n) {C : ℝ} (hC : 0 ≤ C) (hf : ∀ l ∈ x.coefficients.labels n, ∀ j ∈ ParticularWaveAssembly.modes x.coefficients.residualBand, ContDiffAt ℝ (↑m) (ActualCurrentParticularPhysical.localPotentialMode x l j n) w) (hb : ∀ l ∈ x.coefficients.labels n, ∀ j ∈ ParticularWaveAssembly.modes x.coefficients.residualBand, window w ∈ LabelSumBounds.closedWindow (CoordinateAlgebra.D CorrectionInitialization.ActualPrimary.h) (signedLabel l) → ‖iteratedFDeriv ℝ m (ActualCurrentParticularPhysical.localPotentialMode x l j n) w‖ ≤ C) : ‖iteratedFDeriv ℝ m (ActualCurrentParticularPhysical.localPotential x n) w‖ ≤ 2250 * ↑(2 * x.coefficients.residualBand) * C

theorem NavierStokes.CurrentParticularLabelBounds.localPressure_jet_bound_uniform {B N0 : ℕ} (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (x : CorrectionStep.CycleState (Label B N0)) (hs : ∀ (l : Label B N0), HarmonicSourceSupport.InputSupportOn ActualInitialization.geometry.domain (ActualCoreSupport.refinedCarrier (l.2, l.1)) (x.coefficients.blocks l) (x.coefficients.gaussian l) (x.coefficients.aliasCoefficients l)) (n m : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ ValidDyadicBandCover.band CorrectionInitialization.ActualPrimary.h n) {C : ℝ} (hC : 0 ≤ C) (hf : ∀ l ∈ x.coefficients.labels n, ∀ j ∈ ParticularWaveAssembly.modes x.coefficients.residualBand, ContDiffAt ℝ (↑m) (ActualCurrentParticularPhysical.localPressureMode x l j n) w) (hb : ∀ l ∈ x.coefficients.labels n, ∀ j ∈ ParticularWaveAssembly.modes x.coefficients.residualBand, window w ∈ LabelSumBounds.closedWindow (CoordinateAlgebra.D CorrectionInitialization.ActualPrimary.h) (signedLabel l) → ‖iteratedFDeriv ℝ m (ActualCurrentParticularPhysical.localPressureMode x l j n) w‖ ≤ C) : ‖iteratedFDeriv ℝ m (ActualCurrentParticularPhysical.localPressure x n) w‖ ≤ 2250 * ↑(2 * x.coefficients.residualBand) * C

The incoming actual invariant supplies all mode regularity

theorem NavierStokes.CurrentParticularLabelBounds.current_modes_contDiffAt {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (ActualInitialization.Index B N0)} (H : ActualParticularCycleData.Invariant σ x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (l : Label B N0) (j : ℤ) (hj : j ≠ 0) (n : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ ValidDyadicBandCover.band CorrectionInitialization.ActualPrimary.h n) : ContDiffAt ℝ (↑⊤) (ActualCurrentParticularPhysical.localPotentialMode (ActualCycleParameters.particularState x) l j n) w ∧ ContDiffAt ℝ (↑⊤) (ActualCurrentParticularPhysical.localPressureMode (ActualCycleParameters.particularState x) l j n) w

Per-mode physical smoothness on the whole open valid band, including the axis. The invariant supplies source regularity and the actual raw boundary values; at the axis the retained support gives a zero germ.

theorem NavierStokes.CurrentParticularLabelBounds.current_modes_contDiffOn {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (ActualInitialization.Index B N0)} (H : ActualParticularCycleData.Invariant σ x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (l : Label B N0) (j : ℤ) (hj : j ≠ 0) (n : ℕ) : ContDiffOn ℝ (↑⊤) (ActualCurrentParticularPhysical.localPotentialMode (ActualCycleParameters.particularState x) l j n) (ValidDyadicBandCover.band CorrectionInitialization.ActualPrimary.h n) ∧ ContDiffOn ℝ (↑⊤) (ActualCurrentParticularPhysical.localPressureMode (ActualCycleParameters.particularState x) l j n) (ValidDyadicBandCover.band CorrectionInitialization.ActualPrimary.h n)

theorem NavierStokes.CurrentParticularLabelBounds.localPotential_jet_bound_of_invariant {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (ActualInitialization.Index B N0)} (H : ActualParticularCycleData.Invariant σ x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (n m : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ ValidDyadicBandCover.band CorrectionInitialization.ActualPrimary.h n) (C : ℤ → ℝ) (hC : ∀ j ∈ ParticularWaveAssembly.modes x.coefficients.residualBand, 0 ≤ C j) (hb : ∀ l ∈ (ActualCycleParameters.particularState x).coefficients.labels n, ∀ j ∈ ParticularWaveAssembly.modes x.coefficients.residualBand, window w ∈ LabelSumBounds.closedWindow (CoordinateAlgebra.D CorrectionInitialization.ActualPrimary.h) (signedLabel l) → ‖iteratedFDeriv ℝ m (ActualCurrentParticularPhysical.localPotentialMode (ActualCycleParameters.particularState x) l j n) w‖ ≤ C j) : ‖iteratedFDeriv ℝ m (ActualCurrentParticularPhysical.localPotential (ActualCycleParameters.particularState x) n) w‖ ≤ 2250 * ∑ j ∈ ParticularWaveAssembly.modes x.coefficients.residualBand, C j

theorem NavierStokes.CurrentParticularLabelBounds.localPressure_jet_bound_of_invariant {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (ActualInitialization.Index B N0)} (H : ActualParticularCycleData.Invariant σ x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (n m : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ ValidDyadicBandCover.band CorrectionInitialization.ActualPrimary.h n) (C : ℤ → ℝ) (hC : ∀ j ∈ ParticularWaveAssembly.modes x.coefficients.residualBand, 0 ≤ C j) (hb : ∀ l ∈ (ActualCycleParameters.particularState x).coefficients.labels n, ∀ j ∈ ParticularWaveAssembly.modes x.coefficients.residualBand, window w ∈ LabelSumBounds.closedWindow (CoordinateAlgebra.D CorrectionInitialization.ActualPrimary.h) (signedLabel l) → ‖iteratedFDeriv ℝ m (ActualCurrentParticularPhysical.localPressureMode (ActualCycleParameters.particularState x) l j n) w‖ ≤ C j) : ‖iteratedFDeriv ℝ m (ActualCurrentParticularPhysical.localPressure (ActualCycleParameters.particularState x) n) w‖ ≤ 2250 * ∑ j ∈ ParticularWaveAssembly.modes x.coefficients.residualBand, C j

theorem NavierStokes.CurrentParticularLabelBounds.localPotential_jet_bound_uniform_of_invariant {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (ActualInitialization.Index B N0)} (H : ActualParticularCycleData.Invariant σ x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (n m : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ ValidDyadicBandCover.band CorrectionInitialization.ActualPrimary.h n) {C : ℝ} (hC : 0 ≤ C) (hb : ∀ l ∈ (ActualCycleParameters.particularState x).coefficients.labels n, ∀ j ∈ ParticularWaveAssembly.modes x.coefficients.residualBand, window w ∈ LabelSumBounds.closedWindow (CoordinateAlgebra.D CorrectionInitialization.ActualPrimary.h) (signedLabel l) → ‖iteratedFDeriv ℝ m (ActualCurrentParticularPhysical.localPotentialMode (ActualCycleParameters.particularState x) l j n) w‖ ≤ C) : ‖iteratedFDeriv ℝ m (ActualCurrentParticularPhysical.localPotential (ActualCycleParameters.particularState x) n) w‖ ≤ 2250 * ↑(2 * x.coefficients.residualBand) * C

theorem NavierStokes.CurrentParticularLabelBounds.localPressure_jet_bound_uniform_of_invariant {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (ActualInitialization.Index B N0)} (H : ActualParticularCycleData.Invariant σ x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (n m : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ ValidDyadicBandCover.band CorrectionInitialization.ActualPrimary.h n) {C : ℝ} (hC : 0 ≤ C) (hb : ∀ l ∈ (ActualCycleParameters.particularState x).coefficients.labels n, ∀ j ∈ ParticularWaveAssembly.modes x.coefficients.residualBand, window w ∈ LabelSumBounds.closedWindow (CoordinateAlgebra.D CorrectionInitialization.ActualPrimary.h) (signedLabel l) → ‖iteratedFDeriv ℝ m (ActualCurrentParticularPhysical.localPressureMode (ActualCycleParameters.particularState x) l j n) w‖ ≤ C) : ‖iteratedFDeriv ℝ m (ActualCurrentParticularPhysical.localPressure (ActualCycleParameters.particularState x) n) w‖ ≤ 2250 * ↑(2 * x.coefficients.residualBand) * C

@[reducible, inline]

abbrev NavierStokes.GluedStageEstimates.Bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (qbig : ℝ) (f : ProblemStatement.SpaceTime → E) (m : ℕ) (r : ℝ) : Prop

Bound type used in glued stage estimates.

Equations

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

structure NavierStokes.GluedStageEstimates.SignedInputs (D : Type) [NormedAddCommGroup D] [NormedSpace ℝ D] (I : Type u_1) (K : Type u_2) : Type (max u_1 u_2)

These are the original native signed-wave data, without an unrelated particular copy-family field.

• potential : ℕ → PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h D (Fin 3 × I) K (Fin 3)

  Potential of SignedInputs, of type ℕ → PhysicalStageBounds.WaveData h D (Fin 3 × I) K (Fin 3).

• pressure : ℕ → PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h D I K Unit

  Pressure field of SignedInputs, of type ℕ → PhysicalStageBounds.WaveData h D I K Unit.

• potential_exponent (j : ℕ) : 1 / 2 + ActualIterationLedger.sigma j - ChartScales.kappa ≤ (self.potential j).alpha
• pressure_exponent (j : ℕ) : 1 + ActualIterationLedger.sigma j - ChartScales.kappa ≤ (self.pressure j).alpha
• potential_shift (j : ℕ) : (self.potential j).shift = -CorrectionInitialization.ActualPrimary.h
• pressure_shift (j : ℕ) : (self.pressure j).shift = -(2 * CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h)

noncomputable def NavierStokes.GluedStageEstimates.signedMeanPotential {B N0 N : ℕ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (R : ActualStageEstimates.RunData B N0) (M : ActualMeanPhysicalData.InitialCycleInput B N0 N fun (x : ℕ) => ActualCycleParameters.fixedParameters B N0) (hN : 4 ≤ N) (W : SignedInputs D I K) (j : ℕ) : ProblemStatement.VelocityField

Signed mean potential as an element of VelocityField.

Equations

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

noncomputable def NavierStokes.GluedStageEstimates.signedMeanPressure {B N0 N : ℕ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (R : ActualStageEstimates.RunData B N0) (M : ActualMeanPhysicalData.InitialCycleInput B N0 N fun (x : ℕ) => ActualCycleParameters.fixedParameters B N0) (hN : 4 ≤ N) (W : SignedInputs D I K) (j : ℕ) : ProblemStatement.PressureField

Signed mean pressure, defined pointwise by (W.pressure j).pressure w + (ActualStageEstimates.pressureInput R M hN j).family.field w.

Equations

• NavierStokes.GluedStageEstimates.signedMeanPressure R M hN W j w = (W.pressure j).pressure w + (NavierStokes.ActualStageEstimates.pressureInput R M hN j).family.field w

noncomputable def NavierStokes.GluedStageEstimates.direct {B N0 N : ℕ} (R : ActualStageEstimates.RunData B N0) (M : ActualMeanPhysicalData.InitialCycleInput B N0 N fun (x : ℕ) => ActualCycleParameters.fixedParameters B N0) (hN : 4 ≤ N) (j : ℕ) : ProblemStatement.VelocityField

Direct, given by (ActualStageEstimates.angularInput R M hN j).family.angularField.

Equations

• NavierStokes.GluedStageEstimates.direct R M hN j = (NavierStokes.ActualStageEstimates.angularInput R M hN j).family.angularField

theorem NavierStokes.GluedStageEstimates.signedMeanPotential_smooth {B N0 N : ℕ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (R : ActualStageEstimates.RunData B N0) (M : ActualMeanPhysicalData.InitialCycleInput B N0 N fun (x : ℕ) => ActualCycleParameters.fixedParameters B N0) (hN : 4 ≤ N) (W : SignedInputs D I K) {qbig : ℝ} (hq : qbig ≤ ChartScales.Q N) (j : ℕ) : ContDiffOn ℝ (↑⊤) (signedMeanPotential R M hN W j) (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig)

theorem NavierStokes.GluedStageEstimates.signedMeanPressure_smooth {B N0 N : ℕ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (R : ActualStageEstimates.RunData B N0) (M : ActualMeanPhysicalData.InitialCycleInput B N0 N fun (x : ℕ) => ActualCycleParameters.fixedParameters B N0) (hN : 4 ≤ N) (W : SignedInputs D I K) {qbig : ℝ} (hq : qbig ≤ ChartScales.Q N) (j : ℕ) : ContDiffOn ℝ (↑⊤) (signedMeanPressure R M hN W j) (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig)

theorem NavierStokes.GluedStageEstimates.direct_smooth {B N0 N : ℕ} (R : ActualStageEstimates.RunData B N0) (M : ActualMeanPhysicalData.InitialCycleInput B N0 N fun (x : ℕ) => ActualCycleParameters.fixedParameters B N0) (hN : 4 ≤ N) {qbig : ℝ} (hq : qbig ≤ ChartScales.Q N) (j : ℕ) : ContDiffOn ℝ (↑⊤) (direct R M hN j) (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig)

theorem NavierStokes.GluedStageEstimates.signedMeanPotential_bound {B N0 N : ℕ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (R : ActualStageEstimates.RunData B N0) (M : ActualMeanPhysicalData.InitialCycleInput B N0 N fun (x : ℕ) => ActualCycleParameters.fixedParameters B N0) (hN : 4 ≤ N) (W : SignedInputs D I K) {qbig : ℝ} (hq : qbig ≤ ChartScales.Q N) (j m : ℕ) : Bound qbig (signedMeanPotential R M hN W j) m (ActualIterationLedger.gain CorrectionInitialization.ActualPrimary.h (j + 1) - PhysicalStageBounds.potentialLoss CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.h 0 m)

theorem NavierStokes.GluedStageEstimates.signedMeanPressure_bound {B N0 N : ℕ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (R : ActualStageEstimates.RunData B N0) (M : ActualMeanPhysicalData.InitialCycleInput B N0 N fun (x : ℕ) => ActualCycleParameters.fixedParameters B N0) (hN : 4 ≤ N) (W : SignedInputs D I K) {qbig : ℝ} (hq : qbig ≤ ChartScales.Q N) (j m : ℕ) : Bound qbig (signedMeanPressure R M hN W j) m (ActualIterationLedger.gain CorrectionInitialization.ActualPrimary.h (j + 1) - PhysicalStageBounds.pressureLoss CorrectionInitialization.ActualPrimary.h (2 * CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h) 0 m)

theorem NavierStokes.GluedStageEstimates.direct_bound {B N0 N : ℕ} (R : ActualStageEstimates.RunData B N0) (M : ActualMeanPhysicalData.InitialCycleInput B N0 N fun (x : ℕ) => ActualCycleParameters.fixedParameters B N0) (hN : 4 ≤ N) {qbig : ℝ} (hq : qbig ≤ ChartScales.Q N) (j m : ℕ) : Bound qbig (direct R M hN j) m (ActualIterationLedger.gain CorrectionInitialization.ActualPrimary.h (j + 1) - PhysicalStageBounds.directLoss CorrectionInitialization.ActualPrimary.h 0 m)

A physical particular contribution and the same mixed sequence

noncomputable def NavierStokes.GluedStageEstimates.potentialLoss (L : ℕ → ℝ) (m : ℕ) : ℝ

Potential loss, given by max (L m) (PhysicalStageBounds.potentialLoss h h 0 m).

Equations

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

noncomputable def NavierStokes.GluedStageEstimates.pressureLoss (L : ℕ → ℝ) (m : ℕ) : ℝ

Pressure loss, given by max (L m) (PhysicalStageBounds.pressureLoss h (2 * CoordinateAlgebra.A h) 0 m).

Equations

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

noncomputable def NavierStokes.GluedStageEstimates.backgroundLoss (L : ℕ → ℝ) (waveAlpha waveShift : ℝ) : ℕ → ℝ

Background loss, constructed using MixedFiniteBackground.initialBackgroundLoss.

Equations

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

noncomputable def NavierStokes.GluedStageEstimates.potential {B N0 N : ℕ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (R : ActualStageEstimates.RunData B N0) (M : ActualMeanPhysicalData.InitialCycleInput B N0 N fun (x : ℕ) => ActualCycleParameters.fixedParameters B N0) (hN : 4 ≤ N) (W : SignedInputs D I K) (particularA : ℕ → ProblemStatement.VelocityField) (j : ℕ) : ProblemStatement.VelocityField

The four literal contributions use the same order as the physical sequence construction.

Equations

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

noncomputable def NavierStokes.GluedStageEstimates.pressure {B N0 N : ℕ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (R : ActualStageEstimates.RunData B N0) (M : ActualMeanPhysicalData.InitialCycleInput B N0 N fun (x : ℕ) => ActualCycleParameters.fixedParameters B N0) (hN : 4 ≤ N) (W : SignedInputs D I K) (particularP : ℕ → ProblemStatement.PressureField) (j : ℕ) : ProblemStatement.PressureField

Pressure, defined pointwise by particularP j w + (W.pressure j).pressure w + (ActualStageEstimates.pressureInput R M hN j).family.field w.

Equations

• NavierStokes.GluedStageEstimates.pressure R M hN W particularP j w = particularP j w + (W.pressure j).pressure w + (NavierStokes.ActualStageEstimates.pressureInput R M hN j).family.field w

theorem NavierStokes.GluedStageEstimates.potential_eq {B N0 N : ℕ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (R : ActualStageEstimates.RunData B N0) (M : ActualMeanPhysicalData.InitialCycleInput B N0 N fun (x : ℕ) => ActualCycleParameters.fixedParameters B N0) (hN : 4 ≤ N) (W : SignedInputs D I K) (particularA : ℕ → ProblemStatement.VelocityField) (j : ℕ) : potential R M hN W particularA j = fun (w : ProblemStatement.SpaceTime) => particularA j w + signedMeanPotential R M hN W j w

theorem NavierStokes.GluedStageEstimates.pressure_eq {B N0 N : ℕ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (R : ActualStageEstimates.RunData B N0) (M : ActualMeanPhysicalData.InitialCycleInput B N0 N fun (x : ℕ) => ActualCycleParameters.fixedParameters B N0) (hN : 4 ≤ N) (W : SignedInputs D I K) (particularP : ℕ → ProblemStatement.PressureField) (j : ℕ) : pressure R M hN W particularP j = fun (w : ProblemStatement.SpaceTime) => particularP j w + signedMeanPressure R M hN W j w

theorem NavierStokes.GluedStageEstimates.potential_smooth {B N0 N : ℕ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (R : ActualStageEstimates.RunData B N0) (M : ActualMeanPhysicalData.InitialCycleInput B N0 N fun (x : ℕ) => ActualCycleParameters.fixedParameters B N0) (hN : 4 ≤ N) (W : SignedInputs D I K) (particularA : ℕ → ProblemStatement.VelocityField) {qbig : ℝ} (hq : qbig ≤ ChartScales.Q N) (hs : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (particularA j) (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig)) (j : ℕ) : ContDiffOn ℝ (↑⊤) (potential R M hN W particularA j) (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig)

theorem NavierStokes.GluedStageEstimates.pressure_smooth {B N0 N : ℕ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (R : ActualStageEstimates.RunData B N0) (M : ActualMeanPhysicalData.InitialCycleInput B N0 N fun (x : ℕ) => ActualCycleParameters.fixedParameters B N0) (hN : 4 ≤ N) (W : SignedInputs D I K) (particularP : ℕ → ProblemStatement.PressureField) {qbig : ℝ} (hq : qbig ≤ ChartScales.Q N) (hs : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (particularP j) (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig)) (j : ℕ) : ContDiffOn ℝ (↑⊤) (pressure R M hN W particularP j) (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig)

theorem NavierStokes.GluedStageEstimates.potential_bound {B N0 N : ℕ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (R : ActualStageEstimates.RunData B N0) (M : ActualMeanPhysicalData.InitialCycleInput B N0 N fun (x : ℕ) => ActualCycleParameters.fixedParameters B N0) (hN : 4 ≤ N) (W : SignedInputs D I K) (particularA : ℕ → ProblemStatement.VelocityField) {qbig : ℝ} (hq : qbig ≤ ChartScales.Q N) {L : ℕ → ℝ} (hs : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (particularA j) (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig)) (hb : ∀ (j m : ℕ), Bound qbig (particularA j) m (ActualIterationLedger.gain CorrectionInitialization.ActualPrimary.h (j + 1) - L m)) (j m : ℕ) : Bound qbig (potential R M hN W particularA j) m (ActualIterationLedger.gain CorrectionInitialization.ActualPrimary.h (j + 1) - potentialLoss L m)

theorem NavierStokes.GluedStageEstimates.pressure_bound {B N0 N : ℕ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (R : ActualStageEstimates.RunData B N0) (M : ActualMeanPhysicalData.InitialCycleInput B N0 N fun (x : ℕ) => ActualCycleParameters.fixedParameters B N0) (hN : 4 ≤ N) (W : SignedInputs D I K) (particularP : ℕ → ProblemStatement.PressureField) {qbig : ℝ} (hq : qbig ≤ ChartScales.Q N) {L : ℕ → ℝ} (hs : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (particularP j) (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig)) (hb : ∀ (j m : ℕ), Bound qbig (particularP j) m (ActualIterationLedger.gain CorrectionInitialization.ActualPrimary.h (j + 1) - L m)) (j m : ℕ) : Bound qbig (pressure R M hN W particularP j) m (ActualIterationLedger.gain CorrectionInitialization.ActualPrimary.h (j + 1) - pressureLoss L m)

structure NavierStokes.GluedStageEstimates.Representations {B N0 N : ℕ} {D DA0 DP0 : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup DA0] [NormedSpace ℝ DA0] [NormedAddCommGroup DP0] [NormedSpace ℝ DP0] {I : Type u_1} {K : Type u_2} {IA0 : Type u_3} {KA0 : Type u_4} {IP0 : Type u_5} {KP0 : Type u_6} (R : ActualStageEstimates.RunData B N0) (M : ActualMeanPhysicalData.InitialCycleInput B N0 N fun (x : ℕ) => ActualCycleParameters.fixedParameters B N0) (hN : 4 ≤ N) (W : SignedInputs D I K) (particularA : ℕ → ProblemStatement.VelocityField) (particularP : ℕ → ProblemStatement.PressureField) {qbig : ℝ} (WA : PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h DA0 IA0 KA0 (Fin 3)) (WP : PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h DP0 IP0 KP0 Unit) (A Bdirect : ℕ → ProblemStatement.VelocityField) (P : ℕ → ProblemStatement.PressureField) : Prop

Six field identities on the common open sublevel. Their only content is identification of the actual sequence and its physical components.

• potential_zero : Set.EqOn (A 0) (ActualPhysicalStageBounds.initialPotential CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation CorrectionInitialization.ActualPrimary.upper B WA (ActualPhysicalStageBounds.actualInitialTemporalInput B N0 N hN) (ActualPhysicalStageBounds.actualInitialRankInput B N0 N hN)) (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig)
• direct_zero : Set.EqOn (Bdirect 0) (ActualMeanPhysicalData.initialAngularFamily B N0 N).angularField (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig)
• pressure_zero : Set.EqOn (P 0) (fun (w : ProblemStatement.SpaceTime) => FinalSlowBase.pressure CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation CorrectionInitialization.ActualPrimary.upper B w + ActualPhysicalStageBounds.initialPressureIncrement WP (ActualPhysicalStageBounds.actualInitialPressureInput B N0 N hN) w) (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig)
• potential_succ (j : ℕ) : Set.EqOn (potential R M hN W particularA j) (A (j + 1)) (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig)
• direct_succ (j : ℕ) : Set.EqOn (direct R M hN j) (Bdirect (j + 1)) (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig)
• pressure_succ (j : ℕ) : Set.EqOn (pressure R M hN W particularP j) (P (j + 1)) (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig)

theorem NavierStokes.GluedStageEstimates.Representations.potential_smooth {B N0 N : ℕ} {D DA0 DP0 : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup DA0] [NormedSpace ℝ DA0] [NormedAddCommGroup DP0] [NormedSpace ℝ DP0] {I : Type u_1} {K : Type u_2} {IA0 : Type u_3} {KA0 : Type u_4} {IP0 : Type u_5} {KP0 : Type u_6} (R : ActualStageEstimates.RunData B N0) (M : ActualMeanPhysicalData.InitialCycleInput B N0 N fun (x : ℕ) => ActualCycleParameters.fixedParameters B N0) (hN : 4 ≤ N) (W : SignedInputs D I K) (particularA : ℕ → ProblemStatement.VelocityField) (particularP : ℕ → ProblemStatement.PressureField) {qbig : ℝ} (hq : qbig ≤ ChartScales.Q N) (WA : PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h DA0 IA0 KA0 (Fin 3)) (WP : PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h DP0 IP0 KP0 Unit) {A Bdirect : ℕ → ProblemStatement.VelocityField} {P : ℕ → ProblemStatement.PressureField} (e : Representations R M hN W particularA particularP WA WP A Bdirect P) (hs : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (particularA j) (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig)) (j : ℕ) : ContDiffOn ℝ (↑⊤) (A j) (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig)

theorem NavierStokes.GluedStageEstimates.Representations.direct_smooth {B N0 N : ℕ} {D DA0 DP0 : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup DA0] [NormedSpace ℝ DA0] [NormedAddCommGroup DP0] [NormedSpace ℝ DP0] {I : Type u_1} {K : Type u_2} {IA0 : Type u_3} {KA0 : Type u_4} {IP0 : Type u_5} {KP0 : Type u_6} (R : ActualStageEstimates.RunData B N0) (M : ActualMeanPhysicalData.InitialCycleInput B N0 N fun (x : ℕ) => ActualCycleParameters.fixedParameters B N0) (hN : 4 ≤ N) (W : SignedInputs D I K) (particularA : ℕ → ProblemStatement.VelocityField) (particularP : ℕ → ProblemStatement.PressureField) {qbig : ℝ} (hq : qbig ≤ ChartScales.Q N) (WA : PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h DA0 IA0 KA0 (Fin 3)) (WP : PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h DP0 IP0 KP0 Unit) {A Bdirect : ℕ → ProblemStatement.VelocityField} {P : ℕ → ProblemStatement.PressureField} (e : Representations R M hN W particularA particularP WA WP A Bdirect P) (j : ℕ) : ContDiffOn ℝ (↑⊤) (Bdirect j) (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig)

theorem NavierStokes.GluedStageEstimates.Representations.pressure_smooth {B N0 N : ℕ} {D DA0 DP0 : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup DA0] [NormedSpace ℝ DA0] [NormedAddCommGroup DP0] [NormedSpace ℝ DP0] {I : Type u_1} {K : Type u_2} {IA0 : Type u_3} {KA0 : Type u_4} {IP0 : Type u_5} {KP0 : Type u_6} (R : ActualStageEstimates.RunData B N0) (M : ActualMeanPhysicalData.InitialCycleInput B N0 N fun (x : ℕ) => ActualCycleParameters.fixedParameters B N0) (hN : 4 ≤ N) (W : SignedInputs D I K) (particularA : ℕ → ProblemStatement.VelocityField) (particularP : ℕ → ProblemStatement.PressureField) {qbig : ℝ} (hq : qbig ≤ ChartScales.Q N) (WA : PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h DA0 IA0 KA0 (Fin 3)) (WP : PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h DP0 IP0 KP0 Unit) {A Bdirect : ℕ → ProblemStatement.VelocityField} {P : ℕ → ProblemStatement.PressureField} (e : Representations R M hN W particularA particularP WA WP A Bdirect P) (hs : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (particularP j) (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig)) (j : ℕ) : ContDiffOn ℝ (↑⊤) (P j) (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig)

theorem NavierStokes.GluedStageEstimates.represented_raw_bounds {B N0 N : ℕ} {D DA0 DP0 : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup DA0] [NormedSpace ℝ DA0] [NormedAddCommGroup DP0] [NormedSpace ℝ DP0] {I : Type u_1} {K : Type u_2} {IA0 : Type u_3} {KA0 : Type u_4} {IP0 : Type u_5} {KP0 : Type u_6} (R : ActualStageEstimates.RunData B N0) (M : ActualMeanPhysicalData.InitialCycleInput B N0 N fun (x : ℕ) => ActualCycleParameters.fixedParameters B N0) (hN : 4 ≤ N) (W : SignedInputs D I K) (particularA : ℕ → ProblemStatement.VelocityField) (particularP : ℕ → ProblemStatement.PressureField) {qbig : ℝ} (hq : qbig ≤ ChartScales.Q N) (WA : PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h DA0 IA0 KA0 (Fin 3)) (WP : PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h DP0 IP0 KP0 Unit) {A Bdirect : ℕ → ProblemStatement.VelocityField} {P : ℕ → ProblemStatement.PressureField} (e : Representations R M hN W particularA particularP WA WP A Bdirect P) {LA LP : ℕ → ℝ} (hsA : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (particularA j) (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig)) (hsP : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (particularP j) (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig)) (hbA : ∀ (j m : ℕ), Bound qbig (particularA j) m (ActualIterationLedger.gain CorrectionInitialization.ActualPrimary.h (j + 1) - LA m)) (hbP : ∀ (j m : ℕ), Bound qbig (particularP j) m (ActualIterationLedger.gain CorrectionInitialization.ActualPrimary.h (j + 1) - LP m)) : ∃ (CA : ℕ → ℕ → ℝ) (CB : ℕ → ℕ → ℝ) (CP : ℕ → ℕ → ℝ), (∀ (j m : ℕ), 0 ≤ CA j m ∧ 0 ≤ CB j m ∧ 0 ≤ CP j m) ∧ CutStageEstimates.RawStageBounds (PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h) A (ActualIterationLedger.gain CorrectionInitialization.ActualPrimary.h) (potentialLoss LA) CA (fun (x x_1 : ℕ) => 0) (PhysicalWaveSum.preterminal ∩ CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig) ∧ CutStageEstimates.RawStageBounds (PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h) Bdirect (ActualIterationLedger.gain CorrectionInitialization.ActualPrimary.h) (PhysicalStageBounds.directLoss CorrectionInitialization.ActualPrimary.h 0) CB (fun (x x_1 : ℕ) => 0) (PhysicalWaveSum.preterminal ∩ CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig) ∧ CutStageEstimates.RawStageBounds (PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h) P (ActualIterationLedger.gain CorrectionInitialization.ActualPrimary.h) (pressureLoss LP) CP (fun (x x_1 : ℕ) => 0) (PhysicalWaveSum.preterminal ∩ CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig)

The algebraic consumer of the separate current-particular estimates. The fixed-run native inputs derive all signed and mean estimates here.

noncomputable def NavierStokes.GluedStageEstimates.stageEstimatesOfComponentBounds {B N0 N : ℕ} {D DA0 DP0 : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup DA0] [NormedSpace ℝ DA0] [NormedAddCommGroup DP0] [NormedSpace ℝ DP0] {I : Type u_1} {K : Type u_2} {IA0 : Type u_3} {KA0 : Type u_4} {IP0 : Type u_5} {KP0 : Type u_6} (R : ActualStageEstimates.RunData B N0) (M : ActualMeanPhysicalData.InitialCycleInput B N0 N fun (x : ℕ) => ActualCycleParameters.fixedParameters B N0) (hN : 4 ≤ N) (W : SignedInputs D I K) (particularA : ℕ → ProblemStatement.VelocityField) (particularP : ℕ → ProblemStatement.PressureField) {qbig : ℝ} (hq : qbig ≤ ChartScales.Q N) (WA : PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h DA0 IA0 KA0 (Fin 3)) (WP : PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h DP0 IP0 KP0 Unit) {A Bdirect : ℕ → ProblemStatement.VelocityField} {P : ℕ → ProblemStatement.PressureField} (e : Representations R M hN W particularA particularP WA WP A Bdirect P) {LA LP : ℕ → ℝ} (hsA : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (particularA j) (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig)) (hsP : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (particularP j) (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig)) (hbA : ∀ (j m : ℕ), Bound qbig (particularA j) m (ActualIterationLedger.gain CorrectionInitialization.ActualPrimary.h (j + 1) - LA m)) (hbP : ∀ (j m : ℕ), Bound qbig (particularP j) m (ActualIterationLedger.gain CorrectionInitialization.ActualPrimary.h (j + 1) - LP m)) (hqbig : 0 < qbig) (hGeom : ActualCarrierGeometry.geometricThreshold ≤ N0) (d : ∀ (J : ℕ), ActualCycleResidualBounds.PhysicalData B (N + 1) (ActualCyclePreservation.state B N0 J).state (MixedDiagonalResidual.uncutVelocity A Bdirect J) (DiagonalJetBounds.uncutPrefix P (J + 1))) : MixedCandidateAssembly.StageEstimates CorrectionInitialization.ActualPrimary.h qbig A Bdirect P

The residual floor is fixed to the next band. Only exact physical realizations of finite prefixes enter the residual part of the proof.

Equations

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

The literal fields and native source data of the fixed run

noncomputable def NavierStokes.GluedStageEstimates.currentPotential (B N0 N j : ℕ) : ProblemStatement.VelocityField

Current potential, given by ActualValidBandWaves.gluedPotential (ActualCyclePreservation.state B N0 j) N.

Equations

• NavierStokes.GluedStageEstimates.currentPotential B N0 N j = NavierStokes.ActualValidBandWaves.gluedPotential (NavierStokes.ActualCyclePreservation.state B N0 j) N

noncomputable def NavierStokes.GluedStageEstimates.currentPressure (B N0 N j : ℕ) : ProblemStatement.PressureField

Current pressure, given by ActualValidBandWaves.gluedPressure (ActualCyclePreservation.state B N0 j) N.

Equations

• NavierStokes.GluedStageEstimates.currentPressure B N0 N j = NavierStokes.ActualValidBandWaves.gluedPressure (NavierStokes.ActualCyclePreservation.state B N0 j) N

theorem NavierStokes.GluedStageEstimates.glued_bound_of_local {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {N : ℕ} {f : ℕ → ProblemStatement.SpaceTime → E} {qbig r : ℝ} (m : ℕ) (hf : ValidDyadicBandCover.Compatible CorrectionInitialization.ActualPrimary.h N f) (hq : qbig ≤ ChartScales.Q N) (hb : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (n : ℕ), N ≤ n → ∀ w ∈ ValidDyadicBandCover.band CorrectionInitialization.ActualPrimary.h n, PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w ≤ ChartScales.Q n → PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w ≤ 1 → ‖iteratedFDeriv ℝ m (f n) w‖ ≤ C * PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w ^ r) : Bound qbig (ValidDyadicBandCover.field CorrectionInitialization.ActualPrimary.h N f) m r

Transfer a uniform estimate on comparable current bands to their actual glued representative. The bound has no factor counting charts.

theorem NavierStokes.GluedStageEstimates.localPotential_bound_of_modes {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (ActualInitialization.Index B N0)} (H : ActualParticularCycleData.Invariant σ x) (hGeom : ActualCarrierGeometry.geometricThreshold ≤ N0) (m : ℕ) {r : ℝ} (hb : ∀ (k : ℤ), k ≠ 0 → ∃ (C : ℝ), 0 ≤ C ∧ ∀ (l : ActualParticularStageControls.Label B N0) (n : ℕ), 4 ≤ n → ∀ w ∈ ValidDyadicBandCover.band CorrectionInitialization.ActualPrimary.h n, PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w ≤ 1 → ‖iteratedFDeriv ℝ m (ActualCurrentParticularPhysical.localPotentialMode (ActualCycleParameters.particularState x) l k n) w‖ ≤ C * PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w ^ r) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (n : ℕ), 4 ≤ n → ∀ w ∈ ValidDyadicBandCover.band CorrectionInitialization.ActualPrimary.h n, PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w ≤ 1 → ‖iteratedFDeriv ℝ m (ActualValidBandWaves.localPotential x n) w‖ ≤ C * PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w ^ r

The actual finite harmonic sum keeps the geometric factor 2250. The harmonic constants are summed before the band and point are chosen.

theorem NavierStokes.GluedStageEstimates.localPressure_bound_of_modes {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (ActualInitialization.Index B N0)} (H : ActualParticularCycleData.Invariant σ x) (hGeom : ActualCarrierGeometry.geometricThreshold ≤ N0) (m : ℕ) {r : ℝ} (hb : ∀ (k : ℤ), k ≠ 0 → ∃ (C : ℝ), 0 ≤ C ∧ ∀ (l : ActualParticularStageControls.Label B N0) (n : ℕ), 4 ≤ n → ∀ w ∈ ValidDyadicBandCover.band CorrectionInitialization.ActualPrimary.h n, PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w ≤ 1 → ‖iteratedFDeriv ℝ m (ActualCurrentParticularPhysical.localPressureMode (ActualCycleParameters.particularState x) l k n) w‖ ≤ C * PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w ^ r) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (n : ℕ), 4 ≤ n → ∀ w ∈ ValidDyadicBandCover.band CorrectionInitialization.ActualPrimary.h n, PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w ≤ 1 → ‖iteratedFDeriv ℝ m (ActualValidBandWaves.localPressure x n) w‖ ≤ C * PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w ^ r

theorem NavierStokes.GluedStageEstimates.current_preservesCarriers {B N0 : ℕ} (R : ActualStageEstimates.RunData B N0) (j : ℕ) : ActualParticularStageControls.PreservesCarriers (ActualCycleParameters.particularState (ActualCyclePreservation.state B N0 j))

theorem NavierStokes.GluedStageEstimates.current_inputSupport {B N0 : ℕ} (R : ActualStageEstimates.RunData B N0) (j : ℕ) : ActualParticularStageControls.InputSupport (ActualCycleParameters.particularState (ActualCyclePreservation.state B N0 j))

theorem NavierStokes.GluedStageEstimates.current_source_class {B N0 : ℕ} (R : ActualStageEstimates.RunData B N0) (j : ℕ) (k : ℤ) (hk : k ≠ 0) : LabelSumBounds.UniformWaveClass (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip ActualParticularStageControls.slowStrip)) ActualParticularStageControls.nativeEnvelope (1 / 2 + ActualIterationLedger.sigma j) (ActualParticularStageControls.currentSource (ActualCycleParameters.particularState (ActualCyclePreservation.state B N0 j)) k)

The source class is derived from the stored residual invariant and the actual label/coordinate reindexing.

theorem NavierStokes.GluedStageEstimates.current_compatible {B N0 : ℕ} (R : ActualStageEstimates.RunData B N0) (C : ∀ (j : ℕ), ActualCycleCoherence.Coherent (ActualCyclePreservation.state B N0 j)) (hGeom : ActualCarrierGeometry.geometricThreshold ≤ N0) (j N : ℕ) : ValidDyadicBandCover.Compatible CorrectionInitialization.ActualPrimary.h N (ActualValidBandWaves.localPotential (ActualCyclePreservation.state B N0 j)) ∧ ValidDyadicBandCover.Compatible CorrectionInitialization.ActualPrimary.h N (ActualValidBandWaves.localPressure (ActualCyclePreservation.state B N0 j))

theorem NavierStokes.GluedStageEstimates.current_fields_smooth {B N0 N : ℕ} (R : ActualStageEstimates.RunData B N0) (C : ∀ (j : ℕ), ActualCycleCoherence.Coherent (ActualCyclePreservation.state B N0 j)) (hGeom : ActualCarrierGeometry.geometricThreshold ≤ N0) {qbig : ℝ} (hq : qbig ≤ ChartScales.Q N) (j : ℕ) : ContDiffOn ℝ (↑⊤) (currentPotential B N0 N j) (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig) ∧ ContDiffOn ℝ (↑⊤) (currentPressure B N0 N j) (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig)

theorem NavierStokes.GluedStageEstimates.current_label_mem {B N0 : ℕ} (j n : ℕ) (l : ActualParticularStageControls.Label B N0) : l ∈ (ActualCycleParameters.particularState (ActualCyclePreservation.state B N0 j)).coefficients.labels n ↔ (l.2, l.1) ∈ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n

theorem NavierStokes.GluedStageEstimates.gain_le_current_exponent (j : ℕ) : ActualIterationLedger.gain CorrectionInitialization.ActualPrimary.h (j + 1) ≤ CorrectionInitialization.ActualPrimary.h * (1 / 2 + ActualIterationLedger.sigma j + 1 / 2)

theorem NavierStokes.GluedStageEstimates.current_loss_le_wave (degree : ℝ) (m : ℕ) : degree + 2 * CorrectionInitialization.ActualPrimary.h * ↑m + PhysicalGraphBounds.graphLoss m + 1 ≤ PhysicalGraphBounds.waveLoss CorrectionInitialization.ActualPrimary.h m + degree

The current-phase loss fits inside the original physical wave loss. The inequality uses the fixed condition h < 1/2.

theorem NavierStokes.GluedStageEstimates.current_potential_loss_le (m : ℕ) : CorrectionInitialization.ActualPrimary.h + 2 * CorrectionInitialization.ActualPrimary.h * ↑m + PhysicalGraphBounds.graphLoss m + 1 ≤ PhysicalStageBounds.potentialLoss CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.h 0 m

theorem NavierStokes.GluedStageEstimates.current_pressure_loss_le (m : ℕ) : 2 * CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h + 2 * CorrectionInitialization.ActualPrimary.h * ↑m + PhysicalGraphBounds.graphLoss m + 1 ≤ PhysicalStageBounds.pressureLoss CorrectionInitialization.ActualPrimary.h (2 * CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h) 0 m

theorem NavierStokes.GluedStageEstimates.current_potential_bound {B N0 N : ℕ} (R : ActualStageEstimates.RunData B N0) (C : ∀ (j : ℕ), ActualCycleCoherence.Coherent (ActualCyclePreservation.state B N0 j)) (hGeom : ActualCarrierGeometry.geometricThreshold ≤ N0) (hN : 4 ≤ N) {qbig : ℝ} (hq : qbig ≤ ChartScales.Q N) (j m : ℕ) : Bound qbig (currentPotential B N0 N j) m (ActualIterationLedger.gain CorrectionInitialization.ActualPrimary.h (j + 1) - PhysicalStageBounds.potentialLoss CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.h 0 m)

theorem NavierStokes.GluedStageEstimates.current_pressure_bound {B N0 N : ℕ} (R : ActualStageEstimates.RunData B N0) (C : ∀ (j : ℕ), ActualCycleCoherence.Coherent (ActualCyclePreservation.state B N0 j)) (hGeom : ActualCarrierGeometry.geometricThreshold ≤ N0) (hN : 4 ≤ N) {qbig : ℝ} (hq : qbig ≤ ChartScales.Q N) (j m : ℕ) : Bound qbig (currentPressure B N0 N j) m (ActualIterationLedger.gain CorrectionInitialization.ActualPrimary.h (j + 1) - PhysicalStageBounds.pressureLoss CorrectionInitialization.ActualPrimary.h (2 * CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h) 0 m)

@[reducible, inline]

abbrev NavierStokes.GluedStageEstimates.ActualRepresentations {B N0 N : ℕ} (R : ActualStageEstimates.RunData B N0) {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (M : ActualMeanPhysicalData.InitialCycleInput B N0 N fun (x : ℕ) => ActualCycleParameters.fixedParameters B N0) (hN : 4 ≤ N) (W : SignedInputs D I K) (qbig : ℝ) (A Bdirect : ℕ → ProblemStatement.VelocityField) (P : ℕ → ProblemStatement.PressureField) : Prop

The representation record specialized to the exact glued particular fields and the constructed initial primary wave data.

Equations

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

noncomputable def NavierStokes.GluedStageEstimates.actualStageEstimates {B N0 N : ℕ} (R : ActualStageEstimates.RunData B N0) {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (M : ActualMeanPhysicalData.InitialCycleInput B N0 N fun (x : ℕ) => ActualCycleParameters.fixedParameters B N0) (hN : 4 ≤ N) (W : SignedInputs D I K) (C : ∀ (j : ℕ), ActualCycleCoherence.Coherent (ActualCyclePreservation.state B N0 j)) {qbig : ℝ} (hq : qbig ≤ ChartScales.Q N) (hqbig : 0 < qbig) (hGeom : ActualCarrierGeometry.geometricThreshold ≤ N0) (A Bdirect : ℕ → ProblemStatement.VelocityField) (P : ℕ → ProblemStatement.PressureField) (e : ActualRepresentations R M hN W qbig A Bdirect P) (d : ∀ (J : ℕ), ActualCycleResidualBounds.PhysicalData B (N + 1) (ActualCyclePreservation.state B N0 J).state (MixedDiagonalResidual.uncutVelocity A Bdirect J) (DiagonalJetBounds.uncutPrefix P (J + 1))) : MixedCandidateAssembly.StageEstimates CorrectionInitialization.ActualPrimary.h qbig A Bdirect P

The actual glued current-band rates, native signed/mean data, and exact finite-prefix realizations supply the complete mixed-stage record. No physical derivative estimate is a premise of this constructor.

Equations

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

theorem NavierStokes.GluedStageEstimates.actualStageEstimates_ledger {B N0 N : ℕ} (R : ActualStageEstimates.RunData B N0) {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (M : ActualMeanPhysicalData.InitialCycleInput B N0 N fun (x : ℕ) => ActualCycleParameters.fixedParameters B N0) (hN : 4 ≤ N) (W : SignedInputs D I K) (C : ∀ (j : ℕ), ActualCycleCoherence.Coherent (ActualCyclePreservation.state B N0 j)) {qbig : ℝ} (hq : qbig ≤ ChartScales.Q N) (hqbig : 0 < qbig) (hGeom : ActualCarrierGeometry.geometricThreshold ≤ N0) (A Bdirect : ℕ → ProblemStatement.VelocityField) (P : ℕ → ProblemStatement.PressureField) (e : ActualRepresentations R M hN W qbig A Bdirect P) (d : ∀ (J : ℕ), ActualCycleResidualBounds.PhysicalData B (N + 1) (ActualCyclePreservation.state B N0 J).state (MixedDiagonalResidual.uncutVelocity A Bdirect J) (DiagonalJetBounds.uncutPrefix P (J + 1))) : have E := actualStageEstimates R M hN W C hq hqbig hGeom A Bdirect P e d; E.gain = ActualIterationLedger.gain CorrectionInitialization.ActualPrimary.h ∧ E.potentialLoss = PhysicalStageBounds.potentialLoss CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.h 0 ∧ E.directLoss = PhysicalStageBounds.directLoss CorrectionInitialization.ActualPrimary.h 0 ∧ E.pressureLoss = PhysicalStageBounds.pressureLoss CorrectionInitialization.ActualPrimary.h (2 * CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h) 0 ∧ E.backgroundLoss = ActualStageEstimates.backgroundLoss 1 (-CorrectionInitialization.ActualPrimary.h) ∧ E.residualLoss = ActualCycleResidualBounds.fixedLoss