Current-band signed vector potentials and pressure modes

The potential is formed from the literal current common signed coefficient, after its native cutoffs and copy sum. Its scale follows from the actual normal, amplitude and carrier identities, before any physical curl is taken.

@[reducible, inline]

abbrev NavierStokes.ActualSignedPotentialCoherence.Point : Type

Point: an abbreviation for ActualSignedCoherence.Point.

Equations

• NavierStokes.ActualSignedPotentialCoherence.Point = NavierStokes.ActualSignedCoherence.Point

@[reducible, inline]

abbrev NavierStokes.ActualSignedPotentialCoherence.FullPoint : Type

Full point: an abbreviation for ActualSignedCoherence.FullPoint.

Equations

• NavierStokes.ActualSignedPotentialCoherence.FullPoint = NavierStokes.ActualSignedCoherence.FullPoint

noncomputable def NavierStokes.ActualSignedPotentialCoherence.potentialCoefficient {B N0 : ℕ} (l : ActualSignedCoherence.SignedLabel B N0) (u : CorrectionState.State Point) (n : ℕ) (x : FullPoint) : HarmonicCalculus.ComplexVector

The coefficient of the literal current-band vector potential.

Equations

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

noncomputable def NavierStokes.ActualSignedPotentialCoherence.potential {B N0 : ℕ} (l : ActualSignedCoherence.SignedLabel B N0) (u : CorrectionState.State Point) (n : ℕ) : FullPoint → HarmonicCalculus.ComplexVector

The actual current common coefficient's curl potential.

Equations

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

noncomputable def NavierStokes.ActualSignedPotentialCoherence.pressureMode {B N0 : ℕ} (l : ActualSignedCoherence.SignedLabel B N0) (u : CorrectionState.State Point) (n : ℕ) : FullPoint → ℂ

The actual current common pressure, with its carrier retained.

Equations

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

theorem NavierStokes.ActualSignedPotentialCoherence.potential_eq_mode {B N0 : ℕ} (l : ActualSignedCoherence.SignedLabel B N0) (u : CorrectionState.State Point) (n : ℕ) : potential l u n = HarmonicCalculus.vectorMode ((ActualSignedCoherence.copies l u).common.frequency n) ((ActualSignedCoherence.copies l u).common.phase n) (potentialCoefficient l u n)

theorem NavierStokes.ActualSignedPotentialCoherence.potential_eq_curlPotential {B N0 : ℕ} (l : ActualSignedCoherence.SignedLabel B N0) (u : CorrectionState.State Point) (n : ℕ) : potential l u n = (ActualSignedCoherence.copies l u).common.curlPotential ActualSignedCoherence.fullStrip (ActualSignedStageControls.directions B) n

theorem NavierStokes.ActualSignedPotentialCoherence.potential_weight (n m : ℕ) : GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m / GaugeStateCoherence.bandScale n m = PhysicalParticularWave.ratioPower (ChartScales.Q n) (ChartScales.Q m) CorrectionInitialization.ActualPrimary.h

theorem NavierStokes.ActualSignedPotentialCoherence.pressure_weight (n m : ℕ) : GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m * GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m = PhysicalParticularWave.pressureWeight CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (ChartScales.Q m)

theorem NavierStokes.ActualSignedPotentialCoherence.potentialCoefficient_of_request {B N0 : ℕ} (l : ActualSignedCoherence.SignedLabel B N0) (u : CorrectionState.State Point) (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) (x : FullPoint) (hR : ActualSignedCoherence.request B u n x = ActualSignedCoherence.coefficientWeight n m ^ 2 • ActualSignedCoherence.request B u m ((ActualSignedCoherence.chart n m k) x)) : potentialCoefficient l u n x = (GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m / GaugeStateCoherence.bandScale n m) • potentialCoefficient l u m ((ActualSignedCoherence.chart n m k) x)

The inverse carrier cancels the phase scale, leaving velocity divided by radial scale. No smoothness or nonzero-normal assumption is introduced.

theorem NavierStokes.ActualSignedPotentialCoherence.potential_of_request {B N0 : ℕ} (l : ActualSignedCoherence.SignedLabel B N0) (u : CorrectionState.State Point) (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) (x : FullPoint) (hR : ActualSignedCoherence.request B u n x = ActualSignedCoherence.coefficientWeight n m ^ 2 • ActualSignedCoherence.request B u m ((ActualSignedCoherence.chart n m k) x)) : potential l u n x = (GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m / GaugeStateCoherence.bandScale n m) • potential l u m ((ActualSignedCoherence.chart n m k) x)

theorem NavierStokes.ActualSignedPotentialCoherence.pressureMode_of_request {B N0 : ℕ} (l : ActualSignedCoherence.SignedLabel B N0) (u : CorrectionState.State Point) (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) (x : FullPoint) (hR : ActualSignedCoherence.request B u n x = ActualSignedCoherence.coefficientWeight n m ^ 2 • ActualSignedCoherence.request B u m ((ActualSignedCoherence.chart n m k) x)) : pressureMode l u n x = (GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m * GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m) • pressureMode l u m ((ActualSignedCoherence.chart n m k) x)

noncomputable def NavierStokes.ActualSignedPotentialCoherence.rescaledPotential {B N0 : ℕ} (l : ActualSignedCoherence.SignedLabel B N0) (u : CorrectionState.State Point) (n : ℕ) (x : FullPoint) : HarmonicCalculus.ComplexVector

The physical power of the potential, before choosing any physical graph.

Equations

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

noncomputable def NavierStokes.ActualSignedPotentialCoherence.rescaledPressureMode {B N0 : ℕ} (l : ActualSignedCoherence.SignedLabel B N0) (u : CorrectionState.State Point) (n : ℕ) (x : FullPoint) : ℂ

Rescaled pressure mode, given by ChartScales.Q n ^ (-(2 * CoordinateAlgebra.A h)) • pressureMode l u n x.

Equations

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

theorem NavierStokes.ActualSignedPotentialCoherence.potential_transport {B N0 : ℕ} (l : ActualSignedCoherence.SignedLabel B N0) (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData ActualInitialization.geometry.region ActualInitialization.geometry.patch.a ActualInitialization.geometry.patch.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hfixed : (VariableGaugeMean.reconstructState ActualInitialization.geometry.gauge (CorrectionInitialization.ActualPrimary.commonContext B) u).pressure = u.pressure) (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) (HS : 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) (x : FullPoint) (hx : x.1.2.1 ∈ ActualInitialCoherence.overlap n m) : potential l u n x = (GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m / GaugeStateCoherence.bandScale n m) • potential l u m ((ActualSignedCoherence.chart n m k) x)

theorem NavierStokes.ActualSignedPotentialCoherence.pressureMode_transport {B N0 : ℕ} (l : ActualSignedCoherence.SignedLabel B N0) (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData ActualInitialization.geometry.region ActualInitialization.geometry.patch.a ActualInitialization.geometry.patch.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hfixed : (VariableGaugeMean.reconstructState ActualInitialization.geometry.gauge (CorrectionInitialization.ActualPrimary.commonContext B) u).pressure = u.pressure) (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) (HS : 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) (x : FullPoint) (hx : x.1.2.1 ∈ ActualInitialCoherence.overlap n m) : pressureMode l u n x = (GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m * GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m) • pressureMode l u m ((ActualSignedCoherence.chart n m k) x)

theorem NavierStokes.ActualSignedPotentialCoherence.potential_transport_weight {B N0 : ℕ} (l : ActualSignedCoherence.SignedLabel B N0) (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData ActualInitialization.geometry.region ActualInitialization.geometry.patch.a ActualInitialization.geometry.patch.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hfixed : (VariableGaugeMean.reconstructState ActualInitialization.geometry.gauge (CorrectionInitialization.ActualPrimary.commonContext B) u).pressure = u.pressure) (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) (HS : 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) (x : FullPoint) (hx : x.1.2.1 ∈ ActualInitialCoherence.overlap n m) : potential l u n x = PhysicalParticularWave.ratioPower (ChartScales.Q n) (ChartScales.Q m) CorrectionInitialization.ActualPrimary.h • potential l u m ((ActualSignedCoherence.chart n m k) x)

theorem NavierStokes.ActualSignedPotentialCoherence.pressureMode_transport_weight {B N0 : ℕ} (l : ActualSignedCoherence.SignedLabel B N0) (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData ActualInitialization.geometry.region ActualInitialization.geometry.patch.a ActualInitialization.geometry.patch.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hfixed : (VariableGaugeMean.reconstructState ActualInitialization.geometry.gauge (CorrectionInitialization.ActualPrimary.commonContext B) u).pressure = u.pressure) (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) (HS : 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) (x : FullPoint) (hx : x.1.2.1 ∈ ActualInitialCoherence.overlap n m) : pressureMode l u n x = PhysicalParticularWave.pressureWeight CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (ChartScales.Q m) • pressureMode l u m ((ActualSignedCoherence.chart n m k) x)

theorem NavierStokes.ActualSignedPotentialCoherence.rescaledPotential_transport {B N0 : ℕ} (l : ActualSignedCoherence.SignedLabel B N0) (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData ActualInitialization.geometry.region ActualInitialization.geometry.patch.a ActualInitialization.geometry.patch.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hfixed : (VariableGaugeMean.reconstructState ActualInitialization.geometry.gauge (CorrectionInitialization.ActualPrimary.commonContext B) u).pressure = u.pressure) (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) (HS : 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) (x : FullPoint) (hx : x.1.2.1 ∈ ActualInitialCoherence.overlap n m) : rescaledPotential l u n x = rescaledPotential l u m ((ActualSignedCoherence.chart n m k) x)

theorem NavierStokes.ActualSignedPotentialCoherence.rescaledPressureMode_transport {B N0 : ℕ} (l : ActualSignedCoherence.SignedLabel B N0) (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData ActualInitialization.geometry.region ActualInitialization.geometry.patch.a ActualInitialization.geometry.patch.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hfixed : (VariableGaugeMean.reconstructState ActualInitialization.geometry.gauge (CorrectionInitialization.ActualPrimary.commonContext B) u).pressure = u.pressure) (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) (HS : 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) (x : FullPoint) (hx : x.1.2.1 ∈ ActualInitialCoherence.overlap n m) : rescaledPressureMode l u n x = rescaledPressureMode l u m ((ActualSignedCoherence.chart n m k) x)

theorem NavierStokes.ActualSignedPotentialCoherence.potential_transport_germ {B N0 : ℕ} (l : ActualSignedCoherence.SignedLabel B N0) (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData ActualInitialization.geometry.region ActualInitialization.geometry.patch.a ActualInitialization.geometry.patch.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hfixed : (VariableGaugeMean.reconstructState ActualInitialization.geometry.gauge (CorrectionInitialization.ActualPrimary.commonContext B) u).pressure = u.pressure) (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) (HS : 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) (x : FullPoint) (hx : x.1.2.1 ∈ ActualInitialCoherence.overlap n m) : potential l u n =ᶠ[nhds x] fun (y : FullPoint) => (GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m / GaugeStateCoherence.bandScale n m) • potential l u m ((ActualSignedCoherence.chart n m k) y)

theorem NavierStokes.ActualSignedPotentialCoherence.pressureMode_transport_germ {B N0 : ℕ} (l : ActualSignedCoherence.SignedLabel B N0) (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData ActualInitialization.geometry.region ActualInitialization.geometry.patch.a ActualInitialization.geometry.patch.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hfixed : (VariableGaugeMean.reconstructState ActualInitialization.geometry.gauge (CorrectionInitialization.ActualPrimary.commonContext B) u).pressure = u.pressure) (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) (HS : 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) (x : FullPoint) (hx : x.1.2.1 ∈ ActualInitialCoherence.overlap n m) : pressureMode l u n =ᶠ[nhds x] fun (y : FullPoint) => (GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m * GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m) • pressureMode l u m ((ActualSignedCoherence.chart n m k) y)

theorem NavierStokes.ActualSignedPotentialCoherence.rescaledPotential_transport_germ {B N0 : ℕ} (l : ActualSignedCoherence.SignedLabel B N0) (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData ActualInitialization.geometry.region ActualInitialization.geometry.patch.a ActualInitialization.geometry.patch.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hfixed : (VariableGaugeMean.reconstructState ActualInitialization.geometry.gauge (CorrectionInitialization.ActualPrimary.commonContext B) u).pressure = u.pressure) (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) (HS : 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) (x : FullPoint) (hx : x.1.2.1 ∈ ActualInitialCoherence.overlap n m) : rescaledPotential l u n =ᶠ[nhds x] fun (y : FullPoint) => rescaledPotential l u m ((ActualSignedCoherence.chart n m k) y)

theorem NavierStokes.ActualSignedPotentialCoherence.rescaledPressureMode_transport_germ {B N0 : ℕ} (l : ActualSignedCoherence.SignedLabel B N0) (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData ActualInitialization.geometry.region ActualInitialization.geometry.patch.a ActualInitialization.geometry.patch.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hfixed : (VariableGaugeMean.reconstructState ActualInitialization.geometry.gauge (CorrectionInitialization.ActualPrimary.commonContext B) u).pressure = u.pressure) (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) (HS : 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) (x : FullPoint) (hx : x.1.2.1 ∈ ActualInitialCoherence.overlap n m) : rescaledPressureMode l u n =ᶠ[nhds x] fun (y : FullPoint) => rescaledPressureMode l u m ((ActualSignedCoherence.chart n m k) y)

Comparing any two valid current-band representatives

theorem NavierStokes.ActualSignedPotentialCoherence.chart_eq_of_absolute (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) (x y : FullPoint) (hxy : (ActualPrimaryCoherence.absoluteChart n) x = (ActualPrimaryCoherence.absoluteChart m) y) : (ActualSignedCoherence.chart n m k) x = y

theorem NavierStokes.ActualSignedPotentialCoherence.rescaled_eq_of_absolute_of_index {B N0 : ℕ} (l : ActualSignedCoherence.SignedLabel B N0) (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData ActualInitialization.geometry.region ActualInitialization.geometry.patch.a ActualInitialization.geometry.patch.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hfixed : (VariableGaugeMean.reconstructState ActualInitialization.geometry.gauge (CorrectionInitialization.ActualPrimary.commonContext B) u).pressure = u.pressure) (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) (HS : 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) (x y : FullPoint) (hx : x.1.2.1 ∈ CorrectionInitialization.ActualPrimary.standardRegion.carrier) (hy : y.1.2.1 ∈ CorrectionInitialization.ActualPrimary.standardRegion.carrier) (hxy : (ActualPrimaryCoherence.absoluteChart n) x = (ActualPrimaryCoherence.absoluteChart m) y) : rescaledPotential l u n x = rescaledPotential l u m y ∧ rescaledPressureMode l u n x = rescaledPressureMode l u m y

theorem NavierStokes.ActualSignedPotentialCoherence.rescaled_eq_of_absolute {B N0 : ℕ} (l : ActualSignedCoherence.SignedLabel B N0) (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData ActualInitialization.geometry.region ActualInitialization.geometry.patch.a ActualInitialization.geometry.patch.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (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) (n m : ℕ) (x y : FullPoint) (hx : x.1.2.1 ∈ CorrectionInitialization.ActualPrimary.standardRegion.carrier) (hy : y.1.2.1 ∈ CorrectionInitialization.ActualPrimary.standardRegion.carrier) (hxy : (ActualPrimaryCoherence.absoluteChart n) x = (ActualPrimaryCoherence.absoluteChart m) y) : rescaledPotential l u n x = rescaledPotential l u m y ∧ rescaledPressureMode l u n x = rescaledPressureMode l u m y

Either order of the two common indices is allowed. The only coherence input concerns the incoming state, on its actual full-fiber overlaps.

The actual cylindrical graph, with the slow-coordinate swap explicit

noncomputable def NavierStokes.ActualSignedPotentialCoherence.nativePoint (n : ℕ) (z : ProblemStatement.SpaceTime) : FullPoint

commonGraph uses (Z,T); the correction state uses (T,Z).

Equations

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

theorem NavierStokes.ActualSignedPotentialCoherence.nativePoint_absolute (n : ℕ) (z : ProblemStatement.SpaceTime) (hr : 0 < z.2.ofLp 0) : (ActualPrimaryCoherence.absoluteChart n) (nativePoint n z) = ActualPrimaryCoherence.physicalLift z

theorem NavierStokes.ActualSignedPotentialCoherence.chart_nativePoint (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) (z : ProblemStatement.SpaceTime) (hr : 0 < z.2.ofLp 0) : (ActualSignedCoherence.chart n m k) (nativePoint n z) = nativePoint m z

theorem NavierStokes.ActualSignedPotentialCoherence.nativePoint_smoothAt (n : ℕ) (z : ProblemStatement.SpaceTime) (hr : 0 < z.2.ofLp 0) : ContDiffAt ℝ (↑⊤) (nativePoint n) z

noncomputable def NavierStokes.ActualSignedPotentialCoherence.cylindricalPotential {B N0 : ℕ} (l : ActualSignedCoherence.SignedLabel B N0) (u : CorrectionState.State Point) (n : ℕ) (z : ProblemStatement.SpaceTime) : HarmonicCalculus.ComplexVector

Cylindrical potential, given by rescaledPotential l u n (nativePoint n z).

Equations

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

noncomputable def NavierStokes.ActualSignedPotentialCoherence.cylindricalPressureMode {B N0 : ℕ} (l : ActualSignedCoherence.SignedLabel B N0) (u : CorrectionState.State Point) (n : ℕ) (z : ProblemStatement.SpaceTime) : ℂ

Cylindrical pressure mode, given by rescaledPressureMode l u n (nativePoint n z).

Equations

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

noncomputable def NavierStokes.ActualSignedPotentialCoherence.physicalDomain (n : ℕ) : Set ProblemStatement.SpaceTime

A band is used only where its own current slow chart is valid.

Equations

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

theorem NavierStokes.ActualSignedPotentialCoherence.physicalDomain_open (n : ℕ) : IsOpen (physicalDomain n)

theorem NavierStokes.ActualSignedPotentialCoherence.cylindrical_values_eq_of_index {B N0 : ℕ} (l : ActualSignedCoherence.SignedLabel B N0) (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData ActualInitialization.geometry.region ActualInitialization.geometry.patch.a ActualInitialization.geometry.patch.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hfixed : (VariableGaugeMean.reconstructState ActualInitialization.geometry.gauge (CorrectionInitialization.ActualPrimary.commonContext B) u).pressure = u.pressure) (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) (HS : 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) (z : ProblemStatement.SpaceTime) (hn : z ∈ physicalDomain n) (hm : z ∈ physicalDomain m) : cylindricalPotential l u n z = cylindricalPotential l u m z ∧ cylindricalPressureMode l u n z = cylindricalPressureMode l u m z

theorem NavierStokes.ActualSignedPotentialCoherence.cylindrical_values_eq {B N0 : ℕ} (l : ActualSignedCoherence.SignedLabel B N0) (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData ActualInitialization.geometry.region ActualInitialization.geometry.patch.a ActualInitialization.geometry.patch.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (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) (n m : ℕ) (z : ProblemStatement.SpaceTime) (hn : z ∈ physicalDomain n) (hm : z ∈ physicalDomain m) : cylindricalPotential l u n z = cylindricalPotential l u m z ∧ cylindricalPressureMode l u n z = cylindricalPressureMode l u m z

theorem NavierStokes.ActualSignedPotentialCoherence.cylindrical_values_germ {B N0 : ℕ} (l : ActualSignedCoherence.SignedLabel B N0) (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData ActualInitialization.geometry.region ActualInitialization.geometry.patch.a ActualInitialization.geometry.patch.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (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) (n m : ℕ) (z : ProblemStatement.SpaceTime) (hn : z ∈ physicalDomain n) (hm : z ∈ physicalDomain m) : cylindricalPotential l u n =ᶠ[nhds z] cylindricalPotential l u m ∧ cylindricalPressureMode l u n =ᶠ[nhds z] cylindricalPressureMode l u m