The canonical signed physical family and its current-band realization

The dependent family, both signed labels, and its positive physical harmonic are retained. Native faces are treated by the literal zero mask before a current-band comparison is used.

Geometry for current signed waves in physical polar charts

The actual active annulus is covered for every band whose physical scale ratio lies in (1/2,2). An explicit change of the chart radius identifies the scaled Cartesian lift with the full native cylindrical graph.

theorem NavierStokes.ActualSignedPhysicalGeometry.annulus_of_ratio (n : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hactive : w ∈ ActualPolarCoverage.active) (hq : PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w / ChartScales.Q n ∈ Set.Ioo (1 / 2) 2) : (PhysicalGraphBounds.scaledRadial n) w ∈ PhysicalGraphBounds.annulus ActualPolarCoverage.inner ActualPolarCoverage.outer

The annulus estimate uses only comparability of the two positive scales, so it holds throughout the full open native scale window.

theorem NavierStokes.ActualSignedPhysicalGeometry.chart_exists_of_ratio (n : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hactive : w ∈ ActualPolarCoverage.active) (hq : PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w / ChartScales.Q n ∈ Set.Ioo (1 / 2) 2) : ∃ (j : PolarCharts.Index), (PhysicalGraphBounds.scaledRadial n) w ∈ PolarCharts.chartDomain ActualPolarCoverage.inner j

noncomputable def NavierStokes.ActualSignedPhysicalGeometry.chartRadius (a : ℝ) (n : ℕ) : ℝ

The exact unscaled chart radius corresponding to a native chart radius.

Equations

• NavierStokes.ActualSignedPhysicalGeometry.chartRadius a n = a / NavierStokes.ChartScales.Q n ^ (-(1 / 2))

theorem NavierStokes.ActualSignedPhysicalGeometry.chartRadius_pos {a : ℝ} (ha : 0 < a) (n : ℕ) : 0 < chartRadius a n

theorem NavierStokes.ActualSignedPhysicalGeometry.chartDomain_unscale {a c : ℝ} (hc : 0 < c) (j : PolarCharts.Index) {p : PolarCharts.Plane} (hp : c • p ∈ PolarCharts.chartDomain a j) : p ∈ PolarCharts.chartDomain (a / c) j

theorem NavierStokes.ActualSignedPhysicalGeometry.physical_chart_mem (n : ℕ) {a : ℝ} (j : PolarCharts.Index) {w : ProblemStatement.SpaceTime} (hchart : (PhysicalGraphBounds.scaledRadial n) w ∈ PolarCharts.chartDomain a j) : PhysicalGraphBounds.radialProjection w ∈ PolarCharts.chartDomain (chartRadius a n) j

theorem NavierStokes.ActualSignedPhysicalGeometry.physical_chart_scale (n : ℕ) {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) {w : ProblemStatement.SpaceTime} (hchart : (PhysicalGraphBounds.scaledRadial n) w ∈ PolarCharts.chartDomain a j) : PolarCharts.chart a j ((PhysicalGraphBounds.scaledRadial n) w) = (ChartScales.Q n ^ (-(1 / 2)) * (PolarCharts.chart (chartRadius a n) j (PhysicalGraphBounds.radialProjection w)).1, (PolarCharts.chart (chartRadius a n) j (PhysicalGraphBounds.radialProjection w)).2)

The scaled and unscaled charts have exactly the same angle.

theorem NavierStokes.ActualSignedPhysicalGeometry.cylinderAt_physical_chart (h : ℝ) (n : ℕ) {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) {w : ProblemStatement.SpaceTime} (hchart : (PhysicalGraphBounds.scaledRadial n) w ∈ PolarCharts.chartDomain a j) : ActualSignedPhysicalData.cylinderAt a j (PhysicalGraphBounds.physicalLift h n w) = (PhysicalResidualBridge.commonGraph (ChartScales.Q n) h (ChartScales.nativeIndex h n)).map (PhysicalCurlCovariance.polarCoordinates (chartRadius a n) j w)

No angle choice or auxiliary coordinate is discarded by this identity.

theorem NavierStokes.ActualSignedPhysicalGeometry.exists_physical_chart (h : ℝ) (n : ℕ) {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) {w : ProblemStatement.SpaceTime} (hchart : (PhysicalGraphBounds.scaledRadial n) w ∈ PolarCharts.chartDomain a j) : ∃ (b : ℝ), 0 < b ∧ PhysicalGraphBounds.radialProjection w ∈ PolarCharts.chartDomain b j ∧ ActualSignedPhysicalData.cylinderAt a j (PhysicalGraphBounds.physicalLift h n w) = (PhysicalResidualBridge.commonGraph (ChartScales.Q n) h (ChartScales.nativeIndex h n)).map (PhysicalCurlCovariance.polarCoordinates b j w)

theorem NavierStokes.ActualSignedPhysicalGeometry.graph_slow_mem_standard_of_ratio {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (n d : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hq : PhysicalWaveSum.physicalQ h w / ChartScales.Q n ∈ Set.Ioo (1 / 2) 2) : (PhysicalMeanJetBounds.graph h n d w).2.1 ∈ (ActualSignedGeometry.standardSlowRegion hh hh1).carrier

The mean graph's slow coordinate does not depend on its auxiliary cover.

theorem NavierStokes.ActualSignedPhysicalGeometry.commonGraph_slow (h : ℝ) (n i d : ℕ) (z : ProblemStatement.SpaceTime) : (PhysicalResidualTZ.swapCylinder ((PhysicalResidualBridge.commonGraph (ChartScales.Q n) h i).map z)).1.2.1 = (PhysicalMeanJetBounds.graph h n d (z.1, CylindricalResidual.chart z.2)).2.1

This identity is global and needs no radius or time positivity premise.

theorem NavierStokes.ActualSignedPhysicalGeometry.nativePoint_slow (n d : ℕ) (z : ProblemStatement.SpaceTime) : (ActualSignedPotentialCoherence.nativePoint n z).1.2.1 = (PhysicalMeanJetBounds.graph CorrectionInitialization.ActualPrimary.h n d (z.1, CylindricalResidual.chart z.2)).2.1

theorem NavierStokes.ActualSignedPhysicalGeometry.nativePoint_mem_physicalDomain (n : ℕ) (z : ProblemStatement.SpaceTime) (hr : 0 < z.2.ofLp 0) (hw : (z.1, CylindricalResidual.chart z.2) ∈ PhysicalWaveSum.preterminal) (hq : PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h (z.1, CylindricalResidual.chart z.2) / ChartScales.Q n ∈ Set.Ioo (1 / 2) 2) : z ∈ ActualSignedPotentialCoherence.physicalDomain n

theorem NavierStokes.ActualSignedPhysicalGeometry.polarCoordinates_mem_physicalDomain (n : ℕ) {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) {w : ProblemStatement.SpaceTime} (hchart : PhysicalGraphBounds.radialProjection w ∈ PolarCharts.chartDomain a j) (hw : w ∈ PhysicalWaveSum.preterminal) (hq : PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w / ChartScales.Q n ∈ Set.Ioo (1 / 2) 2) : PhysicalCurlCovariance.polarCoordinates a j w ∈ ActualSignedPotentialCoherence.physicalDomain n

theorem NavierStokes.ActualSignedPhysicalGeometry.scaledChart_mem_physicalDomain (n : ℕ) {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) {w : ProblemStatement.SpaceTime} (hchart : (PhysicalGraphBounds.scaledRadial n) w ∈ PolarCharts.chartDomain a j) (hw : w ∈ PhysicalWaveSum.preterminal) (hq : PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w / ChartScales.Q n ∈ Set.Ioo (1 / 2) 2) : PhysicalCurlCovariance.polarCoordinates (chartRadius a n) j w ∈ ActualSignedPotentialCoherence.physicalDomain n

Zeros of the actual signed physical coefficients

The native dyadic mask vanishes at both faces and outside the open native band. This file transfers that literal zero to the canonical physical copy family and to every current-band representation of the same label. The current state and the native reference requests are arbitrary.

@[reducible, inline]

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

Label: an abbreviation for ActualSignedPhysicalBinding.Label.

Equations

• NavierStokes.ActualSignedPhysicalZeros.Label = NavierStokes.ActualSignedPhysicalBinding.Label

@[reducible, inline]

abbrev NavierStokes.ActualSignedPhysicalZeros.Point : Type

Point: an abbreviation for ActualSignedCoherence.Point.

Equations

• NavierStokes.ActualSignedPhysicalZeros.Point = NavierStokes.ActualSignedCoherence.Point

@[reducible, inline]

abbrev NavierStokes.ActualSignedPhysicalZeros.FullPoint : Type

Full point: an abbreviation for ActualSignedCoherence.FullPoint.

Equations

• NavierStokes.ActualSignedPhysicalZeros.FullPoint = NavierStokes.ActualSignedCoherence.FullPoint

@[reducible, inline]

abbrev NavierStokes.ActualSignedPhysicalZeros.Frequency : Type

Frequency: an abbreviation for TorusInverse.Frequency.

Equations

• NavierStokes.ActualSignedPhysicalZeros.Frequency = NavierStokes.TorusInverse.Frequency

theorem NavierStokes.ActualSignedPhysicalZeros.physicalLift_coordinateQ (n : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) : SimilarityCoordinates.coordinateQ (2 * CorrectionInitialization.ActualPrimary.h) ((ActualSignedPhysicalData.cylinderZero (PhysicalGraphBounds.physicalLift CorrectionInitialization.ActualPrimary.h n w)).1.2.1.2, (ActualSignedPhysicalData.cylinderZero (PhysicalGraphBounds.physicalLift CorrectionInitialization.ActualPrimary.h n w)).1.2.1.1) = PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w / ChartScales.Q n

theorem NavierStokes.ActualSignedPhysicalZeros.primary_mask_physicalLift_zero {B N0 : ℕ} (l : Label B N0) (m n : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hq : PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w / ChartScales.Q n ∉ Set.Ioo (1 / 2) 2) : (ActualSignedPhysicalBinding.primary l).mask m (ActualSignedPhysicalData.cylinderZero (PhysicalGraphBounds.physicalLift CorrectionInitialization.ActualPrimary.h n w)) = 0

theorem NavierStokes.ActualSignedPhysicalZeros.canonical_potential_amplitude_zero_of_nativeQ {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (l : Label B N0) (i : Fin 3) (k : Frequency) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hq : PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w / ChartScales.Q (ActualSignedPhysicalBinding.reference l) ∉ Set.Ioo (1 / 2) 2) : ((ActualSignedExterior.family s).potentialCopies CorrectionInitialization.ActualPrimary.slots ⋯ i).amplitude k (ActualSignedPhysicalData.positiveIndex ⟨(ActualSignedExterior.nativeLabel l).val, ⋯⟩) (PhysicalGraphBounds.physicalLift CorrectionInitialization.ActualPrimary.h (ActualSignedPhysicalBinding.reference l) w) = 0

theorem NavierStokes.ActualSignedPhysicalZeros.canonical_pressure_amplitude_zero_of_nativeQ {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (l : Label B N0) (k : Frequency) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hq : PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w / ChartScales.Q (ActualSignedPhysicalBinding.reference l) ∉ Set.Ioo (1 / 2) 2) : ((ActualSignedExterior.family s).pressureCopies CorrectionInitialization.ActualPrimary.slots ⋯).amplitude k (ActualSignedPhysicalData.positiveIndex ⟨(ActualSignedExterior.nativeLabel l).val, ⋯⟩) (PhysicalGraphBounds.physicalLift CorrectionInitialization.ActualPrimary.h (ActualSignedPhysicalBinding.reference l) w) = 0

theorem NavierStokes.ActualSignedPhysicalZeros.canonical_potential_term_zero_of_nativeQ {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (l : Label B N0) (i : Fin 3) (k : Frequency) (a r0 : ℝ) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hq : PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w / ChartScales.Q (ActualSignedPhysicalBinding.reference l) ∉ Set.Ioo (1 / 2) 2) : ((ActualSignedExterior.family s).potentialCopies CorrectionInitialization.ActualPrimary.slots ⋯ i).term a CorrectionInitialization.ActualPrimary.h r0 (ActualSignedPhysicalData.positiveIndex ⟨(ActualSignedExterior.nativeLabel l).val, ⋯⟩) k w = 0

theorem NavierStokes.ActualSignedPhysicalZeros.canonical_pressure_term_zero_of_nativeQ {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (l : Label B N0) (k : Frequency) (a r0 : ℝ) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hq : PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w / ChartScales.Q (ActualSignedPhysicalBinding.reference l) ∉ Set.Ioo (1 / 2) 2) : ((ActualSignedExterior.family s).pressureCopies CorrectionInitialization.ActualPrimary.slots ⋯).term a CorrectionInitialization.ActualPrimary.h r0 (ActualSignedPhysicalData.positiveIndex ⟨(ActualSignedExterior.nativeLabel l).val, ⋯⟩) k w = 0

theorem NavierStokes.ActualSignedPhysicalZeros.canonical_potential_periodized_zero_of_nativeQ {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (l : Label B N0) (i : Fin 3) (a r0 : ℝ) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hq : PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w / ChartScales.Q (ActualSignedPhysicalBinding.reference l) ∉ Set.Ioo (1 / 2) 2) : ((ActualSignedExterior.family s).potentialCopies CorrectionInitialization.ActualPrimary.slots ⋯ i).periodized a CorrectionInitialization.ActualPrimary.h r0 (ActualSignedPhysicalData.positiveIndex ⟨(ActualSignedExterior.nativeLabel l).val, ⋯⟩) w = 0

theorem NavierStokes.ActualSignedPhysicalZeros.canonical_pressure_periodized_zero_of_nativeQ {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (l : Label B N0) (a r0 : ℝ) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hq : PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w / ChartScales.Q (ActualSignedPhysicalBinding.reference l) ∉ Set.Ioo (1 / 2) 2) : ((ActualSignedExterior.family s).pressureCopies CorrectionInitialization.ActualPrimary.slots ⋯).periodized a CorrectionInitialization.ActualPrimary.h r0 (ActualSignedPhysicalData.positiveIndex ⟨(ActualSignedExterior.nativeLabel l).val, ⋯⟩) w = 0

The same native slow point in every current band

theorem NavierStokes.ActualSignedPhysicalZeros.current_nativeSlow_reference {B N0 : ℕ} (l : Label B N0) (n : ℕ) (k : Frequency) (z : ProblemStatement.SpaceTime) (hr : 0 < z.2.ofLp 0) : (ActualSignedStageControls.nativePoint l n k (ActualSignedPotentialCoherence.nativePoint n z)).1 = BaseContextAssembly.slowCoordinates (ActualSignedPotentialCoherence.nativePoint (ActualSignedPhysicalBinding.reference l) z).1

theorem NavierStokes.ActualSignedPhysicalZeros.nativePoint_slowCoordinates (n : ℕ) (z : ProblemStatement.SpaceTime) (hr : 0 < z.2.ofLp 0) : BaseContextAssembly.slowCoordinates (ActualSignedPotentialCoherence.nativePoint n z).1 = ActualSignedPhysicalData.nativeSlow (PhysicalMeanJetBounds.graph CorrectionInitialization.ActualPrimary.h n 0 (z.1, CylindricalResidual.chart z.2))

theorem NavierStokes.ActualSignedPhysicalZeros.current_nativeSlow_physicalLift {B N0 : ℕ} (l : Label B N0) (n : ℕ) (k : Frequency) (z : ProblemStatement.SpaceTime) (hr : 0 < z.2.ofLp 0) : (ActualSignedStageControls.nativePoint l n k (ActualSignedPotentialCoherence.nativePoint n z)).1 = ((ActualSignedPhysicalData.cylinderZero (PhysicalGraphBounds.physicalLift CorrectionInitialization.ActualPrimary.h (ActualSignedPhysicalBinding.reference l) (z.1, CylindricalResidual.chart z.2))).1.1, (ActualSignedPhysicalData.cylinderZero (PhysicalGraphBounds.physicalLift CorrectionInitialization.ActualPrimary.h (ActualSignedPhysicalBinding.reference l) (z.1, CylindricalResidual.chart z.2))).1.2.1)

theorem NavierStokes.ActualSignedPhysicalZeros.current_mask_physicalLift {B N0 : ℕ} (l : Label B N0) (n : ℕ) (k : Frequency) (z : ProblemStatement.SpaceTime) (hr : 0 < z.2.ofLp 0) : ActualSignedStageControls.mask l k n (ActualSignedPotentialCoherence.nativePoint n z) = (ActualSignedPhysicalBinding.primary l).mask n (ActualSignedPhysicalData.cylinderZero (PhysicalGraphBounds.physicalLift CorrectionInitialization.ActualPrimary.h (ActualSignedPhysicalBinding.reference l) (z.1, CylindricalResidual.chart z.2)))

theorem NavierStokes.ActualSignedPhysicalZeros.current_target_physicalLift {B N0 : ℕ} (l : Label B N0) (n : ℕ) (k : Frequency) (z : ProblemStatement.SpaceTime) (hr : 0 < z.2.ofLp 0) : ActualSignedStageControls.target l k n (ActualSignedPotentialCoherence.nativePoint n z) = ActualSignedStageControls.coefficientScale l n ^ 2 • (ActualSignedPhysicalBinding.primary l).target n (ActualSignedPhysicalData.cylinderZero (PhysicalGraphBounds.physicalLift CorrectionInitialization.ActualPrimary.h (ActualSignedPhysicalBinding.reference l) (z.1, CylindricalResidual.chart z.2)))

Passing literal raw zeros through the current copy sum

theorem NavierStokes.ActualSignedPhysicalZeros.common_zero_of_raw {B N0 : ℕ} (l : Label B N0) (u : CorrectionState.State Point) (n : ℕ) (x : FullPoint) (hz : ∀ (k : TorusInverse.Frequency), (ActualSignedCoherence.copies l u).amplitude n k x = 0 ∧ (ActualSignedCoherence.copies l u).pressure n k x = 0) : (ActualSignedCoherence.copies l u).common.amplitude n x = 0 ∧ (ActualSignedCoherence.copies l u).common.pressure n x = 0

theorem NavierStokes.ActualSignedPhysicalZeros.cylindrical_zero_of_raw {B N0 : ℕ} (l : Label B N0) (u : CorrectionState.State Point) (n : ℕ) (z : ProblemStatement.SpaceTime) (hz : ∀ (k : TorusInverse.Frequency), (ActualSignedCoherence.copies l u).amplitude n k (ActualSignedPotentialCoherence.nativePoint n z) = 0 ∧ (ActualSignedCoherence.copies l u).pressure n k (ActualSignedPotentialCoherence.nativePoint n z) = 0) : ActualSignedPotentialCoherence.cylindricalPotential l u n z = 0 ∧ ActualSignedPotentialCoherence.cylindricalPressureMode l u n z = 0

theorem NavierStokes.ActualSignedPhysicalZeros.current_raw_zero_of_nativeQ {B N0 : ℕ} (l : Label B N0) (u : CorrectionState.State Point) (n : ℕ) (k : Frequency) (z : ProblemStatement.SpaceTime) (hr : 0 < z.2.ofLp 0) (hw : (z.1, CylindricalResidual.chart z.2) ∈ PhysicalWaveSum.preterminal) (hq : PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h (z.1, CylindricalResidual.chart z.2) / ChartScales.Q (ActualSignedPhysicalBinding.reference l) ∉ Set.Ioo (1 / 2) 2) : (ActualSignedCoherence.copies l u).amplitude n k (ActualSignedPotentialCoherence.nativePoint n z) = 0 ∧ (ActualSignedCoherence.copies l u).pressure n k (ActualSignedPotentialCoherence.nativePoint n z) = 0

theorem NavierStokes.ActualSignedPhysicalZeros.cylindricalPotential_zero_of_nativeQ {B N0 : ℕ} (l : Label B N0) (u : CorrectionState.State Point) (n : ℕ) (z : ProblemStatement.SpaceTime) (hr : 0 < z.2.ofLp 0) (hw : (z.1, CylindricalResidual.chart z.2) ∈ PhysicalWaveSum.preterminal) (hq : PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h (z.1, CylindricalResidual.chart z.2) / ChartScales.Q (ActualSignedPhysicalBinding.reference l) ∉ Set.Ioo (1 / 2) 2) : ActualSignedPotentialCoherence.cylindricalPotential l u n z = 0

theorem NavierStokes.ActualSignedPhysicalZeros.cylindricalPressureMode_zero_of_nativeQ {B N0 : ℕ} (l : Label B N0) (u : CorrectionState.State Point) (n : ℕ) (z : ProblemStatement.SpaceTime) (hr : 0 < z.2.ofLp 0) (hw : (z.1, CylindricalResidual.chart z.2) ∈ PhysicalWaveSum.preterminal) (hq : PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h (z.1, CylindricalResidual.chart z.2) / ChartScales.Q (ActualSignedPhysicalBinding.reference l) ∉ Set.Ioo (1 / 2) 2) : ActualSignedPotentialCoherence.cylindricalPressureMode l u n z = 0

The fixed physical exterior

theorem NavierStokes.ActualSignedPhysicalZeros.current_raw_zero_of_exterior {B N0 : ℕ} (l : Label B N0) (u : CorrectionState.State Point) (n : ℕ) (k : Frequency) (z : ProblemStatement.SpaceTime) (hr : 0 < z.2.ofLp 0) (hw : (z.1, CylindricalResidual.chart z.2) ∈ PhysicalWaveSum.preterminal) (hout : (z.1, CylindricalResidual.chart z.2) ∉ ActualSignedExterior.active) : (ActualSignedCoherence.copies l u).amplitude n k (ActualSignedPotentialCoherence.nativePoint n z) = 0 ∧ (ActualSignedCoherence.copies l u).pressure n k (ActualSignedPotentialCoherence.nativePoint n z) = 0

theorem NavierStokes.ActualSignedPhysicalZeros.cylindricalPotential_zero_of_exterior {B N0 : ℕ} (l : Label B N0) (u : CorrectionState.State Point) (n : ℕ) (z : ProblemStatement.SpaceTime) (hr : 0 < z.2.ofLp 0) (hw : (z.1, CylindricalResidual.chart z.2) ∈ PhysicalWaveSum.preterminal) (hout : (z.1, CylindricalResidual.chart z.2) ∉ ActualSignedExterior.active) : ActualSignedPotentialCoherence.cylindricalPotential l u n z = 0

theorem NavierStokes.ActualSignedPhysicalZeros.cylindricalPressureMode_zero_of_exterior {B N0 : ℕ} (l : Label B N0) (u : CorrectionState.State Point) (n : ℕ) (z : ProblemStatement.SpaceTime) (hr : 0 < z.2.ofLp 0) (hw : (z.1, CylindricalResidual.chart z.2) ∈ PhysicalWaveSum.preterminal) (hout : (z.1, CylindricalResidual.chart z.2) ∉ ActualSignedExterior.active) : ActualSignedPotentialCoherence.cylindricalPressureMode l u n z = 0

Finite-support sums in physical coordinates

These identities only use finite support and the literal real-coordinate maps. They let a physical wave assembly retain an unrestricted label finsum while identifying its value with the finite active-label sum.

theorem NavierStokes.SignedPhysicalSumCalculus.finsum_eq_sum_of_zero_off {α : Type u_1} {E : Type u_2} [AddCommMonoid E] (s : Finset α) (f : α → E) (hz : ∀ l ∉ s, f l = 0) : ∑ᶠ (l : α), f l = ∑ l ∈ s, f l

theorem NavierStokes.SignedPhysicalSumCalculus.sum_realCoordinate (v : HarmonicCalculus.ComplexVector) : ∑ i : Fin 3, (PhysicalWaveSum.realCoordinate i) (v i) = PhysicalCurlCovariance.realVector v

theorem NavierStokes.SignedPhysicalSumCalculus.real_finsum_eq_sum {α : Type u_1} (s : Finset α) (p : α → ℂ) (q : α → ℝ) (hz : ∀ l ∉ s, p l = 0) (hreal : ∀ (l : α), (p l).re = q l) : (∑ᶠ (l : α), p l).re = ∑ l ∈ s, q l

An unrestricted scalar-label sum becomes the finite real-part sum once the labels outside the specified finite set vanish.

theorem NavierStokes.SignedPhysicalSumCalculus.realCoordinate_finsum_eq_sum {α : Type u_1} (s : Finset α) (F : α → HarmonicCalculus.ComplexVector) (G : α → ProblemStatement.Space) (hz : ∀ l ∉ s, F l = 0) (hreal : ∀ (l : α), PhysicalCurlCovariance.realVector (F l) = G l) : ∑ i : Fin 3, (PhysicalWaveSum.realCoordinate i) (∑ᶠ (l : α), F l i) = ∑ l ∈ s, G l

Reconstructing the Euclidean vector after the componentwise label sums agrees exactly with summing the real vectors of the active labels.

@[reducible, inline]

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

Label: an abbreviation for ActualSignedPhysicalBinding.Label B N0.

Equations

• NavierStokes.ActualSignedPhysicalCoherence.Label B N0 = NavierStokes.ActualSignedPhysicalBinding.Label B N0

@[reducible, inline]

abbrev NavierStokes.ActualSignedPhysicalCoherence.Point : Type

Point: an abbreviation for ActualSignedCoherence.Point.

Equations

• NavierStokes.ActualSignedPhysicalCoherence.Point = NavierStokes.ActualSignedCoherence.Point

@[reducible, inline]

abbrev NavierStokes.ActualSignedPhysicalCoherence.FullPoint : Type

Full point: an abbreviation for ActualSignedCoherence.FullPoint.

Equations

• NavierStokes.ActualSignedPhysicalCoherence.FullPoint = NavierStokes.ActualSignedCoherence.FullPoint

@[reducible, inline]

abbrev NavierStokes.ActualSignedPhysicalCoherence.SpaceTime : Type

Space time: an abbreviation for ProblemStatement.SpaceTime.

Equations

• NavierStokes.ActualSignedPhysicalCoherence.SpaceTime = NavierStokes.ProblemStatement.SpaceTime

@[reducible, inline]

abbrev NavierStokes.ActualSignedPhysicalCoherence.Frequency : Type

Frequency: an abbreviation for TorusInverse.Frequency.

Equations

• NavierStokes.ActualSignedPhysicalCoherence.Frequency = NavierStokes.TorusInverse.Frequency

theorem NavierStokes.ActualSignedPhysicalCoherence.finsum_injective_support {α : Type u_1} {β : Type u_2} {V : Type u_3} [AddCommMonoid V] (e : α → β) (he : Function.Injective e) (f : β → V) (hz : ∀ b ∉ Set.range e, f b = 0) : ∑ᶠ (b : β), f b = ∑ᶠ (a : α), f (e a)

theorem NavierStokes.ActualSignedPhysicalCoherence.finsum_finite_support {α : Type u_1} {V : Type u_3} [AddCommMonoid V] (s : Finset α) (f : α → V) (hz : ∀ a ∉ s, f a = 0) : ∑ᶠ (a : α), f a = ∑ a ∈ s, f a

noncomputable def NavierStokes.ActualSignedPhysicalCoherence.physicalIndex {B N0 : ℕ} (l : Label B N0) : PhysicalWaveSum.WaveIndex 1

Physical index, given by ActualSignedPhysicalData.positiveIndex (ActualSignedExterior.nativeLabel l).

Equations

• NavierStokes.ActualSignedPhysicalCoherence.physicalIndex l = NavierStokes.ActualSignedPhysicalData.positiveIndex ⟨(NavierStokes.ActualSignedExterior.nativeLabel l).val, ⋯⟩

theorem NavierStokes.ActualSignedPhysicalCoherence.physicalIndex_injective {B N0 : ℕ} : Function.Injective physicalIndex

theorem NavierStokes.ActualSignedPhysicalCoherence.mem_range_physicalIndex {B N0 : ℕ} (I : PhysicalWaveSum.WaveIndex 1) : I ∈ Set.range physicalIndex ↔ I.1 ∈ ActualSignedExterior.labels B N0 ∧ ↑I.2 = 1

theorem NavierStokes.ActualSignedPhysicalCoherence.potential_amplitude_zero_unless (f : DependentSignedPhysicalFamily.Family) (i : Fin 3) (I : PhysicalWaveSum.WaveIndex 1) (hbad : I.1 ∉ f.active ∨ ↑I.2 ≠ 1) (k : Frequency) (x : PhysicalGraphBounds.LiftPoint) : (f.potentialCopies CorrectionInitialization.ActualPrimary.slots ⋯ i).amplitude k I x = 0

theorem NavierStokes.ActualSignedPhysicalCoherence.pressure_amplitude_zero_unless (f : DependentSignedPhysicalFamily.Family) (I : PhysicalWaveSum.WaveIndex 1) (hbad : I.1 ∉ f.active ∨ ↑I.2 ≠ 1) (k : Frequency) (x : PhysicalGraphBounds.LiftPoint) : (f.pressureCopies CorrectionInitialization.ActualPrimary.slots ⋯).amplitude k I x = 0

theorem NavierStokes.ActualSignedPhysicalCoherence.potential_term_zero_unless (f : DependentSignedPhysicalFamily.Family) (i : Fin 3) (I : PhysicalWaveSum.WaveIndex 1) (hbad : I.1 ∉ f.active ∨ ↑I.2 ≠ 1) (k : Frequency) (a r0 : ℝ) (w : SpaceTime) : (f.potentialCopies CorrectionInitialization.ActualPrimary.slots ⋯ i).term a CorrectionInitialization.ActualPrimary.h r0 I k w = 0

theorem NavierStokes.ActualSignedPhysicalCoherence.pressure_term_zero_unless (f : DependentSignedPhysicalFamily.Family) (I : PhysicalWaveSum.WaveIndex 1) (hbad : I.1 ∉ f.active ∨ ↑I.2 ≠ 1) (k : Frequency) (a r0 : ℝ) (w : SpaceTime) : (f.pressureCopies CorrectionInitialization.ActualPrimary.slots ⋯).term a CorrectionInitialization.ActualPrimary.h r0 I k w = 0

theorem NavierStokes.ActualSignedPhysicalCoherence.potential_sum_labels {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (i : Fin 3) (a r0 : ℝ) (w : SpaceTime) : ((ActualSignedExterior.family s).potentialCopies CorrectionInitialization.ActualPrimary.slots ⋯ i).sum a CorrectionInitialization.ActualPrimary.h r0 w = ∑ᶠ (l : Label B N0), ((ActualSignedExterior.family s).potentialCopies CorrectionInitialization.ActualPrimary.slots ⋯ i).periodized a CorrectionInitialization.ActualPrimary.h r0 (physicalIndex l) w

theorem NavierStokes.ActualSignedPhysicalCoherence.pressure_sum_labels {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (a r0 : ℝ) (w : SpaceTime) : ((ActualSignedExterior.family s).pressureCopies CorrectionInitialization.ActualPrimary.slots ⋯).sum a CorrectionInitialization.ActualPrimary.h r0 w = ∑ᶠ (l : Label B N0), ((ActualSignedExterior.family s).pressureCopies CorrectionInitialization.ActualPrimary.slots ⋯).periodized a CorrectionInitialization.ActualPrimary.h r0 (physicalIndex l) w

The exact native-to-common physical graph

theorem NavierStokes.ActualSignedPhysicalCoherence.toCommon_nativeGraph {B N0 : ℕ} (l : Label B N0) (z : SpaceTime) (hr : 0 < z.2.ofLp 0) : (ActualSignedPhysicalBinding.toCommonCylinder l) ((PhysicalResidualBridge.commonGraph (ChartScales.Q (ActualSignedPhysicalBinding.reference l)) CorrectionInitialization.ActualPrimary.h (ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (ActualSignedPhysicalBinding.reference l))).map z) = ActualSignedPotentialCoherence.nativePoint (ActualSignedPhysicalBinding.reference l) z

theorem NavierStokes.ActualSignedPhysicalCoherence.nativePoint_radius (n : ℕ) (z : SpaceTime) (hr : 0 < z.2.ofLp 0) : (ActualSignedPotentialCoherence.nativePoint n z).1.1 = ChartScales.Q n ^ (-(1 / 2)) * z.2.ofLp 0

theorem NavierStokes.ActualSignedPhysicalCoherence.nativePoint_time (n : ℕ) (z : SpaceTime) (hr : 0 < z.2.ofLp 0) : (ActualSignedPotentialCoherence.nativePoint n z).1.2.1.1 = (1 - z.1) / ChartScales.Q n

theorem NavierStokes.ActualSignedPhysicalCoherence.reference_cutoff_formula {B N0 : ℕ} (l : Label B N0) (P : SignedStressPrimitive.Patch) (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion P.a P.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion P.a P.b u.pressure) (k : Frequency) (x : FullPoint) : (ActualSignedPhysicalBinding.referenceCopies l P u H hp).cutoff (ActualSignedPhysicalBinding.reference l) k x = ActualSignedPhysicalData.waveMask CorrectionInitialization.ActualPrimary.slots (ActualSignedPhysicalBinding.spatialLabel l) ((ActualSignedPhysicalData.geometry CorrectionInitialization.ActualPrimary.slots (ActualSignedPhysicalBinding.spatialLabel l) 0).coordinates k x.1.2.2)

theorem NavierStokes.ActualSignedPhysicalCoherence.reference_raw_amplitude {B N0 : ℕ} (l : Label B N0) (P : SignedStressPrimitive.Patch) (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion P.a P.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion P.a P.b u.pressure) (x : FullPoint) : (ActualSignedPhysicalBinding.referenceCopies l P u H hp).common.amplitude (ActualSignedPhysicalBinding.reference l) x = (ActualPeriodizedSignedRealization.periodizedPrimary (ActualSignedPhysicalBinding.primary l) (ActualSignedPhysicalBinding.layout l)).raw (ActualSignedPhysicalBinding.nativeStateData l P u H hp).referenceRequest l.2 (ActualSignedPhysicalBinding.reference l) x

theorem NavierStokes.ActualSignedPhysicalCoherence.reference_raw_pressure {B N0 : ℕ} (l : Label B N0) (P : SignedStressPrimitive.Patch) (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion P.a P.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion P.a P.b u.pressure) (x : FullPoint) : (ActualSignedPhysicalBinding.referenceCopies l P u H hp).common.pressure (ActualSignedPhysicalBinding.reference l) x = (ActualPeriodizedSignedRealization.periodizedPrimary (ActualSignedPhysicalBinding.primary l) (ActualSignedPhysicalBinding.layout l)).rawPressure (ActualSignedPhysicalBinding.nativeStateData l P u H hp).referenceRequest l.2 (ActualSignedPhysicalBinding.reference l) x

theorem NavierStokes.ActualSignedPhysicalCoherence.reference_vectorMode {B N0 : ℕ} (l : Label B N0) (P : SignedStressPrimitive.Patch) (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion P.a P.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion P.a P.b u.pressure) (x : FullPoint) : HarmonicCalculus.vectorMode ((ActualSignedPhysicalBinding.primary l).base.frequency (ActualSignedPhysicalBinding.reference l)) ((ActualSignedPhysicalBinding.primary l).base.phase (ActualSignedPhysicalBinding.reference l)) (fun (y : PhysicalSignedWave.Cylinder) => CurlClassBounds.inverseCarrier ((ActualSignedPhysicalBinding.primary l).base.frequency (ActualSignedPhysicalBinding.reference l)) • CurlClassBounds.normalCoefficient ((ActualSignedPhysicalBinding.primary l).base.normal (ActualSignedPhysicalBinding.primary l).strip (ActualSignedPhysicalBinding.primary l).directions (ActualSignedPhysicalBinding.reference l) y) ((ActualPeriodizedSignedRealization.periodizedPrimary (ActualSignedPhysicalBinding.primary l) (ActualSignedPhysicalBinding.layout l)).raw (ActualSignedPhysicalBinding.nativeStateData l P u H hp).referenceRequest l.2 (ActualSignedPhysicalBinding.reference l) y)) x = (ActualSignedPhysicalBinding.referenceCopies l P u H hp).common.curlPotential (ActualSignedPhysicalBinding.primary l).strip (ActualSignedPhysicalBinding.primary l).directions (ActualSignedPhysicalBinding.reference l) x

theorem NavierStokes.ActualSignedPhysicalCoherence.reference_pressureMode {B N0 : ℕ} (l : Label B N0) (P : SignedStressPrimitive.Patch) (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion P.a P.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion P.a P.b u.pressure) (x : FullPoint) : HarmonicCalculus.mode ((ActualSignedPhysicalBinding.primary l).base.frequency (ActualSignedPhysicalBinding.reference l)) ((ActualSignedPhysicalBinding.primary l).base.phase (ActualSignedPhysicalBinding.reference l)) ((ActualPeriodizedSignedRealization.periodizedPrimary (ActualSignedPhysicalBinding.primary l) (ActualSignedPhysicalBinding.layout l)).rawPressure (ActualSignedPhysicalBinding.nativeStateData l P u H hp).referenceRequest l.2 (ActualSignedPhysicalBinding.reference l)) x = HarmonicCalculus.mode ((ActualSignedPhysicalBinding.referenceCopies l P u H hp).common.frequency (ActualSignedPhysicalBinding.reference l)) ((ActualSignedPhysicalBinding.referenceCopies l P u H hp).common.phase (ActualSignedPhysicalBinding.reference l)) ((ActualSignedPhysicalBinding.referenceCopies l P u H hp).common.pressure (ActualSignedPhysicalBinding.reference l)) x

noncomputable def NavierStokes.ActualSignedPhysicalCoherence.measuredStates {B N0 : ℕ} (P : SignedStressPrimitive.Patch) (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion P.a P.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion P.a P.b u.pressure) (l : Label B N0) : (ActualSignedPhysicalBinding.nativeViews l).StateData

Measured states, defined pointwise by ActualSignedPhysicalBinding.nativeStateData l P u H hp.

Equations

• NavierStokes.ActualSignedPhysicalCoherence.measuredStates P u H hp l = NavierStokes.ActualSignedPhysicalBinding.nativeStateData l P u H hp

noncomputable def NavierStokes.ActualSignedPhysicalCoherence.singletonVectorMode {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (l : Label B N0) (x : FullPoint) : HarmonicCalculus.ComplexVector

Singleton vector mode as an element of ComplexVector.

Equations

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

noncomputable def NavierStokes.ActualSignedPhysicalCoherence.singletonPressureMode {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (l : Label B N0) (x : FullPoint) : ℂ

Singleton pressure mode as an element of ℂ.

Equations

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

theorem NavierStokes.ActualSignedPhysicalCoherence.singletonVectorMode_eq {B N0 : ℕ} (l : Label B N0) (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b u.pressure) (x : FullPoint) : singletonVectorMode (measuredStates ActualInitialization.patch u H hp) l x = ActualSignedPotentialCoherence.potential l u (ActualSignedPhysicalBinding.reference l) ((ActualSignedPhysicalBinding.toCommonCylinder l) x)

theorem NavierStokes.ActualSignedPhysicalCoherence.singletonPressureMode_eq {B N0 : ℕ} (l : Label B N0) (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b u.pressure) (x : FullPoint) : singletonPressureMode (measuredStates ActualInitialization.patch u H hp) l x = ActualSignedPotentialCoherence.pressureMode l u (ActualSignedPhysicalBinding.reference l) ((ActualSignedPhysicalBinding.toCommonCylinder l) x)

noncomputable def NavierStokes.ActualSignedPhysicalCoherence.canonicalPotential {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (l : Label B N0) (w : SpaceTime) : HarmonicCalculus.ComplexVector

Canonical potential as an element of ComplexVector.

Equations

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

noncomputable def NavierStokes.ActualSignedPhysicalCoherence.canonicalPressure {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (l : Label B N0) (w : SpaceTime) : ℂ

Canonical pressure as an element of ℂ.

Equations

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

theorem NavierStokes.ActualSignedPhysicalCoherence.canonicalPotential_native {B N0 : ℕ} (l : Label B N0) (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b u.pressure) (w : SpaceTime) (j : PolarCharts.Index) (hw : (PhysicalGraphBounds.scaledRadial (ActualSignedPhysicalBinding.reference l)) w ∈ PhysicalGraphBounds.annulus ActualPolarCoverage.inner ActualPolarCoverage.outer) (hj : (PhysicalGraphBounds.scaledRadial (ActualSignedPhysicalBinding.reference l)) w ∈ PolarCharts.chartDomain ActualPolarCoverage.inner j) : canonicalPotential (measuredStates ActualInitialization.patch u H hp) l w = ActualSignedPhysicalData.rotateCoefficient ((PhysicalGraphBounds.scaledRadial (ActualSignedPhysicalBinding.reference l)) w) (ActualSignedPotentialCoherence.cylindricalPotential l u (ActualSignedPhysicalBinding.reference l) (PhysicalCurlCovariance.polarCoordinates (ActualSignedPhysicalGeometry.chartRadius ActualPolarCoverage.inner (ActualSignedPhysicalBinding.reference l)) j w))

theorem NavierStokes.ActualSignedPhysicalCoherence.canonicalPressure_native {B N0 : ℕ} (l : Label B N0) (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b u.pressure) (w : SpaceTime) (j : PolarCharts.Index) (hw : (PhysicalGraphBounds.scaledRadial (ActualSignedPhysicalBinding.reference l)) w ∈ PhysicalGraphBounds.annulus ActualPolarCoverage.inner ActualPolarCoverage.outer) (hj : (PhysicalGraphBounds.scaledRadial (ActualSignedPhysicalBinding.reference l)) w ∈ PolarCharts.chartDomain ActualPolarCoverage.inner j) : canonicalPressure (measuredStates ActualInitialization.patch u H hp) l w = ActualSignedPotentialCoherence.cylindricalPressureMode l u (ActualSignedPhysicalBinding.reference l) (PhysicalCurlCovariance.polarCoordinates (ActualSignedPhysicalGeometry.chartRadius ActualPolarCoverage.inner (ActualSignedPhysicalBinding.reference l)) j w)

The two literal zero cases, including both native dyadic faces

theorem NavierStokes.ActualSignedPhysicalCoherence.canonical_current_zero {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (l : Label B N0) (u : CorrectionState.State Point) (n : ℕ) (w z : SpaceTime) (hr : 0 < z.2.ofLp 0) (he : (z.1, CylindricalResidual.chart z.2) = w) (hw : w ∈ PhysicalWaveSum.preterminal) (hbad : w ∉ ActualSignedExterior.active ∨ PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w / ChartScales.Q (ActualSignedPhysicalBinding.reference l) ∉ Set.Ioo (1 / 2) 2) : canonicalPotential s l w = 0 ∧ canonicalPressure s l w = 0 ∧ ActualSignedPotentialCoherence.cylindricalPotential l u n z = 0 ∧ ActualSignedPotentialCoherence.cylindricalPressureMode l u n z = 0

theorem NavierStokes.ActualSignedPhysicalCoherence.current_chart_ratio (n : ℕ) {qbig a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) {w : SpaceTime} (hw : w ∈ ActualPhysicalPrefixFields.cartesianChartDomain qbig n a i) : PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w / ChartScales.Q n ∈ Set.Ioo (1 / 2) 2

theorem NavierStokes.ActualSignedPhysicalCoherence.canonical_current_values {B N0 : ℕ} (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b u.pressure) (hfixed : (VariableGaugeMean.reconstructState ActualInitialization.geometry.gauge (CorrectionInitialization.ActualPrimary.commonContext B) u).pressure = u.pressure) (HS : ∀ (n m k : ℕ), CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m → PhysicalResidualNaturality.StateOn (PhysicalMeanDomain.slowDomain (ActualInitialCoherence.overlap n m)) (GaugeStateCoherence.bandChartEquiv CorrectionInitialization.ActualPrimary.h n m k) (GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m) (GaugeStateCoherence.bandScale n m) u u n m) (l : Label B N0) (n : ℕ) {qbig a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) {w : SpaceTime} (hw : w ∈ ActualPhysicalPrefixFields.cartesianChartDomain qbig n a i) : PhysicalCurlCovariance.realVector (canonicalPotential (measuredStates ActualInitialization.patch u H hp) l w) = CurrentSignedCurl.currentPotential l u n a i w ∧ (canonicalPressure (measuredStates ActualInitialization.patch u H hp) l w).re = CurrentSignedCurl.currentPressure l u n a i w ∧ (l ∉ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n → canonicalPotential (measuredStates ActualInitialization.patch u H hp) l w = 0 ∧ canonicalPressure (measuredStates ActualInitialization.patch u H hp) l w = 0)

The physical copy sum has the current-band value. The last conclusion is complex-valued: it justifies truncating the original complex sum before taking real parts.

theorem NavierStokes.ActualSignedPhysicalCoherence.measuredPotential_eq_sum {B N0 : ℕ} (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b u.pressure) (hfixed : (VariableGaugeMean.reconstructState ActualInitialization.geometry.gauge (CorrectionInitialization.ActualPrimary.commonContext B) u).pressure = u.pressure) (HS : ∀ (n m k : ℕ), CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m → PhysicalResidualNaturality.StateOn (PhysicalMeanDomain.slowDomain (ActualInitialCoherence.overlap n m)) (GaugeStateCoherence.bandChartEquiv CorrectionInitialization.ActualPrimary.h n m k) (GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m) (GaugeStateCoherence.bandScale n m) u u n m) (v : CorrectionStep.CycleCoefficients (Label B N0)) (hlabels : v.labels = CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0) (n : ℕ) {qbig a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) {w : SpaceTime} (hw : w ∈ ActualPhysicalPrefixFields.cartesianChartDomain qbig n a i) : ActualSignedExterior.potential (measuredStates ActualInitialization.patch u H hp) w = ∑ l ∈ v.labels n, CurrentSignedCurl.currentPotential l u n a i w

theorem NavierStokes.ActualSignedPhysicalCoherence.measuredPressure_eq_sum {B N0 : ℕ} (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b u.pressure) (hfixed : (VariableGaugeMean.reconstructState ActualInitialization.geometry.gauge (CorrectionInitialization.ActualPrimary.commonContext B) u).pressure = u.pressure) (HS : ∀ (n m k : ℕ), CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m → PhysicalResidualNaturality.StateOn (PhysicalMeanDomain.slowDomain (ActualInitialCoherence.overlap n m)) (GaugeStateCoherence.bandChartEquiv CorrectionInitialization.ActualPrimary.h n m k) (GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m) (GaugeStateCoherence.bandScale n m) u u n m) (v : CorrectionStep.CycleCoefficients (Label B N0)) (hlabels : v.labels = CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0) (n : ℕ) {qbig a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) {w : SpaceTime} (hw : w ∈ ActualPhysicalPrefixFields.cartesianChartDomain qbig n a i) : ActualSignedExterior.pressure (measuredStates ActualInitialization.patch u H hp) w = ∑ l ∈ v.labels n, CurrentSignedCurl.currentPressure l u n a i w

theorem NavierStokes.ActualSignedPhysicalCoherence.measuredPotential_germ {B N0 : ℕ} (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b u.pressure) (hfixed : (VariableGaugeMean.reconstructState ActualInitialization.geometry.gauge (CorrectionInitialization.ActualPrimary.commonContext B) u).pressure = u.pressure) (HS : ∀ (n m k : ℕ), CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m → PhysicalResidualNaturality.StateOn (PhysicalMeanDomain.slowDomain (ActualInitialCoherence.overlap n m)) (GaugeStateCoherence.bandChartEquiv CorrectionInitialization.ActualPrimary.h n m k) (GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m) (GaugeStateCoherence.bandScale n m) u u n m) (v : CorrectionStep.CycleCoefficients (Label B N0)) (hlabels : v.labels = CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0) (n : ℕ) {qbig a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) {w : SpaceTime} (hw : w ∈ ActualPhysicalPrefixFields.cartesianChartDomain qbig n a i) : ActualSignedExterior.potential (measuredStates ActualInitialization.patch u H hp) =ᶠ[nhds w] fun (z : SpaceTime) => ∑ l ∈ v.labels n, CurrentSignedCurl.currentPotential l u n a i z

theorem NavierStokes.ActualSignedPhysicalCoherence.measuredPressure_germ {B N0 : ℕ} (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b u.pressure) (hfixed : (VariableGaugeMean.reconstructState ActualInitialization.geometry.gauge (CorrectionInitialization.ActualPrimary.commonContext B) u).pressure = u.pressure) (HS : ∀ (n m k : ℕ), CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m → PhysicalResidualNaturality.StateOn (PhysicalMeanDomain.slowDomain (ActualInitialCoherence.overlap n m)) (GaugeStateCoherence.bandChartEquiv CorrectionInitialization.ActualPrimary.h n m k) (GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m) (GaugeStateCoherence.bandScale n m) u u n m) (v : CorrectionStep.CycleCoefficients (Label B N0)) (hlabels : v.labels = CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0) (n : ℕ) {qbig a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) {w : SpaceTime} (hw : w ∈ ActualPhysicalPrefixFields.cartesianChartDomain qbig n a i) : ActualSignedExterior.pressure (measuredStates ActualInitialization.patch u H hp) =ᶠ[nhds w] fun (z : SpaceTime) => ∑ l ∈ v.labels n, CurrentSignedCurl.currentPressure l u n a i z

theorem NavierStokes.ActualSignedPhysicalCoherence.measuredPotential_curl {B N0 : ℕ} (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b u.pressure) (hfixed : (VariableGaugeMean.reconstructState ActualInitialization.geometry.gauge (CorrectionInitialization.ActualPrimary.commonContext B) u).pressure = u.pressure) (HS : ∀ (n m k : ℕ), CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m → PhysicalResidualNaturality.StateOn (PhysicalMeanDomain.slowDomain (ActualInitialCoherence.overlap n m)) (GaugeStateCoherence.bandChartEquiv CorrectionInitialization.ActualPrimary.h n m k) (GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m) (GaugeStateCoherence.bandScale n m) u u n m) (v : CorrectionStep.CycleCoefficients (Label B N0)) (hlabels : v.labels = CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0) (n : ℕ) {α : ℝ} (hamp : ∀ l ∈ v.labels n, CurrentSignedCurl.AmplitudeBound l u α) {qbig a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) : Set.EqOn (SpatialCurl.spatialCurl (ActualSignedExterior.potential (measuredStates ActualInitialization.patch u H hp))) ((CyclePhysicalPrefixes.polarVelocityMap a i) ((CyclePhysicalPrefixes.velocityMap (ActualCycleResidualBounds.actualBandGraph n)) (∑ l ∈ v.labels n, ((ActualSignedStageControls.parameters l).exactBlock ActualInitialization.geometry.strip (ActualSignedCoherence.request B u)).oscillation n))) (ActualPhysicalPrefixFields.cartesianChartDomain qbig n a i)

theorem NavierStokes.ActualSignedPhysicalCoherence.measuredPressure_eq {B N0 : ℕ} (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b u.pressure) (hfixed : (VariableGaugeMean.reconstructState ActualInitialization.geometry.gauge (CorrectionInitialization.ActualPrimary.commonContext B) u).pressure = u.pressure) (HS : ∀ (n m k : ℕ), CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m → PhysicalResidualNaturality.StateOn (PhysicalMeanDomain.slowDomain (ActualInitialCoherence.overlap n m)) (GaugeStateCoherence.bandChartEquiv CorrectionInitialization.ActualPrimary.h n m k) (GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m) (GaugeStateCoherence.bandScale n m) u u n m) (v : CorrectionStep.CycleCoefficients (Label B N0)) (hlabels : v.labels = CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0) (n : ℕ) {qbig a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) : Set.EqOn (ActualSignedExterior.pressure (measuredStates ActualInitialization.patch u H hp)) ((CyclePhysicalPrefixes.polarPressureMap a i) ((CyclePhysicalPrefixes.pressureMap (ActualCycleResidualBounds.actualBandGraph n)) (∑ l ∈ v.labels n, ((ActualSignedStageControls.parameters l).exactBlock ActualInitialization.geometry.strip (ActualSignedCoherence.request B u)).oscillatoryPressure n))) (ActualPhysicalPrefixFields.cartesianChartDomain qbig n a i)

The literal correction cycle's physical fields

noncomputable def NavierStokes.ActualSignedPhysicalCoherence.cycleInput {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) : CorrectionState.State Point

Cycle input, given by (ActualCycleParameters.fixedParameters B N0).afterParticular x.coefficients (commonContext B) x.state.

Equations

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

theorem NavierStokes.ActualSignedPhysicalCoherence.cyclePotential_curl {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (Hu : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b (CorrectionInitialization.ActualPrimary.commonContext B) (cycleInput x)) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b (cycleInput x).pressure) (hfixed : (VariableGaugeMean.reconstructState ActualInitialization.geometry.gauge (CorrectionInitialization.ActualPrimary.commonContext B) (cycleInput x)).pressure = (cycleInput x).pressure) (HS : ∀ (n m k : ℕ), CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m → PhysicalResidualNaturality.StateOn (PhysicalMeanDomain.slowDomain (ActualInitialCoherence.overlap n m)) (GaugeStateCoherence.bandChartEquiv CorrectionInitialization.ActualPrimary.h n m k) (GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m) (GaugeStateCoherence.bandScale n m) (cycleInput x) (cycleInput x) n m) (hlabels : x.coefficients.labels = CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0) (n : ℕ) {α : ℝ} (hamp : ∀ l ∈ x.coefficients.labels n, CurrentSignedCurl.AmplitudeBound l (cycleInput x) α) {qbig a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) : Set.EqOn (SpatialCurl.spatialCurl (ActualSignedExterior.cyclePotential x Hu hp)) ((CyclePhysicalPrefixes.polarVelocityMap a i) ((CyclePhysicalPrefixes.velocityMap (ActualCycleResidualBounds.actualBandGraph n)) ((ActualCycleParameters.fixedParameters B N0).signedVelocity x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state n))) (ActualPhysicalPrefixFields.cartesianChartDomain qbig n a i)

Curl is taken only after equality of the canonical physical potential on an open neighborhood has been proved. The sole analytic bound concerns the actual current common amplitude.

theorem NavierStokes.ActualSignedPhysicalCoherence.cyclePressure_eq {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (Hu : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b (CorrectionInitialization.ActualPrimary.commonContext B) (cycleInput x)) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b (cycleInput x).pressure) (hfixed : (VariableGaugeMean.reconstructState ActualInitialization.geometry.gauge (CorrectionInitialization.ActualPrimary.commonContext B) (cycleInput x)).pressure = (cycleInput x).pressure) (HS : ∀ (n m k : ℕ), CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m → PhysicalResidualNaturality.StateOn (PhysicalMeanDomain.slowDomain (ActualInitialCoherence.overlap n m)) (GaugeStateCoherence.bandChartEquiv CorrectionInitialization.ActualPrimary.h n m k) (GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m) (GaugeStateCoherence.bandScale n m) (cycleInput x) (cycleInput x) n m) (hlabels : x.coefficients.labels = CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0) (n : ℕ) {qbig a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) : Set.EqOn (ActualSignedExterior.cyclePressure x Hu hp) ((CyclePhysicalPrefixes.polarPressureMap a i) ((CyclePhysicalPrefixes.pressureMap (ActualCycleResidualBounds.actualBandGraph n)) ((ActualCycleParameters.fixedParameters B N0).signedPressure x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state n))) (ActualPhysicalPrefixFields.cartesianChartDomain qbig n a i)

The canonical physical pressure is the same finite signed pressure sum used by the current correction state.