Geometry of the actual current-mode evaluation point

The physical validity band and the closed nominal radial interval place the normalized Cartesian coordinates in a fixed compact annulus. The same current common-cover chart has the actual native slow domain and exactly the physical profile radius.

Normalized polar germs of the actual current particular modes

The native point below uses the actual common-cover index. The ambient germs retain the current solve, its chosen phase, and its Cartesian rotation.

@[reducible, inline]

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

Label: an abbreviation for ActualCurrentParticularPhysical.Label B N0.

Equations

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

noncomputable def NavierStokes.CurrentPhysicalModeGerms.commonGap (n : ℕ) : ℕ

The cover gap of the actual current-band graph.

Equations

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

theorem NavierStokes.CurrentPhysicalModeGerms.commonGap_le (n : ℕ) : commonGap n ≤ ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h n

theorem NavierStokes.CurrentPhysicalModeGerms.commonGap_index (n : ℕ) : ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h n - commonGap n = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n

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

theorem NavierStokes.CurrentPhysicalModeGerms.cylinderAt_commonLift (h : ℝ) (n d : ℕ) (hd : d ≤ ChartScales.nativeIndex h n) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) {w : ProblemStatement.SpaceTime} (hw : (PhysicalGraphBounds.scaledRadial n) w ∈ PolarCharts.chartDomain a i) : ActualSignedPhysicalData.cylinderAt a i (PhysicalWaveSum.commonLift h n d w) = (PhysicalResidualBridge.commonGraph (ChartScales.Q n) h (ChartScales.nativeIndex h n - d)).map (ResidualPolarGraph.cylindricalPoint a i n w)

The exact common-lift chart is the same cylindrical graph as the one used by the current physical solve.

theorem NavierStokes.CurrentPhysicalModeGerms.realVector_smul (c : ℝ) (v : HarmonicCalculus.ComplexVector) : PhysicalCurlCovariance.realVector (c • v) = c • PhysicalCurlCovariance.realVector v

theorem NavierStokes.CurrentPhysicalModeGerms.radialProjection_eq_sqrt_smul (n : ℕ) (w : ProblemStatement.SpaceTime) : PhysicalGraphBounds.radialProjection w = √(ChartScales.Q n) • (PhysicalGraphBounds.scaledRadial n) w

theorem NavierStokes.CurrentPhysicalModeGerms.physical_chart_mem (n : ℕ) {a : ℝ} (i : PolarCharts.Index) {w : ProblemStatement.SpaceTime} (hw : (PhysicalGraphBounds.scaledRadial n) w ∈ PolarCharts.chartDomain a i) : w ∈ ActualMeanPotentialRealization.cartesianDomain (√(ChartScales.Q n) * a) i

theorem NavierStokes.CurrentPhysicalModeGerms.physical_chart_angle (n : ℕ) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) {w : ProblemStatement.SpaceTime} (hw : (PhysicalGraphBounds.scaledRadial n) w ∈ PolarCharts.chartDomain a i) : (PolarCharts.chart (√(ChartScales.Q n) * a) i (PhysicalGraphBounds.radialProjection w)).2 = ResidualPolarGraph.angle a i n w

theorem NavierStokes.CurrentPhysicalModeGerms.physical_polarCoordinates (n : ℕ) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) {w : ProblemStatement.SpaceTime} (hw : (PhysicalGraphBounds.scaledRadial n) w ∈ PolarCharts.chartDomain a i) : PhysicalCurlCovariance.polarCoordinates (√(ChartScales.Q n) * a) i w = ResidualPolarGraph.cylindricalPoint a i n w

The physical chart uses the same angular branch as the normalized chart, with the physical radius restored.

theorem NavierStokes.CurrentPhysicalModeGerms.nativeMap_commonChart (n : ℕ) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) {w : ProblemStatement.SpaceTime} (hw : (PhysicalGraphBounds.scaledRadial n) w ∈ PolarCharts.chartDomain a i) : PhysicalParticularWave.nativeMap CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n) (PhysicalCurlCovariance.polarCoordinates (√(ChartScales.Q n) * a) i w) = PhysicalParticularWave.waveEquiv (ActualSignedPhysicalData.cylinderAt a i (PhysicalWaveSum.commonLift CorrectionInitialization.ActualPrimary.h n (commonGap n) w))

The current native map uses the common index, as opposed to the larger native index of the unmodified lift.

theorem NavierStokes.CurrentPhysicalModeGerms.rotation_commonLift (h : ℝ) (n d : ℕ) (w : ProblemStatement.SpaceTime) : CartesianCopySource.rotationMap (PhysicalGraphBounds.radialProjection w) = CartesianCopySource.rotationMap (PhysicalGraphBounds.liftXY (PhysicalWaveSum.commonLift h n d w))

theorem NavierStokes.CurrentPhysicalModeGerms.localPotentialMode_eq {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (j : ℤ) (hf : ∀ (n : ℕ), (x.coefficients.blocks l).frequency n = ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n)) (n : ℕ) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) {w : ProblemStatement.SpaceTime} (hw : (PhysicalGraphBounds.scaledRadial n) w ∈ PolarCharts.chartDomain a i) : ActualCurrentParticularPhysical.localPotentialMode x l j n w = ChartScales.Q n ^ (-CorrectionInitialization.ActualPrimary.h) • PhysicalCurlCovariance.realVector ((CartesianCopySource.rotationMap (PhysicalGraphBounds.liftXY (PhysicalWaveSum.commonLift CorrectionInitialization.ActualPrimary.h n (commonGap n) w))) (ActualCurrentParticularPhysical.nativePotential x l j n (PhysicalParticularWave.waveEquiv (ActualSignedPhysicalData.cylinderAt a i (PhysicalWaveSum.commonLift CorrectionInitialization.ActualPrimary.h n (commonGap n) w)))))

Pointwise equality to the literal current potential on a valid normalized polar chart.

theorem NavierStokes.CurrentPhysicalModeGerms.localPressureMode_eq {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (j : ℤ) (hf : ∀ (n : ℕ), (x.coefficients.blocks l).frequency n = ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n)) (n : ℕ) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) {w : ProblemStatement.SpaceTime} (hw : (PhysicalGraphBounds.scaledRadial n) w ∈ PolarCharts.chartDomain a i) : ActualCurrentParticularPhysical.localPressureMode x l j n w = ChartScales.Q n ^ (-2 * CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h) * (ActualCurrentParticularPhysical.nativePressure x l j n (PhysicalParticularWave.waveEquiv (ActualSignedPhysicalData.cylinderAt a i (PhysicalWaveSum.commonLift CorrectionInitialization.ActualPrimary.h n (commonGap n) w)))).re

theorem NavierStokes.CurrentPhysicalModeGerms.localPotentialMode_germ {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (j : ℤ) (hf : ∀ (n : ℕ), (x.coefficients.blocks l).frequency n = ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n)) (n : ℕ) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) {w : ProblemStatement.SpaceTime} (hw : (PhysicalGraphBounds.scaledRadial n) w ∈ PolarCharts.chartDomain a i) : ActualCurrentParticularPhysical.localPotentialMode x l j n =ᶠ[nhds w] fun (y : ProblemStatement.SpaceTime) => ChartScales.Q n ^ (-CorrectionInitialization.ActualPrimary.h) • PhysicalCurlCovariance.realVector ((CartesianCopySource.rotationMap (PhysicalGraphBounds.liftXY (PhysicalWaveSum.commonLift CorrectionInitialization.ActualPrimary.h n (commonGap n) y))) (ActualCurrentParticularPhysical.nativePotential x l j n (PhysicalParticularWave.waveEquiv (ActualSignedPhysicalData.cylinderAt a i (PhysicalWaveSum.commonLift CorrectionInitialization.ActualPrimary.h n (commonGap n) y)))))

Ambient germ equality, suitable for ordinary Cartesian derivatives of every order, with the actual common-cover lift.

theorem NavierStokes.CurrentPhysicalModeGerms.localPressureMode_germ {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (j : ℤ) (hf : ∀ (n : ℕ), (x.coefficients.blocks l).frequency n = ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n)) (n : ℕ) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) {w : ProblemStatement.SpaceTime} (hw : (PhysicalGraphBounds.scaledRadial n) w ∈ PolarCharts.chartDomain a i) : ActualCurrentParticularPhysical.localPressureMode x l j n =ᶠ[nhds w] fun (y : ProblemStatement.SpaceTime) => ChartScales.Q n ^ (-2 * CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h) * (ActualCurrentParticularPhysical.nativePressure x l j n (PhysicalParticularWave.waveEquiv (ActualSignedPhysicalData.cylinderAt a i (PhysicalWaveSum.commonLift CorrectionInitialization.ActualPrimary.h n (commonGap n) y)))).re

noncomputable def NavierStokes.CurrentModeGeometry.chartInner : ℝ

Chart inner, given by PrimaryTargetBounds.leftRadius ActualPrimary.nominal / 4.

Equations

• NavierStokes.CurrentModeGeometry.chartInner = NavierStokes.PrimaryTargetBounds.leftRadius NavierStokes.CorrectionInitialization.ActualPrimary.nominal / 4

noncomputable def NavierStokes.CurrentModeGeometry.chartOuter : ℝ

Chart outer, given by 2 * PrimaryTargetBounds.rightRadius ActualPrimary.nominal.

Equations

• NavierStokes.CurrentModeGeometry.chartOuter = 2 * NavierStokes.PrimaryTargetBounds.rightRadius NavierStokes.CorrectionInitialization.ActualPrimary.nominal

theorem NavierStokes.CurrentModeGeometry.chartInner_pos : 0 < chartInner

theorem NavierStokes.CurrentModeGeometry.chartOuter_pos : 0 < chartOuter

theorem NavierStokes.CurrentModeGeometry.chartInner_lt_chartOuter : chartInner < chartOuter

theorem NavierStokes.CurrentModeGeometry.band_q_comparison (n : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ ValidDyadicBandCover.band CorrectionInitialization.ActualPrimary.h n) : PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w / 2 ≤ ChartScales.Q n ∧ ChartScales.Q n ≤ 2 * PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w

theorem NavierStokes.CurrentModeGeometry.scaledRadial_mem_annulus (n : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ ValidDyadicBandCover.band CorrectionInitialization.ActualPrimary.h n) (hr : ActualCurrentWaveSupport.profileRadius CorrectionInitialization.ActualPrimary.h w ∈ Set.Icc (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal)) : (PhysicalGraphBounds.scaledRadial n) w ∈ PhysicalGraphBounds.annulus chartInner chartOuter

The annulus is derived from the actual physical ratio, independently of any field support or coherent-family assumption.

noncomputable def NavierStokes.CurrentModeGeometry.point (a : ℝ) (i : PolarCharts.Index) (n : ℕ) (w : ProblemStatement.SpaceTime) : PhysicalParticularWave.WaveSpace

The literal current common-cover evaluation point used in the physical mode estimates.

Equations

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

theorem NavierStokes.CurrentModeGeometry.point_eq_nativeMap (n : ℕ) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) {w : ProblemStatement.SpaceTime} (hc : (PhysicalGraphBounds.scaledRadial n) w ∈ PolarCharts.chartDomain a i) : point a i n w = PhysicalParticularWave.nativeMap CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n) (PhysicalCurlCovariance.polarCoordinates (√(ChartScales.Q n) * a) i w)

theorem NavierStokes.CurrentModeGeometry.point_mem_nativeDomain (n : ℕ) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) {w : ProblemStatement.SpaceTime} (hw : w ∈ ValidDyadicBandCover.band CorrectionInitialization.ActualPrimary.h n) (hc : (PhysicalGraphBounds.scaledRadial n) w ∈ PolarCharts.chartDomain a i) : point a i n w ∈ ActualCurrentParticularPhysical.nativeDomain

theorem NavierStokes.CurrentModeGeometry.point_profileRadius (n : ℕ) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) {w : ProblemStatement.SpaceTime} (ht : w.1 < 1) (hc : (PhysicalGraphBounds.scaledRadial n) w ∈ PolarCharts.chartDomain a i) : ActualWaveRegularityData.radius (ActualWaveRegularity.particularChart.symm (point a i n w)) = ActualCurrentWaveSupport.profileRadius CorrectionInitialization.ActualPrimary.h w

theorem NavierStokes.CurrentModeGeometry.point_mem_closed_window (n : ℕ) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) {w : ProblemStatement.SpaceTime} (hw : w ∈ ValidDyadicBandCover.band CorrectionInitialization.ActualPrimary.h n) (hc : (PhysicalGraphBounds.scaledRadial n) w ∈ PolarCharts.chartDomain a i) (hr : ActualCurrentWaveSupport.profileRadius CorrectionInitialization.ActualPrimary.h w ∈ Set.Icc (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal)) : point a i n w ∈ ActualCurrentParticularPhysical.nativeDomain ∧ ActualWaveRegularityData.radius (ActualWaveRegularity.particularChart.symm (point a i n w)) ∈ Set.Icc (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal)