Coherence of the literal signed correction

The current-state request is transported on entire radial and free-fast fibers. The signed quotient, its projected pressure, the native cutoff, the periodized amplitude and the curl correction are then compared in the actual charts. No coherence of a signed output is assumed.

@[reducible, inline]

abbrev NavierStokes.ActualSignedCoherence.Point : Type

Point: an abbreviation for LocalSignedRequest.Point.

Equations

• NavierStokes.ActualSignedCoherence.Point = NavierStokes.LocalSignedRequest.Point

@[reducible, inline]

abbrev NavierStokes.ActualSignedCoherence.FullPoint : Type

Full point: an abbreviation for Point × ℝ.

Equations

• NavierStokes.ActualSignedCoherence.FullPoint = (NavierStokes.ActualSignedCoherence.Point × ℝ)

@[reducible, inline]

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

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

Equations

• NavierStokes.ActualSignedCoherence.SignedLabel B N0 = NavierStokes.ActualSignedStageControls.SignedLabel B N0

noncomputable def NavierStokes.ActualSignedCoherence.fullStrip : WeightedClasses.StripData FullPoint

Full strip, given by HarmonicWaveInteraction.productStrip ActualInitialization.geometry.strip.

Equations

• NavierStokes.ActualSignedCoherence.fullStrip = NavierStokes.HarmonicWaveInteraction.productStrip NavierStokes.ActualInitialization.geometry.strip

noncomputable def NavierStokes.ActualSignedCoherence.request (B : ℕ) (u : CorrectionState.State Point) : ℕ → FullPoint → SignedWaveUpdate.Vec2

Request, constructed using LocalSignedRequest.fullRequest.

Equations

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

noncomputable def NavierStokes.ActualSignedCoherence.copies {B N0 : ℕ} (l : SignedLabel B N0) (u : CorrectionState.State Point) : PeriodizedWaveBounds.CopyData FullPoint TorusInverse.Frequency

Copies, given by (ActualSignedStageControls.parameters l).copyData ActualInitialization.geometry.strip (request B u).

Equations

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

noncomputable def NavierStokes.ActualSignedCoherence.chart (n m k : ℕ) : FullPoint ≃L[ℝ] FullPoint

Chart, bundling toFun, invFun, left_inv, right_inv and the required compatibility proofs.

Equations

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

@[simp]

theorem NavierStokes.ActualSignedCoherence.chart_apply (n m k : ℕ) (x : FullPoint) : (chart n m k) x = ((GaugeStateCoherence.bandChartEquiv CorrectionInitialization.ActualPrimary.h n m k) x.1, x.2)

noncomputable def NavierStokes.ActualSignedCoherence.coefficientWeight (n m : ℕ) : ℝ

Coefficient weight, given by PhysicalSignedWave.coefficientScale (ChartScales.epsilon h n) (ChartScales.epsilon h m) (bandVelocityScale h n m).

Equations

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

noncomputable def NavierStokes.ActualSignedCoherence.phaseWeight (n m : ℕ) : ℝ

Phase weight, given by (ChartScales.carrier h m : ℝ) / (ChartScales.carrier h n : ℝ).

Equations

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

noncomputable def NavierStokes.ActualSignedCoherence.clockWeight (n m : ℕ) : ℝ

Clock weight, given by PhysicalParticularWave.clockWeight h (ChartScales.Q n) (ChartScales.Q m).

Equations

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

theorem NavierStokes.ActualSignedCoherence.velocityWeight_eq (n m : ℕ) : PhysicalParticularWave.velocityWeight CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (ChartScales.Q m) = GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m

theorem NavierStokes.ActualSignedCoherence.radiusWeight_eq (n m : ℕ) : PhysicalParticularWave.ratioPower (ChartScales.Q n) (ChartScales.Q m) (1 / 2) = GaugeStateCoherence.bandScale n m

theorem NavierStokes.ActualSignedCoherence.velocity_pos (n m : ℕ) : 0 < GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m

theorem NavierStokes.ActualSignedCoherence.coefficientWeight_pos (n m : ℕ) : 0 < coefficientWeight n m

theorem NavierStokes.ActualSignedCoherence.carrier_pos (n : ℕ) : 0 < ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n)

theorem NavierStokes.ActualSignedCoherence.phaseWeight_ne (n m : ℕ) : phaseWeight n m ≠ 0

theorem NavierStokes.ActualSignedCoherence.carrier_phaseWeight (n m : ℕ) : ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n) * phaseWeight n m = ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h m)

theorem NavierStokes.ActualSignedCoherence.sqrt_scale (n m : ℕ) : √(ChartScales.Q n) = GaugeStateCoherence.bandScale n m * √(ChartScales.Q m)

theorem NavierStokes.ActualSignedCoherence.slowChange_eq (n m : ℕ) : PhysicalSignedWave.slowChange CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (ChartScales.Q m) = ↑(GaugeStateCoherence.bandSlowEquiv CorrectionInitialization.ActualPrimary.h n m)

theorem NavierStokes.ActualSignedCoherence.requestChart_eq (n m k : ℕ) : PhysicalSignedWave.requestChart CorrectionInitialization.ActualPrimary.h ⋯ ⋯ k = GaugeStateCoherence.bandChartEquiv CorrectionInitialization.ActualPrimary.h n m k

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

theorem NavierStokes.ActualSignedCoherence.nativePoint_transport {B N0 : ℕ} (l : SignedLabel B N0) (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) (copy : TorusInverse.Frequency) (x : FullPoint) : ActualSignedStageControls.nativePoint l n copy x = ActualSignedStageControls.nativePoint l m copy ((chart n m k) x)

theorem NavierStokes.ActualSignedCoherence.chart_radius (n m k : ℕ) (x : FullPoint) : ((chart n m k) x).1.1 = GaugeStateCoherence.bandScale n m * x.1.1

theorem NavierStokes.ActualSignedCoherence.chart_radial {B : ℕ} (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) (x : FullPoint) : (chart n m k) ((ActualSignedStageControls.directions B).radialField n x) = GaugeStateCoherence.bandScale n m • (ActualSignedStageControls.directions B).radialField m ((chart n m k) x)

theorem NavierStokes.ActualSignedCoherence.chart_angular {B : ℕ} (n m k : ℕ) (_hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) (_x : FullPoint) : (chart n m k) (ActualSignedStageControls.directions B).angular = (ActualSignedStageControls.directions B).angular

theorem NavierStokes.ActualSignedCoherence.chart_axial {B : ℕ} (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) (x : FullPoint) : (chart n m k) ((ActualSignedStageControls.directions B).axialField fullStrip n x) = GaugeStateCoherence.bandScale n m • (ActualSignedStageControls.directions B).axialField fullStrip m ((chart n m k) x)

theorem NavierStokes.ActualSignedCoherence.clockWeight_eq (n m : ℕ) : clockWeight n m = GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m * GaugeStateCoherence.bandScale n m

theorem NavierStokes.ActualSignedCoherence.clockWeight_fast (n m : ℕ) : ChartScales.Q n ^ (1 + CorrectionInitialization.ActualPrimary.h) = clockWeight n m * ChartScales.Q m ^ (1 + CorrectionInitialization.ActualPrimary.h)

theorem NavierStokes.ActualSignedCoherence.chart_fast {B : ℕ} (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) (x : FullPoint) : (chart n m k) ((ActualSignedStageControls.directions B).fastField n x) = clockWeight n m • (ActualSignedStageControls.directions B).fastField m ((chart n m k) x)

theorem NavierStokes.ActualSignedCoherence.ratioPower_comp (n m r : ℕ) (a : ℝ) : PhysicalParticularWave.ratioPower (ChartScales.Q n) (ChartScales.Q r) a = PhysicalParticularWave.ratioPower (ChartScales.Q n) (ChartScales.Q m) a * PhysicalParticularWave.ratioPower (ChartScales.Q m) (ChartScales.Q r) a

theorem NavierStokes.ActualSignedCoherence.coefficientScale_comp {B N0 : ℕ} (l : SignedLabel B N0) (n m : ℕ) : ActualSignedStageControls.coefficientScale l n = coefficientWeight n m * ActualSignedStageControls.coefficientScale l m

theorem NavierStokes.ActualSignedCoherence.normalScale_comp {B N0 : ℕ} (l : SignedLabel B N0) (n m : ℕ) : ActualSignedStageControls.normalScale l n = phaseWeight n m * GaugeStateCoherence.bandScale n m * ActualSignedStageControls.normalScale l m

theorem NavierStokes.ActualSignedCoherence.clockScale_comp {B N0 : ℕ} (l : SignedLabel B N0) (n m : ℕ) : ActualSignedStageControls.clockScale l n = clockWeight n m * ActualSignedStageControls.clockScale l m

theorem NavierStokes.ActualSignedCoherence.target_transport {B N0 : ℕ} (l : SignedLabel B N0) (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) (copy : TorusInverse.Frequency) (x : FullPoint) : ActualSignedStageControls.target l copy n x = coefficientWeight n m ^ 2 • ActualSignedStageControls.target l copy m ((chart n m k) x)

theorem NavierStokes.ActualSignedCoherence.cutoff_transport {B N0 : ℕ} (l : SignedLabel B N0) (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) (copy : TorusInverse.Frequency) (x : FullPoint) : ActualSignedStageControls.cutoff l copy n x = ActualSignedStageControls.cutoff l copy m ((chart n m k) x)

theorem NavierStokes.ActualSignedCoherence.phase_transport {B N0 : ℕ} (l : SignedLabel B N0) (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) : (CorrectionInitialization.ActualPrimary.chartCoefficients l.2 l.1).phase n = fun (x : FullPoint) => phaseWeight n m * (CorrectionInitialization.ActualPrimary.chartCoefficients l.2 l.1).phase m ((chart n m k) x)

theorem NavierStokes.ActualSignedCoherence.carrier_transport {B N0 : ℕ} (l : SignedLabel B N0) (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) (x : FullPoint) : (CorrectionInitialization.ActualPrimary.chartCoefficients l.2 l.1).frequency n * (CorrectionInitialization.ActualPrimary.chartCoefficients l.2 l.1).phase n x = (CorrectionInitialization.ActualPrimary.chartCoefficients l.2 l.1).frequency m * (CorrectionInitialization.ActualPrimary.chartCoefficients l.2 l.1).phase m ((chart n m k) x)

theorem NavierStokes.ActualSignedCoherence.normal_transport {B N0 : ℕ} (l : SignedLabel B N0) (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) (x : FullPoint) : (CorrectionInitialization.ActualPrimary.chartCoefficients l.2 l.1).normal fullStrip (ActualSignedStageControls.directions B) n x = (phaseWeight n m * GaugeStateCoherence.bandScale n m) • (CorrectionInitialization.ActualPrimary.chartCoefficients l.2 l.1).normal fullStrip (ActualSignedStageControls.directions B) m ((chart n m k) x)

theorem NavierStokes.ActualSignedCoherence.normalMotion_transport {B N0 : ℕ} (l : SignedLabel B N0) (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) (copy : TorusInverse.Frequency) (x : FullPoint) : ActualSignedStageControls.normalMotion l copy n x = (phaseWeight n m * GaugeStateCoherence.bandScale n m * clockWeight n m) • ActualSignedStageControls.normalMotion l copy m ((chart n m k) x)

theorem NavierStokes.ActualSignedCoherence.action_transport {B N0 : ℕ} (l : SignedLabel B N0) (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) (copy : TorusInverse.Frequency) (x : FullPoint) : ActualSignedStageControls.action l copy n x = clockWeight n m • ActualSignedStageControls.action l copy m ((chart n m k) x)

The request follows from the incoming state on all integration fibers.

theorem NavierStokes.ActualSignedCoherence.fullRequest_transport {B : ℕ} (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) : request B u n x = coefficientWeight n m ^ 2 • request B u m ((chart n m k) x)

The literal signed quotient and homogeneous pressure

theorem NavierStokes.ActualSignedCoherence.signedVector_of_request {B N0 : ℕ} (l : 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) (copy : TorusInverse.Frequency) (x : FullPoint) (hR : request B u n x = coefficientWeight n m ^ 2 • request B u m ((chart n m k) x)) : SignedWaveUpdate.signedVector fullStrip (ActualSignedStageControls.matrix l copy) (ActualSignedStageControls.target l copy) (request B u) (ActualSignedStageControls.mask l copy) (ActualSignedStageControls.fundamental l copy) l.2 n x = GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m • SignedWaveUpdate.signedVector fullStrip (ActualSignedStageControls.matrix l copy) (ActualSignedStageControls.target l copy) (request B u) (ActualSignedStageControls.mask l copy) (ActualSignedStageControls.fundamental l copy) l.2 m ((chart n m k) x)

theorem NavierStokes.ActualSignedCoherence.raw_amplitude_of_request {B N0 : ℕ} (l : 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) (copy : TorusInverse.Frequency) (x : FullPoint) (hR : request B u n x = coefficientWeight n m ^ 2 • request B u m ((chart n m k) x)) : (copies l u).amplitude n copy x = GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m • (copies l u).amplitude m copy ((chart n m k) x)

theorem NavierStokes.ActualSignedCoherence.raw_amplitude_transport {B N0 : ℕ} (l : 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) (copy : TorusInverse.Frequency) (x : FullPoint) (hx : x.1.2.1 ∈ ActualInitialCoherence.overlap n m) : (copies l u).amplitude n copy x = GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m • (copies l u).amplitude m copy ((chart n m k) x)

theorem NavierStokes.ActualSignedCoherence.pressure_factor (n m : ℕ) : clockWeight n m * GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m / (phaseWeight n m * GaugeStateCoherence.bandScale n m) * phaseWeight n m = GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m * GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m

theorem NavierStokes.ActualSignedCoherence.raw_pressure_of_request {B N0 : ℕ} (l : 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) (copy : TorusInverse.Frequency) (x : FullPoint) (hR : request B u n x = coefficientWeight n m ^ 2 • request B u m ((chart n m k) x)) : (copies l u).pressure n copy x = (GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m * GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m) • (copies l u).pressure m copy ((chart n m k) x)

theorem NavierStokes.ActualSignedCoherence.common_amplitude_of_request {B N0 : ℕ} (l : 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 : request B u n x = coefficientWeight n m ^ 2 • request B u m ((chart n m k) x)) : (copies l u).common.amplitude n x = GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m • (copies l u).common.amplitude m ((chart n m k) x)

theorem NavierStokes.ActualSignedCoherence.common_pressure_of_request {B N0 : ℕ} (l : 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 : request B u n x = coefficientWeight n m ^ 2 • request B u m ((chart n m k) x)) : (copies l u).common.pressure n x = (GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m * GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m) • (copies l u).common.pressure m ((chart n m k) x)

theorem NavierStokes.ActualSignedCoherence.common_amplitude_germ {B N0 : ℕ} (l : 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) : (copies l u).common.amplitude n =ᶠ[nhds x] fun (y : FullPoint) => GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m • (copies l u).common.amplitude m ((chart n m k) y)

theorem NavierStokes.ActualSignedCoherence.corrected_amplitude_transport {B N0 : ℕ} (l : 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) : ((copies l u).commonCorrected fullStrip (ActualSignedStageControls.directions B)).amplitude n x = GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m • ((copies l u).commonCorrected fullStrip (ActualSignedStageControls.directions B)).amplitude m ((chart n m k) x)

theorem NavierStokes.ActualSignedCoherence.exactBlock_velocity_transport {B N0 : ℕ} (l : 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 : Point) (hx : x.2.1 ∈ ActualInitialCoherence.overlap n m) (theta : ℝ) (i : Fin 3) : ((ActualSignedStageControls.parameters l).exactBlock ActualInitialization.geometry.strip (request B u)).oscillation n (x, theta) i = GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m * ((ActualSignedStageControls.parameters l).exactBlock ActualInitialization.geometry.strip (request B u)).oscillation m ((GaugeStateCoherence.bandChartEquiv CorrectionInitialization.ActualPrimary.h n m k) x, theta) i

theorem NavierStokes.ActualSignedCoherence.exactBlock_pressure_transport {B N0 : ℕ} (l : 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 : Point) (hx : x.2.1 ∈ ActualInitialCoherence.overlap n m) (theta : ℝ) : ((ActualSignedStageControls.parameters l).exactBlock ActualInitialization.geometry.strip (request B u)).oscillatoryPressure n (x, theta) = GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m * GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m * ((ActualSignedStageControls.parameters l).exactBlock ActualInitialization.geometry.strip (request B u)).oscillatoryPressure m ((GaugeStateCoherence.bandChartEquiv CorrectionInitialization.ActualPrimary.h n m k) x, theta)