Physical data of the actual native signed copies

The primitive signed quotient is unchanged. Its compact auxiliary cutoff is repartitioned exactly, and the physical carrier uses the midpoint of each actual lattice-translated slot.

@[reducible, inline]

abbrev NavierStokes.ActualSignedPhysicalData.Plane : Type

Plane: an abbreviation for TorusInverse.Plane.

Equations

• NavierStokes.ActualSignedPhysicalData.Plane = NavierStokes.TorusInverse.Plane

@[reducible, inline]

abbrev NavierStokes.ActualSignedPhysicalData.Frequency : Type

Frequency: an abbreviation for TorusInverse.Frequency.

Equations

• NavierStokes.ActualSignedPhysicalData.Frequency = NavierStokes.TorusInverse.Frequency

@[reducible, inline]

abbrev NavierStokes.ActualSignedPhysicalData.Cylinder : Type

Cylinder: an abbreviation for PhysicalResidualBridge.Cylinder.

Equations

• NavierStokes.ActualSignedPhysicalData.Cylinder = NavierStokes.PhysicalResidualBridge.Cylinder

@[reducible, inline]

abbrev NavierStokes.ActualSignedPhysicalData.LiftPoint : Type

Lift point: an abbreviation for PhysicalGraphBounds.LiftPoint.

Equations

• NavierStokes.ActualSignedPhysicalData.LiftPoint = NavierStokes.PhysicalGraphBounds.LiftPoint

@[reducible, inline]

abbrev NavierStokes.ActualSignedPhysicalData.Mat2 : Type

Mat2: an abbreviation for SmoothCovariance.Mat2.

Equations

• NavierStokes.ActualSignedPhysicalData.Mat2 = NavierStokes.SmoothCovariance.Mat2

@[reducible, inline]

abbrev NavierStokes.ActualSignedPhysicalData.Vec2 : Type

Vec2: an abbreviation for SmoothCovariance.Vec2.

Equations

• NavierStokes.ActualSignedPhysicalData.Vec2 = NavierStokes.SmoothCovariance.Vec2

theorem NavierStokes.ActualSignedPhysicalData.repartition_amplitude {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : LinearWaveBounds.WaveCoefficients D) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) (H : ℕ → D → Mat2) (T R : ℕ → D → Vec2) (mask factor cutoff : ℕ → D → ℝ) (unit Ndot : ℕ → D → ProblemStatement.Space) (A : ℕ → D → ProblemStatement.Space →L[ℝ] ProblemStatement.Space) (j : Fin 2) (n : ℕ) (x : D) : ((SignedWaveUpdate.coefficients a s d H T R (fun (n : ℕ) (x : D) => mask n x * factor n x) unit Ndot A j).withCutoff cutoff).amplitude n x = ((SignedWaveUpdate.coefficients a s d H T R mask unit Ndot A j).withCutoff fun (n : ℕ) (x : D) => cutoff n x * factor n x).amplitude n x

theorem NavierStokes.ActualSignedPhysicalData.repartition_pressure {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : LinearWaveBounds.WaveCoefficients D) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) (H : ℕ → D → Mat2) (T R : ℕ → D → Vec2) (mask factor cutoff : ℕ → D → ℝ) (unit Ndot : ℕ → D → ProblemStatement.Space) (A : ℕ → D → ProblemStatement.Space →L[ℝ] ProblemStatement.Space) (j : Fin 2) (n : ℕ) (x : D) : ((SignedWaveUpdate.coefficients a s d H T R (fun (n : ℕ) (x : D) => mask n x * factor n x) unit Ndot A j).withCutoff cutoff).pressure n x = ((SignedWaveUpdate.coefficients a s d H T R mask unit Ndot A j).withCutoff fun (n : ℕ) (x : D) => cutoff n x * factor n x).pressure n x

theorem NavierStokes.ActualSignedPhysicalData.coefficients_repartition {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : LinearWaveBounds.WaveCoefficients D) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) (H : ℕ → D → Mat2) (T R : ℕ → D → Vec2) (mask factor cutoff : ℕ → D → ℝ) (unit Ndot : ℕ → D → ProblemStatement.Space) (A : ℕ → D → ProblemStatement.Space →L[ℝ] ProblemStatement.Space) (j : Fin 2) : (SignedWaveUpdate.coefficients a s d H T R (fun (n : ℕ) (x : D) => mask n x * factor n x) unit Ndot A j).withCutoff cutoff = (SignedWaveUpdate.coefficients a s d H T R mask unit Ndot A j).withCutoff fun (n : ℕ) (x : D) => cutoff n x * factor n x

Moving a scalar cutoff from the raw signed mask to the final cutoff preserves both coefficients, before any differentiation.

theorem NavierStokes.ActualSignedPhysicalData.coefficients_outer {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : LinearWaveBounds.WaveCoefficients D) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) (H : ℕ → D → Mat2) (T R : ℕ → D → Vec2) (mask : ℕ → D → ℝ) (unit Ndot : ℕ → D → ProblemStatement.Space) (A : ℕ → D → ProblemStatement.Space →L[ℝ] ProblemStatement.Space) (j : Fin 2) (clock : ℕ → D → ℝ) : ((SignedWaveUpdate.coefficients a s d H T R (fun (n : ℕ) (x : D) => mask n x * PrimaryCopyBounds.outerCutoff (clock n x)) unit Ndot A j).withCutoff fun (n : ℕ) (x : D) => GaussianTailFlat.profile (clock n x)) = (SignedWaveUpdate.coefficients a s d H T R mask unit Ndot A j).withCutoff fun (n : ℕ) (x : D) => GaussianTailFlat.profile (clock n x)

The outer bump is one on the Gaussian support, so it can be removed from the raw mask without changing the actual once-cutoff signed wave.

theorem NavierStokes.ActualSignedPhysicalData.corrected_outer {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : LinearWaveBounds.WaveCoefficients D) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) (H : ℕ → D → Mat2) (T R : ℕ → D → Vec2) (mask : ℕ → D → ℝ) (unit Ndot : ℕ → D → ProblemStatement.Space) (A : ℕ → D → ProblemStatement.Space →L[ℝ] ProblemStatement.Space) (j : Fin 2) (clock : ℕ → D → ℝ) : ((SignedWaveUpdate.coefficients a s d H T R (fun (n : ℕ) (x : D) => mask n x * PrimaryCopyBounds.outerCutoff (clock n x)) unit Ndot A j).corrected s d fun (n : ℕ) (x : D) => GaussianTailFlat.profile (clock n x)) = (SignedWaveUpdate.coefficients a s d H T R mask unit Ndot A j).corrected s d fun (n : ℕ) (x : D) => GaussianTailFlat.profile (clock n x)

theorem NavierStokes.ActualSignedPhysicalData.common_eq_of_localized {D K : Type} (f g : PeriodizedWaveBounds.CopyData D K) (hb : f.background = g.background) (he : ∀ (k : K), f.localized k = g.localized k) : f.common = g.common

Equality of every actual localized copy is enough for equality of the whole common coefficients. Summability is not assumed here.

theorem NavierStokes.ActualSignedPhysicalData.commonCorrected_eq_of_localized {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {K : Type} (f g : PeriodizedWaveBounds.CopyData D K) (hb : f.background = g.background) (he : ∀ (k : K), f.localized k = g.localized k) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) : f.commonCorrected s d = g.commonCorrected s d

noncomputable def NavierStokes.ActualSignedPhysicalData.geometry {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (label : SlotColoring.Label) (gap : ℕ) : CommonCoverSolve.Geometry

Geometry, given by ActualSignedGeometry.slotGeometry sys ActualSignedGeometry.vectors_det label gap.

Equations

• NavierStokes.ActualSignedPhysicalData.geometry sys label gap = NavierStokes.ActualSignedGeometry.slotGeometry sys NavierStokes.ActualSignedGeometry.vectors_det label gap

noncomputable def NavierStokes.ActualSignedPhysicalData.center {h : ℝ} (label : SlotColoring.Label) (k : Frequency) : Plane

The carrier center is the midpoint of the physical slot, including this copy's own lattice translation.

Equations

• NavierStokes.ActualSignedPhysicalData.center label k = NavierStokes.PartitionedCovariance.slotCenter h label + NavierStokes.TorusAverages.latticePoint k

theorem NavierStokes.ActualSignedPhysicalData.center_eq_anchor {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (label : SlotColoring.Label) (gap : ℕ) (k : Frequency) : center label k = PhysicalCopyBounds.nativeCenter (geometry sys label gap) k + sys.radius • ActualSignedGeometry.temporalVector

theorem NavierStokes.ActualSignedPhysicalData.eta_basis {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (label : SlotColoring.Label) (gap : ℕ) (z : Plane) : PhysicalGraphBounds.etaCoordinate ((geometry sys label gap).basis z) = ChartScales.timeCoefficient h label.1 * z.2

theorem NavierStokes.ActualSignedPhysicalData.eta_offset {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (label : SlotColoring.Label) (gap : ℕ) (k : Frequency) (Y : Plane) : PhysicalGraphBounds.etaCoordinate ((CommonCoverSolve.coverPower gap) Y - center label k) = ChartScales.timeCoefficient h label.1 * ((geometry sys label gap).coordinates k Y).2 - sys.radius

theorem NavierStokes.ActualSignedPhysicalData.clock_eq_native {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (label : SlotColoring.Label) (gap : ℕ) (k : Frequency) (Y : Plane) : (PhysicalGraphBounds.etaCoordinate ((CommonCoverSolve.coverPower gap) Y - center label k) + sys.radius) / ChartScales.timeCoefficient h label.1 = ((geometry sys label gap).coordinates k Y).2

The physical + radius convention recovers the native clock exactly; using the lower endpoint as carrier center would count this shift twice.

theorem NavierStokes.ActualSignedPhysicalData.width_on_core {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (label : SlotColoring.Label) (gap : ℕ) (k : Frequency) (Y : Plane) (hy : (geometry sys label gap).coordinates k Y ∈ (ActualSignedGeometry.clockWindow sys label.1).core) : |PhysicalGraphBounds.etaCoordinate ((CommonCoverSolve.coverPower gap) Y - center label k)| ≤ sys.radius

noncomputable def NavierStokes.ActualSignedPhysicalData.nativeMask {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (label : SlotColoring.Label) (z : Plane) : ℝ

Native mask, given by PartitionedCovariance.cutoff sys.radius z.1 * PrimaryCopyBounds.outerCutoff (z.2 / ChartScales.slotLength sys.radius h label.1).

Equations

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

theorem NavierStokes.ActualSignedPhysicalData.nativeMask_smooth {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (label : SlotColoring.Label) : ContDiff ℝ (↑⊤) (nativeMask sys label)

theorem NavierStokes.ActualSignedPhysicalData.nativeMask_support {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (label : SlotColoring.Label) : Function.support (nativeMask sys label) ⊆ (ActualSignedGeometry.clockWindow sys label.1).core

noncomputable def NavierStokes.ActualSignedPhysicalData.layout {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) (label : SlotColoring.Label) (hl : 4 ≤ label.1) (gap : ℕ) : ActualPeriodizedSignedRealization.Layout

The concrete compact native layout used to periodize the same signed reference. Its geometry is the existing selected slot geometry.

Equations

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

noncomputable def NavierStokes.ActualSignedPhysicalData.carrier {h : ℝ} (label : SlotColoring.Label) (k : Frequency) (p pz x0 : ℝ) (F G : PhysicalGraphBounds.Slow → ℝ) : PhysicalWaveSum.CarrierData

The actual native carrier, retaining the individual lattice midpoint.

Equations

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

noncomputable def NavierStokes.ActualSignedPhysicalData.cylinderAt (a : ℝ) (chart : PolarCharts.Index) (x : LiftPoint) : Cylinder

Polar coordinates are used only as a chart for the actual Cartesian lift; the free torus coordinate remains unchanged.

Equations

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

theorem NavierStokes.ActualSignedPhysicalData.slotMap_eq_native {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (label : SlotColoring.Label) (gap : ℕ) (k : Frequency) (a : ℝ) (chart : PolarCharts.Index) (x : LiftPoint) : PhysicalGraphBounds.slotMap (PolarCharts.chart a chart) (ChartScales.timeCoefficient h label.1) (center label k) sys.radius ((PhysicalWaveSum.upLift gap) x) = ActualSignedGeometry.slotCoordinates (geometry sys label gap) k (cylinderAt a chart x)

theorem NavierStokes.ActualSignedPhysicalData.carrier_phase_eq_native {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (label : SlotColoring.Label) (gap : ℕ) (k : Frequency) (p pz x0 : ℝ) (F G : PhysicalGraphBounds.Slow → ℝ) (a : ℝ) (chart : PolarCharts.Index) (x : LiftPoint) : ((carrier label k p pz x0 F G).withChart chart).phase a h label.1 sys.radius ((PhysicalWaveSum.upLift gap) x) = PhaseCalculus.phase (ChartScales.epsilon h label.1) p pz x0 F G (ActualSignedGeometry.slotCoordinates (geometry sys label gap) k (cylinderAt a chart x))

noncomputable def NavierStokes.ActualSignedPhysicalData.dynamicCoefficients {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) (label : SlotColoring.Label) (hl : 4 ≤ label.1) (gap : ℕ) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) {reference : ℕ} (V : B.Views reference) (request : ℕ → Cylinder → Vec2) (j : Fin 2) (k : Frequency) : LinearWaveBounds.WaveCoefficients Cylinder

Dynamic coefficients, constructed using ActualPeriodizedSignedRealization.coefficientsWith.

Equations

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

noncomputable def NavierStokes.ActualSignedPhysicalData.dynamicCopyData {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) (label : SlotColoring.Label) (hl : 4 ≤ label.1) (gap : ℕ) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) {reference : ℕ} (V : B.Views reference) (request : ℕ → Cylinder → Vec2) (j : Fin 2) : PeriodizedWaveBounds.CopyData Cylinder Frequency

The raw mask carries only the slow cutoff. The transverse mask and Gaussian together form the final compact native cutoff.

Equations

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

theorem NavierStokes.ActualSignedPhysicalData.dynamic_localized_eq {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) (label : SlotColoring.Label) (hl : 4 ≤ label.1) (gap : ℕ) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) {reference : ℕ} (V : B.Views reference) (request : ℕ → Cylinder → Vec2) (j : Fin 2) (k : Frequency) : (dynamicCopyData sys hh label hl gap B V request j).localized k = (ActualPeriodizedSignedRealization.copyData B (layout sys hh label hl gap) V request j).localized k

theorem NavierStokes.ActualSignedPhysicalData.dynamic_common_eq {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) (label : SlotColoring.Label) (hl : 4 ≤ label.1) (gap : ℕ) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) {reference : ℕ} (V : B.Views reference) (request : ℕ → Cylinder → Vec2) (j : Fin 2) : (dynamicCopyData sys hh label hl gap B V request j).common = (ActualPeriodizedSignedRealization.copyData B (layout sys hh label hl gap) V request j).common

theorem NavierStokes.ActualSignedPhysicalData.dynamic_commonCorrected_eq {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) (label : SlotColoring.Label) (hl : 4 ≤ label.1) (gap : ℕ) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) {reference : ℕ} (V : B.Views reference) (request : ℕ → Cylinder → Vec2) (j : Fin 2) : (dynamicCopyData sys hh label hl gap B V request j).commonCorrected V.strip V.directions = (ActualPeriodizedSignedRealization.views B (layout sys hh label hl gap) V).exactCoefficients request j

Literal physical copies of the same signed reference data

structure NavierStokes.ActualSignedPhysicalData.NativeLabel (active : Set PhysicalWaveSum.BandLabel) : Type

An actual active label, retaining the native slot label and its band bound without selecting data for omitted labels.

• val : SlotColoring.Label

  Val of NativeLabel, of type SlotColoring.Label.

• property : 4 ≤ self.val.1
• mem : ⟨self.val, ⋯⟩ ∈ active

@[instance_reducible]

instance NavierStokes.ActualSignedPhysicalData.instCoeOutNativeLabelBandLabel {active : Set PhysicalWaveSum.BandLabel} : CoeOut (NativeLabel active) PhysicalWaveSum.BandLabel

Equations

• NavierStokes.ActualSignedPhysicalData.instCoeOutNativeLabelBandLabel = { coe := fun (L : NavierStokes.ActualSignedPhysicalData.NativeLabel active) => ⟨L.val, ⋯⟩ }

structure NavierStokes.ActualSignedPhysicalData.SignedFamily (U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow) : Type

The same primary/view/state triple is stored only for actual active labels. Omitted physical labels will be exactly zero.

• active : Set PhysicalWaveSum.BandLabel

  Active of SignedFamily, of type Set PhysicalWaveSum.BandLabel.

• primary : NativeLabel self.active → PhysicalSignedWave.PrimaryData U

  Primary of SignedFamily, of type NativeLabel active → PhysicalSignedWave.PrimaryData U.

• view (L : NativeLabel self.active) : (self.primary L).Views L.val.1

  View of SignedFamily, of type (L : NativeLabel active) → (primary L).Views L.val.1.

• state (L : NativeLabel self.active) : (self.view L).StateData

  State of SignedFamily, of type (L : NativeLabel active) → (view L).StateData.

• column : NativeLabel self.active → Fin 2

  Column of SignedFamily, of type NativeLabel active → Fin 2.

noncomputable def NavierStokes.ActualSignedPhysicalData.positiveIndex (L : PhysicalWaveSum.BandLabel) : PhysicalWaveSum.WaveIndex 1

Positive index, given by (L, ⟨1, by decide⟩).

Equations

• NavierStokes.ActualSignedPhysicalData.positiveIndex L = (L, ⟨1, NavierStokes.ActualSignedPhysicalData.positiveIndex._proof_1⟩)

noncomputable def NavierStokes.ActualSignedPhysicalData.cylinderZero (x : LiftPoint) : Cylinder

Cylinder zero, given by ((PolarCharts.radius (PhysicalGraphBounds.liftXY x), (PhysicalGraphBounds.liftZT x, x.2)), 0).

Equations

• NavierStokes.ActualSignedPhysicalData.cylinderZero x = ((NavierStokes.PolarCharts.radius (NavierStokes.PhysicalGraphBounds.liftXY x), NavierStokes.PhysicalGraphBounds.liftZT x, x.2), 0)

noncomputable def NavierStokes.ActualSignedPhysicalData.rotateCoefficient (Y : Plane) (v : HarmonicCalculus.ComplexVector) : HarmonicCalculus.ComplexVector

Rotation into Cartesian components using the actual Cartesian coordinates. No choice of angular branch appears in the amplitude.

Equations

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

theorem NavierStokes.ActualSignedPhysicalData.rotateCoefficient_zero (Y : Plane) : rotateCoefficient Y 0 = 0

noncomputable def NavierStokes.ActualSignedPhysicalData.rotationMap (Y : Plane) : HarmonicCalculus.ComplexVector →L[ℝ] HarmonicCalculus.ComplexVector

Rotation map, constructed using ContinuousLinearMap.pi.

Equations

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

theorem NavierStokes.ActualSignedPhysicalData.rotationMap_apply (Y : Plane) (v : HarmonicCalculus.ComplexVector) : (rotationMap Y) v = rotateCoefficient Y v

theorem NavierStokes.ActualSignedPhysicalData.rotateCoefficient_real_smul (Y : Plane) (c : ℝ) (v : HarmonicCalculus.ComplexVector) : rotateCoefficient Y (c • v) = c • rotateCoefficient Y v

theorem NavierStokes.ActualSignedPhysicalData.rotateCoefficient_complex_smul (Y : Plane) (c : ℂ) (v : HarmonicCalculus.ComplexVector) : rotateCoefficient Y (c • v) = c • rotateCoefficient Y v

theorem NavierStokes.ActualSignedPhysicalData.rotateCoefficient_vectorMode (Y : Plane) (K : ℝ) (Phi : Cylinder → ℝ) (v : Cylinder → HarmonicCalculus.ComplexVector) (x : Cylinder) (i : Fin 3) : rotateCoefficient Y (HarmonicCalculus.vectorMode K Phi v x) i = rotateCoefficient Y (v x) i * HarmonicCalculus.carrier K Phi x

theorem NavierStokes.ActualSignedPhysicalData.chart_radius {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) {Y : Plane} (hY : Y ∈ PolarCharts.chartDomain a j) : (PolarCharts.chart a j Y).1 = PolarCharts.radius Y

theorem NavierStokes.ActualSignedPhysicalData.chart_radius_pos {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) {Y : Plane} (hY : Y ∈ PolarCharts.chartDomain a j) : 0 < PolarCharts.radius Y

theorem NavierStokes.ActualSignedPhysicalData.rotateCoefficient_chart_re {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) {Y : Plane} (hY : Y ∈ PolarCharts.chartDomain a j) (v : HarmonicCalculus.ComplexVector) (i : Fin 3) : (rotateCoefficient Y v i).re = ((CylindricalResidual.frame (PolarCharts.chart a j Y).2) (PhysicalCurlCovariance.realVector v)).ofLp i

theorem NavierStokes.ActualSignedPhysicalData.cylinderAt_fst {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) {x : LiftPoint} (hx : PhysicalGraphBounds.liftXY x ∈ PolarCharts.chartDomain a j) : (cylinderAt a j x).1 = (cylinderZero x).1

theorem NavierStokes.ActualSignedPhysicalData.radiusPower_eq_radius (d : ℝ) (Y : Plane) : PhysicalGraphBounds.radiusPower d Y = PolarCharts.radius Y ^ d

theorem NavierStokes.ActualSignedPhysicalData.scaledRadial_forward (n : ℕ) (z : ProblemStatement.SpaceTime) : (PhysicalGraphBounds.scaledRadial n) (z.1, CylindricalResidual.chart z.2) = PolarCharts.polar (ChartScales.Q n ^ (-(1 / 2)) * z.2.ofLp 0, z.2.ofLp 1)

theorem NavierStokes.ActualSignedPhysicalData.cylinderAt_physical_forward (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) : cylinderAt a j (PhysicalGraphBounds.physicalLift h n (z.1, CylindricalResidual.chart z.2)) = (PhysicalResidualBridge.commonGraph (ChartScales.Q n) h (ChartScales.nativeIndex h n)).map z

The exact physical Cartesian lift and the common cylindrical graph have identical coordinates; in particular no fast variable is discarded.

noncomputable def NavierStokes.ActualSignedPhysicalData.waveMask {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (label : SlotColoring.Label) (z : Plane) : ℝ

Wave mask, given by PartitionedCovariance.cutoff sys.radius z.1 * GaussianTailFlat.profile (z.2 / ChartScales.slotLength sys.radius h label.1).

Equations

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

theorem NavierStokes.ActualSignedPhysicalData.waveMask_eq_compact {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (label : SlotColoring.Label) (z : Plane) : waveMask sys label z = nativeMask sys label z * GaussianTailFlat.profile (z.2 / ChartScales.slotLength sys.radius h label.1)

theorem NavierStokes.ActualSignedPhysicalData.waveMask_support {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (label : SlotColoring.Label) : Function.support (waveMask sys label) ⊆ (ActualSignedGeometry.clockWindow sys label.1).core

noncomputable def NavierStokes.ActualSignedPhysicalData.selectedCarrier {h : ℝ} {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) (L : NativeLabel f.active) (k : Frequency) : PhysicalWaveSum.CarrierData

Selected carrier, constructed using carrier.

Equations

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

noncomputable def NavierStokes.ActualSignedPhysicalData.extendedCarrier {h : ℝ} {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) (L : PhysicalWaveSum.BandLabel) (k : Frequency) : PhysicalWaveSum.CarrierData

Extended carrier, with branches according to hL : L ∈ f.active.

Equations

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

theorem NavierStokes.ActualSignedPhysicalData.extendedCarrier_active {h : ℝ} {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) (L : NativeLabel f.active) (k : Frequency) : extendedCarrier f ⟨L.val, ⋯⟩ k = selectedCarrier f L k

theorem NavierStokes.ActualSignedPhysicalData.extendedCarrier_center {h : ℝ} {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) (L : PhysicalWaveSum.BandLabel) (k : Frequency) : (extendedCarrier f L k).center = center (↑L) k

noncomputable def NavierStokes.ActualSignedPhysicalData.rawSignedAmplitude {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) (L : NativeLabel f.active) (k : Frequency) (x : Cylinder) : HarmonicCalculus.ComplexVector

Raw signed amplitude, constructed using ActualPeriodizedSignedRealization.referenceScalar.

Equations

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

noncomputable def NavierStokes.ActualSignedPhysicalData.rawPotential {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) (L : NativeLabel f.active) (k : Frequency) (x : Cylinder) : HarmonicCalculus.ComplexVector

Raw potential, constructed using CurlClassBounds.inverseCarrier.

Equations

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

noncomputable def NavierStokes.ActualSignedPhysicalData.rawPressure {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) (L : NativeLabel f.active) (k : Frequency) (x : Cylinder) : ℂ

Raw pressure, constructed using ActualPeriodizedSignedRealization.referenceScalar.

Equations

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

noncomputable def NavierStokes.ActualSignedPhysicalData.potentialFamily {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) (i : Fin 3) : PhysicalCopyBounds.CopyFamily 1 Frequency

One positive harmonic suffices because the physical field takes the real part. Its native copies retain their individual centers and phases.

Equations

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

noncomputable def NavierStokes.ActualSignedPhysicalData.pressureFamily {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) : PhysicalCopyBounds.CopyFamily 1 Frequency

Pressure family, bundling gap, carrier, amplitude.

Equations

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

theorem NavierStokes.ActualSignedPhysicalData.potential_term_active {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) (L : NativeLabel f.active) (k : Frequency) (i : Fin 3) (a : ℝ) (w : ProblemStatement.SpaceTime) : (potentialFamily sys hh f i).term a h sys.radius (positiveIndex ⟨L.val, ⋯⟩) k w = PhysicalWaveSum.globalWave a h L.val.1 0 sys.radius (selectedCarrier f L k) ((potentialFamily sys hh f i).amplitude k (positiveIndex ⟨L.val, ⋯⟩)) 1 w

theorem NavierStokes.ActualSignedPhysicalData.pressure_term_active {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) (L : NativeLabel f.active) (k : Frequency) (a : ℝ) (w : ProblemStatement.SpaceTime) : (pressureFamily sys hh f).term a h sys.radius (positiveIndex ⟨L.val, ⋯⟩) k w = PhysicalWaveSum.globalWave a h L.val.1 0 sys.radius (selectedCarrier f L k) ((pressureFamily sys hh f).amplitude k (positiveIndex ⟨L.val, ⋯⟩)) 1 w

theorem NavierStokes.ActualSignedPhysicalData.potential_amplitude_mem {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) (i : Fin 3) (k : Frequency) (I : PhysicalWaveSum.WaveIndex 1) (x : LiftPoint) (hx : (potentialFamily sys hh f i).amplitude k I x ≠ 0) : (geometry sys (↑I.1) 0).coordinates k x.2 ∈ (ActualSignedGeometry.clockWindow sys (↑I.1).1).core

theorem NavierStokes.ActualSignedPhysicalData.pressure_amplitude_mem {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) (k : Frequency) (I : PhysicalWaveSum.WaveIndex 1) (x : LiftPoint) (hx : (pressureFamily sys hh f).amplitude k I x ≠ 0) : (geometry sys (↑I.1) 0).coordinates k x.2 ∈ (ActualSignedGeometry.clockWindow sys (↑I.1).1).core

noncomputable def NavierStokes.ActualSignedPhysicalData.potentialCells {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) (i : Fin 3) : PhysicalCopyBounds.SupportCells (potentialFamily sys hh f i)

Potential cells, constructed using PhysicalCopyBounds.nativeSupportCells.

Equations

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

noncomputable def NavierStokes.ActualSignedPhysicalData.pressureCells {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) : PhysicalCopyBounds.SupportCells (pressureFamily sys hh f)

Pressure cells, constructed using PhysicalCopyBounds.nativeSupportCells.

Equations

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

theorem NavierStokes.ActualSignedPhysicalData.waveMask_summable_smul {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (L : PhysicalWaveSum.BandLabel) (Y : Plane) (v : Frequency → E) : Summable fun (k : TorusInverse.Frequency) => waveMask sys (↑L) ((geometry sys (↑L) 0).coordinates k Y) • v k

Finite native support justifies applying any linear potential operation before or after the copy sum.

theorem NavierStokes.ActualSignedPhysicalData.signed_raw_eq_sum {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) (L : NativeLabel f.active) (x : Cylinder) : (ActualPeriodizedSignedRealization.periodizedPrimary (f.primary L) (layout sys hh L.val ⋯ 0)).raw (f.state L).referenceRequest (f.column L) L.val.1 x = ∑' (k : TorusInverse.Frequency), waveMask sys L.val ((geometry sys L.val 0).coordinates k x.1.2.2) • rawSignedAmplitude sys hh f L k x

noncomputable def NavierStokes.ActualSignedPhysicalData.potentialMap (K : ℝ) (N : ProblemStatement.Space) : HarmonicCalculus.ComplexVector →L[ℝ] HarmonicCalculus.ComplexVector

Potential map, given by CurlClassBounds.inverseCarrier K • ((‖N‖ ^ 2)⁻¹ • CurlClassBounds.complexCrossLinear (CurlClassBounds.complexify N)).

Equations

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

theorem NavierStokes.ActualSignedPhysicalData.potentialMap_apply (K : ℝ) (N : ProblemStatement.Space) (v : HarmonicCalculus.ComplexVector) : (potentialMap K N) v = CurlClassBounds.inverseCarrier K • CurlClassBounds.normalCoefficient N v

theorem NavierStokes.ActualSignedPhysicalData.signed_potential_eq_sum {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) (L : NativeLabel f.active) (x : Cylinder) : CurlClassBounds.inverseCarrier ((f.primary L).base.frequency L.val.1) • CurlClassBounds.normalCoefficient ((f.primary L).base.normal (f.primary L).strip (f.primary L).directions L.val.1 x) ((ActualPeriodizedSignedRealization.periodizedPrimary (f.primary L) (layout sys hh L.val ⋯ 0)).raw (f.state L).referenceRequest (f.column L) L.val.1 x) = ∑' (k : TorusInverse.Frequency), waveMask sys L.val ((geometry sys L.val 0).coordinates k x.1.2.2) • rawPotential sys hh f L k x

theorem NavierStokes.ActualSignedPhysicalData.signed_pressure_eq_sum {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) (L : NativeLabel f.active) (x : Cylinder) : (ActualPeriodizedSignedRealization.periodizedPrimary (f.primary L) (layout sys hh L.val ⋯ 0)).rawPressure (f.state L).referenceRequest (f.column L) L.val.1 x = ∑' (k : TorusInverse.Frequency), waveMask sys L.val ((geometry sys L.val 0).coordinates k x.1.2.2) • rawPressure sys hh f L k x

structure NavierStokes.ActualSignedPhysicalData.ReferenceGeometry {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) : Type

Primitive reference identities. The selected phase is the actual periodic clock phase; all geometric and angular statements concern the uncorrected inputs, never the output potential or velocity.

• frequency (L : NativeLabel f.active) : (f.primary L).base.frequency L.val.1 = ↑(ChartScales.carrier h L.val.1)
• phase (L : NativeLabel f.active) : (f.primary L).base.phase L.val.1 = ActualSignedGeometry.periodicPhase sys L.val 0 (ChartScales.epsilon h L.val.1) (((f.primary L).pulse (f.column L)).phase.p L.val.1) (((f.primary L).pulse (f.column L)).phase.pz L.val.1) (((f.primary L).pulse (f.column L)).phase.x0 L.val.1) (((f.primary L).pulse (f.column L)).phase.F L.val.1) (((f.primary L).pulse (f.column L)).phase.G L.val.1)
• angular (L : NativeLabel f.active) : (f.primary L).Angular (f.state L).referenceRequest L.val.1

  Angular of ReferenceGeometry, of type ∀ L, (f.primary L).Angular (f.state L).referenceRequest L.val.1.

• chart (L : NativeLabel f.active) : PhysicalSignedWave.ChartGeometry (f.primary L).base (f.primary L).strip (f.primary L).directions L.val.1 h (ChartScales.Q L.val.1) (ChartScales.nativeIndex h L.val.1)
• exponent (L : NativeLabel f.active) : (f.view L).exponent = h
• scale (L : NativeLabel f.active) : (f.view L).referenceScale = ChartScales.Q L.val.1
• cover (L : NativeLabel f.active) : (f.view L).referenceCover = ChartScales.nativeIndex h L.val.1

theorem NavierStokes.ActualSignedPhysicalData.rawSignedAmplitude_invariant {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) (G : ReferenceGeometry sys f) (L : NativeLabel f.active) (k : Frequency) : CopyAngularInvariance.Invariant (0, 1) (rawSignedAmplitude sys hh f L k)

theorem NavierStokes.ActualSignedPhysicalData.rawPotential_invariant {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) (G : ReferenceGeometry sys f) (L : NativeLabel f.active) (k : Frequency) : CopyAngularInvariance.Invariant (0, 1) (rawPotential sys hh f L k)

theorem NavierStokes.ActualSignedPhysicalData.rawPressure_invariant {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) (G : ReferenceGeometry sys f) (L : NativeLabel f.active) (k : Frequency) : CopyAngularInvariance.Invariant (0, 1) (rawPressure sys hh f L k)

theorem NavierStokes.ActualSignedPhysicalData.invariant_angle_zero {E : Type} (F : Cylinder → E) (hF : CopyAngularInvariance.Invariant (0, 1) F) (x : Cylinder) : F x = F (x.1, 0)

theorem NavierStokes.ActualSignedPhysicalData.phase_eq_native {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) (G : ReferenceGeometry sys f) (L : NativeLabel f.active) (k : Frequency) (a : ℝ) (chart : PolarCharts.Index) (x : LiftPoint) (hx : (geometry sys L.val 0).coordinates k x.2 ∈ (ActualSignedGeometry.clockWindow sys L.val.1).core) : (f.primary L).base.phase L.val.1 (cylinderAt a chart x) = ((selectedCarrier f L k).withChart chart).phase a h L.val.1 sys.radius x

theorem NavierStokes.ActualSignedPhysicalData.commonLift_zero (h : ℝ) (n : ℕ) (w : ProblemStatement.SpaceTime) : PhysicalWaveSum.commonLift h n 0 w = PhysicalGraphBounds.physicalLift h n w

theorem NavierStokes.ActualSignedPhysicalData.rawPotential_cylinderAt {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) (G : ReferenceGeometry sys f) (L : NativeLabel f.active) (k : Frequency) {a : ℝ} (ha : 0 < a) (chart : PolarCharts.Index) {x : LiftPoint} (hx : PhysicalGraphBounds.liftXY x ∈ PolarCharts.chartDomain a chart) : rawPotential sys hh f L k (cylinderAt a chart x) = rawPotential sys hh f L k (cylinderZero x)

theorem NavierStokes.ActualSignedPhysicalData.rawPressure_cylinderAt {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) (G : ReferenceGeometry sys f) (L : NativeLabel f.active) (k : Frequency) {a : ℝ} (ha : 0 < a) (chart : PolarCharts.Index) {x : LiftPoint} (hx : PhysicalGraphBounds.liftXY x ∈ PolarCharts.chartDomain a chart) : rawPressure sys hh f L k (cylinderAt a chart x) = rawPressure sys hh f L k (cylinderZero x)

theorem NavierStokes.ActualSignedPhysicalData.pressure_commonWave {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) (G : ReferenceGeometry sys f) (L : NativeLabel f.active) (k : Frequency) {a : ℝ} (ha : 0 < a) (chart : PolarCharts.Index) (w : ProblemStatement.SpaceTime) (hchart : (PhysicalGraphBounds.scaledRadial L.val.1) w ∈ PolarCharts.chartDomain a chart) : PhysicalWaveSum.commonWave a h L.val.1 0 sys.radius ((selectedCarrier f L k).withChart chart) ((pressureFamily sys hh f).amplitude k (positiveIndex ⟨L.val, ⋯⟩)) 1 w = ChartScales.Q L.val.1 ^ (-(2 * CoordinateAlgebra.A h)) • waveMask sys L.val ((geometry sys L.val 0).coordinates k (PhysicalGraphBounds.physicalLift h L.val.1 w).2) • rawPressure sys hh f L k (cylinderAt a chart (PhysicalGraphBounds.physicalLift h L.val.1 w)) * HarmonicCalculus.carrier ((f.primary L).base.frequency L.val.1) ((f.primary L).base.phase L.val.1) (cylinderAt a chart (PhysicalGraphBounds.physicalLift h L.val.1 w))

The local oscillatory pressure is the native pressure with its actual copy phase. Equality with the common periodic phase is used only where this copy's cutoff is nonzero.

theorem NavierStokes.ActualSignedPhysicalData.pressure_periodized {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) (G : ReferenceGeometry sys f) (L : NativeLabel f.active) {a b : ℝ} (ha : 0 < a) (w : ProblemStatement.SpaceTime) (hw : (PhysicalGraphBounds.scaledRadial L.val.1) w ∈ PhysicalGraphBounds.annulus a b) : (pressureFamily sys hh f).periodized a h sys.radius (positiveIndex ⟨L.val, ⋯⟩) w = ChartScales.Q L.val.1 ^ (-(2 * CoordinateAlgebra.A h)) • HarmonicCalculus.mode ((f.primary L).base.frequency L.val.1) ((f.primary L).base.phase L.val.1) ((ActualPeriodizedSignedRealization.periodizedPrimary (f.primary L) (layout sys hh L.val ⋯ 0)).rawPressure (f.state L).referenceRequest (f.column L) L.val.1) (cylinderAt a (PhysicalWaveSum.chooseChart a ((PhysicalGraphBounds.scaledRadial L.val.1) w)) (PhysicalGraphBounds.physicalLift h L.val.1 w))

The complete copy sum is exactly the same reference pressure mode.

theorem NavierStokes.ActualSignedPhysicalData.potential_commonWave {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) (G : ReferenceGeometry sys f) (L : NativeLabel f.active) (k : Frequency) (i : Fin 3) {a : ℝ} (ha : 0 < a) (chart : PolarCharts.Index) (w : ProblemStatement.SpaceTime) (hchart : (PhysicalGraphBounds.scaledRadial L.val.1) w ∈ PolarCharts.chartDomain a chart) : PhysicalWaveSum.commonWave a h L.val.1 0 sys.radius ((selectedCarrier f L k).withChart chart) ((potentialFamily sys hh f i).amplitude k (positiveIndex ⟨L.val, ⋯⟩)) 1 w = ChartScales.Q L.val.1 ^ (-h) • waveMask sys L.val ((geometry sys L.val 0).coordinates k (PhysicalGraphBounds.physicalLift h L.val.1 w).2) • rotateCoefficient (PhysicalGraphBounds.liftXY (PhysicalGraphBounds.physicalLift h L.val.1 w)) (rawPotential sys hh f L k (cylinderAt a chart (PhysicalGraphBounds.physicalLift h L.val.1 w))) i * HarmonicCalculus.carrier ((f.primary L).base.frequency L.val.1) ((f.primary L).base.phase L.val.1) (cylinderAt a chart (PhysicalGraphBounds.physicalLift h L.val.1 w))

noncomputable def NavierStokes.ActualSignedPhysicalData.referencePotentialCoefficient {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) (L : NativeLabel f.active) (x : Cylinder) : HarmonicCalculus.ComplexVector

Reference potential coefficient, constructed using CurlClassBounds.inverseCarrier.

Equations

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

theorem NavierStokes.ActualSignedPhysicalData.rotatedPotential_sum {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) (L : NativeLabel f.active) (x : Cylinder) (Y : Plane) (i : Fin 3) : ∑' (k : TorusInverse.Frequency), waveMask sys L.val ((geometry sys L.val 0).coordinates k x.1.2.2) • rotateCoefficient Y (rawPotential sys hh f L k x) i = rotateCoefficient Y (referencePotentialCoefficient sys hh f L x) i

theorem NavierStokes.ActualSignedPhysicalData.potential_periodized {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) (G : ReferenceGeometry sys f) (L : NativeLabel f.active) (i : Fin 3) {a b : ℝ} (ha : 0 < a) (w : ProblemStatement.SpaceTime) (hw : (PhysicalGraphBounds.scaledRadial L.val.1) w ∈ PhysicalGraphBounds.annulus a b) : (potentialFamily sys hh f i).periodized a h sys.radius (positiveIndex ⟨L.val, ⋯⟩) w = ChartScales.Q L.val.1 ^ (-h) • (rotateCoefficient (PhysicalGraphBounds.liftXY (PhysicalGraphBounds.physicalLift h L.val.1 w)) (referencePotentialCoefficient sys hh f L (cylinderAt a (PhysicalWaveSum.chooseChart a ((PhysicalGraphBounds.scaledRadial L.val.1) w)) (PhysicalGraphBounds.physicalLift h L.val.1 w))) i * HarmonicCalculus.carrier ((f.primary L).base.frequency L.val.1) ((f.primary L).base.phase L.val.1) (cylinderAt a (PhysicalWaveSum.chooseChart a ((PhysicalGraphBounds.scaledRadial L.val.1) w)) (PhysicalGraphBounds.physicalLift h L.val.1 w)))

The complete vector-potential copy sum retains the same reference coefficient. The rotation acts on the actual sum, not a surrogate field.

theorem NavierStokes.ActualSignedPhysicalData.angular_integer {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) (G : ReferenceGeometry sys f) (L : NativeLabel f.active) (k : Frequency) : ↑(ChartScales.carrier h L.val.1) * (selectedCarrier f L k).angular = ↑(G.angular L).mode

theorem NavierStokes.ActualSignedPhysicalData.pressure_periodized_of_chart {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) (G : ReferenceGeometry sys f) (L : NativeLabel f.active) {a b : ℝ} (ha : 0 < a) (w : ProblemStatement.SpaceTime) (hw : (PhysicalGraphBounds.scaledRadial L.val.1) w ∈ PhysicalGraphBounds.annulus a b) (j : PolarCharts.Index) (hj : (PhysicalGraphBounds.scaledRadial L.val.1) w ∈ PolarCharts.chartDomain a j) : (pressureFamily sys hh f).periodized a h sys.radius (positiveIndex ⟨L.val, ⋯⟩) w = ChartScales.Q L.val.1 ^ (-(2 * CoordinateAlgebra.A h)) • HarmonicCalculus.mode ((f.primary L).base.frequency L.val.1) ((f.primary L).base.phase L.val.1) ((ActualPeriodizedSignedRealization.periodizedPrimary (f.primary L) (layout sys hh L.val ⋯ 0)).rawPressure (f.state L).referenceRequest (f.column L) L.val.1) (cylinderAt a j (PhysicalGraphBounds.physicalLift h L.val.1 w))

theorem NavierStokes.ActualSignedPhysicalData.potential_periodized_of_chart {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) (G : ReferenceGeometry sys f) (L : NativeLabel f.active) (i : Fin 3) {a b : ℝ} (ha : 0 < a) (w : ProblemStatement.SpaceTime) (hw : (PhysicalGraphBounds.scaledRadial L.val.1) w ∈ PhysicalGraphBounds.annulus a b) (j : PolarCharts.Index) (hj : (PhysicalGraphBounds.scaledRadial L.val.1) w ∈ PolarCharts.chartDomain a j) : (potentialFamily sys hh f i).periodized a h sys.radius (positiveIndex ⟨L.val, ⋯⟩) w = ChartScales.Q L.val.1 ^ (-h) • (rotateCoefficient (PhysicalGraphBounds.liftXY (PhysicalGraphBounds.physicalLift h L.val.1 w)) (referencePotentialCoefficient sys hh f L (cylinderAt a j (PhysicalGraphBounds.physicalLift h L.val.1 w))) i * HarmonicCalculus.carrier ((f.primary L).base.frequency L.val.1) ((f.primary L).base.phase L.val.1) (cylinderAt a j (PhysicalGraphBounds.physicalLift h L.val.1 w)))

theorem NavierStokes.ActualSignedPhysicalData.pressure_periodized_physical {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) (G : ReferenceGeometry sys f) (L : NativeLabel f.active) {a b delta : ℝ} (ha : 0 < a) (hdelta : 0 < delta) (j : PolarCharts.Index) (z : ProblemStatement.SpaceTime) (hz : z ∈ PhysicalCurlCovariance.validCylindrical delta j) (hw : (PhysicalGraphBounds.scaledRadial L.val.1) (z.1, CylindricalResidual.chart z.2) ∈ PhysicalGraphBounds.annulus a b) (hj : (PhysicalGraphBounds.scaledRadial L.val.1) (z.1, CylindricalResidual.chart z.2) ∈ PolarCharts.chartDomain a j) : ((pressureFamily sys hh f).periodized a h sys.radius (positiveIndex ⟨L.val, ⋯⟩) (z.1, CylindricalResidual.chart z.2)).re = ActualPeriodizedSignedRealization.physicalPressure (f.primary L) (layout sys hh L.val ⋯ 0) (f.view L) (f.state L) (f.column L) delta (z.1, CylindricalResidual.chart z.2)

Equality with the original Cartesian signed pressure, not merely a newly defined coefficient sum.

theorem NavierStokes.ActualSignedPhysicalData.referencePotential_eq_mode {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) (G : ReferenceGeometry sys f) (L : NativeLabel f.active) (hPhi : ContDiffOn ℝ (↑⊤) ((f.primary L).base.phase L.val.1) (f.primary L).strip.domain) (z : ProblemStatement.SpaceTime) (hr : 0 < z.2.ofLp 0) (hz : (PhysicalResidualBridge.commonGraph (ChartScales.Q L.val.1) h (ChartScales.nativeIndex h L.val.1)).map z ∈ (f.primary L).strip.domain) : (ActualPeriodizedSignedRealization.views (f.primary L) (layout sys hh L.val ⋯ 0) (f.view L)).referencePotential (f.state L).referenceRequest (f.column L) z = ChartScales.Q L.val.1 ^ (-h) • HarmonicCalculus.vectorMode ((f.primary L).base.frequency L.val.1) ((f.primary L).base.phase L.val.1) (referencePotentialCoefficient sys hh f L) ((PhysicalResidualBridge.commonGraph (ChartScales.Q L.val.1) h (ChartScales.nativeIndex h L.val.1)).map z)

The original physical potential is the pulled-back native coefficient mode, with the potential scale derived by the actual curl construction.

theorem NavierStokes.ActualSignedPhysicalData.potential_periodized_physical {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) (G : ReferenceGeometry sys f) (L : NativeLabel f.active) (i : Fin 3) (hPhi : ContDiffOn ℝ (↑⊤) ((f.primary L).base.phase L.val.1) (f.primary L).strip.domain) {a b delta : ℝ} (ha : 0 < a) (hdelta : 0 < delta) (j : PolarCharts.Index) (z : ProblemStatement.SpaceTime) (hz : z ∈ PhysicalCurlCovariance.validCylindrical delta j) (hsource : (PhysicalResidualBridge.commonGraph (ChartScales.Q L.val.1) h (ChartScales.nativeIndex h L.val.1)).map z ∈ (f.primary L).strip.domain) (hw : (PhysicalGraphBounds.scaledRadial L.val.1) (z.1, CylindricalResidual.chart z.2) ∈ PhysicalGraphBounds.annulus a b) (hj : (PhysicalGraphBounds.scaledRadial L.val.1) (z.1, CylindricalResidual.chart z.2) ∈ PolarCharts.chartDomain a j) : ((potentialFamily sys hh f i).periodized a h sys.radius (positiveIndex ⟨L.val, ⋯⟩) (z.1, CylindricalResidual.chart z.2)).re = (ActualPeriodizedSignedRealization.physicalPotential (f.primary L) (layout sys hh L.val ⋯ 0) (f.view L) (f.state L) (f.column L) delta (z.1, CylindricalResidual.chart z.2)).ofLp i

Equality with the same signed Cartesian potential. Every native copy, cutoff and the potential's actual derivative normalization is retained.

Explicit native sources and their physical class adapter

@[reducible, inline]

abbrev NavierStokes.ActualSignedPhysicalData.Native : Type

Native: an abbreviation for CartesianCopySource.Native.

Equations

• NavierStokes.ActualSignedPhysicalData.Native = NavierStokes.CartesianCopySource.Native

@[reducible, inline]

abbrev NavierStokes.ActualSignedPhysicalData.SourceIndex : Type

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

Equations

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

noncomputable def NavierStokes.ActualSignedPhysicalData.nativeCylinder (y : Native) : Cylinder

Native cylinder, given by ((y.1, ((y.2.1.2, y.2.1.1), y.2.2)), 0).

Equations

• NavierStokes.ActualSignedPhysicalData.nativeCylinder y = ((y.1, (y.2.1.2, y.2.1.1), y.2.2), 0)

theorem NavierStokes.ActualSignedPhysicalData.nativeCylinder_map (x : LiftPoint) : nativeCylinder (PhysicalClassBounds.cylindricalMap x) = cylinderZero x

theorem NavierStokes.ActualSignedPhysicalData.cartesian_rotation (Y : Plane) (v : HarmonicCalculus.ComplexVector) : (CartesianCopySource.rotationMap Y) v = rotateCoefficient Y v

noncomputable def NavierStokes.ActualSignedPhysicalData.nativePotentialSource {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) (I : SourceIndex) (n : ℕ) (y : Native) : HarmonicCalculus.ComplexVector

Native potential source, with branches according to hL : I.1.1 ∈ f.active.

Equations

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

noncomputable def NavierStokes.ActualSignedPhysicalData.nativePressureSource {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) (I : SourceIndex) (n : ℕ) (y : Native) : ℂ

Native pressure source, with branches according to hL : I.1.1 ∈ f.active.

Equations

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

theorem NavierStokes.ActualSignedPhysicalData.potential_amplitude_eq_source {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) (i : Fin 3) (k : Frequency) (I : PhysicalWaveSum.WaveIndex 1) (x : LiftPoint) : (potentialFamily sys hh f i).amplitude k I x = ChartScales.Q (↑I.1).1 ^ (-h) • CartesianCopySource.rotatedSource (nativePotentialSource sys hh f) (I, k) (↑I.1).1 x i

theorem NavierStokes.ActualSignedPhysicalData.pressure_amplitude_eq_source {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) (k : Frequency) (I : PhysicalWaveSum.WaveIndex 1) (x : LiftPoint) : (pressureFamily sys hh f).amplitude k I x = ChartScales.Q (↑I.1).1 ^ (-(2 * CoordinateAlgebra.A h)) • nativePressureSource sys hh f (I, k) (↑I.1).1 (PhysicalClassBounds.cylindricalMap x)

theorem NavierStokes.ActualSignedPhysicalData.increment_zero_target (H : Mat2) (R : Vec2) (j : Fin 2) : SignedCovariance.increment H 0 R j = 0

theorem NavierStokes.ActualSignedPhysicalData.rawPotential_zero {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) (L : NativeLabel f.active) (k : Frequency) (x : Cylinder) (hx : (f.primary L).mask L.val.1 x = 0 ∨ (f.primary L).target L.val.1 x = 0) : rawPotential sys hh f L k x = 0

theorem NavierStokes.ActualSignedPhysicalData.rawPressure_zero {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) (L : NativeLabel f.active) (k : Frequency) (x : Cylinder) (hx : (f.primary L).mask L.val.1 x = 0 ∨ (f.primary L).target L.val.1 x = 0) : rawPressure sys hh f L k x = 0

theorem NavierStokes.ActualSignedPhysicalData.potential_amplitude_inputs {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) (i : Fin 3) (k : Frequency) (I : PhysicalWaveSum.WaveIndex 1) (x : LiftPoint) (hx : (potentialFamily sys hh f i).amplitude k I x ≠ 0) : ∃ (hL : I.1 ∈ f.active), ↑I.2 = 1 ∧ (f.primary { val := ↑I.1, property := ⋯, mem := hL }).mask (↑I.1).1 (cylinderZero x) ≠ 0 ∧ (f.primary { val := ↑I.1, property := ⋯, mem := hL }).target (↑I.1).1 (cylinderZero x) ≠ 0

theorem NavierStokes.ActualSignedPhysicalData.pressure_amplitude_inputs {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) (k : Frequency) (I : PhysicalWaveSum.WaveIndex 1) (x : LiftPoint) (hx : (pressureFamily sys hh f).amplitude k I x ≠ 0) : ∃ (hL : I.1 ∈ f.active), ↑I.2 = 1 ∧ (f.primary { val := ↑I.1, property := ⋯, mem := hL }).mask (↑I.1).1 (cylinderZero x) ≠ 0 ∧ (f.primary { val := ↑I.1, property := ⋯, mem := hL }).target (↑I.1).1 (cylinderZero x) ≠ 0

structure NavierStokes.ActualSignedPhysicalData.PrimitiveLocalization {h : ℝ} {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) (a b : ℝ) (s : WeightedClasses.StripData Native) : Prop

Localization facts about the original shared mask and target. The native domain condition is on every slow/fast fiber. No support statement about a corrected velocity, potential, pressure, or copy sum is assumed.

• normalized (L : NativeLabel f.active) (y : Native) : 0 ≤ y.1 → (f.primary L).mask L.val.1 (nativeCylinder y) ≠ 0 → (f.primary L).target L.val.1 (nativeCylinder y) ≠ 0 → 0 < y.2.1.1 ∧ 1 / 2 ≤ SimilarityCoordinates.coordinateQ (2 * h) y.2.1 ∧ SimilarityCoordinates.coordinateQ (2 * h) y.2.1 ≤ 2 ∧ a ≤ y.1 / √(SimilarityCoordinates.coordinateQ (2 * h) y.2.1) ∧ y.1 / √(SimilarityCoordinates.coordinateQ (2 * h) y.2.1) ≤ b
• domain (L : NativeLabel f.active) (y : Native) : 0 ≤ y.1 → (f.primary L).mask L.val.1 (nativeCylinder y) ≠ 0 → (f.primary L).target L.val.1 (nativeCylinder y) ≠ 0 → y ∈ s.domain
• mask_pullback (L : NativeLabel f.active) (w : ProblemStatement.SpaceTime) : w ∈ PhysicalWaveSum.preterminal → (f.primary L).mask L.val.1 (cylinderZero (PhysicalGraphBounds.physicalLift h L.val.1 w)) = PhysicalWaveSum.physicalMask (CoordinateAlgebra.D h) L.val (PhysicalWaveSum.physicalParams h w)

theorem NavierStokes.ActualSignedPhysicalData.normalized_slow_norm {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : Plane} (ht : 0 < p.1) (hlo : 1 / 2 ≤ SimilarityCoordinates.coordinateQ (2 * h) p) (hhi : SimilarityCoordinates.coordinateQ (2 * h) p ≤ 2) : ‖p‖ ≤ 2

theorem NavierStokes.ActualSignedPhysicalData.primitive_annulus {h : ℝ} {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) {a b : ℝ} {s : WeightedClasses.StripData Native} (hloc : PrimitiveLocalization f a b s) (hh0 : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hb : 0 < b) (L : NativeLabel f.active) (x : LiftPoint) (hm : (f.primary L).mask L.val.1 (cylinderZero x) ≠ 0) (hT : (f.primary L).target L.val.1 (cylinderZero x) ≠ 0) : PhysicalGraphBounds.liftXY x ∈ PhysicalGraphBounds.annulus (a / 4) (2 * b) ∧ ‖PhysicalGraphBounds.liftZT x‖ ≤ 2

theorem NavierStokes.ActualSignedPhysicalData.primitive_domain {h : ℝ} {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) {a b : ℝ} {s : WeightedClasses.StripData Native} (hloc : PrimitiveLocalization f a b s) (L : NativeLabel f.active) (x : LiftPoint) (hm : (f.primary L).mask L.val.1 (cylinderZero x) ≠ 0) (hT : (f.primary L).target L.val.1 (cylinderZero x) ≠ 0) : PhysicalClassBounds.cylindricalMap x ∈ s.domain

theorem NavierStokes.ActualSignedPhysicalData.potential_support {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) {a b : ℝ} {s : WeightedClasses.StripData Native} (hloc : PrimitiveLocalization f a b s) (G : ReferenceGeometry sys f) (hh0 : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hb : 0 < b) (i : Fin 3) : LocalPhysicalCopyBounds.SupportData (potentialFamily sys hh f i) (a / 4) (2 * b) h sys.radius 2 0

theorem NavierStokes.ActualSignedPhysicalData.pressure_support {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) {a b : ℝ} {s : WeightedClasses.StripData Native} (hloc : PrimitiveLocalization f a b s) (G : ReferenceGeometry sys f) (hh0 : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hb : 0 < b) : LocalPhysicalCopyBounds.SupportData (pressureFamily sys hh f) (a / 4) (2 * b) h sys.radius 2 0

noncomputable def NavierStokes.ActualSignedPhysicalData.copyPotential {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) {a b : ℝ} {s : WeightedClasses.StripData Native} (hloc : PrimitiveLocalization f a b s) (G : ReferenceGeometry sys f) (hh0 : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hb : 0 < b) : MixedAxisPreservation.CopyPotential h

The actual vector-potential sum is an axis-preserving copy potential, with the same fixed outer radius used by the physical stage estimates.

Equations

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

theorem NavierStokes.ActualSignedPhysicalData.copyPotential_field {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) {a b : ℝ} {s : WeightedClasses.StripData Native} (hloc : PrimitiveLocalization f a b s) (G : ReferenceGeometry sys f) (hh0 : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hb : 0 < b) : (copyPotential sys hh f hloc G hh0 hh1 ha hb).field = PhysicalCopyBounds.vectorSum (potentialFamily sys hh f) (a / 4) h sys.radius

A fixed native region for the selected carrier profiles

noncomputable def NavierStokes.ActualSignedPhysicalData.carrierRegion (h a b : ℝ) : Set PhysicalGraphBounds.Slow

Carrier region, given by {p | p.1 ∈ Ioo (a / 8) (4 * b + 1) ∧ (p.2.2, p.2.1) ∈ PhysicalMeanDomain.normalizedSlowDomain (2 * h) (1 / 4) 4}.

Equations

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

theorem NavierStokes.ActualSignedPhysicalData.carrierRegion_open {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (a b : ℝ) : IsOpen (carrierRegion h a b)

theorem NavierStokes.ActualSignedPhysicalData.carrierRegion_contains {h a b : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (c : PhysicalWaveSum.CarrierData) (r0 : ℝ) (L : PhysicalWaveSum.BandLabel) (w : ProblemStatement.SpaceTime) (hw : w ∈ PhysicalWaveSum.preterminal) (hregion : PhysicalWaveSum.physicalParams h w ∈ PhysicalWaveSum.labelRegion (CoordinateAlgebra.D h) ↑L) (hann : (PhysicalGraphBounds.scaledRadial (↑L).1) w ∈ PhysicalGraphBounds.annulus (a / 4) (2 * b)) (j : PolarCharts.Index) (hj : (PhysicalGraphBounds.scaledRadial (↑L).1) w ∈ PolarCharts.chartDomain (a / 4) j) : LocalPhysicalCopyBounds.slotSlow (c.withChart j) (a / 4) h (↑L).1 r0 w ∈ carrierRegion h a b

Carrier profile arguments lie in a fixed open native region. The native phase center affects the clock, but not this slow argument.

theorem NavierStokes.ActualSignedPhysicalData.term_tsupport_labelRegion {H : ℕ} {K : Type u_1} {f : PhysicalCopyBounds.CopyFamily H K} {a b h r0 Z : ℝ} {gap : ℕ} (hr : LocalPhysicalCopyBounds.SupportData f a b h r0 Z gap) (hh : 0 < h) (hh1 : h < 1 / 2) (I : PhysicalWaveSum.WaveIndex H) (k : K) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (ht : w ∈ tsupport (f.term a h r0 I k)) : PhysicalWaveSum.physicalParams h w ∈ PhysicalWaveSum.labelRegion (CoordinateAlgebra.D h) ↑I.1

Support of one full native carrier implies closed label membership, including the edge of the actual zero-extended coefficient.

noncomputable def NavierStokes.ActualSignedPhysicalData.nativeSlow (y : Native) : PhysicalGraphBounds.Slow

Native slow, given by (y.1, (y.2.1.2, y.2.1.1)).

Equations

• NavierStokes.ActualSignedPhysicalData.nativeSlow y = (y.1, y.2.1.2, y.2.1.1)

theorem NavierStokes.ActualSignedPhysicalData.slotSlow_eq_nativeSlow {a : ℝ} (ha : 0 < a) (c : PhysicalWaveSum.CarrierData) (h : ℝ) (n : ℕ) (r0 : ℝ) (j : PolarCharts.Index) (w : ProblemStatement.SpaceTime) (hj : (PhysicalGraphBounds.scaledRadial n) w ∈ PolarCharts.chartDomain a j) : LocalPhysicalCopyBounds.slotSlow (c.withChart j) a h n r0 w = nativeSlow (PhysicalMeanJetBounds.graph h n 0 w)

noncomputable def NavierStokes.ActualSignedPhysicalData.nativePast : Set Native

Native past, given by {y | 0 < y.2.1.1}.

Equations

• NavierStokes.ActualSignedPhysicalData.nativePast = {y : NavierStokes.ActualSignedPhysicalData.Native | 0 < y.2.1.1}

theorem NavierStokes.ActualSignedPhysicalData.nativePast_open : IsOpen nativePast

noncomputable def NavierStokes.ActualSignedPhysicalData.restrictCells {E : Type u_1} {K : Type u_2} [TopologicalSpace E] (c : PeriodizedWaveBounds.Cells E K) (s : Set E) (hs : IsClosed s) : PeriodizedWaveBounds.Cells E K

Intersecting native cells with one closed slow support retains their actual local finiteness and their disjointness.

Equations

• NavierStokes.ActualSignedPhysicalData.restrictCells c s hs = { carrier := fun (n : ℕ) (k : K) => c.carrier n k ∩ s, closed := ⋯, locallyFinite := ⋯, unique := ⋯ }

noncomputable def NavierStokes.ActualSignedPhysicalData.primitiveCore {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) (L : PhysicalWaveSum.BandLabel) : Set LiftPoint

Primitive core as an element of Set LiftPoint.

Equations

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

noncomputable def NavierStokes.ActualSignedPhysicalData.localizedPotentialCells {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) (i : Fin 3) : PhysicalCopyBounds.SupportCells (potentialFamily sys hh f i)

The native cell is narrowed only by the support of the original mask and target. This avoids asking for phase estimates outside their Prepared region and does not change any coefficient.

Equations

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

noncomputable def NavierStokes.ActualSignedPhysicalData.localizedPressureCells {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) : PhysicalCopyBounds.SupportCells (pressureFamily sys hh f)

Localized pressure cells, bundling cells, support, obtain.

Equations

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

structure NavierStokes.ActualSignedPhysicalData.NativeProfiles {h : ℝ} {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) : Type

The same selected profile functions on their genuine Prepared native regions. Only the slow coordinate cover and native polynomial jets are stored; no physical bound or carrier representation is an input.

• region : PhysicalWaveSum.BandLabel → Set PhysicalGraphBounds.Slow

  Region of NativeProfiles, of type PhysicalWaveSum.BandLabel → Set PhysicalGraphBounds.Slow.

• region_open (L : PhysicalWaveSum.BandLabel) : IsOpen (self.region L)
• jets : PhaseJetBounds.PolynomialJets (PhysicalCopyBounds.copyBandDomain (fun (x : Frequency) (L : PhysicalWaveSum.BandLabel) => self.region L) ⋯) fun (I : Frequency × PhysicalWaveSum.BandLabel) (p : PhysicalGraphBounds.Slow) => ((extendedCarrier f I.2 I.1).F p, (extendedCarrier f I.2 I.1).G p)
• covers (L : PhysicalWaveSum.BandLabel) (w : ProblemStatement.SpaceTime) : w ∈ PhysicalWaveSum.preterminal → PhysicalWaveSum.physicalParams h w ∈ PhysicalWaveSum.labelRegion (CoordinateAlgebra.D h) ↑L → PhysicalGraphBounds.physicalLift h (↑L).1 w ∈ closure (primitiveCore f L) → nativeSlow (PhysicalMeanJetBounds.graph h (↑L).1 0 w) ∈ self.region L

structure NavierStokes.ActualSignedPhysicalData.NativeRegular {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) : Prop

Qualitative regularity of the literal native cut sources. The moving edge construction supplies these statements before any physical pullback.

• potential (I : SourceIndex) (n : ℕ) : ContDiffOn ℝ (↑⊤) (nativePotentialSource sys hh f I n) nativePast
• pressure (I : SourceIndex) (n : ℕ) : ContDiffOn ℝ (↑⊤) (nativePressureSource sys hh f I n) nativePast

noncomputable def NavierStokes.ActualSignedPhysicalData.potentialCarrier {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) {a b : ℝ} (ha : 0 < a) (hp : NativeProfiles f) (i : Fin 3) : PhysicalCopyBounds.CarrierBounds (potentialFamily sys hh f i) (localizedPotentialCells sys hh f i) (a / 4) (2 * b) h sys.radius

Potential carrier, bundling region, open_region, jets, contains and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.ActualSignedPhysicalData.pressureCarrier {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) {a b : ℝ} (ha : 0 < a) (hp : NativeProfiles f) : PhysicalCopyBounds.CarrierBounds (pressureFamily sys hh f) (localizedPressureCells sys hh f) (a / 4) (2 * b) h sys.radius

Pressure carrier, bundling region, open_region, jets, contains and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.ActualSignedPhysicalData.liftedNativePast (a b : ℝ) : Set LiftPoint

Lifted native past, given by PhysicalClassBounds.cylindricalDomain (a / 4) (2 * b) ∩ PhysicalClassBounds.cylindricalMap ⁻¹' nativePast.

Equations

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

theorem NavierStokes.ActualSignedPhysicalData.liftedNativePast_open (a b : ℝ) : IsOpen (liftedNativePast a b)

theorem NavierStokes.ActualSignedPhysicalData.potential_amplitude_smooth {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) {a b : ℝ} (ha : 0 < a) (hn : NativeRegular sys hh f) (i : Fin 3) (k : Frequency) (I : PhysicalWaveSum.WaveIndex 1) : ContDiffOn ℝ (↑⊤) ((potentialFamily sys hh f i).amplitude k I) (liftedNativePast a b)

theorem NavierStokes.ActualSignedPhysicalData.pressure_amplitude_smooth {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) {a b : ℝ} (ha : 0 < a) (hn : NativeRegular sys hh f) (k : Frequency) (I : PhysicalWaveSum.WaveIndex 1) : ContDiffOn ℝ (↑⊤) ((pressureFamily sys hh f).amplitude k I) (liftedNativePast a b)

theorem NavierStokes.ActualSignedPhysicalData.commonLift_mem_liftedNativePast {h a b : ℝ} (ha : 0 < a) (n : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hann : (PhysicalGraphBounds.scaledRadial n) w ∈ PhysicalGraphBounds.annulus (a / 4) (2 * b)) : PhysicalWaveSum.commonLift h n 0 w ∈ liftedNativePast a b

theorem NavierStokes.ActualSignedPhysicalData.potentialSmooth {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) {a b : ℝ} (ha : 0 < a) (hp : NativeProfiles f) (hn : NativeRegular sys hh f) {s : WeightedClasses.StripData Native} (hloc : PrimitiveLocalization f a b s) (G : ReferenceGeometry sys f) (hh0 : 0 < h) (hh1 : h < 1 / 2) (hb : 0 < b) (i : Fin 3) : LocalPhysicalCopyBounds.SmoothData (potentialFamily sys hh f i) (a / 4) h sys.radius

theorem NavierStokes.ActualSignedPhysicalData.pressureSmooth {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) {a b : ℝ} (ha : 0 < a) (hp : NativeProfiles f) (hn : NativeRegular sys hh f) {s : WeightedClasses.StripData Native} (hloc : PrimitiveLocalization f a b s) (G : ReferenceGeometry sys f) (hh0 : 0 < h) (hh1 : h < 1 / 2) (hb : 0 < b) : LocalPhysicalCopyBounds.SmoothData (pressureFamily sys hh f) (a / 4) h sys.radius

From native source estimates to actual physical wave data

theorem NavierStokes.ActualSignedPhysicalData.componentSourceBounds {ι X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] {s : WeightedClasses.StripData X} {w : ι → ℕ → X → ℝ} {h α : ℝ} {f : ι → ℕ → X → HarmonicCalculus.ComplexVector} (hf : LocalPhysicalCopyBounds.LocalSourceBounds s h α w f) : LocalPhysicalCopyBounds.LocalSourceBounds s h α (fun (q : Fin 3 × ι) => w q.2) fun (q : Fin 3 × ι) (n : ℕ) (x : X) => f q.2 n x q.1

Taking all three components preserves one constant before the component, label, copy, and band indices.

noncomputable def NavierStokes.ActualSignedPhysicalData.identitySourceChart {N : ℕ} {K I : Type} (f : PhysicalCopyBounds.CopyFamily N K) (cells : 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) (x : PhysicalWaveSum.LiftPoint), f.amplitude k J x = ChartScales.Q (↑J.1).1 ^ σ • source (idx k J) (↑J.1).1 x) (hd : ∀ (k : K) (J : PhysicalWaveSum.WaveIndex N) (x : PhysicalWaveSum.LiftPoint), f.amplitude k J x ≠ 0 → x ∈ s.domain) : LocalPhysicalCopyBounds.CommonChart f cells a b h r σ source

An identity source chart, with its closure property derived from the actual amplitude support. No physical derivative bound is an input.

Equations

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

theorem NavierStokes.ActualSignedPhysicalData.potential_source_domain {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) {a b : ℝ} {s : WeightedClasses.StripData Native} (hloc : PrimitiveLocalization f a b s) (hh0 : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hb : 0 < b) (i : Fin 3) (k : Frequency) (I : PhysicalWaveSum.WaveIndex 1) (x : LiftPoint) (hx : (potentialFamily sys hh f i).amplitude k I x ≠ 0) : x ∈ (CartesianCopySource.pullStrip s (a / 4) (2 * b) ⋯).domain

theorem NavierStokes.ActualSignedPhysicalData.pressure_source_domain {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) {a b : ℝ} {s : WeightedClasses.StripData Native} (hloc : PrimitiveLocalization f a b s) (hh0 : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hb : 0 < b) (k : Frequency) (I : PhysicalWaveSum.WaveIndex 1) (x : LiftPoint) (hx : (pressureFamily sys hh f).amplitude k I x ≠ 0) : x ∈ (CartesianCopySource.pullStrip s (a / 4) (2 * b) ⋯).domain

theorem NavierStokes.ActualSignedPhysicalData.carrier_frequencies {h : ℝ} {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) {P : ℝ} (hP : 1 ≤ P) (hf : ∀ (L : NativeLabel f.active), |((f.primary L).pulse (f.column L)).phase.p L.val.1| ≤ P ∧ |((f.primary L).pulse (f.column L)).phase.pz L.val.1| ≤ P ∧ |((f.primary L).pulse (f.column L)).phase.x0 L.val.1| ≤ P) (k : Frequency) (L : PhysicalWaveSum.BandLabel) : |(extendedCarrier f L k).angular| ≤ P ∧ |(extendedCarrier f L k).axial| ≤ P ∧ |(extendedCarrier f L k).radial| ≤ P

noncomputable def NavierStokes.ActualSignedPhysicalData.potentialWaveData {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) {a b : ℝ} {s : WeightedClasses.StripData Native} (hloc : PrimitiveLocalization f a b s) (G : ReferenceGeometry sys f) (hh0 : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hb : 0 < b) (hp : NativeProfiles f) (hn : NativeRegular sys hh f) {P : ℝ} (hP : 1 ≤ P) (hf : ∀ (L : NativeLabel f.active), |((f.primary L).pulse (f.column L)).phase.p L.val.1| ≤ P ∧ |((f.primary L).pulse (f.column L)).phase.pz L.val.1| ≤ P ∧ |((f.primary L).pulse (f.column L)).phase.x0 L.val.1| ≤ P) {α : ℝ} {w : SourceIndex → ℕ → Native → ℝ} (hs : LocalPhysicalCopyBounds.LocalSourceBounds s h α w (nativePotentialSource sys hh f)) : PhysicalStageBounds.WaveData h LiftPoint (Fin 3 × SourceIndex) Frequency (Fin 3)

The physical potential estimate is constructed from the literal cut native potential, Cartesian rotation, and the actual copy geometry.

Equations

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

noncomputable def NavierStokes.ActualSignedPhysicalData.pressureWaveData {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) {a b : ℝ} {s : WeightedClasses.StripData Native} (hloc : PrimitiveLocalization f a b s) (G : ReferenceGeometry sys f) (hh0 : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hb : 0 < b) (hp : NativeProfiles f) (hn : NativeRegular sys hh f) {P : ℝ} (hP : 1 ≤ P) (hf : ∀ (L : NativeLabel f.active), |((f.primary L).pulse (f.column L)).phase.p L.val.1| ≤ P ∧ |((f.primary L).pulse (f.column L)).phase.pz L.val.1| ≤ P ∧ |((f.primary L).pulse (f.column L)).phase.x0 L.val.1| ≤ P) {α : ℝ} {w : SourceIndex → ℕ → Native → ℝ} (hs : LocalPhysicalCopyBounds.LocalSourceBounds s h α w (nativePressureSource sys hh f)) : PhysicalStageBounds.WaveData h LiftPoint SourceIndex Frequency Unit

Pressure retains its own physical factor, exactly once.

Equations

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

theorem NavierStokes.ActualSignedPhysicalData.potentialWaveData_vector {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) {a b : ℝ} {s : WeightedClasses.StripData Native} (hloc : PrimitiveLocalization f a b s) (G : ReferenceGeometry sys f) (hh0 : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hb : 0 < b) (hp : NativeProfiles f) (hn : NativeRegular sys hh f) {P : ℝ} (hP : 1 ≤ P) (hf : ∀ (L : NativeLabel f.active), |((f.primary L).pulse (f.column L)).phase.p L.val.1| ≤ P ∧ |((f.primary L).pulse (f.column L)).phase.pz L.val.1| ≤ P ∧ |((f.primary L).pulse (f.column L)).phase.x0 L.val.1| ≤ P) {α : ℝ} {w : SourceIndex → ℕ → Native → ℝ} (hpotential : LocalPhysicalCopyBounds.LocalSourceBounds s h α w (nativePotentialSource sys hh f)) : (potentialWaveData sys hh f hloc G hh0 hh1 ha hb hp hn hP hf hpotential).vector = PhysicalCopyBounds.vectorSum (potentialFamily sys hh f) (a / 4) h sys.radius

theorem NavierStokes.ActualSignedPhysicalData.pressureWaveData_pressure {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) {a b : ℝ} {s : WeightedClasses.StripData Native} (hloc : PrimitiveLocalization f a b s) (G : ReferenceGeometry sys f) (hh0 : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hb : 0 < b) (hp : NativeProfiles f) (hn : NativeRegular sys hh f) {P : ℝ} (hP : 1 ≤ P) (hf : ∀ (L : NativeLabel f.active), |((f.primary L).pulse (f.column L)).phase.p L.val.1| ≤ P ∧ |((f.primary L).pulse (f.column L)).phase.pz L.val.1| ≤ P ∧ |((f.primary L).pulse (f.column L)).phase.x0 L.val.1| ≤ P) {α : ℝ} {w : SourceIndex → ℕ → Native → ℝ} (hpressure : LocalPhysicalCopyBounds.LocalSourceBounds s h α w (nativePressureSource sys hh f)) : (pressureWaveData sys hh f hloc G hh0 hh1 ha hb hp hn hP hf hpressure).pressure = fun (x : ProblemStatement.SpaceTime) => ((pressureFamily sys hh f).sum (a / 4) h sys.radius x).re

theorem NavierStokes.ActualSignedPhysicalData.potentialWaveData_copyPotential {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) {a b : ℝ} {s : WeightedClasses.StripData Native} (hloc : PrimitiveLocalization f a b s) (G : ReferenceGeometry sys f) (hh0 : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hb : 0 < b) (hp : NativeProfiles f) (hn : NativeRegular sys hh f) {P : ℝ} (hP : 1 ≤ P) (hf : ∀ (L : NativeLabel f.active), |((f.primary L).pulse (f.column L)).phase.p L.val.1| ≤ P ∧ |((f.primary L).pulse (f.column L)).phase.pz L.val.1| ≤ P ∧ |((f.primary L).pulse (f.column L)).phase.x0 L.val.1| ≤ P) {α : ℝ} {w : SourceIndex → ℕ → Native → ℝ} (hpotential : LocalPhysicalCopyBounds.LocalSourceBounds s h α w (nativePotentialSource sys hh f)) : (potentialWaveData sys hh f hloc G hh0 hh1 ha hb hp hn hP hf hpotential).vector = (copyPotential sys hh f hloc G hh0 hh1 ha hb).field

theorem NavierStokes.ActualSignedPhysicalData.potentialWaveData_outer {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) {a b : ℝ} {s : WeightedClasses.StripData Native} (hloc : PrimitiveLocalization f a b s) (G : ReferenceGeometry sys f) (hh0 : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hb : 0 < b) (hp : NativeProfiles f) (hn : NativeRegular sys hh f) {P : ℝ} (hP : 1 ≤ P) (hf : ∀ (L : NativeLabel f.active), |((f.primary L).pulse (f.column L)).phase.p L.val.1| ≤ P ∧ |((f.primary L).pulse (f.column L)).phase.pz L.val.1| ≤ P ∧ |((f.primary L).pulse (f.column L)).phase.x0 L.val.1| ≤ P) {α : ℝ} {w : SourceIndex → ℕ → Native → ℝ} (hpotential : LocalPhysicalCopyBounds.LocalSourceBounds s h α w (nativePotentialSource sys hh f)) : (potentialWaveData sys hh f hloc G hh0 hh1 ha hb hp hn hP hf hpotential).upperRadius = 2 * b

theorem NavierStokes.ActualSignedPhysicalData.pressureWaveData_outer {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) {a b : ℝ} {s : WeightedClasses.StripData Native} (hloc : PrimitiveLocalization f a b s) (G : ReferenceGeometry sys f) (hh0 : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hb : 0 < b) (hp : NativeProfiles f) (hn : NativeRegular sys hh f) {P : ℝ} (hP : 1 ≤ P) (hf : ∀ (L : NativeLabel f.active), |((f.primary L).pulse (f.column L)).phase.p L.val.1| ≤ P ∧ |((f.primary L).pulse (f.column L)).phase.pz L.val.1| ≤ P ∧ |((f.primary L).pulse (f.column L)).phase.x0 L.val.1| ≤ P) {α : ℝ} {w : SourceIndex → ℕ → Native → ℝ} (hpressure : LocalPhysicalCopyBounds.LocalSourceBounds s h α w (nativePressureSource sys hh f)) : (pressureWaveData sys hh f hloc G hh0 hh1 ha hb hp hn hP hf hpressure).upperRadius = 2 * b

theorem NavierStokes.ActualSignedPhysicalData.potential_physical_bound {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) {a b : ℝ} {s : WeightedClasses.StripData Native} (hloc : PrimitiveLocalization f a b s) (G : ReferenceGeometry sys f) (hh0 : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hb : 0 < b) (hp : NativeProfiles f) (hn : NativeRegular sys hh f) {P : ℝ} (hP : 1 ≤ P) (hf : ∀ (L : NativeLabel f.active), |((f.primary L).pulse (f.column L)).phase.p L.val.1| ≤ P ∧ |((f.primary L).pulse (f.column L)).phase.pz L.val.1| ≤ P ∧ |((f.primary L).pulse (f.column L)).phase.x0 L.val.1| ≤ P) {α : ℝ} {w : SourceIndex → ℕ → Native → ℝ} (hpotential : LocalPhysicalCopyBounds.LocalSourceBounds s h α w (nativePotentialSource sys hh f)) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ x ∈ PhysicalWaveSum.preterminal, PhysicalWaveSum.physicalQ h x ≤ 1 → ‖iteratedFDeriv ℝ m (PhysicalCopyBounds.vectorSum (potentialFamily sys hh f) (a / 4) h sys.radius) x‖ ≤ C * PhysicalWaveSum.physicalQ h x ^ (h * α - PhysicalClassBounds.physicalLoss h (-h) m)

theorem NavierStokes.ActualSignedPhysicalData.pressure_physical_bound {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) {a b : ℝ} {s : WeightedClasses.StripData Native} (hloc : PrimitiveLocalization f a b s) (G : ReferenceGeometry sys f) (hh0 : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hb : 0 < b) (hp : NativeProfiles f) (hn : NativeRegular sys hh f) {P : ℝ} (hP : 1 ≤ P) (hf : ∀ (L : NativeLabel f.active), |((f.primary L).pulse (f.column L)).phase.p L.val.1| ≤ P ∧ |((f.primary L).pulse (f.column L)).phase.pz L.val.1| ≤ P ∧ |((f.primary L).pulse (f.column L)).phase.x0 L.val.1| ≤ P) {α : ℝ} {w : SourceIndex → ℕ → Native → ℝ} (hpressure : LocalPhysicalCopyBounds.LocalSourceBounds s h α w (nativePressureSource sys hh f)) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ x ∈ PhysicalWaveSum.preterminal, PhysicalWaveSum.physicalQ h x ≤ 1 → ‖iteratedFDeriv ℝ m (fun (y : ProblemStatement.SpaceTime) => ((pressureFamily sys hh f).sum (a / 4) h sys.radius y).re) x‖ ≤ C * PhysicalWaveSum.physicalQ h x ^ (h * α - PhysicalClassBounds.physicalLoss h (-(2 * CoordinateAlgebra.A h)) m)

Cartesian germs of the original reference fields

theorem NavierStokes.ActualSignedPhysicalData.polarCoordinates_backward {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) {x : ProblemStatement.SpaceTime} (hx : PhysicalGraphBounds.radialProjection x ∈ PolarCharts.chartDomain a j) : ((PhysicalCurlCovariance.polarCoordinates a j x).1, CylindricalResidual.chart (PhysicalCurlCovariance.polarCoordinates a j x).2) = x

theorem NavierStokes.ActualSignedPhysicalData.polarCoordinates_valid {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) {x : ProblemStatement.SpaceTime} (hx : PhysicalGraphBounds.radialProjection x ∈ PolarCharts.chartDomain a j) : PhysicalCurlCovariance.polarCoordinates a j x ∈ PhysicalCurlCovariance.validCylindrical a j

noncomputable def NavierStokes.ActualSignedPhysicalData.labelPotential {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) (L : NativeLabel f.active) (a : ℝ) : ProblemStatement.VelocityField

Label potential, defined pointwise by PhysicalCurlCovariance.realVector (fun i => (potentialFamily sys hh f i).periodized a h sys.radius (positiveIndex L) x).

Equations

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

noncomputable def NavierStokes.ActualSignedPhysicalData.labelPressure {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) (L : NativeLabel f.active) (a : ℝ) : ProblemStatement.PressureField

Label pressure, defined pointwise by ((pressureFamily sys hh f).periodized a h sys.radius (positiveIndex L) x).re.

Equations

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

noncomputable def NavierStokes.ActualSignedPhysicalData.referencePatch {h : ℝ} {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) (L : NativeLabel f.active) (a b delta : ℝ) (j : PolarCharts.Index) : Set ProblemStatement.SpaceTime

Only coordinate domains and the original native phase domain occur in this set. Its definition contains no output-field equality.

Equations

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

theorem NavierStokes.ActualSignedPhysicalData.labelPotential_eq_reference {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) (G : ReferenceGeometry sys f) (L : NativeLabel f.active) (hPhi : ContDiffOn ℝ (↑⊤) ((f.primary L).base.phase L.val.1) (f.primary L).strip.domain) {a b delta : ℝ} (ha : 0 < a) (hd : 0 < delta) (j : PolarCharts.Index) {x : ProblemStatement.SpaceTime} (hx : x ∈ referencePatch f L a b delta j) : labelPotential sys hh f L a x = ActualPeriodizedSignedRealization.physicalPotential (f.primary L) (layout sys hh L.val ⋯ 0) (f.view L) (f.state L) (f.column L) delta x

theorem NavierStokes.ActualSignedPhysicalData.labelPressure_eq_reference {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) (G : ReferenceGeometry sys f) (L : NativeLabel f.active) {a b delta : ℝ} (ha : 0 < a) (hd : 0 < delta) (j : PolarCharts.Index) {x : ProblemStatement.SpaceTime} (hx : x ∈ referencePatch f L a b delta j) : labelPressure sys hh f L a x = ActualPeriodizedSignedRealization.physicalPressure (f.primary L) (layout sys hh L.val ⋯ 0) (f.view L) (f.state L) (f.column L) delta x

theorem NavierStokes.ActualSignedPhysicalData.labelPotential_germ {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) (G : ReferenceGeometry sys f) (L : NativeLabel f.active) (hPhi : ContDiffOn ℝ (↑⊤) ((f.primary L).base.phase L.val.1) (f.primary L).strip.domain) {a b delta : ℝ} (ha : 0 < a) (hd : 0 < delta) (j : PolarCharts.Index) {x : ProblemStatement.SpaceTime} (hx : x ∈ interior (referencePatch f L a b delta j)) : labelPotential sys hh f L a =ᶠ[nhds x] ActualPeriodizedSignedRealization.physicalPotential (f.primary L) (layout sys hh L.val ⋯ 0) (f.view L) (f.state L) (f.column L) delta

theorem NavierStokes.ActualSignedPhysicalData.labelPressure_germ {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) (G : ReferenceGeometry sys f) (L : NativeLabel f.active) {a b delta : ℝ} (ha : 0 < a) (hd : 0 < delta) (j : PolarCharts.Index) {x : ProblemStatement.SpaceTime} (hx : x ∈ interior (referencePatch f L a b delta j)) : labelPressure sys hh f L a =ᶠ[nhds x] ActualPeriodizedSignedRealization.physicalPressure (f.primary L) (layout sys hh L.val ⋯ 0) (f.view L) (f.state L) (f.column L) delta

theorem NavierStokes.ActualSignedPhysicalData.labelVelocity_eq_reference {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) (G : ReferenceGeometry sys f) (L : NativeLabel f.active) (hPhi : ContDiffOn ℝ (↑⊤) ((f.primary L).base.phase L.val.1) (f.primary L).strip.domain) {a b delta : ℝ} (ha : 0 < a) (hd : 0 < delta) (j : PolarCharts.Index) {x : ProblemStatement.SpaceTime} (hx : x ∈ interior (referencePatch f L a b delta j)) : SpatialCurl.spatialCurl (labelPotential sys hh f L a) x = ActualPeriodizedSignedRealization.physicalVelocity (f.primary L) (layout sys hh L.val ⋯ 0) (f.view L) (f.state L) (f.column L) delta x

theorem NavierStokes.ActualSignedPhysicalData.labelPotential_jets_eq_reference {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : SignedFamily U) (G : ReferenceGeometry sys f) (L : NativeLabel f.active) (hPhi : ContDiffOn ℝ (↑⊤) ((f.primary L).base.phase L.val.1) (f.primary L).strip.domain) {a b delta : ℝ} (ha : 0 < a) (hd : 0 < delta) (j : PolarCharts.Index) {x : ProblemStatement.SpaceTime} (hx : x ∈ interior (referencePatch f L a b delta j)) (m : ℕ) : iteratedFDeriv ℝ m (labelPotential sys hh f L a) x = iteratedFDeriv ℝ m (ActualPeriodizedSignedRealization.physicalPotential (f.primary L) (layout sys hh L.val ⋯ 0) (f.view L) (f.state L) (f.column L) delta) x