The actual initial primary potential and its physical copies

Every field below uses the fixed ActualPrimary.choice B N0. The normal-potential operator is applied to the actual cutoff amplitude; its estimates are obtained from the existing support-local primitive controls. The lattice index is retained through Cartesian realization.

Full-chart regularity of the initial native copy coefficients

The copied fields use the actual flat radial attachment. Their regularity holds across its boundary, rather than only inside the native estimate domain. The stripped coefficients are independent of the angular variable.

@[reducible, inline]

abbrev NavierStokes.InitialNativeRegularity.Point : Type

Point: an abbreviation for ActualPrimary.FullPoint.

Equations

• NavierStokes.InitialNativeRegularity.Point = NavierStokes.CorrectionInitialization.ActualPrimary.FullPoint

@[reducible, inline]

abbrev NavierStokes.InitialNativeRegularity.Frequency : Type

Frequency: an abbreviation for TorusInverse.Frequency.

Equations

• NavierStokes.InitialNativeRegularity.Frequency = NavierStokes.TorusInverse.Frequency

noncomputable def NavierStokes.InitialNativeRegularity.copyAmplitude {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) (k : Frequency) (n : ℕ) (x : Point) : HarmonicCalculus.ComplexVector

The same copied amplitude used by InitialPhysicalData.

Equations

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

noncomputable def NavierStokes.InitialNativeRegularity.copyPressureCoefficient {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) (k : Frequency) (n : ℕ) (x : Point) : ℂ

The pressure scaling exponent is twice the velocity exponent.

Equations

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

noncomputable def NavierStokes.InitialNativeRegularity.copyPotentialCoefficient {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) (k : Frequency) (n : ℕ) (x : Point) : HarmonicCalculus.ComplexVector

The actual inverse-carrier potential formed from the copied amplitude.

Equations

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

theorem NavierStokes.InitialNativeRegularity.gaussian_smooth {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) : ContDiff ℝ (↑⊤) (CorrectionInitialization.ActualPrimary.gaussian l.2)

theorem NavierStokes.InitialNativeRegularity.cutNativeVelocity_smooth {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) : ContDiffOn ℝ (↑⊤) (ActualPrimaryBounds.cutNativeVelocity l) WaveEdgeExtension.nativeSlowDomain

The radial-edge attachment is used before taking the copy.

theorem NavierStokes.InitialNativeRegularity.cutNativePressure_smooth {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) : ContDiffOn ℝ (↑⊤) (ActualPrimaryBounds.cutNativePressure l) WaveEdgeExtension.nativeSlowDomain

theorem NavierStokes.InitialNativeRegularity.copyPoint_mapsTo {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) (k : Frequency) (n : ℕ) : Set.MapsTo (fun (x : Point) => ActualPrimaryBounds.copyPoint l n k (ActualPrimaryBounds.nativeOfFull x)) ActualPrimaryCoherence.positiveChart WaveEdgeExtension.nativeSlowDomain

theorem NavierStokes.InitialNativeRegularity.copied_smooth {B N0 : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (a : ℝ) (f : ActualPrimaryBounds.SignedLabel B N0 → ActualPrimaryBounds.Native → E) (hf : ∀ (l : ActualPrimaryBounds.SignedLabel B N0), ContDiffOn ℝ (↑⊤) (f l) WaveEdgeExtension.nativeSlowDomain) (l : ActualPrimaryBounds.SignedLabel B N0) (k : Frequency) (n : ℕ) : ContDiffOn ℝ (↑⊤) (fun (x : Point) => ActualPrimaryBounds.copied a f l n k (ActualPrimaryBounds.nativeOfFull x)) ActualPrimaryCoherence.positiveChart

The band cutoff is discrete. In active bands the copy map preserves positive native time, and in all other bands the field is identically zero.

theorem NavierStokes.InitialNativeRegularity.copyAmplitude_smooth {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) (k : Frequency) (n : ℕ) : ContDiffOn ℝ (↑⊤) (copyAmplitude l k n) ActualPrimaryCoherence.positiveChart

theorem NavierStokes.InitialNativeRegularity.copyPressureCoefficient_smooth {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) (k : Frequency) (n : ℕ) : ContDiffOn ℝ (↑⊤) (copyPressureCoefficient l k n) ActualPrimaryCoherence.positiveChart

This holds on the larger positive-time chart, including zero radius.

theorem NavierStokes.InitialNativeRegularity.cutNormal_eq {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) (n : ℕ) : (ActualPrimaryBounds.cutCoefficients l).normal ActualPrimaryBounds.fullStrip (ActualPrimaryBounds.directions B) n = (CorrectionInitialization.ActualPrimary.chartCoefficients l.1 l.2).normal ActualPrimaryBounds.fullStrip (ActualPrimaryBounds.directions B) n

theorem NavierStokes.InitialNativeRegularity.normal_eq_absolute {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) (n : ℕ) : (ActualPrimaryBounds.cutCoefficients l).normal ActualPrimaryBounds.fullStrip (ActualPrimaryBounds.directions B) n = fun (x : ActualPrimaryCoherence.ChartPoint) => (1 / ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n) * √(ChartScales.Q n)) • ActualPrimaryCoherence.absoluteNormal l.1 l.2 ((ActualPrimaryCoherence.absoluteChart n) x)

theorem NavierStokes.InitialNativeRegularity.normal_smooth {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) (n : ℕ) : ContDiffOn ℝ (↑⊤) ((ActualPrimaryBounds.cutCoefficients l).normal ActualPrimaryBounds.fullStrip (ActualPrimaryBounds.directions B) n) ActualPrimaryCoherence.positiveRadialChart

theorem NavierStokes.InitialNativeRegularity.normal_ne {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) (n : ℕ) {x : Point} (hx : x ∈ ActualPrimaryCoherence.positiveRadialChart) : (ActualPrimaryBounds.cutCoefficients l).normal ActualPrimaryBounds.fullStrip (ActualPrimaryBounds.directions B) n x ≠ 0

theorem NavierStokes.InitialNativeRegularity.copyPotentialCoefficient_smooth {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) (k : Frequency) (n : ℕ) : ContDiffOn ℝ (↑⊤) (copyPotentialCoefficient l k n) ActualPrimaryCoherence.positiveRadialChart

Joint smoothness includes every radial support boundary at positive radius and time. There is no interior-support restriction.

theorem NavierStokes.InitialNativeRegularity.copyPressureCoefficient_smooth_radial {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) (k : Frequency) (n : ℕ) : ContDiffOn ℝ (↑⊤) (copyPressureCoefficient l k n) ActualPrimaryCoherence.positiveRadialChart

theorem NavierStokes.InitialNativeRegularity.normal_invariant {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) (n : ℕ) : CopyAngularInvariance.Invariant (0, 1) ((ActualPrimaryBounds.cutCoefficients l).normal ActualPrimaryBounds.fullStrip (ActualPrimaryBounds.directions B) n)

The true phase is affine in angle, so its actual phase normal is angle-independent even where derivatives are defined by totalization.

theorem NavierStokes.InitialNativeRegularity.copyAmplitude_invariant {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) (k : Frequency) (n : ℕ) : CopyAngularInvariance.Invariant (0, 1) (copyAmplitude l k n)

theorem NavierStokes.InitialNativeRegularity.copyPressureCoefficient_invariant {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) (k : Frequency) (n : ℕ) : CopyAngularInvariance.Invariant (0, 1) (copyPressureCoefficient l k n)

theorem NavierStokes.InitialNativeRegularity.copyPotentialCoefficient_invariant {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) (k : Frequency) (n : ℕ) : CopyAngularInvariance.Invariant (0, 1) (copyPotentialCoefficient l k n)

theorem NavierStokes.InitialNativeRegularity.copyAmplitude_angle {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) (k : Frequency) (n : ℕ) (x : LocalSignedRequest.Point) (θ : ℝ) : copyAmplitude l k n (x, θ) = copyAmplitude l k n (x, 0)

theorem NavierStokes.InitialNativeRegularity.copyPressureCoefficient_angle {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) (k : Frequency) (n : ℕ) (x : LocalSignedRequest.Point) (θ : ℝ) : copyPressureCoefficient l k n (x, θ) = copyPressureCoefficient l k n (x, 0)

theorem NavierStokes.InitialNativeRegularity.copyPotentialCoefficient_angle {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) (k : Frequency) (n : ℕ) (x : LocalSignedRequest.Point) (θ : ℝ) : copyPotentialCoefficient l k n (x, θ) = copyPotentialCoefficient l k n (x, 0)

@[reducible, inline]

abbrev NavierStokes.InitialPhysicalData.Point : Type

Point: an abbreviation for ActualPrimary.FullPoint.

Equations

• NavierStokes.InitialPhysicalData.Point = NavierStokes.CorrectionInitialization.ActualPrimary.FullPoint

@[reducible, inline]

abbrev NavierStokes.InitialPhysicalData.SignedLabel (B N0 : ℕ) : Type

Signed label: an abbreviation for ActualPrimaryBounds.SignedLabel B N0.

Equations

• NavierStokes.InitialPhysicalData.SignedLabel B N0 = NavierStokes.ActualPrimaryBounds.SignedLabel B N0

@[reducible, inline]

abbrev NavierStokes.InitialPhysicalData.Frequency : Type

Frequency: an abbreviation for TorusInverse.Frequency.

Equations

• NavierStokes.InitialPhysicalData.Frequency = NavierStokes.TorusInverse.Frequency

noncomputable def NavierStokes.InitialPhysicalData.potentialCoefficient {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) (x : Point) : HarmonicCalculus.ComplexVector

The coefficient of the genuine vector potential, before restoring its carrier. The Gaussian cutoff occurs in cutCoefficients once.

Equations

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

theorem NavierStokes.InitialPhysicalData.potentialCoefficient_zero {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) (x : Point) (ha : (ActualPrimaryBounds.cutCoefficients l).amplitude n x = 0) : potentialCoefficient l n x = 0

theorem NavierStokes.InitialPhysicalData.potentialCoefficient_zero_germ {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) {x : Point} (ha : (ActualPrimaryBounds.cutCoefficients l).amplitude n =ᶠ[nhds x] fun (x : Point) => 0) : potentialCoefficient l n =ᶠ[nhds x] fun (x : Point) => 0

theorem NavierStokes.InitialPhysicalData.potentialCoefficient_local {B N0 : ℕ} : LocalizedWaveBounds.LocalWave ActualPrimaryBounds.fullStrip ActualPrimaryBounds.controlCell (fun (n : ℕ) (i : ActualPrimaryBounds.CopyIndex B N0) => ActualPrimaryBounds.fullEnvelope i.1 n) 1 fun (n : ℕ) (i : ActualPrimaryBounds.CopyIndex B N0) => potentialCoefficient i.1 n

theorem NavierStokes.InitialPhysicalData.potentialCoefficient_uniform {B N0 : ℕ} : LabelSumBounds.UniformWaveClass ActualPrimaryBounds.fullStrip ActualPrimaryBounds.fullEnvelope 1 potentialCoefficient

Uniformity is over the entire signed label family. On the complement of the genuine phase patches the actual amplitude has a zero germ.

theorem NavierStokes.InitialPhysicalData.uniform_of_germ_or_zero {D E I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {w : I → ℕ → D → ℝ} {α : ℝ} {f0 g0 : I → ℕ → D → E} (hf : LabelSumBounds.UniformClass s w α f0) (hg : ∀ (i : I) (n : ℕ), ∀ x ∈ s.domain, g0 i n =ᶠ[nhds x] f0 i n ∨ g0 i n =ᶠ[nhds x] fun (x : D) => 0) : LabelSumBounds.UniformClass s w α g0

A supported copy inherits the same constants when it is locally equal to the full coefficient or to zero.

noncomputable def NavierStokes.InitialPhysicalData.copyAmplitude {B N0 : ℕ} (l : SignedLabel B N0) (k : Frequency) (n : ℕ) (x : Point) : HarmonicCalculus.ComplexVector

Copy amplitude, given by copied (CoordinateAlgebra.A ActualPrimary.h) cutNativeVelocity l n k (nativeOfFull x).

Equations

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

noncomputable def NavierStokes.InitialPhysicalData.copyPressureCoefficient {B N0 : ℕ} (l : SignedLabel B N0) (k : Frequency) (n : ℕ) (x : Point) : ℂ

Copy pressure coefficient, given by copied (2 * CoordinateAlgebra.A ActualPrimary.h) cutNativePressure l n k (nativeOfFull x).

Equations

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

noncomputable def NavierStokes.InitialPhysicalData.copyPotentialCoefficient {B N0 : ℕ} (l : SignedLabel B N0) (k : Frequency) (n : ℕ) (x : Point) : HarmonicCalculus.ComplexVector

Copy potential coefficient, constructed using CurlClassBounds.inverseCarrier.

Equations

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

theorem NavierStokes.InitialPhysicalData.copyAmplitude_germ {B N0 : ℕ} (l : SignedLabel B N0) (k : Frequency) (n : ℕ) {x : Point} (hx : x ∈ ActualPrimaryBounds.fullStrip.domain) (hk : ActualPrimaryBounds.nativeOfFull x ∈ (ActualPrimaryBounds.copyCells l).carrier n k) : copyAmplitude l k n =ᶠ[nhds x] (ActualPrimaryBounds.cutCoefficients l).amplitude n

theorem NavierStokes.InitialPhysicalData.copyAmplitude_zero_germ {B N0 : ℕ} (l : SignedLabel B N0) (k : Frequency) (n : ℕ) {x : Point} (hk : ActualPrimaryBounds.nativeOfFull x ∉ (ActualPrimaryBounds.copyCells l).carrier n k) : copyAmplitude l k n =ᶠ[nhds x] fun (x : Point) => 0

theorem NavierStokes.InitialPhysicalData.copyPotential_germ {B N0 : ℕ} (l : SignedLabel B N0) (k : Frequency) (n : ℕ) {x : Point} (hx : x ∈ ActualPrimaryBounds.fullStrip.domain) (hk : ActualPrimaryBounds.nativeOfFull x ∈ (ActualPrimaryBounds.copyCells l).carrier n k) : copyPotentialCoefficient l k n =ᶠ[nhds x] potentialCoefficient l n

theorem NavierStokes.InitialPhysicalData.copyPotential_zero_germ {B N0 : ℕ} (l : SignedLabel B N0) (k : Frequency) (n : ℕ) {x : Point} (hk : ActualPrimaryBounds.nativeOfFull x ∉ (ActualPrimaryBounds.copyCells l).carrier n k) : copyPotentialCoefficient l k n =ᶠ[nhds x] fun (x : Point) => 0

theorem NavierStokes.InitialPhysicalData.copyPressure_germ {B N0 : ℕ} (l : SignedLabel B N0) (k : Frequency) (n : ℕ) {x : Point} (hx : x ∈ ActualPrimaryBounds.fullStrip.domain) (hk : ActualPrimaryBounds.nativeOfFull x ∈ (ActualPrimaryBounds.copyCells l).carrier n k) : copyPressureCoefficient l k n =ᶠ[nhds x] (ActualPrimaryBounds.cutCoefficients l).pressure n

theorem NavierStokes.InitialPhysicalData.copyPressure_zero_germ {B N0 : ℕ} (l : SignedLabel B N0) (k : Frequency) (n : ℕ) {x : Point} (hk : ActualPrimaryBounds.nativeOfFull x ∉ (ActualPrimaryBounds.copyCells l).carrier n k) : copyPressureCoefficient l k n =ᶠ[nhds x] fun (x : Point) => 0

theorem NavierStokes.InitialPhysicalData.copyPotential_uniform {B N0 : ℕ} : LabelSumBounds.UniformWaveClass ActualPrimaryBounds.fullStrip (fun (i : SignedLabel B N0 × Frequency) => ActualPrimaryBounds.fullEnvelope i.1) 1 fun (i : SignedLabel B N0 × Frequency) => copyPotentialCoefficient i.1 i.2

theorem NavierStokes.InitialPhysicalData.copyPressure_uniform {B N0 : ℕ} : LabelSumBounds.UniformWaveClass ActualPrimaryBounds.fullStrip (fun (i : SignedLabel B N0 × Frequency) => ActualPrimaryBounds.fullEnvelope i.1) 1 fun (i : SignedLabel B N0 × Frequency) => copyPressureCoefficient i.1 i.2

noncomputable def NavierStokes.InitialPhysicalData.bandLabel {B N0 : ℕ} (l : SignedLabel B N0) : PhysicalWaveSum.BandLabel

Band label, given by ⟨spatialLabel l, label_large l⟩.

Equations

• NavierStokes.InitialPhysicalData.bandLabel l = ⟨NavierStokes.ActualPrimaryBounds.spatialLabel l, ⋯⟩

theorem NavierStokes.InitialPhysicalData.bandLabel_injective {B N0 : ℕ} : Function.Injective bandLabel

noncomputable def NavierStokes.InitialPhysicalData.active {B N0 : ℕ} : Set PhysicalWaveSum.BandLabel

Active, given by Set.range (bandLabel (B := B) (N0 := N0)).

Equations

• NavierStokes.InitialPhysicalData.active = Set.range NavierStokes.InitialPhysicalData.bandLabel

noncomputable def NavierStokes.InitialPhysicalData.selected {B N0 : ℕ} (L : PhysicalWaveSum.BandLabel) (hL : L ∈ active) : SignedLabel B N0

Selected, given by hL.choose.

Equations

• NavierStokes.InitialPhysicalData.selected L hL = Exists.choose hL

theorem NavierStokes.InitialPhysicalData.selected_label {B N0 : ℕ} (L : PhysicalWaveSum.BandLabel) (hL : L ∈ active) : bandLabel (selected L hL) = L

theorem NavierStokes.InitialPhysicalData.selected_band {B N0 : ℕ} (L : PhysicalWaveSum.BandLabel) (hL : L ∈ active) : BaseChartJets.cellBand (selected L hL).2 = (↑L).1

theorem NavierStokes.InitialPhysicalData.selected_eq {B N0 : ℕ} (l : SignedLabel B N0) (hL : bandLabel l ∈ active) : selected (bandLabel l) hL = l

noncomputable def NavierStokes.InitialPhysicalData.gap (L : PhysicalWaveSum.BandLabel) : ℕ

Gap, given by ChartScales.nativeIndex ActualPrimary.h L.val.1 - CommonWindow.index ActualPrimary.h L.val.1.

Equations

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

noncomputable def NavierStokes.InitialPhysicalData.geometry (L : PhysicalWaveSum.BandLabel) : CommonCoverSolve.Geometry

Geometry, given by ActualSignedPhysicalData.geometry ActualPrimary.slots L.val (gap L).

Equations

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

theorem NavierStokes.InitialPhysicalData.geometry_bandLabel {B N0 : ℕ} (l : SignedLabel B N0) : geometry (bandLabel l) = CorrectionInitialization.ActualPrimary.chartGeometry (BaseChartJets.cellBand l.2) l.1 l.2

noncomputable def NavierStokes.InitialPhysicalData.selectedCarrier {B N0 : ℕ} (l : SignedLabel B N0) (k : Frequency) : PhysicalWaveSum.CarrierData

Selected carrier, constructed using ActualSignedPhysicalData.carrier.

Equations

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

noncomputable def NavierStokes.InitialPhysicalData.carrier {B N0 : ℕ} (L : PhysicalWaveSum.BandLabel) (k : Frequency) : PhysicalWaveSum.CarrierData

Carrier, with branches according to hL : L ∈ active (B := B) (N0 := N0).

Equations

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

theorem NavierStokes.InitialPhysicalData.carrier_bandLabel {B N0 : ℕ} (l : SignedLabel B N0) (k : Frequency) : carrier (bandLabel l) k = selectedCarrier l k

theorem NavierStokes.InitialPhysicalData.selectedCarrier_center {B N0 : ℕ} (l : SignedLabel B N0) (k : Frequency) : (selectedCarrier l k).center = ActualSignedPhysicalData.center (ActualPrimaryBounds.spatialLabel l) k

@[reducible, inline]

abbrev NavierStokes.InitialPhysicalData.SourceIndex : Type

Source index: an abbreviation for PhysicalWaveSum.WaveIndex 1 × Frequency.

Equations

• NavierStokes.InitialPhysicalData.SourceIndex = (NavierStokes.PhysicalWaveSum.WaveIndex 1 × NavierStokes.InitialPhysicalData.Frequency)

noncomputable def NavierStokes.InitialPhysicalData.sourceChoice {B N0 : ℕ} (I : SourceIndex) : Option (SignedLabel B N0 × Frequency)

Source choice, with branches according to hL : I.1.1 ∈ active (B := B) (N0 := N0).

Equations

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

noncomputable def NavierStokes.InitialPhysicalData.sourceFamily {B N0 : ℕ} {E : Type} [Zero E] (f : SignedLabel B N0 × Frequency → ℕ → LocalSignedRequest.Point → E) (I : SourceIndex) (n : ℕ) (x : LocalSignedRequest.Point) : E

Source family, with branches according to n = I.1.1.val.1.

Equations

• NavierStokes.InitialPhysicalData.sourceFamily f I n x = if n = (↑I.1.1).1 then match NavierStokes.InitialPhysicalData.sourceChoice I with | some l => f l n x | none => 0 else 0

theorem NavierStokes.InitialPhysicalData.sourceFamily_eq_some {B N0 : ℕ} {E : Type} [Zero E] (f : SignedLabel B N0 × Frequency → ℕ → LocalSignedRequest.Point → E) (I : SourceIndex) (n : ℕ) (hn : n = (↑I.1.1).1) (l : SignedLabel B N0 × Frequency) (hl : sourceChoice I = some l) : sourceFamily f I n = f l n

theorem NavierStokes.InitialPhysicalData.sourceFamily_eq_zero {B N0 : ℕ} {E : Type} [Zero E] (f : SignedLabel B N0 × Frequency → ℕ → LocalSignedRequest.Point → E) (I : SourceIndex) (n : ℕ) (hz : n ≠ (↑I.1.1).1 ∨ sourceChoice I = none) : sourceFamily f I n = fun (x : LocalSignedRequest.Point) => 0

theorem NavierStokes.InitialPhysicalData.sourceFamily_uniform {B N0 : ℕ} {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : SignedLabel B N0 × Frequency → ℕ → LocalSignedRequest.Point → E} (hf : LabelSumBounds.UniformClass ActualPrimaryBounds.strip (fun (x : SignedLabel B N0 × Frequency) (x_1 : ℕ) (x_2 : ActualPrimaryBounds.Point) => √(ActualPrimaryBounds.strip.zeta x_2)) 1 f) : LabelSumBounds.UniformClass ActualPrimaryBounds.strip (fun (x : SourceIndex) (x_1 : ℕ) (x_2 : ActualPrimaryBounds.Point) => √(ActualPrimaryBounds.strip.zeta x_2)) 1 (sourceFamily f)

noncomputable def NavierStokes.InitialPhysicalData.nativePotentialSource (B N0 : ℕ) : SourceIndex → ℕ → LocalSignedRequest.Point → HarmonicCalculus.ComplexVector

Native potential source, given by sourceFamily (fun (l : SignedLabel B N0 × Frequency) n x => copyPotentialCoefficient l.1 l.2 n (x, 0)).

Equations

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

noncomputable def NavierStokes.InitialPhysicalData.nativePressureSource (B N0 : ℕ) : SourceIndex → ℕ → LocalSignedRequest.Point → ℂ

Native pressure source, given by sourceFamily (fun (l : SignedLabel B N0 × Frequency) n x => copyPressureCoefficient l.1 l.2 n (x, 0)).

Equations

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

theorem NavierStokes.InitialPhysicalData.nativePotentialSource_uniform {B N0 : ℕ} : LabelSumBounds.UniformClass ActualPrimaryBounds.strip (fun (x : SourceIndex) (x_1 : ℕ) (x_2 : ActualPrimaryBounds.Point) => √(ActualPrimaryBounds.strip.zeta x_2)) 1 (nativePotentialSource B N0)

theorem NavierStokes.InitialPhysicalData.nativePressureSource_uniform {B N0 : ℕ} : LabelSumBounds.UniformClass ActualPrimaryBounds.strip (fun (x : SourceIndex) (x_1 : ℕ) (x_2 : ActualPrimaryBounds.Point) => √(ActualPrimaryBounds.strip.zeta x_2)) 1 (nativePressureSource B N0)

noncomputable def NavierStokes.InitialPhysicalData.potentialFamily (B N0 : ℕ) (i : Fin 3) : PhysicalCopyBounds.CopyFamily 1 Frequency

Potential family, bundling gap, carrier, amplitude, CartesianCopySource.

Equations

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

noncomputable def NavierStokes.InitialPhysicalData.pressureFamily (B N0 : ℕ) : PhysicalCopyBounds.CopyFamily 1 Frequency

Pressure family, bundling gap, carrier, amplitude, nativePressureSource.

Equations

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

theorem NavierStokes.InitialPhysicalData.strip_flat_geometry : ∃ (cL : ℝ) (cR : ℝ) (L : ℝ) (ρ : LocalSignedRequest.Point → ℝ), PhysicalClassBounds.FlatGeometry ActualPrimaryBounds.strip cL cR L ρ

theorem NavierStokes.InitialPhysicalData.native_source_bounds {E I : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : I → ℕ → LocalSignedRequest.Point → E} (hf : LabelSumBounds.UniformClass ActualPrimaryBounds.strip (fun (x : I) (x_1 : ℕ) (x_2 : ActualPrimaryBounds.Point) => √(ActualPrimaryBounds.strip.zeta x_2)) 1 f) : LocalPhysicalCopyBounds.LocalSourceBounds ActualPrimaryBounds.strip CorrectionInitialization.ActualPrimary.h 1 (fun (x : I) (x_1 : ℕ) (x_2 : ActualPrimaryBounds.Point) => √(ActualPrimaryBounds.strip.zeta x_2)) f

theorem NavierStokes.InitialPhysicalData.nativePotentialSource_bounds {B N0 : ℕ} : LocalPhysicalCopyBounds.LocalSourceBounds ActualPrimaryBounds.strip CorrectionInitialization.ActualPrimary.h 1 (fun (x : SourceIndex) (x_1 : ℕ) (x_2 : ActualPrimaryBounds.Point) => √(ActualPrimaryBounds.strip.zeta x_2)) (nativePotentialSource B N0)

theorem NavierStokes.InitialPhysicalData.nativePressureSource_bounds {B N0 : ℕ} : LocalPhysicalCopyBounds.LocalSourceBounds ActualPrimaryBounds.strip CorrectionInitialization.ActualPrimary.h 1 (fun (x : SourceIndex) (x_1 : ℕ) (x_2 : ActualPrimaryBounds.Point) => √(ActualPrimaryBounds.strip.zeta x_2)) (nativePressureSource B N0)

theorem NavierStokes.InitialPhysicalData.near_self {B N0 : ℕ} (l : SignedLabel B N0) : ActualPrimaryBounds.near l (BaseChartJets.cellBand l.2)

theorem NavierStokes.InitialPhysicalData.copyPoint_self {B N0 : ℕ} (l : SignedLabel B N0) (k : Frequency) (x : ActualSignedGeometry.Native) : ActualPrimaryBounds.copyPoint l (BaseChartJets.cellBand l.2) k x = (x.1, (geometry (bandLabel l)).coordinates k x.2)

theorem NavierStokes.InitialPhysicalData.copied_self {B N0 : ℕ} {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (a : ℝ) (f : SignedLabel B N0 → ActualSignedGeometry.Native → E) (l : SignedLabel B N0) (k : Frequency) (x : ActualSignedGeometry.Native) : ActualPrimaryBounds.copied a f l (BaseChartJets.cellBand l.2) k x = f l (x.1, (geometry (bandLabel l)).coordinates k x.2)

theorem NavierStokes.InitialPhysicalData.attached_pair_support {B N0 : ℕ} (l : SignedLabel B N0) (x : ActualSignedGeometry.Native) (hne : CorrectionInitialization.ActualPrimary.attachedRawVelocity l.1 l.2 x ≠ 0 ∨ CorrectionInitialization.ActualPrimary.attachedRawPressure l.1 l.2 x ≠ 0) : WaveEdgeExtension.nativeRadius CorrectionInitialization.ActualPrimary.h x ∈ Set.Ioo (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal) ∧ SimilarityHomogeneity.chartQ CorrectionInitialization.ActualPrimary.h x.1 ∈ Set.Ioo (1 / 2) 2 ∧ x.1 ∈ ActualGaussianCoverage.actualSlowCore CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation (CorrectionInitialization.ActualPrimary.choice B N0).prepared l.2 ∧ x.2 ∈ (CorrectionInitialization.ActualPrimary.clockWindow l.2).core

theorem NavierStokes.InitialPhysicalData.cut_pair_support {B N0 : ℕ} (l : SignedLabel B N0) (x : ActualSignedGeometry.Native) (hne : ActualPrimaryBounds.cutNativeVelocity l x ≠ 0 ∨ ActualPrimaryBounds.cutNativePressure l x ≠ 0) : WaveEdgeExtension.nativeRadius CorrectionInitialization.ActualPrimary.h x ∈ Set.Ioo (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal) ∧ SimilarityHomogeneity.chartQ CorrectionInitialization.ActualPrimary.h x.1 ∈ Set.Ioo (1 / 2) 2 ∧ x.1 ∈ ActualGaussianCoverage.actualSlowCore CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation (CorrectionInitialization.ActualPrimary.choice B N0).prepared l.2 ∧ x.2 ∈ (CorrectionInitialization.ActualPrimary.clockWindow l.2).core

@[reducible, inline]

abbrev NavierStokes.InitialPhysicalData.LiftPoint : Type

Lift point: an abbreviation for PhysicalGraphBounds.LiftPoint.

Equations

• NavierStokes.InitialPhysicalData.LiftPoint = NavierStokes.PhysicalGraphBounds.LiftPoint

noncomputable def NavierStokes.InitialPhysicalData.slowInput (x : LiftPoint) : PhaseCalculus.Slow

Slow input, given by (ActualSignedGeometry.meanEquiv.symm (PhysicalClassBounds.cylindricalMap x)).1.

Equations

• NavierStokes.InitialPhysicalData.slowInput x = (NavierStokes.ActualSignedGeometry.meanEquiv.symm (NavierStokes.PhysicalClassBounds.cylindricalMap x)).1

theorem NavierStokes.InitialPhysicalData.slowInput_continuous : Continuous slowInput

noncomputable def NavierStokes.InitialPhysicalData.nativeAt (L : PhysicalWaveSum.BandLabel) (k : Frequency) (x : LiftPoint) : ActualSignedGeometry.Native

Native at, given by (slowInput x, (geometry L).coordinates k x.2).

Equations

• NavierStokes.InitialPhysicalData.nativeAt L k x = (NavierStokes.InitialPhysicalData.slowInput x, (NavierStokes.InitialPhysicalData.geometry L).coordinates k x.2)

theorem NavierStokes.InitialPhysicalData.copyAmplitude_nativeAt {B N0 : ℕ} (l : SignedLabel B N0) (k : Frequency) (x : LiftPoint) : copyAmplitude l k (BaseChartJets.cellBand l.2) (PhysicalClassBounds.cylindricalMap x, 0) = ActualPrimaryBounds.cutNativeVelocity l (nativeAt (bandLabel l) k x)

theorem NavierStokes.InitialPhysicalData.copyPressure_nativeAt {B N0 : ℕ} (l : SignedLabel B N0) (k : Frequency) (x : LiftPoint) : copyPressureCoefficient l k (BaseChartJets.cellBand l.2) (PhysicalClassBounds.cylindricalMap x, 0) = ActualPrimaryBounds.cutNativePressure l (nativeAt (bandLabel l) k x)

theorem NavierStokes.InitialPhysicalData.sourceFamily_nonzero {B N0 : ℕ} {E : Type} [Zero E] (f : SignedLabel B N0 × Frequency → ℕ → LocalSignedRequest.Point → E) (I : SourceIndex) (n : ℕ) (x : LocalSignedRequest.Point) (hne : sourceFamily f I n x ≠ 0) : ∃ (l : SignedLabel B N0), bandLabel l = I.1.1 ∧ ↑I.1.2 = 1 ∧ n = (↑I.1.1).1 ∧ f (l, I.2) n x ≠ 0

theorem NavierStokes.InitialPhysicalData.potential_amplitude_data {B N0 : ℕ} (i : Fin 3) (k : Frequency) (I : PhysicalWaveSum.WaveIndex 1) (x : LiftPoint) (hx : (potentialFamily B N0 i).amplitude k I x ≠ 0) : ∃ (l : SignedLabel B N0), bandLabel l = I.1 ∧ ↑I.2 = 1 ∧ 0 < x.1.1 ∧ ActualPrimaryBounds.cutNativeVelocity l (nativeAt I.1 k x) ≠ 0

theorem NavierStokes.InitialPhysicalData.pressure_amplitude_data {B N0 : ℕ} (k : Frequency) (I : PhysicalWaveSum.WaveIndex 1) (x : LiftPoint) (hx : (pressureFamily B N0).amplitude k I x ≠ 0) : ∃ (l : SignedLabel B N0), bandLabel l = I.1 ∧ ↑I.2 = 1 ∧ 0 < x.1.1 ∧ ActualPrimaryBounds.cutNativePressure l (nativeAt I.1 k x) ≠ 0

noncomputable def NavierStokes.InitialPhysicalData.baseCells (L : PhysicalWaveSum.BandLabel) : PeriodizedWaveBounds.Cells LiftPoint Frequency

Base cells, constructed using PeriodizedWaveBounds.nativeCells.

Equations

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

noncomputable def NavierStokes.InitialPhysicalData.slowCell {B N0 : ℕ} (L : PhysicalWaveSum.BandLabel) : Set LiftPoint

Slow cell, with branches according to hL : L ∈ active (B := B) (N0 := N0).

Equations

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

theorem NavierStokes.InitialPhysicalData.slowCell_closed {B N0 : ℕ} (L : PhysicalWaveSum.BandLabel) : IsClosed (slowCell L)

noncomputable def NavierStokes.InitialPhysicalData.cells {B N0 : ℕ} (L : PhysicalWaveSum.BandLabel) : PeriodizedWaveBounds.Cells LiftPoint Frequency

Closed slow support is retained alongside the individual native rectangle. Phase bounds are never requested outside this support.

Equations

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

theorem NavierStokes.InitialPhysicalData.cells_bandLabel {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) (k : Frequency) (x : LiftPoint) : x ∈ (cells (bandLabel l)).carrier n k ↔ (nativeAt (bandLabel l) k x).2 ∈ (CorrectionInitialization.ActualPrimary.clockWindow l.2).core ∧ (nativeAt (bandLabel l) k x).1 ∈ ActualGaussianCoverage.actualSlowCore CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation (CorrectionInitialization.ActualPrimary.choice B N0).prepared l.2

noncomputable def NavierStokes.InitialPhysicalData.potentialCells (B N0 : ℕ) (i : Fin 3) : PhysicalCopyBounds.SupportCells (potentialFamily B N0 i)

Potential cells, bundling cells, support, obtain, have and the required compatibility proofs.

Equations

• NavierStokes.InitialPhysicalData.potentialCells B N0 i = { cells := NavierStokes.InitialPhysicalData.cells, support := ⋯ }

noncomputable def NavierStokes.InitialPhysicalData.pressureCells (B N0 : ℕ) : PhysicalCopyBounds.SupportCells (pressureFamily B N0)

Pressure cells, bundling cells, support, obtain, have and the required compatibility proofs.

Equations

• NavierStokes.InitialPhysicalData.pressureCells B N0 = { cells := NavierStokes.InitialPhysicalData.cells, support := ⋯ }

noncomputable def NavierStokes.InitialPhysicalData.innerRadius : ℝ

Inner radius, given by PrimaryTargetBounds.leftRadius ActualPrimary.nominal / 4.

Equations

• NavierStokes.InitialPhysicalData.innerRadius = NavierStokes.PrimaryTargetBounds.leftRadius NavierStokes.CorrectionInitialization.ActualPrimary.nominal / 4

noncomputable def NavierStokes.InitialPhysicalData.outerRadius : ℝ

Outer radius, given by 2 * PrimaryTargetBounds.rightRadius ActualPrimary.nominal.

Equations

• NavierStokes.InitialPhysicalData.outerRadius = 2 * NavierStokes.PrimaryTargetBounds.rightRadius NavierStokes.CorrectionInitialization.ActualPrimary.nominal

theorem NavierStokes.InitialPhysicalData.innerRadius_pos : 0 < innerRadius

theorem NavierStokes.InitialPhysicalData.cut_pair_mask {B N0 : ℕ} (l : SignedLabel B N0) (x : ActualSignedGeometry.Native) (hne : ActualPrimaryBounds.cutNativeVelocity l x ≠ 0 ∨ ActualPrimaryBounds.cutNativePressure l x ≠ 0) : CorrectionInitialization.ActualPrimary.spatialMask l.2 x.1 ≠ 0

theorem NavierStokes.InitialPhysicalData.cut_pair_domain {B N0 : ℕ} (l : SignedLabel B N0) (L : PhysicalWaveSum.BandLabel) (k : Frequency) (x : LiftPoint) (ht : 0 < x.1.1) (hne : ActualPrimaryBounds.cutNativeVelocity l (nativeAt L k x) ≠ 0 ∨ ActualPrimaryBounds.cutNativePressure l (nativeAt L k x) ≠ 0) : PhysicalClassBounds.cylindricalMap x ∈ ActualPrimaryBounds.strip.domain

theorem NavierStokes.InitialPhysicalData.cut_pair_annulus {B N0 : ℕ} (l : SignedLabel B N0) (L : PhysicalWaveSum.BandLabel) (k : Frequency) (x : LiftPoint) (ht : 0 < x.1.1) (hne : ActualPrimaryBounds.cutNativeVelocity l (nativeAt L k x) ≠ 0 ∨ ActualPrimaryBounds.cutNativePressure l (nativeAt L k x) ≠ 0) : PhysicalGraphBounds.liftXY x ∈ PhysicalGraphBounds.annulus innerRadius outerRadius ∧ ‖PhysicalGraphBounds.liftZT x‖ ≤ 2

theorem NavierStokes.InitialPhysicalData.liftXY_common (h : ℝ) (n d : ℕ) (w : ProblemStatement.SpaceTime) : PhysicalGraphBounds.liftXY (PhysicalWaveSum.commonLift h n d w) = (PhysicalGraphBounds.scaledRadial n) w

theorem NavierStokes.InitialPhysicalData.liftZT_common (h : ℝ) (n d : ℕ) (w : ProblemStatement.SpaceTime) : PhysicalGraphBounds.liftZT (PhysicalWaveSum.commonLift h n d w) = PhysicalGraphBounds.liftZT (PhysicalGraphBounds.physicalLift h n w)

theorem NavierStokes.InitialPhysicalData.slowInput_common (h : ℝ) (n d : ℕ) (w : ProblemStatement.SpaceTime) : slowInput (PhysicalWaveSum.commonLift h n d w) = ActualSignedPhysicalData.nativeSlow (PhysicalMeanJetBounds.graph h n 0 w)

theorem NavierStokes.InitialPhysicalData.carrier_center {B N0 : ℕ} (L : PhysicalWaveSum.BandLabel) (k : Frequency) : (carrier L k).center = ActualSignedPhysicalData.center (↑L) k

theorem NavierStokes.InitialPhysicalData.carrier_integer {B N0 : ℕ} (L : PhysicalWaveSum.BandLabel) (k : Frequency) : ∃ (m : ℤ), ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h (↑L).1) * (carrier L k).angular = ↑m

theorem NavierStokes.InitialPhysicalData.gap_bound (L : PhysicalWaveSum.BandLabel) : gap L ≤ CorrectionInitialization.CommonWindow.gap CorrectionInitialization.ActualPrimary.h

theorem NavierStokes.InitialPhysicalData.gap_native (L : PhysicalWaveSum.BandLabel) : gap L ≤ ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (↑L).1

theorem NavierStokes.InitialPhysicalData.physicalPosition_graph (n d : ℕ) (w : ProblemStatement.SpaceTime) : CorrectionInitialization.ActualPrimary.physicalPosition n (PhysicalMeanJetBounds.graph CorrectionInitialization.ActualPrimary.h n d w) = PhysicalWaveSum.physicalPosition w

theorem NavierStokes.InitialPhysicalData.physicalScale_graph (n d : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) : CorrectionInitialization.ActualPrimary.physicalScale n (PhysicalMeanJetBounds.graph CorrectionInitialization.ActualPrimary.h n d w) = PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w

theorem NavierStokes.InitialPhysicalData.spatialMask_physical {B N0 : ℕ} (l : SignedLabel B N0) (d : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) : CorrectionInitialization.ActualPrimary.spatialMask l.2 (slowInput (PhysicalWaveSum.commonLift CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2) d w)) = PhysicalWaveSum.physicalMask (CoordinateAlgebra.D CorrectionInitialization.ActualPrimary.h) (↑(bandLabel l)) (PhysicalWaveSum.physicalParams CorrectionInitialization.ActualPrimary.h w)

theorem NavierStokes.InitialPhysicalData.width_physical {B N0 : ℕ} (L : PhysicalWaveSum.BandLabel) (k : Frequency) (w : ProblemStatement.SpaceTime) (hc : (geometry L).coordinates k (PhysicalWaveSum.commonLift CorrectionInitialization.ActualPrimary.h (↑L).1 (gap L) w).2 ∈ (ActualSignedGeometry.clockWindow CorrectionInitialization.ActualPrimary.slots (↑L).1).core) : |PhysicalGraphBounds.etaCoordinate (PhysicalGraphBounds.nativeGraph CorrectionInitialization.ActualPrimary.h (↑L).1 w - (carrier L k).center)| ≤ CorrectionInitialization.ActualPrimary.slots.radius

theorem NavierStokes.InitialPhysicalData.potential_support (B N0 : ℕ) (i : Fin 3) : LocalPhysicalCopyBounds.SupportData (potentialFamily B N0 i) innerRadius outerRadius CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius 2 (CorrectionInitialization.CommonWindow.gap CorrectionInitialization.ActualPrimary.h)

theorem NavierStokes.InitialPhysicalData.pressure_support (B N0 : ℕ) : LocalPhysicalCopyBounds.SupportData (pressureFamily B N0) innerRadius outerRadius CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius 2 (CorrectionInitialization.CommonWindow.gap CorrectionInitialization.ActualPrimary.h)

noncomputable def NavierStokes.InitialPhysicalData.potential (B N0 : ℕ) : ProblemStatement.VelocityField

The actual initial primary potential. The physical construction is zero on the unused future side of the preterminal domain.

Equations

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

noncomputable def NavierStokes.InitialPhysicalData.pressure (B N0 : ℕ) : ProblemStatement.PressureField

Pressure, defined pointwise by ((pressureFamily B N0).sum innerRadius ActualPrimary.h ActualPrimary.slots.radius w).re.

Equations

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

noncomputable def NavierStokes.InitialPhysicalData.copyPotential (B N0 : ℕ) : MixedAxisPreservation.CopyPotential CorrectionInitialization.ActualPrimary.h

Copy potential, bundling Copy, harmonics, family, inner and the required compatibility proofs.

Equations

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

theorem NavierStokes.InitialPhysicalData.copyPotential_field (B N0 : ℕ) : (copyPotential B N0).field = potential B N0

noncomputable def NavierStokes.InitialPhysicalData.profileRegion {B N0 : ℕ} (L : PhysicalWaveSum.BandLabel) : Set PhaseCalculus.Slow

Profile region, with branches according to hL : L ∈ active (B := B) (N0 := N0).

Equations

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

theorem NavierStokes.InitialPhysicalData.profileRegion_open {B N0 : ℕ} (L : PhysicalWaveSum.BandLabel) : IsOpen (profileRegion L)

theorem NavierStokes.InitialPhysicalData.carrierProfiles {B N0 : ℕ} : PhaseJetBounds.PolynomialJets (PhysicalCopyBounds.copyBandDomain (fun (x : Frequency) (L : PhysicalWaveSum.BandLabel) => profileRegion L) ⋯) fun (i : Frequency × PhysicalWaveSum.BandLabel) (p : PhaseCalculus.Slow) => ((carrier i.2 i.1).F p, (carrier i.2 i.1).G p)

theorem NavierStokes.InitialPhysicalData.profileRegion_contains {B N0 : ℕ} (L : PhysicalWaveSum.BandLabel) (k : Frequency) (w : ProblemStatement.SpaceTime) (hw : w ∈ PhysicalWaveSum.preterminal) (hc : PhysicalWaveSum.commonLift CorrectionInitialization.ActualPrimary.h (↑L).1 (gap L) w ∈ (cells L).carrier (↑L).1 k) (j : PolarCharts.Index) (hj : (PhysicalGraphBounds.scaledRadial (↑L).1) w ∈ PolarCharts.chartDomain innerRadius j) : LocalPhysicalCopyBounds.slotSlow ((carrier L k).withChart j) innerRadius CorrectionInitialization.ActualPrimary.h (↑L).1 CorrectionInitialization.ActualPrimary.slots.radius w ∈ profileRegion L

noncomputable def NavierStokes.InitialPhysicalData.potentialCarrier (B N0 : ℕ) (i : Fin 3) : PhysicalCopyBounds.CarrierBounds (potentialFamily B N0 i) (potentialCells B N0 i) innerRadius outerRadius CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius

Potential carrier, bundling region, open_region, jets, contains.

Equations

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

noncomputable def NavierStokes.InitialPhysicalData.pressureCarrier (B N0 : ℕ) : PhysicalCopyBounds.CarrierBounds (pressureFamily B N0) (pressureCells B N0) innerRadius outerRadius CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius

Pressure carrier, bundling region, open_region, jets, contains.

Equations

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

noncomputable def NavierStokes.InitialPhysicalData.sourceStrip : WeightedClasses.StripData LiftPoint

Source strip, given by CartesianCopySource.pullStrip strip innerRadius outerRadius innerRadius_pos.

Equations

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

noncomputable def NavierStokes.InitialPhysicalData.potentialSource (B N0 : ℕ) (I : Fin 3 × SourceIndex) (n : ℕ) (x : LiftPoint) : ℂ

Potential source, given by CartesianCopySource.rotatedSource (nativePotentialSource B N0) I.2 n x I.1.

Equations

• NavierStokes.InitialPhysicalData.potentialSource B N0 I n x = NavierStokes.CartesianCopySource.rotatedSource (NavierStokes.InitialPhysicalData.nativePotentialSource B N0) I.2 n x I.1

noncomputable def NavierStokes.InitialPhysicalData.pressureSource (B N0 : ℕ) (I : SourceIndex) (n : ℕ) (x : LiftPoint) : ℂ

Pressure source, given by nativePressureSource B N0 I n (PhysicalClassBounds.cylindricalMap x).

Equations

• NavierStokes.InitialPhysicalData.pressureSource B N0 I n x = NavierStokes.InitialPhysicalData.nativePressureSource B N0 I n (NavierStokes.PhysicalClassBounds.cylindricalMap x)

theorem NavierStokes.InitialPhysicalData.potentialSource_bounds (B N0 : ℕ) : LocalPhysicalCopyBounds.LocalSourceBounds sourceStrip CorrectionInitialization.ActualPrimary.h 1 (fun (x : Fin 3 × SourceIndex) (x_1 : ℕ) (x_2 : LiftPoint) => √(sourceStrip.zeta x_2)) (potentialSource B N0)

theorem NavierStokes.InitialPhysicalData.pressureSource_bounds (B N0 : ℕ) : LocalPhysicalCopyBounds.LocalSourceBounds sourceStrip CorrectionInitialization.ActualPrimary.h 1 (fun (x : SourceIndex) (x_1 : ℕ) (x_2 : LiftPoint) => √(sourceStrip.zeta x_2)) (pressureSource B N0)

theorem NavierStokes.InitialPhysicalData.cut_pair_source_domain {B N0 : ℕ} (l : SignedLabel B N0) (L : PhysicalWaveSum.BandLabel) (k : Frequency) (x : LiftPoint) (ht : 0 < x.1.1) (hne : ActualPrimaryBounds.cutNativeVelocity l (nativeAt L k x) ≠ 0 ∨ ActualPrimaryBounds.cutNativePressure l (nativeAt L k x) ≠ 0) : x ∈ sourceStrip.domain

theorem NavierStokes.InitialPhysicalData.potential_source_domain (B N0 : ℕ) (i : Fin 3) (k : Frequency) (I : PhysicalWaveSum.WaveIndex 1) (x : LiftPoint) (hx : (potentialFamily B N0 i).amplitude k I x ≠ 0) : x ∈ sourceStrip.domain

theorem NavierStokes.InitialPhysicalData.pressure_source_domain (B N0 : ℕ) (k : Frequency) (I : PhysicalWaveSum.WaveIndex 1) (x : LiftPoint) (hx : (pressureFamily B N0).amplitude k I x ≠ 0) : x ∈ sourceStrip.domain

theorem NavierStokes.InitialPhysicalData.sourceStrip_time {x : LiftPoint} (hx : x ∈ sourceStrip.domain) : 0 < x.1.1

theorem NavierStokes.InitialPhysicalData.potential_amplitude_source (B N0 : ℕ) (i : Fin 3) (k : Frequency) (I : PhysicalWaveSum.WaveIndex 1) : Set.EqOn ((potentialFamily B N0 i).amplitude k I) (fun (x : PhysicalWaveSum.LiftPoint) => ChartScales.Q (↑I.1).1 ^ (-CorrectionInitialization.ActualPrimary.h) • potentialSource B N0 (i, I, k) (↑I.1).1 x) sourceStrip.domain

theorem NavierStokes.InitialPhysicalData.pressure_amplitude_source (B N0 : ℕ) (k : Frequency) (I : PhysicalWaveSum.WaveIndex 1) : Set.EqOn ((pressureFamily B N0).amplitude k I) (fun (x : PhysicalWaveSum.LiftPoint) => ChartScales.Q (↑I.1).1 ^ (-(2 * CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h)) • pressureSource B N0 (I, k) (↑I.1).1 x) sourceStrip.domain

noncomputable def NavierStokes.InitialPhysicalData.identitySourceChartOn {N : ℕ} {K I : Type} (f : PhysicalCopyBounds.CopyFamily N K) (hc : PhysicalCopyBounds.SupportCells f) {a b h r Z σ : ℝ} {gap : ℕ} (ha : 0 < a) (hs : LocalPhysicalCopyBounds.SupportData f a b h r Z gap) (s : WeightedClasses.StripData LiftPoint) (source : I → ℕ → LiftPoint → ℂ) (idx : K → PhysicalWaveSum.WaveIndex N → I) (he : ∀ (k : K) (J : PhysicalWaveSum.WaveIndex N), Set.EqOn (f.amplitude k J) (fun (x : PhysicalWaveSum.LiftPoint) => ChartScales.Q (↑J.1).1 ^ σ • source (idx k J) (↑J.1).1 x) s.domain) (hd : ∀ (k : K) (J : PhysicalWaveSum.WaveIndex N) (x : PhysicalWaveSum.LiftPoint), f.amplitude k J x ≠ 0 → x ∈ s.domain) : LocalPhysicalCopyBounds.CommonChart f hc a b h r σ source

The identity chart only needs its formula on the genuine source domain. Its closure condition follows from actual amplitude support.

Equations

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

noncomputable def NavierStokes.InitialPhysicalData.potentialChart (B N0 : ℕ) (i : Fin 3) : LocalPhysicalCopyBounds.CommonChart (potentialFamily B N0 i) (potentialCells B N0 i) innerRadius outerRadius CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius (-CorrectionInitialization.ActualPrimary.h) (potentialSource B N0)

Potential chart, constructed using identitySourceChartOn.

Equations

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

noncomputable def NavierStokes.InitialPhysicalData.pressureChart (B N0 : ℕ) : LocalPhysicalCopyBounds.CommonChart (pressureFamily B N0) (pressureCells B N0) innerRadius outerRadius CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius (-(2 * CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h)) (pressureSource B N0)

Pressure chart, constructed using identitySourceChartOn.

Equations

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

theorem NavierStokes.InitialPhysicalData.carrier_frequencies {B N0 : ℕ} (L : PhysicalWaveSum.BandLabel) (k : Frequency) : |(carrier L k).angular| ≤ ActualPhaseJetBounds.phaseSize B N0 ∧ |(carrier L k).axial| ≤ ActualPhaseJetBounds.phaseSize B N0 ∧ |(carrier L k).radial| ≤ ActualPhaseJetBounds.phaseSize B N0

noncomputable def NavierStokes.InitialPhysicalData.nativePast : Set LocalSignedRequest.Point

Native past, given by {x | 0 < x.1 ∧ 0 < x.2.1.1}.

Equations

• NavierStokes.InitialPhysicalData.nativePast = {x : NavierStokes.LocalSignedRequest.Point | 0 < x.1 ∧ 0 < x.2.1.1}

theorem NavierStokes.InitialPhysicalData.sourceFamily_smooth {B N0 : ℕ} {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : SignedLabel B N0 × Frequency → ℕ → LocalSignedRequest.Point → E) (hf : ∀ (l : SignedLabel B N0 × Frequency) (n : ℕ), ContDiffOn ℝ (↑⊤) (f l n) nativePast) (I : SourceIndex) (n : ℕ) : ContDiffOn ℝ (↑⊤) (sourceFamily f I n) nativePast

theorem NavierStokes.InitialPhysicalData.nativePotentialSource_smooth (B N0 : ℕ) (I : SourceIndex) (n : ℕ) : ContDiffOn ℝ (↑⊤) (nativePotentialSource B N0 I n) nativePast

theorem NavierStokes.InitialPhysicalData.nativePressureSource_smooth (B N0 : ℕ) (I : SourceIndex) (n : ℕ) : ContDiffOn ℝ (↑⊤) (nativePressureSource B N0 I n) nativePast

noncomputable def NavierStokes.InitialPhysicalData.paddedPast : Set LiftPoint

Padded past, given by PhysicalClassBounds.cylindricalDomain innerRadius outerRadius ∩ {x | 0 < x.1.1}.

Equations

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

theorem NavierStokes.InitialPhysicalData.paddedPast_open : IsOpen paddedPast

theorem NavierStokes.InitialPhysicalData.paddedPast_map : Set.MapsTo PhysicalClassBounds.cylindricalMap paddedPast nativePast

theorem NavierStokes.InitialPhysicalData.potential_amplitude_smooth (B N0 : ℕ) (i : Fin 3) (k : Frequency) (I : PhysicalWaveSum.WaveIndex 1) : ContDiffOn ℝ (↑⊤) ((potentialFamily B N0 i).amplitude k I) paddedPast

theorem NavierStokes.InitialPhysicalData.pressure_amplitude_smooth (B N0 : ℕ) (k : Frequency) (I : PhysicalWaveSum.WaveIndex 1) : ContDiffOn ℝ (↑⊤) ((pressureFamily B N0).amplitude k I) paddedPast

theorem NavierStokes.InitialPhysicalData.commonLift_mem_paddedPast (n d : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hann : (PhysicalGraphBounds.scaledRadial n) w ∈ PhysicalGraphBounds.annulus innerRadius outerRadius) : PhysicalWaveSum.commonLift CorrectionInitialization.ActualPrimary.h n d w ∈ paddedPast

theorem NavierStokes.InitialPhysicalData.potentialSmooth (B N0 : ℕ) (i : Fin 3) : LocalPhysicalCopyBounds.SmoothData (potentialFamily B N0 i) innerRadius CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius

theorem NavierStokes.InitialPhysicalData.pressureSmooth (B N0 : ℕ) : LocalPhysicalCopyBounds.SmoothData (pressureFamily B N0) innerRadius CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius

noncomputable def NavierStokes.InitialPhysicalData.potentialWaveData (B N0 : ℕ) : PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h LiftPoint (Fin 3 × SourceIndex) Frequency (Fin 3)

Actual initial potential copies with their proved support, local regularity and uniform native jets.

Equations

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

noncomputable def NavierStokes.InitialPhysicalData.pressureWaveData (B N0 : ℕ) : PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h LiftPoint SourceIndex Frequency Unit

The pressure has the same copied source construction and its actual physical pressure factor.

Equations

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

theorem NavierStokes.InitialPhysicalData.potentialWaveData_vector (B N0 : ℕ) : (potentialWaveData B N0).vector = potential B N0

theorem NavierStokes.InitialPhysicalData.pressureWaveData_pressure (B N0 : ℕ) : (pressureWaveData B N0).pressure = pressure B N0

theorem NavierStokes.InitialPhysicalData.potential_smooth (B N0 : ℕ) : ContDiffOn ℝ (↑⊤) (potential B N0) PhysicalWaveSum.preterminal

theorem NavierStokes.InitialPhysicalData.pressure_smooth (B N0 : ℕ) : ContDiffOn ℝ (↑⊤) (pressure B N0) PhysicalWaveSum.preterminal

noncomputable def NavierStokes.InitialPhysicalData.positiveIndex {B N0 : ℕ} (l : SignedLabel B N0) : PhysicalWaveSum.WaveIndex 1

Positive index, given by ActualSignedPhysicalData.positiveIndex (bandLabel l).

Equations

• NavierStokes.InitialPhysicalData.positiveIndex l = NavierStokes.ActualSignedPhysicalData.positiveIndex (NavierStokes.InitialPhysicalData.bandLabel l)

theorem NavierStokes.InitialPhysicalData.positiveIndex_band {B N0 : ℕ} (l : SignedLabel B N0) : (↑(positiveIndex l).1).1 = BaseChartJets.cellBand l.2

theorem NavierStokes.InitialPhysicalData.copyAmplitude_summable {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) (x : Point) : Summable fun (k : Frequency) => copyAmplitude l k n x

theorem NavierStokes.InitialPhysicalData.cut_amplitude_self {B N0 : ℕ} (l : SignedLabel B N0) (x : Point) : (ActualPrimaryBounds.cutCoefficients l).amplitude (BaseChartJets.cellBand l.2) x = ∑' (k : Frequency), copyAmplitude l k (BaseChartJets.cellBand l.2) x

theorem NavierStokes.InitialPhysicalData.cut_pressure_self {B N0 : ℕ} (l : SignedLabel B N0) (x : Point) : (ActualPrimaryBounds.cutCoefficients l).pressure (BaseChartJets.cellBand l.2) x = ∑' (k : Frequency), copyPressureCoefficient l k (BaseChartJets.cellBand l.2) x

theorem NavierStokes.InitialPhysicalData.potentialCoefficient_self {B N0 : ℕ} (l : SignedLabel B N0) (x : Point) : potentialCoefficient l (BaseChartJets.cellBand l.2) x = ∑' (k : Frequency), copyPotentialCoefficient l k (BaseChartJets.cellBand l.2) x

theorem NavierStokes.InitialPhysicalData.nativePotentialSource_active {B N0 : ℕ} (l : SignedLabel B N0) (k : Frequency) : nativePotentialSource B N0 (positiveIndex l, k) (BaseChartJets.cellBand l.2) = fun (x : LocalSignedRequest.Point) => copyPotentialCoefficient l k (BaseChartJets.cellBand l.2) (x, 0)

theorem NavierStokes.InitialPhysicalData.nativePressureSource_active {B N0 : ℕ} (l : SignedLabel B N0) (k : Frequency) : nativePressureSource B N0 (positiveIndex l, k) (BaseChartJets.cellBand l.2) = fun (x : LocalSignedRequest.Point) => copyPressureCoefficient l k (BaseChartJets.cellBand l.2) (x, 0)

theorem NavierStokes.InitialPhysicalData.dynamics_copyPoint_self {B N0 : ℕ} (l : SignedLabel B N0) (k : Frequency) (x : Point) : ActualPrimaryDynamics.copyPoint l.1 l.2 (BaseChartJets.cellBand l.2) k x = ((ActualPrimaryBounds.nativeOfFull x).1, (geometry (bandLabel l)).coordinates k (ActualPrimaryBounds.nativeOfFull x).2)

noncomputable def NavierStokes.InitialPhysicalData.polarPoint (a : ℝ) (j : PolarCharts.Index) (x : LiftPoint) : Point

Polar point, given by PhysicalResidualTZ.swapCylinder (ActualSignedPhysicalData.cylinderAt a j x).

Equations

• NavierStokes.InitialPhysicalData.polarPoint a j x = NavierStokes.PhysicalResidualTZ.swapCylinder (NavierStokes.ActualSignedPhysicalData.cylinderAt a j x)

theorem NavierStokes.InitialPhysicalData.polarPoint_fst {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) {x : LiftPoint} (hx : PhysicalGraphBounds.liftXY x ∈ PolarCharts.chartDomain a j) : (polarPoint a j x).1 = PhysicalClassBounds.cylindricalMap x

theorem NavierStokes.InitialPhysicalData.slotPoint_polar {B N0 : ℕ} (l : SignedLabel B N0) (k : Frequency) (a : ℝ) (j : PolarCharts.Index) (x : LiftPoint) : ActualPrimaryDynamics.slotPoint l.1 l.2 (BaseChartJets.cellBand l.2) k (polarPoint a j x) = ActualSignedGeometry.slotCoordinates (geometry (bandLabel l)) k (ActualSignedPhysicalData.cylinderAt a j x)

theorem NavierStokes.InitialPhysicalData.phase_polar {B N0 : ℕ} (l : SignedLabel B N0) (k : Frequency) (a : ℝ) (j : PolarCharts.Index) (x : LiftPoint) (hc : (geometry (bandLabel l)).coordinates k x.2 ∈ (CorrectionInitialization.ActualPrimary.clockWindow l.2).core) : (ActualPrimaryBounds.cutCoefficients l).phase (BaseChartJets.cellBand l.2) (polarPoint a j x) = ((selectedCarrier l k).withChart j).phase a CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2) CorrectionInitialization.ActualPrimary.slots.radius ((PhysicalWaveSum.upLift (gap (bandLabel l))) x)

theorem NavierStokes.InitialPhysicalData.copyPotential_fast {B N0 : ℕ} (l : SignedLabel B N0) (k : Frequency) {x : Point} (hx : copyPotentialCoefficient l k (BaseChartJets.cellBand l.2) x ≠ 0) : (geometry (bandLabel l)).coordinates k x.1.2.2 ∈ (CorrectionInitialization.ActualPrimary.clockWindow l.2).core

theorem NavierStokes.InitialPhysicalData.copyPressure_fast {B N0 : ℕ} (l : SignedLabel B N0) (k : Frequency) {x : Point} (hx : copyPressureCoefficient l k (BaseChartJets.cellBand l.2) x ≠ 0) : (geometry (bandLabel l)).coordinates k x.1.2.2 ∈ (CorrectionInitialization.ActualPrimary.clockWindow l.2).core

theorem NavierStokes.InitialPhysicalData.up_commonLift (h : ℝ) (n d : ℕ) (w : ProblemStatement.SpaceTime) : (PhysicalWaveSum.upLift d) (PhysicalWaveSum.commonLift h n d w) = PhysicalGraphBounds.physicalLift h n w

theorem NavierStokes.InitialPhysicalData.graph_aux_common (h : ℝ) (n d : ℕ) (w : ProblemStatement.SpaceTime) : (PhysicalMeanJetBounds.graph h n d w).2.2 = (PhysicalWaveSum.commonLift h n d w).2

theorem NavierStokes.InitialPhysicalData.potential_amplitude_active {B N0 : ℕ} (l : SignedLabel B N0) (k : Frequency) (i : Fin 3) (x : LiftPoint) (ht : 0 < x.1.1) : (potentialFamily B N0 i).amplitude k (positiveIndex l) x = ChartScales.Q (BaseChartJets.cellBand l.2) ^ (-CorrectionInitialization.ActualPrimary.h) • (CartesianCopySource.rotationMap (PhysicalGraphBounds.liftXY x)) (copyPotentialCoefficient l k (BaseChartJets.cellBand l.2) (PhysicalClassBounds.cylindricalMap x, 0)) i

theorem NavierStokes.InitialPhysicalData.pressure_amplitude_active {B N0 : ℕ} (l : SignedLabel B N0) (k : Frequency) (x : LiftPoint) (ht : 0 < x.1.1) : (pressureFamily B N0).amplitude k (positiveIndex l) x = ChartScales.Q (BaseChartJets.cellBand l.2) ^ (-(2 * CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h)) • copyPressureCoefficient l k (BaseChartJets.cellBand l.2) (PhysicalClassBounds.cylindricalMap x, 0)

theorem NavierStokes.InitialPhysicalData.potential_term {B N0 : ℕ} (l : SignedLabel B N0) (k : Frequency) (i : Fin 3) (w : ProblemStatement.SpaceTime) : (potentialFamily B N0 i).term innerRadius CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius (positiveIndex l) k w = PhysicalWaveSum.commonWave innerRadius CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2) (gap (bandLabel l)) CorrectionInitialization.ActualPrimary.slots.radius ((selectedCarrier l k).withChart (PhysicalWaveSum.chooseChart innerRadius ((PhysicalGraphBounds.scaledRadial (BaseChartJets.cellBand l.2)) w))) ((potentialFamily B N0 i).amplitude k (positiveIndex l)) 1 w

theorem NavierStokes.InitialPhysicalData.pressure_term {B N0 : ℕ} (l : SignedLabel B N0) (k : Frequency) (w : ProblemStatement.SpaceTime) : (pressureFamily B N0).term innerRadius CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius (positiveIndex l) k w = PhysicalWaveSum.commonWave innerRadius CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2) (gap (bandLabel l)) CorrectionInitialization.ActualPrimary.slots.radius ((selectedCarrier l k).withChart (PhysicalWaveSum.chooseChart innerRadius ((PhysicalGraphBounds.scaledRadial (BaseChartJets.cellBand l.2)) w))) ((pressureFamily B N0).amplitude k (positiveIndex l)) 1 w

theorem NavierStokes.InitialPhysicalData.potential_commonWave {B N0 : ℕ} (l : SignedLabel B N0) (k : Frequency) (i : Fin 3) (j : PolarCharts.Index) (w : ProblemStatement.SpaceTime) (hw : w ∈ PhysicalWaveSum.preterminal) : PhysicalWaveSum.commonWave innerRadius CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2) (gap (bandLabel l)) CorrectionInitialization.ActualPrimary.slots.radius ((selectedCarrier l k).withChart j) ((potentialFamily B N0 i).amplitude k (positiveIndex l)) 1 w = ChartScales.Q (BaseChartJets.cellBand l.2) ^ (-CorrectionInitialization.ActualPrimary.h) • (CartesianCopySource.rotationMap (PhysicalGraphBounds.liftXY (PhysicalWaveSum.commonLift CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2) (gap (bandLabel l)) w))) (copyPotentialCoefficient l k (BaseChartJets.cellBand l.2) (PhysicalMeanJetBounds.graph CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2) (gap (bandLabel l)) w, 0)) i * HarmonicCalculus.carrier ((ActualPrimaryBounds.cutCoefficients l).frequency (BaseChartJets.cellBand l.2)) ((ActualPrimaryBounds.cutCoefficients l).phase (BaseChartJets.cellBand l.2)) (polarPoint innerRadius j (PhysicalWaveSum.commonLift CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2) (gap (bandLabel l)) w))

theorem NavierStokes.InitialPhysicalData.pressure_commonWave {B N0 : ℕ} (l : SignedLabel B N0) (k : Frequency) (j : PolarCharts.Index) (w : ProblemStatement.SpaceTime) (hw : w ∈ PhysicalWaveSum.preterminal) : PhysicalWaveSum.commonWave innerRadius CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2) (gap (bandLabel l)) CorrectionInitialization.ActualPrimary.slots.radius ((selectedCarrier l k).withChart j) ((pressureFamily B N0).amplitude k (positiveIndex l)) 1 w = ChartScales.Q (BaseChartJets.cellBand l.2) ^ (-(2 * CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h)) • copyPressureCoefficient l k (BaseChartJets.cellBand l.2) (PhysicalMeanJetBounds.graph CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2) (gap (bandLabel l)) w, 0) * HarmonicCalculus.carrier ((ActualPrimaryBounds.cutCoefficients l).frequency (BaseChartJets.cellBand l.2)) ((ActualPrimaryBounds.cutCoefficients l).phase (BaseChartJets.cellBand l.2)) (polarPoint innerRadius j (PhysicalWaveSum.commonLift CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2) (gap (bandLabel l)) w))

theorem NavierStokes.InitialPhysicalData.potential_rotated_sum {B N0 : ℕ} (l : SignedLabel B N0) (x : Point) (Y : PhysicalGraphBounds.Plane) (i : Fin 3) : ∑' (k : Frequency), (CartesianCopySource.rotationMap Y) (copyPotentialCoefficient l k (BaseChartJets.cellBand l.2) x) i = (CartesianCopySource.rotationMap Y) (potentialCoefficient l (BaseChartJets.cellBand l.2) x) i

theorem NavierStokes.InitialPhysicalData.potential_periodized {B N0 : ℕ} (l : SignedLabel B N0) (i : Fin 3) (w : ProblemStatement.SpaceTime) (hw : w ∈ PhysicalWaveSum.preterminal) : (potentialFamily B N0 i).periodized innerRadius CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius (positiveIndex l) w = ChartScales.Q (BaseChartJets.cellBand l.2) ^ (-CorrectionInitialization.ActualPrimary.h) • (CartesianCopySource.rotationMap ((PhysicalGraphBounds.scaledRadial (BaseChartJets.cellBand l.2)) w)) (potentialCoefficient l (BaseChartJets.cellBand l.2) (PhysicalMeanJetBounds.graph CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2) (gap (bandLabel l)) w, 0)) i * HarmonicCalculus.carrier ((ActualPrimaryBounds.cutCoefficients l).frequency (BaseChartJets.cellBand l.2)) ((ActualPrimaryBounds.cutCoefficients l).phase (BaseChartJets.cellBand l.2)) (polarPoint innerRadius (PhysicalWaveSum.chooseChart innerRadius ((PhysicalGraphBounds.scaledRadial (BaseChartJets.cellBand l.2)) w)) (PhysicalWaveSum.commonLift CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2) (gap (bandLabel l)) w))

theorem NavierStokes.InitialPhysicalData.pressure_periodized {B N0 : ℕ} (l : SignedLabel B N0) (w : ProblemStatement.SpaceTime) (hw : w ∈ PhysicalWaveSum.preterminal) : (pressureFamily B N0).periodized innerRadius CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius (positiveIndex l) w = ChartScales.Q (BaseChartJets.cellBand l.2) ^ (-(2 * CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h)) • (ActualPrimaryBounds.cutCoefficients l).pressure (BaseChartJets.cellBand l.2) (PhysicalMeanJetBounds.graph CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2) (gap (bandLabel l)) w, 0) * HarmonicCalculus.carrier ((ActualPrimaryBounds.cutCoefficients l).frequency (BaseChartJets.cellBand l.2)) ((ActualPrimaryBounds.cutCoefficients l).phase (BaseChartJets.cellBand l.2)) (polarPoint innerRadius (PhysicalWaveSum.chooseChart innerRadius ((PhysicalGraphBounds.scaledRadial (BaseChartJets.cellBand l.2)) w)) (PhysicalWaveSum.commonLift CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2) (gap (bandLabel l)) w))

noncomputable def NavierStokes.InitialPhysicalData.physicalX (w : ProblemStatement.SpaceTime) : ℝ

Physical X, given by PhysicalWaveSum.physicalPosition w 0 ^ 2 / (2 * PhysicalWaveSum.physicalQ ActualPrimary.h w).

Equations

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

theorem NavierStokes.InitialPhysicalData.cut_pair_physicalX {B N0 : ℕ} (l : SignedLabel B N0) (L : PhysicalWaveSum.BandLabel) (k : Frequency) (w : ProblemStatement.SpaceTime) (hw : w ∈ PhysicalWaveSum.preterminal) (hne : ActualPrimaryBounds.cutNativeVelocity l (nativeAt L k (PhysicalWaveSum.commonLift CorrectionInitialization.ActualPrimary.h (↑L).1 (gap L) w)) ≠ 0 ∨ ActualPrimaryBounds.cutNativePressure l (nativeAt L k (PhysicalWaveSum.commonLift CorrectionInitialization.ActualPrimary.h (↑L).1 (gap L) w)) ≠ 0) : physicalX w ∈ Set.Ioo (NominalConeAssembly.activeLeft CorrectionInitialization.ActualPrimary.nominal) (NominalConeAssembly.activeRight CorrectionInitialization.ActualPrimary.nominal)

theorem NavierStokes.InitialPhysicalData.potential_amplitude_zero_exterior (B N0 : ℕ) (i : Fin 3) (k : Frequency) (I : PhysicalWaveSum.WaveIndex 1) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hX : physicalX w ∉ Set.Icc (NominalConeAssembly.activeLeft CorrectionInitialization.ActualPrimary.nominal) (NominalConeAssembly.activeRight CorrectionInitialization.ActualPrimary.nominal)) : (potentialFamily B N0 i).amplitude k I (PhysicalWaveSum.commonLift CorrectionInitialization.ActualPrimary.h (↑I.1).1 (gap I.1) w) = 0

theorem NavierStokes.InitialPhysicalData.pressure_amplitude_zero_exterior (B N0 : ℕ) (k : Frequency) (I : PhysicalWaveSum.WaveIndex 1) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hX : physicalX w ∉ Set.Icc (NominalConeAssembly.activeLeft CorrectionInitialization.ActualPrimary.nominal) (NominalConeAssembly.activeRight CorrectionInitialization.ActualPrimary.nominal)) : (pressureFamily B N0).amplitude k I (PhysicalWaveSum.commonLift CorrectionInitialization.ActualPrimary.h (↑I.1).1 (gap I.1) w) = 0

theorem NavierStokes.InitialPhysicalData.copy_sum_zero_of_amplitudes_zero {N : ℕ} {K : Type} (f : PhysicalCopyBounds.CopyFamily N K) (a h r : ℝ) (w : ProblemStatement.SpaceTime) (hz : ∀ (I : PhysicalWaveSum.WaveIndex N) (k : K), f.amplitude k I (PhysicalWaveSum.commonLift h (↑I.1).1 (f.gap I.1) w) = 0) : f.sum a h r w = 0

theorem NavierStokes.InitialPhysicalData.potential_zero_exterior (B N0 : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hX : physicalX w ∉ Set.Icc (NominalConeAssembly.activeLeft CorrectionInitialization.ActualPrimary.nominal) (NominalConeAssembly.activeRight CorrectionInitialization.ActualPrimary.nominal)) : potential B N0 w = 0

theorem NavierStokes.InitialPhysicalData.pressure_zero_exterior (B N0 : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hX : physicalX w ∉ Set.Icc (NominalConeAssembly.activeLeft CorrectionInitialization.ActualPrimary.nominal) (NominalConeAssembly.activeRight CorrectionInitialization.ActualPrimary.nominal)) : pressure B N0 w = 0

theorem NavierStokes.InitialPhysicalData.normal_withCutoff {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : LinearWaveBounds.WaveCoefficients D) (χ : ℕ → D → ℝ) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) (n : ℕ) : (a.withCutoff χ).normal s d n = a.normal s d n

theorem NavierStokes.InitialPhysicalData.cut_normal_lifted {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) (x : Point) : (ActualPrimaryBounds.cutCoefficients l).normal ActualPrimaryBounds.fullStrip (ActualPrimaryBounds.directions B) n (PhysicalResidualTZ.swapCylinder x) = HarmonicCalculus.phaseNormal PhysicalResidualBridge.ScaledGraph.radius (PhysicalResidualBridge.commonGraph (ChartScales.Q n) CorrectionInitialization.ActualPrimary.h (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n)).radial PhysicalResidualBridge.ScaledGraph.angular (PhysicalResidualBridge.commonGraph (ChartScales.Q n) CorrectionInitialization.ActualPrimary.h (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n)).axial (ActualPrimaryCoherence.liftedPhase l.1 l.2 n) x

theorem NavierStokes.InitialPhysicalData.graph_cartesian_forward (h : ℝ) (n d : ℕ) (hd : d ≤ ChartScales.nativeIndex h n) (z : ProblemStatement.SpaceTime) (hr : 0 < z.2.ofLp 0) : PhysicalMeanJetBounds.graph h n d (z.1, CylindricalResidual.chart z.2) = (PhysicalResidualTZ.swapCylinder ((PhysicalResidualBridge.commonGraph (ChartScales.Q n) h (ChartScales.nativeIndex h n - d)).map z)).1

theorem NavierStokes.InitialPhysicalData.polarPoint_common_forward (h : ℝ) (n d : ℕ) (hd : d ≤ ChartScales.nativeIndex h n) {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) (z : ProblemStatement.SpaceTime) (hr : 0 < z.2.ofLp 0) (hangle : z.2.ofLp 1 - PolarCharts.offset j ∈ Set.Ioo (-(Real.pi / 2)) (Real.pi / 2)) (hchart : (PhysicalGraphBounds.scaledRadial n) (z.1, CylindricalResidual.chart z.2) ∈ PolarCharts.chartDomain a j) : polarPoint a j (PhysicalWaveSum.commonLift h n d (z.1, CylindricalResidual.chart z.2)) = PhysicalResidualTZ.swapCylinder ((PhysicalResidualBridge.commonGraph (ChartScales.Q n) h (ChartScales.nativeIndex h n - d)).map z)

theorem NavierStokes.InitialPhysicalData.commonIndex_gap (L : PhysicalWaveSum.BandLabel) : ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (↑L).1 - gap L = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h (↑L).1

theorem NavierStokes.InitialPhysicalData.liftedPotential_eq_mode {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) (x : Point) : CurlClassBounds.vectorPotential ((ActualPrimaryBounds.cutCoefficients l).frequency n) PhysicalResidualBridge.ScaledGraph.radius (PhysicalResidualBridge.commonGraph (ChartScales.Q n) CorrectionInitialization.ActualPrimary.h (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n)).radial PhysicalResidualBridge.ScaledGraph.angular (PhysicalResidualBridge.commonGraph (ChartScales.Q n) CorrectionInitialization.ActualPrimary.h (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n)).axial (ActualPrimaryCoherence.liftedPhase l.1 l.2 n) (ActualPrimaryCoherence.liftedAmplitude l.1 l.2 n) x = HarmonicCalculus.vectorMode ((ActualPrimaryBounds.cutCoefficients l).frequency n) ((ActualPrimaryBounds.cutCoefficients l).phase n) (potentialCoefficient l n) (PhysicalResidualTZ.swapCylinder x)

theorem NavierStokes.InitialPhysicalData.physicalPotential_eq_mode {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) {z : ProblemStatement.SpaceTime} (ht : z.1 < 1) (hr : 0 < z.2.ofLp 0) : ActualPrimaryCoherence.physicalPotential l.1 l.2 z = ChartScales.Q n ^ (-CorrectionInitialization.ActualPrimary.h) • HarmonicCalculus.vectorMode ((ActualPrimaryBounds.cutCoefficients l).frequency n) ((ActualPrimaryBounds.cutCoefficients l).phase n) (potentialCoefficient l n) (PhysicalResidualTZ.swapCylinder ((PhysicalResidualBridge.commonGraph (ChartScales.Q n) CorrectionInitialization.ActualPrimary.h (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n)).map z))

theorem NavierStokes.InitialPhysicalData.potentialCoefficient_angle {B N0 : ℕ} (l : SignedLabel B N0) (x : LocalSignedRequest.Point) (θ : ℝ) : potentialCoefficient l (BaseChartJets.cellBand l.2) (x, θ) = potentialCoefficient l (BaseChartJets.cellBand l.2) (x, 0)

theorem NavierStokes.InitialPhysicalData.potentialCoefficient_polar {B N0 : ℕ} (l : SignedLabel B N0) {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) {x : LiftPoint} (hx : PhysicalGraphBounds.liftXY x ∈ PolarCharts.chartDomain a j) : potentialCoefficient l (BaseChartJets.cellBand l.2) (polarPoint a j x) = potentialCoefficient l (BaseChartJets.cellBand l.2) (PhysicalClassBounds.cylindricalMap x, 0)

theorem NavierStokes.InitialPhysicalData.commonIndex_gap_selected {B N0 : ℕ} (l : SignedLabel B N0) : ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2) - gap (bandLabel l) = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2)

theorem NavierStokes.InitialPhysicalData.potential_periodized_of_chart {B N0 : ℕ} (l : SignedLabel B N0) (i : Fin 3) (j : PolarCharts.Index) (w : ProblemStatement.SpaceTime) (hw : w ∈ PhysicalWaveSum.preterminal) (hann : (PhysicalGraphBounds.scaledRadial (BaseChartJets.cellBand l.2)) w ∈ PhysicalGraphBounds.annulus innerRadius outerRadius) (hj : (PhysicalGraphBounds.scaledRadial (BaseChartJets.cellBand l.2)) w ∈ PolarCharts.chartDomain innerRadius j) : (potentialFamily B N0 i).periodized innerRadius CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius (positiveIndex l) w = ChartScales.Q (BaseChartJets.cellBand l.2) ^ (-CorrectionInitialization.ActualPrimary.h) • (CartesianCopySource.rotationMap ((PhysicalGraphBounds.scaledRadial (BaseChartJets.cellBand l.2)) w)) (potentialCoefficient l (BaseChartJets.cellBand l.2) (PhysicalMeanJetBounds.graph CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2) (gap (bandLabel l)) w, 0)) i * HarmonicCalculus.carrier ((ActualPrimaryBounds.cutCoefficients l).frequency (BaseChartJets.cellBand l.2)) ((ActualPrimaryBounds.cutCoefficients l).phase (BaseChartJets.cellBand l.2)) (polarPoint innerRadius j (PhysicalWaveSum.commonLift CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2) (gap (bandLabel l)) w))

theorem NavierStokes.InitialPhysicalData.pressure_periodized_of_chart {B N0 : ℕ} (l : SignedLabel B N0) (j : PolarCharts.Index) (w : ProblemStatement.SpaceTime) (hw : w ∈ PhysicalWaveSum.preterminal) (hann : (PhysicalGraphBounds.scaledRadial (BaseChartJets.cellBand l.2)) w ∈ PhysicalGraphBounds.annulus innerRadius outerRadius) (hj : (PhysicalGraphBounds.scaledRadial (BaseChartJets.cellBand l.2)) w ∈ PolarCharts.chartDomain innerRadius j) : (pressureFamily B N0).periodized innerRadius CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius (positiveIndex l) w = ChartScales.Q (BaseChartJets.cellBand l.2) ^ (-(2 * CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h)) • (ActualPrimaryBounds.cutCoefficients l).pressure (BaseChartJets.cellBand l.2) (PhysicalMeanJetBounds.graph CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2) (gap (bandLabel l)) w, 0) * HarmonicCalculus.carrier ((ActualPrimaryBounds.cutCoefficients l).frequency (BaseChartJets.cellBand l.2)) ((ActualPrimaryBounds.cutCoefficients l).phase (BaseChartJets.cellBand l.2)) (polarPoint innerRadius j (PhysicalWaveSum.commonLift CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2) (gap (bandLabel l)) w))

theorem NavierStokes.InitialPhysicalData.potential_periodized_mode {B N0 : ℕ} (l : SignedLabel B N0) (i : Fin 3) (j : PolarCharts.Index) (w : ProblemStatement.SpaceTime) (hw : w ∈ PhysicalWaveSum.preterminal) (hann : (PhysicalGraphBounds.scaledRadial (BaseChartJets.cellBand l.2)) w ∈ PhysicalGraphBounds.annulus innerRadius outerRadius) (hj : (PhysicalGraphBounds.scaledRadial (BaseChartJets.cellBand l.2)) w ∈ PolarCharts.chartDomain innerRadius j) : (potentialFamily B N0 i).periodized innerRadius CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius (positiveIndex l) w = ChartScales.Q (BaseChartJets.cellBand l.2) ^ (-CorrectionInitialization.ActualPrimary.h) • ActualSignedPhysicalData.rotateCoefficient ((PhysicalGraphBounds.scaledRadial (BaseChartJets.cellBand l.2)) w) (HarmonicCalculus.vectorMode ((ActualPrimaryBounds.cutCoefficients l).frequency (BaseChartJets.cellBand l.2)) ((ActualPrimaryBounds.cutCoefficients l).phase (BaseChartJets.cellBand l.2)) (potentialCoefficient l (BaseChartJets.cellBand l.2)) (polarPoint innerRadius j (PhysicalWaveSum.commonLift CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2) (gap (bandLabel l)) w))) i

theorem NavierStokes.InitialPhysicalData.pressureCoefficient_polar {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) {x : LiftPoint} (hx : PhysicalGraphBounds.liftXY x ∈ PolarCharts.chartDomain a j) : (ActualPrimaryBounds.cutCoefficients l).pressure n (polarPoint a j x) = (ActualPrimaryBounds.cutCoefficients l).pressure n (PhysicalClassBounds.cylindricalMap x, 0)

theorem NavierStokes.InitialPhysicalData.pressure_periodized_mode {B N0 : ℕ} (l : SignedLabel B N0) (j : PolarCharts.Index) (w : ProblemStatement.SpaceTime) (hw : w ∈ PhysicalWaveSum.preterminal) (hann : (PhysicalGraphBounds.scaledRadial (BaseChartJets.cellBand l.2)) w ∈ PhysicalGraphBounds.annulus innerRadius outerRadius) (hj : (PhysicalGraphBounds.scaledRadial (BaseChartJets.cellBand l.2)) w ∈ PolarCharts.chartDomain innerRadius j) : (pressureFamily B N0).periodized innerRadius CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius (positiveIndex l) w = ChartScales.Q (BaseChartJets.cellBand l.2) ^ (-(2 * CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h)) • HarmonicCalculus.mode ((ActualPrimaryBounds.cutCoefficients l).frequency (BaseChartJets.cellBand l.2)) ((ActualPrimaryBounds.cutCoefficients l).phase (BaseChartJets.cellBand l.2)) ((ActualPrimaryBounds.cutCoefficients l).pressure (BaseChartJets.cellBand l.2)) (polarPoint innerRadius j (PhysicalWaveSum.commonLift CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2) (gap (bandLabel l)) w))

theorem NavierStokes.InitialPhysicalData.potential_periodized_cartesian {B N0 : ℕ} (l : SignedLabel B N0) (i : Fin 3) (j : PolarCharts.Index) (z : ProblemStatement.SpaceTime) (ht : z.1 < 1) (hr : 0 < z.2.ofLp 0) (hangle : z.2.ofLp 1 - PolarCharts.offset j ∈ Set.Ioo (-(Real.pi / 2)) (Real.pi / 2)) (hann : (PhysicalGraphBounds.scaledRadial (BaseChartJets.cellBand l.2)) (z.1, CylindricalResidual.chart z.2) ∈ PhysicalGraphBounds.annulus innerRadius outerRadius) (hj : (PhysicalGraphBounds.scaledRadial (BaseChartJets.cellBand l.2)) (z.1, CylindricalResidual.chart z.2) ∈ PolarCharts.chartDomain innerRadius j) : ((potentialFamily B N0 i).periodized innerRadius CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius (positiveIndex l) (z.1, CylindricalResidual.chart z.2)).re = (ActualPrimaryCoherence.cartesianPotential l.1 l.2 (z.1, CylindricalResidual.chart z.2)).ofLp i

theorem NavierStokes.InitialPhysicalData.pressure_periodized_physical {B N0 : ℕ} (l : SignedLabel B N0) (j : PolarCharts.Index) (z : ProblemStatement.SpaceTime) (ht : z.1 < 1) (hr : 0 < z.2.ofLp 0) (hangle : z.2.ofLp 1 - PolarCharts.offset j ∈ Set.Ioo (-(Real.pi / 2)) (Real.pi / 2)) (hann : (PhysicalGraphBounds.scaledRadial (BaseChartJets.cellBand l.2)) (z.1, CylindricalResidual.chart z.2) ∈ PhysicalGraphBounds.annulus innerRadius outerRadius) (hj : (PhysicalGraphBounds.scaledRadial (BaseChartJets.cellBand l.2)) (z.1, CylindricalResidual.chart z.2) ∈ PolarCharts.chartDomain innerRadius j) : ((pressureFamily B N0).periodized innerRadius CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius (positiveIndex l) (z.1, CylindricalResidual.chart z.2)).re = ActualPrimaryCoherence.physicalPressure l.1 l.2 z

noncomputable def NavierStokes.InitialPhysicalData.scaledRepresentative (a : ℝ) (j : PolarCharts.Index) (n : ℕ) (w : ProblemStatement.SpaceTime) : ProblemStatement.SpaceTime

Scaled representative as an element of ProblemStatement.SpaceTime.

Equations

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

theorem NavierStokes.InitialPhysicalData.scaledRepresentative_spec {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) (n : ℕ) (w : ProblemStatement.SpaceTime) (hj : (PhysicalGraphBounds.scaledRadial n) w ∈ PolarCharts.chartDomain a j) : (scaledRepresentative a j n w).1 = w.1 ∧ 0 < (scaledRepresentative a j n w).2.ofLp 0 ∧ (scaledRepresentative a j n w).2.ofLp 1 - PolarCharts.offset j ∈ Set.Ioo (-(Real.pi / 2)) (Real.pi / 2) ∧ ((scaledRepresentative a j n w).1, CylindricalResidual.chart (scaledRepresentative a j n w).2) = w

theorem NavierStokes.InitialPhysicalData.exists_scaledRepresentative (n : ℕ) (w : ProblemStatement.SpaceTime) (hw : PhysicalGraphBounds.radialProjection w ≠ 0) : ∃ (z : ProblemStatement.SpaceTime), z.1 = w.1 ∧ 0 < z.2.ofLp 0 ∧ (z.1, CylindricalResidual.chart z.2) = w

theorem NavierStokes.InitialPhysicalData.cartesianPotential_zero_of_common_zero {B N0 : ℕ} (l : SignedLabel B N0) (w : ProblemStatement.SpaceTime) (hw : w ∈ PhysicalWaveSum.preterminal) (hz : potentialCoefficient l (BaseChartJets.cellBand l.2) (PhysicalMeanJetBounds.graph CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2) (gap (bandLabel l)) w, 0) = 0) : ActualPrimaryCoherence.cartesianPotential l.1 l.2 w = 0

theorem NavierStokes.InitialPhysicalData.potentialCoefficient_zero_off_annulus {B N0 : ℕ} (l : SignedLabel B N0) (w : ProblemStatement.SpaceTime) (hw : w ∈ PhysicalWaveSum.preterminal) (hann : (PhysicalGraphBounds.scaledRadial (BaseChartJets.cellBand l.2)) w ∉ PhysicalGraphBounds.annulus innerRadius outerRadius) : potentialCoefficient l (BaseChartJets.cellBand l.2) (PhysicalMeanJetBounds.graph CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2) (gap (bandLabel l)) w, 0) = 0

theorem NavierStokes.InitialPhysicalData.potential_periodized_eq {B N0 : ℕ} (l : SignedLabel B N0) (i : Fin 3) (w : ProblemStatement.SpaceTime) (hw : w ∈ PhysicalWaveSum.preterminal) : ((potentialFamily B N0 i).periodized innerRadius CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius (positiveIndex l) w).re = (ActualPrimaryCoherence.cartesianPotential l.1 l.2 w).ofLp i

Every actual periodized initial potential is the pre-existing Cartesian primary potential, including the zero region and the axis.

noncomputable def NavierStokes.InitialPhysicalData.physicalPressureCoefficient {B N0 : ℕ} (l : SignedLabel B N0) (z : ProblemStatement.SpaceTime) : ℂ

Physical pressure coefficient, constructed using ActualPrimary.periodicGaussian.

Equations

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

theorem NavierStokes.InitialPhysicalData.physicalPressureCoefficient_invariant {B N0 : ℕ} (l : SignedLabel B N0) : CopyAngularInvariance.Invariant ActualPrimaryCoherence.physicalAngular (physicalPressureCoefficient l)

theorem NavierStokes.InitialPhysicalData.physicalPressure_mode {B N0 : ℕ} (l : SignedLabel B N0) (z : ProblemStatement.SpaceTime) : ActualPrimaryCoherence.physicalPressure l.1 l.2 z = (HarmonicCalculus.mode 1 (ActualPrimaryCoherence.physicalPhase l.1 l.2) (physicalPressureCoefficient l) z).re

theorem NavierStokes.InitialPhysicalData.physicalPressure_periodic {B N0 : ℕ} (l : SignedLabel B N0) (t r z : ℝ) : Function.Periodic (fun (θ : ℝ) => ActualPrimaryCoherence.physicalPressure l.1 l.2 (t, AxisymmetricResidual.pack r θ z)) (2 * Real.pi)

theorem NavierStokes.InitialPhysicalData.space_pack (q : ProblemStatement.Space) : AxisymmetricResidual.pack (q.ofLp 0) (q.ofLp 1) (q.ofLp 2) = q

theorem NavierStokes.InitialPhysicalData.physicalPressure_eq_of_chart_eq {B N0 : ℕ} (l : SignedLabel B N0) {z z' : ProblemStatement.SpaceTime} (hr : 0 < z.2.ofLp 0) (hr' : 0 < z'.2.ofLp 0) (he : (z.1, CylindricalResidual.chart z.2) = (z'.1, CylindricalResidual.chart z'.2)) : ActualPrimaryCoherence.physicalPressure l.1 l.2 z = ActualPrimaryCoherence.physicalPressure l.1 l.2 z'

theorem NavierStokes.InitialPhysicalData.pressureCoefficient_zero_off_annulus {B N0 : ℕ} (l : SignedLabel B N0) (w : ProblemStatement.SpaceTime) (hw : w ∈ PhysicalWaveSum.preterminal) (hann : (PhysicalGraphBounds.scaledRadial (BaseChartJets.cellBand l.2)) w ∉ PhysicalGraphBounds.annulus innerRadius outerRadius) : (ActualPrimaryBounds.cutCoefficients l).pressure (BaseChartJets.cellBand l.2) (PhysicalMeanJetBounds.graph CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2) (gap (bandLabel l)) w, 0) = 0

theorem NavierStokes.InitialPhysicalData.physicalPressure_zero_of_common_zero {B N0 : ℕ} (l : SignedLabel B N0) (z : ProblemStatement.SpaceTime) (hr : 0 < z.2.ofLp 0) (hz : (ActualPrimaryBounds.cutCoefficients l).pressure (BaseChartJets.cellBand l.2) (PhysicalMeanJetBounds.graph CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2) (gap (bandLabel l)) (z.1, CylindricalResidual.chart z.2), 0) = 0) : ActualPrimaryCoherence.physicalPressure l.1 l.2 z = 0

theorem NavierStokes.InitialPhysicalData.pressure_periodized_eq {B N0 : ℕ} (l : SignedLabel B N0) (z : ProblemStatement.SpaceTime) (ht : z.1 < 1) (hr : 0 < z.2.ofLp 0) : ((pressureFamily B N0).periodized innerRadius CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius (positiveIndex l) (z.1, CylindricalResidual.chart z.2)).re = ActualPrimaryCoherence.physicalPressure l.1 l.2 z

The actual periodized pressure agrees with the original cylindrical pressure on every positive-radius physical chart, with all angular branches identified by the proved integer harmonic periodicity.

noncomputable def NavierStokes.InitialPhysicalData.primaryIndex {B N0 : ℕ} (l : CorrectionInitialization.ActualPrimary.Label B N0 × Fin 2) : PhysicalWaveSum.WaveIndex 1

Primary index, given by positiveIndex (l.2, l.1).

Equations

• NavierStokes.InitialPhysicalData.primaryIndex l = NavierStokes.InitialPhysicalData.positiveIndex (l.2, l.1)

theorem NavierStokes.InitialPhysicalData.primaryIndex_injective {B N0 : ℕ} : Function.Injective primaryIndex

theorem NavierStokes.InitialPhysicalData.eq_primaryIndex_of_data {B N0 : ℕ} (l : SignedLabel B N0) (I : PhysicalWaveSum.WaveIndex 1) (hl : bandLabel l = I.1) (hi : ↑I.2 = 1) : primaryIndex (l.2, l.1) = I

theorem NavierStokes.InitialPhysicalData.periodized_nonzero_copy {H : ℕ} {K : Type u_1} (f : PhysicalCopyBounds.CopyFamily H K) (a h r0 : ℝ) (I : PhysicalWaveSum.WaveIndex H) (w : ProblemStatement.SpaceTime) (hn : f.periodized a h r0 I w ≠ 0) : ∃ (k : K), f.term a h r0 I k w ≠ 0

theorem NavierStokes.InitialPhysicalData.potential_periodized_index {B N0 : ℕ} (i : Fin 3) (I : PhysicalWaveSum.WaveIndex 1) (w : ProblemStatement.SpaceTime) (hn : (potentialFamily B N0 i).periodized innerRadius CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius I w ≠ 0) : ∃ (l : CorrectionInitialization.ActualPrimary.Label B N0 × Fin 2), primaryIndex l = I

theorem NavierStokes.InitialPhysicalData.pressure_periodized_index {B N0 : ℕ} (I : PhysicalWaveSum.WaveIndex 1) (w : ProblemStatement.SpaceTime) (hn : (pressureFamily B N0).periodized innerRadius CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius I w ≠ 0) : ∃ (l : CorrectionInitialization.ActualPrimary.Label B N0 × Fin 2), primaryIndex l = I

theorem NavierStokes.InitialPhysicalData.periodized_sum_eq_active {B N0 : ℕ} (f : PhysicalCopyBounds.CopyFamily 1 Frequency) (hsource : ∀ (I : PhysicalWaveSum.WaveIndex 1) (w : ProblemStatement.SpaceTime), f.periodized innerRadius CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius I w ≠ 0 → ∃ (l : CorrectionInitialization.ActualPrimary.Label B N0 × Fin 2), primaryIndex l = I) (hsupport : ∀ (I : PhysicalWaveSum.WaveIndex 1), ∀ w ∈ PhysicalWaveSum.preterminal, f.periodized innerRadius CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius I w ≠ 0 → PhysicalWaveSum.physicalParams CorrectionInitialization.ActualPrimary.h w ∈ PhysicalWaveSum.labelRegion (CoordinateAlgebra.D CorrectionInitialization.ActualPrimary.h) ↑I.1) (n d : ℕ) (w : ProblemStatement.SpaceTime) (hw : w ∈ PhysicalWaveSum.preterminal) (hx : PhysicalMeanJetBounds.graph CorrectionInitialization.ActualPrimary.h n d w ∈ ActualPrimaryBounds.strip.domain) : f.sum innerRadius CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius w = ∑ l ∈ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n, f.periodized innerRadius CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius (primaryIndex l) w

theorem NavierStokes.InitialPhysicalData.potential_sum_eq_active {B N0 : ℕ} (i : Fin 3) (n d : ℕ) (w : ProblemStatement.SpaceTime) (hw : w ∈ PhysicalWaveSum.preterminal) (hx : PhysicalMeanJetBounds.graph CorrectionInitialization.ActualPrimary.h n d w ∈ ActualPrimaryBounds.strip.domain) : (potentialFamily B N0 i).sum innerRadius CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius w = ∑ l ∈ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n, (potentialFamily B N0 i).periodized innerRadius CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius (primaryIndex l) w

theorem NavierStokes.InitialPhysicalData.pressure_sum_eq_active {B N0 : ℕ} (n d : ℕ) (w : ProblemStatement.SpaceTime) (hw : w ∈ PhysicalWaveSum.preterminal) (hx : PhysicalMeanJetBounds.graph CorrectionInitialization.ActualPrimary.h n d w ∈ ActualPrimaryBounds.strip.domain) : (pressureFamily B N0).sum innerRadius CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius w = ∑ l ∈ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n, (pressureFamily B N0).periodized innerRadius CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius (primaryIndex l) w

theorem NavierStokes.InitialPhysicalData.vectorSum_apply {H : ℕ} {K : Type u_1} (f : Fin 3 → PhysicalCopyBounds.CopyFamily H K) (a h r0 : ℝ) (w : ProblemStatement.SpaceTime) (i : Fin 3) : (PhysicalCopyBounds.vectorSum f a h r0 w).ofLp i = ((f i).sum a h r0 w).re

theorem NavierStokes.InitialPhysicalData.graph_smooth_of_strip (n d : ℕ) {w : ProblemStatement.SpaceTime} (hx : PhysicalMeanJetBounds.graph CorrectionInitialization.ActualPrimary.h n d w ∈ ActualPrimaryBounds.strip.domain) : ContDiffAt ℝ (↑⊤) (PhysicalMeanJetBounds.graph CorrectionInitialization.ActualPrimary.h n d) w

theorem NavierStokes.InitialPhysicalData.spatialCurl_finset_sum {I : Type u_1} (s : Finset I) (A : I → ProblemStatement.VelocityField) {w : ProblemStatement.SpaceTime} (hA : ∀ i ∈ s, DifferentiableAt ℝ (A i) w) : SpatialCurl.spatialCurl (fun (z : ProblemStatement.SpaceTime) => ∑ i ∈ s, A i z) w = ∑ i ∈ s, SpatialCurl.spatialCurl (A i) w

theorem NavierStokes.InitialPhysicalData.primary_cartesianCurl_sum {B N0 : ℕ} (s : Finset (CorrectionInitialization.ActualPrimary.Label B N0 × Fin 2)) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) : SpatialCurl.spatialCurl (fun (z : ProblemStatement.SpaceTime) => ∑ l ∈ s, ActualPrimaryCoherence.cartesianPotential l.2 l.1 z) w = ∑ l ∈ s, ActualPrimaryCoherence.cartesianVelocity l.2 l.1 w

theorem NavierStokes.InitialPhysicalData.potential_eq_active {B N0 : ℕ} (n d : ℕ) (w : ProblemStatement.SpaceTime) (hw : w ∈ PhysicalWaveSum.preterminal) (hx : PhysicalMeanJetBounds.graph CorrectionInitialization.ActualPrimary.h n d w ∈ ActualPrimaryBounds.strip.domain) : potential B N0 w = ∑ l ∈ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n, ActualPrimaryCoherence.cartesianPotential l.2 l.1 w

The constructed global potential is the literal finite primary sum on every valid current-band chart.

theorem NavierStokes.InitialPhysicalData.potential_germ_eq_active {B N0 : ℕ} (n d : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hx : PhysicalMeanJetBounds.graph CorrectionInitialization.ActualPrimary.h n d w ∈ ActualPrimaryBounds.strip.domain) : potential B N0 =ᶠ[nhds w] fun (z : ProblemStatement.SpaceTime) => ∑ l ∈ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n, ActualPrimaryCoherence.cartesianPotential l.2 l.1 z

The same fixed finite family represents the potential on a full spacetime neighborhood; hence its spatial curl may be taken termwise.

theorem NavierStokes.InitialPhysicalData.curl_eq_active {B N0 : ℕ} (n d : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hx : PhysicalMeanJetBounds.graph CorrectionInitialization.ActualPrimary.h n d w ∈ ActualPrimaryBounds.strip.domain) : SpatialCurl.spatialCurl (potential B N0) w = ∑ l ∈ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n, ActualPrimaryCoherence.cartesianVelocity l.2 l.1 w

theorem NavierStokes.InitialPhysicalData.pressure_eq_active {B N0 : ℕ} (n d : ℕ) (z : ProblemStatement.SpaceTime) (ht : z.1 < 1) (hr : 0 < z.2.ofLp 0) (hx : PhysicalMeanJetBounds.graph CorrectionInitialization.ActualPrimary.h n d (z.1, CylindricalResidual.chart z.2) ∈ ActualPrimaryBounds.strip.domain) : pressure B N0 (z.1, CylindricalResidual.chart z.2) = ∑ l ∈ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n, ActualPrimaryCoherence.physicalPressure l.2 l.1 z

theorem NavierStokes.InitialPhysicalData.velocity_chart {B N0 : ℕ} (n d : ℕ) (z : ProblemStatement.SpaceTime) (ht : z.1 < 1) (hr : 0 < z.2.ofLp 0) (hx : PhysicalMeanJetBounds.graph CorrectionInitialization.ActualPrimary.h n d (z.1, CylindricalResidual.chart z.2) ∈ ActualPrimaryBounds.strip.domain) (i : Fin 3) : ∑ l ∈ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n, (CorrectionInitialization.ActualPrimary.piece CorrectionInitialization.ActualPrimary.standardRegion l.2 l.1).velocity n (PhysicalResidualTZ.swapCylinder ((PhysicalResidualBridge.commonGraph (ChartScales.Q n) CorrectionInitialization.ActualPrimary.h (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n)).map z)) i = ChartScales.Q n ^ CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h * ((CylindricalResidual.frame (-z.2.ofLp 1)) (SpatialCurl.spatialCurl (potential B N0) (z.1, CylindricalResidual.chart z.2))).ofLp i

Exact normalized velocity of the initialized primary aggregate. The right side is the curl of the actual Cartesian potential constructed above.

theorem NavierStokes.InitialPhysicalData.pressure_chart {B N0 : ℕ} (n d : ℕ) (z : ProblemStatement.SpaceTime) (ht : z.1 < 1) (hr : 0 < z.2.ofLp 0) (hx : PhysicalMeanJetBounds.graph CorrectionInitialization.ActualPrimary.h n d (z.1, CylindricalResidual.chart z.2) ∈ ActualPrimaryBounds.strip.domain) : ∑ l ∈ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n, (CorrectionInitialization.ActualPrimary.piece CorrectionInitialization.ActualPrimary.standardRegion l.2 l.1).pressure n (PhysicalResidualTZ.swapCylinder ((PhysicalResidualBridge.commonGraph (ChartScales.Q n) CorrectionInitialization.ActualPrimary.h (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n)).map z)) = ChartScales.Q n ^ (2 * CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h) * pressure B N0 (z.1, CylindricalResidual.chart z.2)

theorem NavierStokes.InitialPhysicalData.physicalX_eq_profileRadius_sq (n d : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) : physicalX w = PrimaryTargetBounds.profileRadius CorrectionInitialization.ActualPrimary.h (BaseContextAssembly.slowCoordinates (PhysicalMeanJetBounds.graph CorrectionInitialization.ActualPrimary.h n d w)) ^ 2 / 2

theorem NavierStokes.InitialPhysicalData.graph_mem_strip_of_activeX (n d : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hs : (PhysicalMeanJetBounds.graph CorrectionInitialization.ActualPrimary.h n d w).2.1 ∈ CorrectionInitialization.ActualPrimary.standardRegion.carrier) (hX : physicalX w ∈ Set.Ioo (NominalConeAssembly.activeLeft CorrectionInitialization.ActualPrimary.nominal) (NominalConeAssembly.activeRight CorrectionInitialization.ActualPrimary.nominal)) : PhysicalMeanJetBounds.graph CorrectionInitialization.ActualPrimary.h n d w ∈ ActualPrimaryBounds.strip.domain

theorem NavierStokes.InitialPhysicalData.potential_periodized_activeX {B N0 : ℕ} (i : Fin 3) (I : PhysicalWaveSum.WaveIndex 1) (w : ProblemStatement.SpaceTime) (hw : w ∈ PhysicalWaveSum.preterminal) (hn : (potentialFamily B N0 i).periodized innerRadius CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius I w ≠ 0) : physicalX w ∈ Set.Ioo (NominalConeAssembly.activeLeft CorrectionInitialization.ActualPrimary.nominal) (NominalConeAssembly.activeRight CorrectionInitialization.ActualPrimary.nominal)

theorem NavierStokes.InitialPhysicalData.pressure_periodized_activeX {B N0 : ℕ} (I : PhysicalWaveSum.WaveIndex 1) (w : ProblemStatement.SpaceTime) (hw : w ∈ PhysicalWaveSum.preterminal) (hn : (pressureFamily B N0).periodized innerRadius CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius I w ≠ 0) : physicalX w ∈ Set.Ioo (NominalConeAssembly.activeLeft CorrectionInitialization.ActualPrimary.nominal) (NominalConeAssembly.activeRight CorrectionInitialization.ActualPrimary.nominal)

theorem NavierStokes.InitialPhysicalData.periodized_sum_eq_active_of_support {B N0 : ℕ} (f : PhysicalCopyBounds.CopyFamily 1 Frequency) (hsource : ∀ (I : PhysicalWaveSum.WaveIndex 1) (w : ProblemStatement.SpaceTime), f.periodized innerRadius CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius I w ≠ 0 → ∃ (l : CorrectionInitialization.ActualPrimary.Label B N0 × Fin 2), primaryIndex l = I) (hsupport : ∀ (I : PhysicalWaveSum.WaveIndex 1), ∀ w ∈ PhysicalWaveSum.preterminal, f.periodized innerRadius CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius I w ≠ 0 → PhysicalWaveSum.physicalParams CorrectionInitialization.ActualPrimary.h w ∈ PhysicalWaveSum.labelRegion (CoordinateAlgebra.D CorrectionInitialization.ActualPrimary.h) ↑I.1) (n d : ℕ) (w : ProblemStatement.SpaceTime) (hw : w ∈ PhysicalWaveSum.preterminal) (hstrip : ∀ (I : PhysicalWaveSum.WaveIndex 1), f.periodized innerRadius CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius I w ≠ 0 → PhysicalMeanJetBounds.graph CorrectionInitialization.ActualPrimary.h n d w ∈ ActualPrimaryBounds.strip.domain) : f.sum innerRadius CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius w = ∑ l ∈ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n, f.periodized innerRadius CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius (primaryIndex l) w

theorem NavierStokes.InitialPhysicalData.potential_sum_eq_active_slow {B N0 : ℕ} (i : Fin 3) (n d : ℕ) (w : ProblemStatement.SpaceTime) (hw : w ∈ PhysicalWaveSum.preterminal) (hs : (PhysicalMeanJetBounds.graph CorrectionInitialization.ActualPrimary.h n d w).2.1 ∈ CorrectionInitialization.ActualPrimary.standardRegion.carrier) : (potentialFamily B N0 i).sum innerRadius CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius w = ∑ l ∈ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n, (potentialFamily B N0 i).periodized innerRadius CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius (primaryIndex l) w

theorem NavierStokes.InitialPhysicalData.pressure_sum_eq_active_slow {B N0 : ℕ} (n d : ℕ) (w : ProblemStatement.SpaceTime) (hw : w ∈ PhysicalWaveSum.preterminal) (hs : (PhysicalMeanJetBounds.graph CorrectionInitialization.ActualPrimary.h n d w).2.1 ∈ CorrectionInitialization.ActualPrimary.standardRegion.carrier) : (pressureFamily B N0).sum innerRadius CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius w = ∑ l ∈ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n, (pressureFamily B N0).periodized innerRadius CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius (primaryIndex l) w

theorem NavierStokes.InitialPhysicalData.potential_eq_active_slow {B N0 : ℕ} (n d : ℕ) (w : ProblemStatement.SpaceTime) (hw : w ∈ PhysicalWaveSum.preterminal) (hs : (PhysicalMeanJetBounds.graph CorrectionInitialization.ActualPrimary.h n d w).2.1 ∈ CorrectionInitialization.ActualPrimary.standardRegion.carrier) : potential B N0 w = ∑ l ∈ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n, ActualPrimaryCoherence.cartesianPotential l.2 l.1 w

The finite primary identity holds throughout the slow chart, including both radial edges and every positive exterior radius.

theorem NavierStokes.InitialPhysicalData.potential_germ_eq_active_slow {B N0 : ℕ} (n d : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hs : (PhysicalMeanJetBounds.graph CorrectionInitialization.ActualPrimary.h n d w).2.1 ∈ CorrectionInitialization.ActualPrimary.standardRegion.carrier) : potential B N0 =ᶠ[nhds w] fun (z : ProblemStatement.SpaceTime) => ∑ l ∈ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n, ActualPrimaryCoherence.cartesianPotential l.2 l.1 z

theorem NavierStokes.InitialPhysicalData.curl_eq_active_slow {B N0 : ℕ} (n d : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hs : (PhysicalMeanJetBounds.graph CorrectionInitialization.ActualPrimary.h n d w).2.1 ∈ CorrectionInitialization.ActualPrimary.standardRegion.carrier) : SpatialCurl.spatialCurl (potential B N0) w = ∑ l ∈ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n, ActualPrimaryCoherence.cartesianVelocity l.2 l.1 w

theorem NavierStokes.InitialPhysicalData.pressure_eq_active_slow {B N0 : ℕ} (n d : ℕ) (z : ProblemStatement.SpaceTime) (ht : z.1 < 1) (hr : 0 < z.2.ofLp 0) (hs : (PhysicalMeanJetBounds.graph CorrectionInitialization.ActualPrimary.h n d (z.1, CylindricalResidual.chart z.2)).2.1 ∈ CorrectionInitialization.ActualPrimary.standardRegion.carrier) : pressure B N0 (z.1, CylindricalResidual.chart z.2) = ∑ l ∈ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n, ActualPrimaryCoherence.physicalPressure l.2 l.1 z

theorem NavierStokes.InitialPhysicalData.velocity_chart_slow {B N0 : ℕ} (n d : ℕ) (z : ProblemStatement.SpaceTime) (ht : z.1 < 1) (hr : 0 < z.2.ofLp 0) (hs : (PhysicalMeanJetBounds.graph CorrectionInitialization.ActualPrimary.h n d (z.1, CylindricalResidual.chart z.2)).2.1 ∈ CorrectionInitialization.ActualPrimary.standardRegion.carrier) (i : Fin 3) : ∑ l ∈ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n, (CorrectionInitialization.ActualPrimary.piece CorrectionInitialization.ActualPrimary.standardRegion l.2 l.1).velocity n (PhysicalResidualTZ.swapCylinder ((PhysicalResidualBridge.commonGraph (ChartScales.Q n) CorrectionInitialization.ActualPrimary.h (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n)).map z)) i = ChartScales.Q n ^ CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h * ((CylindricalResidual.frame (-z.2.ofLp 1)) (SpatialCurl.spatialCurl (potential B N0) (z.1, CylindricalResidual.chart z.2))).ofLp i

Full positive-radius version of the initial velocity chart identity. Only slow-chart membership is required; the radial edges are included.

theorem NavierStokes.InitialPhysicalData.pressure_chart_slow {B N0 : ℕ} (n d : ℕ) (z : ProblemStatement.SpaceTime) (ht : z.1 < 1) (hr : 0 < z.2.ofLp 0) (hs : (PhysicalMeanJetBounds.graph CorrectionInitialization.ActualPrimary.h n d (z.1, CylindricalResidual.chart z.2)).2.1 ∈ CorrectionInitialization.ActualPrimary.standardRegion.carrier) : ∑ l ∈ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n, (CorrectionInitialization.ActualPrimary.piece CorrectionInitialization.ActualPrimary.standardRegion l.2 l.1).pressure n (PhysicalResidualTZ.swapCylinder ((PhysicalResidualBridge.commonGraph (ChartScales.Q n) CorrectionInitialization.ActualPrimary.h (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n)).map z)) = ChartScales.Q n ^ (2 * CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h) * pressure B N0 (z.1, CylindricalResidual.chart z.2)