Cartesian realization of the actual reference particular update

The source is the current state's literal harmonic residual. The common solve, its transported cutoff, its curl correction, and its finite harmonic assembly are retained in the realization.

@[reducible, inline]

abbrev NavierStokes.ActualParticularRealization.Parameter : Type

Parameter: an abbreviation for PhysicalParticularWave.Parameter.

Equations

• NavierStokes.ActualParticularRealization.Parameter = NavierStokes.PhysicalParticularWave.Parameter

@[reducible, inline]

abbrev NavierStokes.ActualParticularRealization.Plane : Type

Plane: an abbreviation for TorusInverse.Plane.

Equations

• NavierStokes.ActualParticularRealization.Plane = NavierStokes.TorusInverse.Plane

@[reducible, inline]

abbrev NavierStokes.ActualParticularRealization.Associated : Type

Associated: an abbreviation for Parameter × Plane.

Equations

• NavierStokes.ActualParticularRealization.Associated = (NavierStokes.ActualParticularRealization.Parameter × NavierStokes.ActualParticularRealization.Plane)

@[reducible, inline]

abbrev NavierStokes.ActualParticularRealization.WaveSpace : Type

Wave space: an abbreviation for PhysicalParticularWave.WaveSpace.

Equations

• NavierStokes.ActualParticularRealization.WaveSpace = NavierStokes.PhysicalParticularWave.WaveSpace

@[reducible, inline]

abbrev NavierStokes.ActualParticularRealization.Cylinder : Type

Cylinder: an abbreviation for PhysicalParticularWave.Cylinder.

Equations

• NavierStokes.ActualParticularRealization.Cylinder = NavierStokes.PhysicalParticularWave.Cylinder

theorem NavierStokes.ActualParticularRealization.normal_pull {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (e : E ≃ₗᵢ[ℝ] F) (R Φ : F → ℝ) (Vr Vθ Vz : F → F) : (HarmonicCalculus.phaseNormal (fun (x : E) => R (e x)) (StateReindex.vector e Vr) (StateReindex.vector e Vθ) (StateReindex.vector e Vz) fun (x : E) => Φ (e x)) = fun (x : E) => HarmonicCalculus.phaseNormal R Vr Vθ Vz Φ (e x)

An invertible linear coordinate change transports the actual Fréchet derivative, including its totalized value away from differentiability.

theorem NavierStokes.ActualParticularRealization.curl_pull {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (e : E ≃ₗᵢ[ℝ] F) (R : F → ℝ) (Vr Vθ Vz : F → F) (a : F → HarmonicCalculus.ComplexVector) : (CurlClassBounds.cylindricalCurl (fun (x : E) => R (e x)) (StateReindex.vector e Vr) (StateReindex.vector e Vθ) (StateReindex.vector e Vz) fun (x : E) => a (e x)) = fun (x : E) => CurlClassBounds.cylindricalCurl R Vr Vθ Vz a (e x)

theorem NavierStokes.ActualParticularRealization.realizedCoefficient_pull {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (e : E ≃ₗᵢ[ℝ] F) (K : ℝ) (R Φ : F → ℝ) (Vr Vθ Vz : F → F) (a : F → HarmonicCalculus.ComplexVector) : (CurlClassBounds.realizedCoefficient K (fun (x : E) => R (e x)) (StateReindex.vector e Vr) (StateReindex.vector e Vθ) (StateReindex.vector e Vz) (fun (x : E) => Φ (e x)) fun (x : E) => a (e x)) = fun (x : E) => CurlClassBounds.realizedCoefficient K R Vr Vθ Vz Φ a (e x)

theorem NavierStokes.ActualParticularRealization.realizedCoefficient_phase_germ {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {Φ Ψ : E → ℝ} {x : E} (hΦ : Φ =ᶠ[nhds x] Ψ) (K : ℝ) (R : E → ℝ) (Vr Vθ Vz : E → E) (a : E → HarmonicCalculus.ComplexVector) : CurlClassBounds.realizedCoefficient K R Vr Vθ Vz Φ a =ᶠ[nhds x] CurlClassBounds.realizedCoefficient K R Vr Vθ Vz Ψ a

Phase agreement on a neighborhood suffices for the complete curl correction; no global continuation of the phase identity is required.

noncomputable def NavierStokes.ActualParticularRealization.raw (D : ParticularWaveAssembly.AssemblyData Parameter) (h : ℝ) (gap : ℕ → ℕ) (j : ℤ) : LinearWaveBounds.WaveCoefficients WaveSpace

Raw as an element of LinearWaveBounds.WaveCoefficients WaveSpace.

Equations

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

noncomputable def NavierStokes.ActualParticularRealization.corrected (D : ParticularWaveAssembly.AssemblyData Parameter) (s : WeightedClasses.StripData Associated) (h : ℝ) (gap : ℕ → ℕ) (j : ℤ) : LinearWaveBounds.WaveCoefficients WaveSpace

Corrected, given by (CorrectionStep.ParticularParameters.fromReference D h gap).wave s D.context D.state D.carrierBlock D.gaussianInput D.aliasInput j.

Equations

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

structure NavierStokes.ActualParticularRealization.TargetChart (D : ParticularWaveAssembly.AssemblyData Parameter) (s : WeightedClasses.StripData Associated) (h : ℝ) (n i : ℕ) : Prop

Only the primitive radius and differential directions are matched. No solved coefficient or output field occurs in this record.

• radius : (fun (x : PhysicalParticularWave.Cylinder) => D.background.radius n (PhysicalParticularWave.waveEquiv x)) = PhysicalResidualBridge.ScaledGraph.radius
• radial : StateReindex.vector PhysicalParticularWave.waveEquiv (D.directions.radialField n) = (PhysicalResidualBridge.commonGraph (ChartScales.Q n) h i).radial
• angular : (StateReindex.vector PhysicalParticularWave.waveEquiv fun (x : PhysicalParticularWave.WaveSpace) => D.directions.angular) = PhysicalResidualBridge.ScaledGraph.angular
• axial : StateReindex.vector PhysicalParticularWave.waveEquiv (D.directions.axialField (CorrectionStep.ParticularParameters.nativeStrip s) n) = (PhysicalResidualBridge.commonGraph (ChartScales.Q n) h i).axial

theorem NavierStokes.ActualParticularRealization.raw_amplitude_pull (D : ParticularWaveAssembly.AssemblyData Parameter) (h : ℝ) (gap : ℕ → ℕ) (n i : ℕ) (H : PhysicalResidualNaturality.BandCoherence D h ⋯ ⋯ i (gap n) n) (hn : PhysicalResidualNaturality.PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput n) (hr : PhysicalResidualNaturality.PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput D.reference.band) (j : ℤ) : (fun (x : PhysicalParticularWave.Cylinder) => (raw D h gap j).amplitude n (PhysicalParticularWave.waveEquiv x)) = PhysicalParticularWave.bandRaw D h ⋯ ⋯ (gap n) (↑j * D.carrierBlock.frequency n) j

theorem NavierStokes.ActualParticularRealization.raw_pressure_pull (D : ParticularWaveAssembly.AssemblyData Parameter) (h : ℝ) (gap : ℕ → ℕ) (n i : ℕ) (H : PhysicalResidualNaturality.BandCoherence D h ⋯ ⋯ i (gap n) n) (hn : PhysicalResidualNaturality.PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput n) (hr : PhysicalResidualNaturality.PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput D.reference.band) (j : ℤ) (hk : ↑j * D.carrierBlock.frequency n ≠ 0) : (fun (x : PhysicalParticularWave.Cylinder) => (raw D h gap j).pressure n (PhysicalParticularWave.waveEquiv x)) = PhysicalParticularWave.bandRawPressure D h ⋯ ⋯ (gap n) (↑j * D.carrierBlock.frequency n) j

theorem NavierStokes.ActualParticularRealization.bandPhase_eq (D : ParticularWaveAssembly.AssemblyData Parameter) (h : ℝ) (gap : ℕ → ℕ) (n i : ℕ) (H : PhysicalResidualNaturality.BandCoherence D h ⋯ ⋯ i (gap n) n) (j : ℤ) (hj : j ≠ 0) (hf : ∀ (m : ℕ), D.carrierBlock.frequency m ≠ 0) {x : Cylinder} (hx : 0 < x.1.1) : PhysicalParticularWave.bandPhase D h (ChartScales.Q n) (ChartScales.Q D.reference.band) (gap n) (↑j * D.carrierBlock.frequency n) j x = (raw D h gap j).phase n (PhysicalParticularWave.waveEquiv x)

The phase identity is derived on the full positive-radius lift from the current-state band coherence and the same integer angular harmonic.

theorem NavierStokes.ActualParticularRealization.bandPhase_germ (D : ParticularWaveAssembly.AssemblyData Parameter) (h : ℝ) (gap : ℕ → ℕ) (n i : ℕ) (H : PhysicalResidualNaturality.BandCoherence D h ⋯ ⋯ i (gap n) n) (j : ℤ) (hj : j ≠ 0) (hf : ∀ (m : ℕ), D.carrierBlock.frequency m ≠ 0) {x : Cylinder} (hx : 0 < x.1.1) : (fun (y : Cylinder) => (raw D h gap j).phase n (PhysicalParticularWave.waveEquiv y)) =ᶠ[nhds x] PhysicalParticularWave.bandPhase D h (ChartScales.Q n) (ChartScales.Q D.reference.band) (gap n) (↑j * D.carrierBlock.frequency n) j

theorem NavierStokes.ActualParticularRealization.corrected_amplitude_pull (D : ParticularWaveAssembly.AssemblyData Parameter) (s : WeightedClasses.StripData Associated) (h : ℝ) (gap : ℕ → ℕ) (n i : ℕ) (H : PhysicalResidualNaturality.BandCoherence D h ⋯ ⋯ i (gap n) n) (hn : PhysicalResidualNaturality.PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput n) (hr : PhysicalResidualNaturality.PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput D.reference.band) (T : TargetChart D s h n i) (j : ℤ) : (fun (x : PhysicalParticularWave.Cylinder) => (corrected D s h gap j).amplitude n (PhysicalParticularWave.waveEquiv x)) = CurlClassBounds.realizedCoefficient (↑j * D.carrierBlock.frequency n) PhysicalResidualBridge.ScaledGraph.radius (PhysicalResidualBridge.commonGraph (ChartScales.Q n) h i).radial PhysicalResidualBridge.ScaledGraph.angular (PhysicalResidualBridge.commonGraph (ChartScales.Q n) h i).axial (fun (x : PhysicalResidualBridge.Cylinder) => (raw D h gap j).phase n (PhysicalParticularWave.waveEquiv x)) (PhysicalParticularWave.bandRaw D h ⋯ ⋯ (gap n) (↑j * D.carrierBlock.frequency n) j)

theorem NavierStokes.ActualParticularRealization.corrected_velocity_eq_band (D : ParticularWaveAssembly.AssemblyData Parameter) (s : WeightedClasses.StripData Associated) (h : ℝ) (gap : ℕ → ℕ) (n i : ℕ) (H : PhysicalResidualNaturality.BandCoherence D h ⋯ ⋯ i (gap n) n) (hn : PhysicalResidualNaturality.PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput n) (hr : PhysicalResidualNaturality.PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput D.reference.band) (T : TargetChart D s h n i) (j : ℤ) (hj : j ≠ 0) (hf : ∀ (m : ℕ), D.carrierBlock.frequency m ≠ 0) {x : Cylinder} (hx : 0 < x.1.1) : HarmonicCalculus.vectorMode ((corrected D s h gap j).frequency n) ((corrected D s h gap j).phase n) ((corrected D s h gap j).amplitude n) (PhysicalParticularWave.waveEquiv x) = PhysicalParticularWave.bandVelocity D h ⋯ ⋯ i (gap n) (↑j * D.carrierBlock.frequency n) j x

theorem NavierStokes.ActualParticularRealization.corrected_pressure_eq_band (D : ParticularWaveAssembly.AssemblyData Parameter) (s : WeightedClasses.StripData Associated) (h : ℝ) (gap : ℕ → ℕ) (n i : ℕ) (H : PhysicalResidualNaturality.BandCoherence D h ⋯ ⋯ i (gap n) n) (hn : PhysicalResidualNaturality.PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput n) (hr : PhysicalResidualNaturality.PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput D.reference.band) (j : ℤ) (hj : j ≠ 0) (hf : ∀ (m : ℕ), D.carrierBlock.frequency m ≠ 0) {x : Cylinder} (hx : 0 < x.1.1) : HarmonicCalculus.mode ((corrected D s h gap j).frequency n) ((corrected D s h gap j).phase n) ((corrected D s h gap j).pressure n) (PhysicalParticularWave.waveEquiv x) = PhysicalParticularWave.bandPressureMode D h ⋯ ⋯ (gap n) (↑j * D.carrierBlock.frequency n) j x

The literal finite harmonic block

noncomputable def NavierStokes.ActualParticularRealization.block (D : ParticularWaveAssembly.AssemblyData Parameter) (s : WeightedClasses.StripData Associated) (h : ℝ) (gap : ℕ → ℕ) (N : ℕ) : CorrectionState.HarmonicBlock Associated

Block as an element of HarmonicBlock Associated.

Equations

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

noncomputable def NavierStokes.ActualParticularRealization.associatedCylinder : Cylinder ≃ₗᵢ[ℝ] Associated × ℝ

Cylindrical coordinates with the cycle's slow-coordinate order and the association used by the harmonic coefficient block.

Equations

• NavierStokes.ActualParticularRealization.associatedCylinder = NavierStokes.StateReindex.cylinder NavierStokes.PhysicalResidualNaturality.associatedToLift.symm

theorem NavierStokes.ActualParticularRealization.angleShuffle_associatedCylinder (x : Cylinder) : ParticularWaveAssembly.angleShuffle (associatedCylinder x) = PhysicalParticularWave.waveEquiv x

theorem NavierStokes.ActualParticularRealization.corrected_amplitude_invariant (D : ParticularWaveAssembly.AssemblyData Parameter) (s : WeightedClasses.StripData Associated) (h : ℝ) (gap : ℕ → ℕ) (j : ℤ) (B : ParticularWaveAssembly.BackgroundControl (CorrectionStep.ParticularParameters.nativeStrip s) D.directions D.background D.carrierBlock j) (n : ℕ) : CopyAngularInvariance.Invariant ((0, 1), 0) ((corrected D s h gap j).amplitude n)

theorem NavierStokes.ActualParticularRealization.corrected_pressure_invariant (D : ParticularWaveAssembly.AssemblyData Parameter) (s : WeightedClasses.StripData Associated) (h : ℝ) (gap : ℕ → ℕ) {n : ℕ} (j : ℤ) (hK : ↑j * D.carrierBlock.frequency n ≠ 0) : CopyAngularInvariance.Invariant ((0, 1), 0) ((corrected D s h gap j).pressure n)

theorem NavierStokes.ActualParticularRealization.block_velocity_represents (D : ParticularWaveAssembly.AssemblyData Parameter) (s : WeightedClasses.StripData Associated) (h : ℝ) (gap : ℕ → ℕ) {N : ℕ} (B : ∀ j ∈ ParticularWaveAssembly.modes N, ParticularWaveAssembly.BackgroundControl (CorrectionStep.ParticularParameters.nativeStrip s) D.directions D.background D.carrierBlock j) (hf : ∀ (m : ℕ), D.carrierBlock.frequency m ≠ 0) (n : ℕ) (x : Associated × ℝ) (k : Fin 3) : (block D s h gap N).oscillation n x k = ∑ j ∈ ParticularWaveAssembly.modes N, (HarmonicCalculus.vectorMode ((corrected D s h gap j).frequency n) ((corrected D s h gap j).phase n) ((corrected D s h gap j).amplitude n) (ParticularWaveAssembly.angleShuffle x) k).re

theorem NavierStokes.ActualParticularRealization.block_pressure_represents (D : ParticularWaveAssembly.AssemblyData Parameter) (s : WeightedClasses.StripData Associated) (h : ℝ) (gap : ℕ → ℕ) {N : ℕ} (hj : ∀ j ∈ ParticularWaveAssembly.modes N, j ≠ 0) (hf : ∀ (m : ℕ), D.carrierBlock.frequency m ≠ 0) (n : ℕ) (x : Associated × ℝ) : (block D s h gap N).oscillatoryPressure n x = ∑ j ∈ ParticularWaveAssembly.modes N, (HarmonicCalculus.mode ((corrected D s h gap j).frequency n) ((corrected D s h gap j).phase n) ((corrected D s h gap j).pressure n) (ParticularWaveAssembly.angleShuffle x)).re

theorem NavierStokes.ActualParticularRealization.block_velocity_eq_band (D : ParticularWaveAssembly.AssemblyData Parameter) (s : WeightedClasses.StripData Associated) (h : ℝ) (gap : ℕ → ℕ) (n i : ℕ) (H : PhysicalResidualNaturality.BandCoherence D h ⋯ ⋯ i (gap n) n) (hn : PhysicalResidualNaturality.PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput n) (hr : PhysicalResidualNaturality.PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput D.reference.band) (T : TargetChart D s h n i) {N : ℕ} (B : ∀ j ∈ ParticularWaveAssembly.modes N, ParticularWaveAssembly.BackgroundControl (CorrectionStep.ParticularParameters.nativeStrip s) D.directions D.background D.carrierBlock j) (hj : ∀ j ∈ ParticularWaveAssembly.modes N, j ≠ 0) (hf : ∀ (m : ℕ), D.carrierBlock.frequency m ≠ 0) {x : Cylinder} (hx : 0 < x.1.1) (k : Fin 3) : (block D s h gap N).oscillation n (associatedCylinder x) k = PhysicalParticularWave.labelBandVelocity D h ⋯ ⋯ i (gap n) (fun (j : ℤ) => ↑j * D.carrierBlock.frequency n) N x k

theorem NavierStokes.ActualParticularRealization.block_pressure_eq_band (D : ParticularWaveAssembly.AssemblyData Parameter) (s : WeightedClasses.StripData Associated) (h : ℝ) (gap : ℕ → ℕ) (n i : ℕ) (H : PhysicalResidualNaturality.BandCoherence D h ⋯ ⋯ i (gap n) n) (hn : PhysicalResidualNaturality.PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput n) (hr : PhysicalResidualNaturality.PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput D.reference.band) {N : ℕ} (hj : ∀ j ∈ ParticularWaveAssembly.modes N, j ≠ 0) (hf : ∀ (m : ℕ), D.carrierBlock.frequency m ≠ 0) {x : Cylinder} (hx : 0 < x.1.1) : (block D s h gap N).oscillatoryPressure n (associatedCylinder x) = PhysicalParticularWave.labelBandPressure D h ⋯ ⋯ (gap n) (fun (j : ℤ) => ↑j * D.carrierBlock.frequency n) N x

Primitive frame matching

theorem NavierStokes.ActualParticularRealization.targetChart_of_frameMatch (D : ParticularWaveAssembly.AssemblyData Parameter) (s : WeightedClasses.StripData Associated) (h : ℝ) (n i : ℕ) (hm : CorrectionStep.WaveFrameMatch D.context (HarmonicWaveInteraction.productStrip s) (ParticularWaveBounds.reindexDirections ParticularWaveAssembly.angleShuffle D.directions) (ParticularWaveBounds.reindexCoefficients ParticularWaveAssembly.angleShuffle D.background)) (hframe : HarmonicResidual.contextFrame D.context n = PhysicalResidualNaturality.associatedFrame h (ChartScales.Q n) i) : TargetChart D s h n i

One fixed Cartesian reference label

theorem NavierStokes.ActualParticularRealization.block_velocity_physical (D : ParticularWaveAssembly.AssemblyData Parameter) (s : WeightedClasses.StripData Associated) (h : ℝ) (gap : ℕ → ℕ) (n i : ℕ) (H : PhysicalResidualNaturality.BandCoherence D h ⋯ ⋯ i (gap n) n) (hn : PhysicalResidualNaturality.PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput n) (hr : PhysicalResidualNaturality.PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput D.reference.band) (T : TargetChart D s h n i) {N : ℕ} {α κ : ℝ} (C : D.controls N α κ) (hstrip : D.strip = CorrectionStep.ParticularParameters.nativeStrip s) (Href : PhysicalParticularWave.ReferenceChart D h (ChartScales.Q D.reference.band) (i + gap n)) {U : Set Parameter} (hU : IsOpen U) (R : ∀ j ∈ ParticularWaveAssembly.modes N, PhysicalParticularWave.ReferenceODE D j U) {z : ProblemStatement.SpaceTime} (hz : z ∈ (PhysicalResidualBridge.commonGraph (ChartScales.Q n) h i).source (PhysicalParticularWave.bandDomain D h (ChartScales.Q n) (ChartScales.Q D.reference.band) (gap n) U)) {delta : ℝ} (hdelta : 0 < delta) (chart : PolarCharts.Index) (hchart : z ∈ PhysicalCurlCovariance.validCylindrical delta chart) (k : Fin 3) : (block D s h gap N).oscillation n (associatedCylinder ((PhysicalResidualBridge.commonGraph (ChartScales.Q n) h i).map z)) k = ChartScales.Q n ^ CoordinateAlgebra.A h * ((CylindricalResidual.frame (-z.2.ofLp 1)) (PhysicalParticularWave.labelVelocity D h (ChartScales.Q D.reference.band) (i + gap n) delta N (z.1, CylindricalResidual.chart z.2))).ofLp k

theorem NavierStokes.ActualParticularRealization.block_pressure_physical (D : ParticularWaveAssembly.AssemblyData Parameter) (s : WeightedClasses.StripData Associated) (h : ℝ) (gap : ℕ → ℕ) (n i : ℕ) (H : PhysicalResidualNaturality.BandCoherence D h ⋯ ⋯ i (gap n) n) (hn : PhysicalResidualNaturality.PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput n) (hr : PhysicalResidualNaturality.PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput D.reference.band) {N : ℕ} {α κ : ℝ} (C : D.controls N α κ) {U : Set Parameter} (R : ∀ j ∈ ParticularWaveAssembly.modes N, PhysicalParticularWave.ReferenceODE D j U) {z : ProblemStatement.SpaceTime} (hz : 0 < z.2.ofLp 0) (hp : PhysicalParticularWave.parameterChange h (ChartScales.Q n) (ChartScales.Q D.reference.band) (PhysicalParticularWave.nativeMap h (ChartScales.Q n) i z).1.1 ∈ U) {delta : ℝ} (hdelta : 0 < delta) (chart : PolarCharts.Index) (hchart : z ∈ PhysicalCurlCovariance.validCylindrical delta chart) : (block D s h gap N).oscillatoryPressure n (associatedCylinder ((PhysicalResidualBridge.commonGraph (ChartScales.Q n) h i).map z)) = ChartScales.Q n ^ (2 * CoordinateAlgebra.A h) * PhysicalParticularWave.labelPressure D h (ChartScales.Q D.reference.band) (i + gap n) delta N (z.1, CylindricalResidual.chart z.2)

The cycle's actual coordinate layout

noncomputable def NavierStokes.ActualParticularRealization.cycleBlock (D : ParticularWaveAssembly.AssemblyData Parameter) (s : WeightedClasses.StripData Associated) (h : ℝ) (gap : ℕ → ℕ) (N : ℕ) : CorrectionState.HarmonicBlock CorrectionStep.CyclePoint

Cycle block, given by StateReindex.block CorrectionStep.cycleAssoc (block D s h gap N).

Equations

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

theorem NavierStokes.ActualParticularRealization.cycleBlock_velocity (D : ParticularWaveAssembly.AssemblyData Parameter) (s : WeightedClasses.StripData Associated) (h : ℝ) (gap : ℕ → ℕ) (N n : ℕ) (x : Cylinder) : (cycleBlock D s h gap N).oscillation n (PhysicalResidualTZ.swapCylinder x) = (block D s h gap N).oscillation n (associatedCylinder x)

theorem NavierStokes.ActualParticularRealization.cycleBlock_pressure (D : ParticularWaveAssembly.AssemblyData Parameter) (s : WeightedClasses.StripData Associated) (h : ℝ) (gap : ℕ → ℕ) (N n : ℕ) (x : Cylinder) : (cycleBlock D s h gap N).oscillatoryPressure n (PhysicalResidualTZ.swapCylinder x) = (block D s h gap N).oscillatoryPressure n (associatedCylinder x)

theorem NavierStokes.ActualParticularRealization.cycle_velocity_cylindrical (D : ParticularWaveAssembly.AssemblyData Parameter) (s : WeightedClasses.StripData Associated) (h : ℝ) (gap : ℕ → ℕ) (n i : ℕ) (H : PhysicalResidualNaturality.BandCoherence D h ⋯ ⋯ i (gap n) n) (hn : PhysicalResidualNaturality.PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput n) (hr : PhysicalResidualNaturality.PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput D.reference.band) (T : TargetChart D s h n i) {N : ℕ} {α κ : ℝ} (C : D.controls N α κ) (hstrip : D.strip = CorrectionStep.ParticularParameters.nativeStrip s) {I : ℕ} (hcover : i + gap n = I) (Href : PhysicalParticularWave.ReferenceChart D h (ChartScales.Q D.reference.band) I) {U : Set Parameter} (hU : IsOpen U) (R : ∀ j ∈ ParticularWaveAssembly.modes N, PhysicalParticularWave.ReferenceODE D j U) {delta : ℝ} (hdelta : 0 < delta) (chart : PolarCharts.Index) {z : ProblemStatement.SpaceTime} (hz : z ∈ (PhysicalResidualBridge.commonGraph (ChartScales.Q n) h i).source (PhysicalParticularWave.bandDomain D h (ChartScales.Q n) (ChartScales.Q D.reference.band) (gap n) U)) (hchart : z ∈ PhysicalCurlCovariance.validCylindrical delta chart) : (CyclePhysicalPrefixes.velocityMap (PhysicalResidualBridge.commonGraph (ChartScales.Q n) h i)) ((cycleBlock D s h gap N).oscillation n) z = (CylindricalResidual.frame (-z.2.ofLp 1)) (PhysicalParticularWave.labelVelocity D h (ChartScales.Q D.reference.band) I delta N (z.1, CylindricalResidual.chart z.2))

The exact cycle block is the cylindrical view of one fixed reference curl. The covering index enters only through i + gap n = I.

theorem NavierStokes.ActualParticularRealization.cycle_velocity_realization (D : ParticularWaveAssembly.AssemblyData Parameter) (s : WeightedClasses.StripData Associated) (h : ℝ) (gap : ℕ → ℕ) (n i : ℕ) (H : PhysicalResidualNaturality.BandCoherence D h ⋯ ⋯ i (gap n) n) (hn : PhysicalResidualNaturality.PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput n) (hr : PhysicalResidualNaturality.PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput D.reference.band) (T : TargetChart D s h n i) {N : ℕ} {α κ : ℝ} (C : D.controls N α κ) (hstrip : D.strip = CorrectionStep.ParticularParameters.nativeStrip s) {I : ℕ} (hcover : i + gap n = I) (Href : PhysicalParticularWave.ReferenceChart D h (ChartScales.Q D.reference.band) I) {U : Set Parameter} (hU : IsOpen U) (R : ∀ j ∈ ParticularWaveAssembly.modes N, PhysicalParticularWave.ReferenceODE D j U) {delta : ℝ} (hdelta : 0 < delta) (chart : PolarCharts.Index) {z : ProblemStatement.SpaceTime} (hz : z ∈ (PhysicalResidualBridge.commonGraph (ChartScales.Q n) h i).source (PhysicalParticularWave.bandDomain D h (ChartScales.Q n) (ChartScales.Q D.reference.band) (gap n) U)) (hchart : z ∈ PhysicalCurlCovariance.validCylindrical delta chart) : (CyclePhysicalPrefixes.polarVelocityMap delta chart) ((CyclePhysicalPrefixes.velocityMap (PhysicalResidualBridge.commonGraph (ChartScales.Q n) h i)) ((cycleBlock D s h gap N).oscillation n)) (z.1, CylindricalResidual.chart z.2) = SpatialCurl.spatialCurl (PhysicalParticularWave.labelPotential D h (ChartScales.Q D.reference.band) I delta N) (z.1, CylindricalResidual.chart z.2)

Cartesian realization of the literal stored finite harmonic block, using the same physical potential for every compatible covering.

theorem NavierStokes.ActualParticularRealization.cycle_pressure_realization (D : ParticularWaveAssembly.AssemblyData Parameter) (s : WeightedClasses.StripData Associated) (h : ℝ) (gap : ℕ → ℕ) (n i : ℕ) (H : PhysicalResidualNaturality.BandCoherence D h ⋯ ⋯ i (gap n) n) (hn : PhysicalResidualNaturality.PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput n) (hr : PhysicalResidualNaturality.PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput D.reference.band) {N : ℕ} {α κ : ℝ} (C : D.controls N α κ) {I : ℕ} (hcover : i + gap n = I) {U : Set Parameter} (R : ∀ j ∈ ParticularWaveAssembly.modes N, PhysicalParticularWave.ReferenceODE D j U) {delta : ℝ} (hdelta : 0 < delta) (chart : PolarCharts.Index) {z : ProblemStatement.SpaceTime} (hz : 0 < z.2.ofLp 0) (hp : PhysicalParticularWave.parameterChange h (ChartScales.Q n) (ChartScales.Q D.reference.band) (PhysicalParticularWave.nativeMap h (ChartScales.Q n) i z).1.1 ∈ U) (hchart : z ∈ PhysicalCurlCovariance.validCylindrical delta chart) : (CyclePhysicalPrefixes.polarPressureMap delta chart) ((CyclePhysicalPrefixes.pressureMap (PhysicalResidualBridge.commonGraph (ChartScales.Q n) h i)) ((cycleBlock D s h gap N).oscillatoryPressure n)) (z.1, CylindricalResidual.chart z.2) = PhysicalParticularWave.labelPressure D h (ChartScales.Q D.reference.band) I delta N (z.1, CylindricalResidual.chart z.2)

Binding to the current cycle inputs

structure NavierStokes.ActualParticularRealization.CurrentInputs {ι : Type} (D : ParticularWaveAssembly.AssemblyData Parameter) (p : CorrectionStep.CycleParameters ι) (v : CorrectionStep.CycleCoefficients ι) (c : CorrectionState.Context CorrectionStep.CyclePoint) (u : CorrectionState.State CorrectionStep.CyclePoint) (l : ι) (h : ℝ) (gap : ℕ → ℕ) : Prop

These are equalities of the current input fields and primitive solver data. There is no equality of a solved field in the interface.

• context : D.context = StateReindex.context CorrectionStep.cycleAssoc.symm c
• state : D.state = StateReindex.state CorrectionStep.cycleAssoc.symm u
• carrier : D.carrierBlock = StateReindex.block CorrectionStep.cycleAssoc.symm (v.blocks l)
• gaussian : D.gaussianInput = StateReindex.blockCoefficients CorrectionStep.cycleAssoc.symm (v.gaussian l)
• aliasError : D.aliasInput = StateReindex.blockCoefficients CorrectionStep.cycleAssoc.symm (v.aliasCoefficients l)
• parameters : p.particular l = CorrectionStep.ParticularParameters.fromReference D h gap

theorem NavierStokes.ActualParticularRealization.CurrentInputs.particularBlock {ι : Type} {D : ParticularWaveAssembly.AssemblyData Parameter} {p : CorrectionStep.CycleParameters ι} {v : CorrectionStep.CycleCoefficients ι} {c : CorrectionState.Context CorrectionStep.CyclePoint} {u : CorrectionState.State CorrectionStep.CyclePoint} {l : ι} {h : ℝ} {gap : ℕ → ℕ} (J : CurrentInputs D p v c u l h gap) : p.particularBlock v c u l = cycleBlock D (ParticularWaveBounds.reindexStrip CorrectionStep.cycleAssoc.symm p.strip) h gap v.residualBand

Full-variable transport of the curl correction

structure NavierStokes.ActualParticularRealization.SpatialScaling {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (Γ : E → F) (r : E → ℝ) (R : F → ℝ) (Sr Sθ Sz : E → E) (Vr Vθ Vz : F → F) (l : ℝ) (U : Set E) : Prop

Primitive spatial scaling on an open set. Angular differentiation has unit scale and the two spatial directions have scale l.

• isOpen : IsOpen U
• scale_ne : l ≠ 0
• radius_ne (x : E) : x ∈ U → r x ≠ 0
• differentiable (x : E) : x ∈ U → DifferentiableAt ℝ Γ x
• radial (x : E) : x ∈ U → (fderiv ℝ Γ x) (Sr x) = l • Vr (Γ x)
• angular (x : E) : x ∈ U → (fderiv ℝ Γ x) (Sθ x) = Vθ (Γ x)
• axial (x : E) : x ∈ U → (fderiv ℝ Γ x) (Sz x) = l • Vz (Γ x)
• radius (x : E) : x ∈ U → R (Γ x) = l * r x

theorem NavierStokes.ActualParticularRealization.realizedCoefficient_scaled {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Γ : E → F} {r : E → ℝ} {R : F → ℝ} {Sr Sθ Sz : E → E} {Vr Vθ Vz : F → F} {l : ℝ} {U : Set E} (G : SpatialScaling Γ r R Sr Sθ Sz Vr Vθ Vz l U) {Φ : F → ℝ} {a : F → HarmonicCalculus.ComplexVector} {K L b : ℝ} (c : ℝ) (hK : K ≠ 0) (hb : b ≠ 0) (hKL : K * b = L) (hΦ : ∀ y ∈ U, DifferentiableAt ℝ Φ (Γ y)) {x : E} (hx : x ∈ U) (hB : ∀ (k : Fin 3), DifferentiableAt ℝ (fun (y : F) => CurlClassBounds.coefficient R Vr Vθ Vz Φ a y k) (Γ x)) : CurlClassBounds.realizedCoefficient K r Sr Sθ Sz (fun (y : E) => b * Φ (Γ y)) (fun (y : E) => c • a (Γ y)) x = c • CurlClassBounds.realizedCoefficient L R Vr Vθ Vz Φ a (Γ x)

The complete differentiated coefficient has the velocity scale. This uses actual Fréchet derivatives, not an assumed curl-output covariance.

theorem NavierStokes.ActualParticularRealization.correctedMode_scaled {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Γ : E → F} {r : E → ℝ} {R : F → ℝ} {Sr Sθ Sz : E → E} {Vr Vθ Vz : F → F} {l : ℝ} {U : Set E} (G : SpatialScaling Γ r R Sr Sθ Sz Vr Vθ Vz l U) {Φ : F → ℝ} {a : F → HarmonicCalculus.ComplexVector} {K L b : ℝ} (c : ℝ) (hK : K ≠ 0) (hb : b ≠ 0) (hKL : K * b = L) (hΦ : ∀ y ∈ U, DifferentiableAt ℝ Φ (Γ y)) {x : E} (hx : x ∈ U) (hB : ∀ (k : Fin 3), DifferentiableAt ℝ (fun (y : F) => CurlClassBounds.coefficient R Vr Vθ Vz Φ a y k) (Γ x)) : HarmonicCalculus.vectorMode K (fun (y : E) => b * Φ (Γ y)) (CurlClassBounds.realizedCoefficient K r Sr Sθ Sz (fun (y : E) => b * Φ (Γ y)) fun (y : E) => c • a (Γ y)) x = c • HarmonicCalculus.vectorMode L Φ (CurlClassBounds.realizedCoefficient L R Vr Vθ Vz Φ a) (Γ x)

Full lifted corrected-mode covariance, before evaluation on any physical graph. The integer-carrier matching is K * b = L.

theorem NavierStokes.ActualParticularRealization.SpatialScaling.commonChart {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (h : ℝ) (i gap : ℕ) {U : Set Cylinder} (hU : IsOpen U) (hpos : ∀ x ∈ U, 0 < x.1.1) : SpatialScaling (⇑(PhysicalParticularWave.cylinderChange h Q Qr gap)) PhysicalResidualBridge.ScaledGraph.radius PhysicalResidualBridge.ScaledGraph.radius (PhysicalResidualBridge.commonGraph Q h i).radial PhysicalResidualBridge.ScaledGraph.angular (PhysicalResidualBridge.commonGraph Q h i).axial (PhysicalResidualBridge.commonGraph Qr h (i + gap)).radial PhysicalResidualBridge.ScaledGraph.angular (PhysicalResidualBridge.commonGraph Qr h (i + gap)).axial (PhysicalParticularWave.ratioPower Q Qr (1 / 2)) U

theorem NavierStokes.ActualParticularRealization.liftCoefficient_smooth (D : ParticularWaveAssembly.AssemblyData Parameter) {h Qr : ℝ} {I : ℕ} (H : PhysicalParticularWave.ReferenceChart D h Qr I) {j : ℤ} {α κ : ℝ} (C : ParticularWaveAssembly.LocalControl D.reference D.charts D.context D.state D.carrierBlock D.gaussianInput D.aliasInput j D.background D.copy D.strip D.directions α κ) : ContDiffOn ℝ (↑⊤) (CurlClassBounds.coefficient PhysicalResidualBridge.ScaledGraph.radius (PhysicalResidualBridge.commonGraph Qr h I).radial PhysicalResidualBridge.ScaledGraph.angular (PhysicalResidualBridge.commonGraph Qr h I).axial (PhysicalParticularWave.liftPhase D j) (PhysicalParticularWave.liftRaw D j)) (PhysicalParticularWave.referenceDomain D)

noncomputable def NavierStokes.ActualParticularRealization.referenceLiftVelocity (D : ParticularWaveAssembly.AssemblyData Parameter) (h Qr : ℝ) (I : ℕ) (j : ℤ) : Cylinder → HarmonicCalculus.ComplexVector

The same reference corrected wave as a function of all free lifted variables. No graph evaluation occurs in this definition.

Equations

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

theorem NavierStokes.ActualParticularRealization.referenceLiftVelocity_eq_wave (D : ParticularWaveAssembly.AssemblyData Parameter) {h Qr : ℝ} {I : ℕ} (H : PhysicalParticularWave.ReferenceChart D h Qr I) {j : ℤ} : referenceLiftVelocity D h Qr I j = fun (x : PhysicalParticularWave.Cylinder) => HarmonicCalculus.vectorMode ((D.wave j).frequency D.reference.band) ((D.wave j).phase D.reference.band) ((D.wave j).amplitude D.reference.band) (PhysicalParticularWave.waveEquiv x)

theorem NavierStokes.ActualParticularRealization.bandVelocity_eq_reference (D : ParticularWaveAssembly.AssemblyData Parameter) {h Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (i gap : ℕ) (H : PhysicalParticularWave.ReferenceChart D h Qr (i + gap)) {j : ℤ} {α κ : ℝ} (C : ParticularWaveAssembly.LocalControl D.reference D.charts D.context D.state D.carrierBlock D.gaussianInput D.aliasInput j D.background D.copy D.strip D.directions α κ) {K : ℝ} (hK : K ≠ 0) {U : Set Parameter} (hU : IsOpen U) (R : PhysicalParticularWave.ReferenceODE D j U) {x : Cylinder} (hx : x ∈ PhysicalParticularWave.bandDomain D h Q Qr gap U) : PhysicalParticularWave.bandVelocity D h hQ hQr i gap K j x = PhysicalParticularWave.velocityWeight h Q Qr • referenceLiftVelocity D h Qr (i + gap) j ((PhysicalParticularWave.cylinderChange h Q Qr gap) x)

Exact covariance of the actual curl-corrected transported solve on the full positive lift. This is stronger than equality on a graph.

noncomputable def NavierStokes.ActualParticularRealization.referenceLiftPressure (D : ParticularWaveAssembly.AssemblyData Parameter) (j : ℤ) : Cylinder → ℂ

Reference lift pressure, constructed using mode.

Equations

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

theorem NavierStokes.ActualParticularRealization.bandPressureMode_eq_reference (D : ParticularWaveAssembly.AssemblyData Parameter) (h : ℝ) {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (gap : ℕ) {K : ℝ} (hK : K ≠ 0) (j : ℤ) (hKr : PhysicalParticularWave.referenceFrequency D j ≠ 0) {U : Set Parameter} (R : PhysicalParticularWave.ReferenceODE D j U) (x : Cylinder) (hx : PhysicalParticularWave.parameterChange h Q Qr (PhysicalParticularWave.waveEquiv x).1.1 ∈ U) : PhysicalParticularWave.bandPressureMode D h hQ hQr gap K j x = ↑(PhysicalParticularWave.pressureWeight h Q Qr) * referenceLiftPressure D j ((PhysicalParticularWave.cylinderChange h Q Qr gap) x)

theorem NavierStokes.ActualParticularRealization.referenceLiftPressure_eq_wave (D : ParticularWaveAssembly.AssemblyData Parameter) (H : PhysicalParticularWave.ReferenceIdentity D) (j : ℤ) (hj : j ≠ 0) (hf : ∀ (m : ℕ), D.carrierBlock.frequency m ≠ 0) : referenceLiftPressure D j = fun (x : PhysicalParticularWave.Cylinder) => HarmonicCalculus.mode ((D.wave j).frequency D.reference.band) ((D.wave j).phase D.reference.band) ((D.wave j).pressure D.reference.band) (PhysicalParticularWave.waveEquiv x)

theorem NavierStokes.ActualParticularRealization.associatedCylinder_change (h : ℝ) {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (gap : ℕ) (x : Cylinder) : associatedCylinder ((PhysicalParticularWave.cylinderChange h Q Qr gap) x) = ((PhysicalResidualNaturality.associatedChart h hQ hQr gap) (associatedCylinder x).1, (associatedCylinder x).2)

theorem NavierStokes.ActualParticularRealization.corrected_velocity_eq_reference (D : ParticularWaveAssembly.AssemblyData Parameter) (s : WeightedClasses.StripData Associated) (h : ℝ) (gap : ℕ → ℕ) (n i : ℕ) (H : PhysicalResidualNaturality.BandCoherence D h ⋯ ⋯ i (gap n) n) (hn : PhysicalResidualNaturality.PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput n) (hr : PhysicalResidualNaturality.PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput D.reference.band) (T : TargetChart D s h n i) (Href : PhysicalParticularWave.ReferenceChart D h (ChartScales.Q D.reference.band) (i + gap n)) {U : Set Parameter} (hU : IsOpen U) {j : ℤ} {α κ : ℝ} (C : ParticularWaveAssembly.LocalControl D.reference D.charts D.context D.state D.carrierBlock D.gaussianInput D.aliasInput j D.background D.copy D.strip D.directions α κ) (R : PhysicalParticularWave.ReferenceODE D j U) {x : Cylinder} (hx : x ∈ PhysicalParticularWave.bandDomain D h (ChartScales.Q n) (ChartScales.Q D.reference.band) (gap n) U) : HarmonicCalculus.vectorMode ((corrected D s h gap j).frequency n) ((corrected D s h gap j).phase n) ((corrected D s h gap j).amplitude n) (PhysicalParticularWave.waveEquiv x) = PhysicalParticularWave.velocityWeight h (ChartScales.Q n) (ChartScales.Q D.reference.band) • HarmonicCalculus.vectorMode ((D.wave j).frequency D.reference.band) ((D.wave j).phase D.reference.band) ((D.wave j).amplitude D.reference.band) (PhysicalParticularWave.waveEquiv ((PhysicalParticularWave.cylinderChange h (ChartScales.Q n) (ChartScales.Q D.reference.band) (gap n)) x))

theorem NavierStokes.ActualParticularRealization.corrected_pressure_eq_reference (D : ParticularWaveAssembly.AssemblyData Parameter) (s : WeightedClasses.StripData Associated) (h : ℝ) (gap : ℕ → ℕ) (n i : ℕ) (H : PhysicalResidualNaturality.BandCoherence D h ⋯ ⋯ i (gap n) n) (hn : PhysicalResidualNaturality.PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput n) (hr : PhysicalResidualNaturality.PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput D.reference.band) (Href : PhysicalParticularWave.ReferenceChart D h (ChartScales.Q D.reference.band) (i + gap n)) {U : Set Parameter} {j : ℤ} {α κ : ℝ} (C : ParticularWaveAssembly.LocalControl D.reference D.charts D.context D.state D.carrierBlock D.gaussianInput D.aliasInput j D.background D.copy D.strip D.directions α κ) (R : PhysicalParticularWave.ReferenceODE D j U) {x : Cylinder} (hx : x ∈ PhysicalParticularWave.bandDomain D h (ChartScales.Q n) (ChartScales.Q D.reference.band) (gap n) U) : HarmonicCalculus.mode ((corrected D s h gap j).frequency n) ((corrected D s h gap j).phase n) ((corrected D s h gap j).pressure n) (PhysicalParticularWave.waveEquiv x) = ↑(PhysicalParticularWave.pressureWeight h (ChartScales.Q n) (ChartScales.Q D.reference.band)) * HarmonicCalculus.mode ((D.wave j).frequency D.reference.band) ((D.wave j).phase D.reference.band) ((D.wave j).pressure D.reference.band) (PhysicalParticularWave.waveEquiv ((PhysicalParticularWave.cylinderChange h (ChartScales.Q n) (ChartScales.Q D.reference.band) (gap n)) x))

theorem NavierStokes.ActualParticularRealization.block_velocity_eq_reference (D : ParticularWaveAssembly.AssemblyData Parameter) (s : WeightedClasses.StripData Associated) (h : ℝ) (gap : ℕ → ℕ) (n i : ℕ) (H : PhysicalResidualNaturality.BandCoherence D h ⋯ ⋯ i (gap n) n) (hn : PhysicalResidualNaturality.PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput n) (hr : PhysicalResidualNaturality.PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput D.reference.band) (T : TargetChart D s h n i) (Href : PhysicalParticularWave.ReferenceChart D h (ChartScales.Q D.reference.band) (i + gap n)) {U : Set Parameter} (hU : IsOpen U) {N : ℕ} {α κ : ℝ} (C : D.controls N α κ) (hstrip : D.strip = CorrectionStep.ParticularParameters.nativeStrip s) (hf : ∀ (m : ℕ), D.carrierBlock.frequency m ≠ 0) (R : ∀ j ∈ ParticularWaveAssembly.modes N, PhysicalParticularWave.ReferenceODE D j U) {x : Cylinder} (hx : x ∈ PhysicalParticularWave.bandDomain D h (ChartScales.Q n) (ChartScales.Q D.reference.band) (gap n) U) (k : Fin 3) : (block D s h gap N).oscillation n (associatedCylinder x) k = PhysicalParticularWave.velocityWeight h (ChartScales.Q n) (ChartScales.Q D.reference.band) * (D.updateBlock N).oscillation D.reference.band (associatedCylinder ((PhysicalParticularWave.cylinderChange h (ChartScales.Q n) (ChartScales.Q D.reference.band) (gap n)) x)) k

The entire literal target block equals the same finite reference block, on the full radial/free-torus/angular domain.

theorem NavierStokes.ActualParticularRealization.block_pressure_eq_reference (D : ParticularWaveAssembly.AssemblyData Parameter) (s : WeightedClasses.StripData Associated) (h : ℝ) (gap : ℕ → ℕ) (n i : ℕ) (H : PhysicalResidualNaturality.BandCoherence D h ⋯ ⋯ i (gap n) n) (hn : PhysicalResidualNaturality.PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput n) (hr : PhysicalResidualNaturality.PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput D.reference.band) (Href : PhysicalParticularWave.ReferenceChart D h (ChartScales.Q D.reference.band) (i + gap n)) {U : Set Parameter} {N : ℕ} {α κ : ℝ} (C : D.controls N α κ) (hf : ∀ (m : ℕ), D.carrierBlock.frequency m ≠ 0) (R : ∀ j ∈ ParticularWaveAssembly.modes N, PhysicalParticularWave.ReferenceODE D j U) {x : Cylinder} (hx : x ∈ PhysicalParticularWave.bandDomain D h (ChartScales.Q n) (ChartScales.Q D.reference.band) (gap n) U) : (block D s h gap N).oscillatoryPressure n (associatedCylinder x) = PhysicalParticularWave.pressureWeight h (ChartScales.Q n) (ChartScales.Q D.reference.band) * (D.updateBlock N).oscillatoryPressure D.reference.band (associatedCylinder ((PhysicalParticularWave.cylinderChange h (ChartScales.Q n) (ChartScales.Q D.reference.band) (gap n)) x))

Direct consumers for the current correction step

theorem NavierStokes.ActualParticularRealization.CurrentInputs.velocity_realization {ι : Type} {D : ParticularWaveAssembly.AssemblyData Parameter} {p : CorrectionStep.CycleParameters ι} {v : CorrectionStep.CycleCoefficients ι} {c : CorrectionState.Context CorrectionStep.CyclePoint} {u : CorrectionState.State CorrectionStep.CyclePoint} {label : ι} {h : ℝ} {gap : ℕ → ℕ} (J : CurrentInputs D p v c u label h gap) (n i : ℕ) (H : PhysicalResidualNaturality.BandCoherence D h ⋯ ⋯ i (gap n) n) (hn : PhysicalResidualNaturality.PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput n) (hr : PhysicalResidualNaturality.PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput D.reference.band) {α κ : ℝ} (C : D.controls v.residualBand α κ) (hstrip : D.strip = CorrectionStep.ParticularParameters.nativeStrip (ParticularWaveBounds.reindexStrip CorrectionStep.cycleAssoc.symm p.strip)) (hm : CorrectionStep.WaveFrameMatch D.context (HarmonicWaveInteraction.productStrip (ParticularWaveBounds.reindexStrip CorrectionStep.cycleAssoc.symm p.strip)) (ParticularWaveBounds.reindexDirections ParticularWaveAssembly.angleShuffle D.directions) (ParticularWaveBounds.reindexCoefficients ParticularWaveAssembly.angleShuffle D.background)) {I : ℕ} (hcover : i + gap n = I) (Href : PhysicalParticularWave.ReferenceChart D h (ChartScales.Q D.reference.band) I) {U : Set Parameter} (hU : IsOpen U) (R : ∀ j ∈ ParticularWaveAssembly.modes v.residualBand, PhysicalParticularWave.ReferenceODE D j U) {delta : ℝ} (hdelta : 0 < delta) (chart : PolarCharts.Index) {z : ProblemStatement.SpaceTime} (hz : z ∈ (PhysicalResidualBridge.commonGraph (ChartScales.Q n) h i).source (PhysicalParticularWave.bandDomain D h (ChartScales.Q n) (ChartScales.Q D.reference.band) (gap n) U)) (hchart : z ∈ PhysicalCurlCovariance.validCylindrical delta chart) : (CyclePhysicalPrefixes.polarVelocityMap delta chart) ((CyclePhysicalPrefixes.velocityMap (PhysicalResidualBridge.commonGraph (ChartScales.Q n) h i)) ((p.particularBlock v c u label).oscillation n)) (z.1, CylindricalResidual.chart z.2) = SpatialCurl.spatialCurl (PhysicalParticularWave.labelPotential D h (ChartScales.Q D.reference.band) I delta v.residualBand) (z.1, CylindricalResidual.chart z.2)

theorem NavierStokes.ActualParticularRealization.CurrentInputs.pressure_realization {ι : Type} {D : ParticularWaveAssembly.AssemblyData Parameter} {p : CorrectionStep.CycleParameters ι} {v : CorrectionStep.CycleCoefficients ι} {c : CorrectionState.Context CorrectionStep.CyclePoint} {u : CorrectionState.State CorrectionStep.CyclePoint} {label : ι} {h : ℝ} {gap : ℕ → ℕ} (J : CurrentInputs D p v c u label h gap) (n i : ℕ) (H : PhysicalResidualNaturality.BandCoherence D h ⋯ ⋯ i (gap n) n) (hn : PhysicalResidualNaturality.PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput n) (hr : PhysicalResidualNaturality.PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput D.reference.band) {α κ : ℝ} (C : D.controls v.residualBand α κ) {I : ℕ} (hcover : i + gap n = I) {U : Set Parameter} (R : ∀ j ∈ ParticularWaveAssembly.modes v.residualBand, PhysicalParticularWave.ReferenceODE D j U) {delta : ℝ} (hdelta : 0 < delta) (chart : PolarCharts.Index) {z : ProblemStatement.SpaceTime} (hz : 0 < z.2.ofLp 0) (hp : PhysicalParticularWave.parameterChange h (ChartScales.Q n) (ChartScales.Q D.reference.band) (PhysicalParticularWave.nativeMap h (ChartScales.Q n) i z).1.1 ∈ U) (hchart : z ∈ PhysicalCurlCovariance.validCylindrical delta chart) : (CyclePhysicalPrefixes.polarPressureMap delta chart) ((CyclePhysicalPrefixes.pressureMap (PhysicalResidualBridge.commonGraph (ChartScales.Q n) h i)) ((p.particularBlock v c u label).oscillatoryPressure n)) (z.1, CylindricalResidual.chart z.2) = PhysicalParticularWave.labelPressure D h (ChartScales.Q D.reference.band) I delta v.residualBand (z.1, CylindricalResidual.chart z.2)

noncomputable def NavierStokes.ActualParticularRealization.physicalDomain (D : ParticularWaveAssembly.AssemblyData Parameter) (h : ℝ) (n i gap : ℕ) (U : Set Parameter) (delta : ℝ) (chart : PolarCharts.Index) : Set ProblemStatement.SpaceTime

The Cartesian image of the actual common-chart domain and valid polar branch; no extension of the raw formulas beyond this set is used.

Equations

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

theorem NavierStokes.ActualParticularRealization.cycle_velocity_eqOn (D : ParticularWaveAssembly.AssemblyData Parameter) (s : WeightedClasses.StripData Associated) (h : ℝ) (gap : ℕ → ℕ) (n i : ℕ) (H : PhysicalResidualNaturality.BandCoherence D h ⋯ ⋯ i (gap n) n) (hn : PhysicalResidualNaturality.PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput n) (hr : PhysicalResidualNaturality.PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput D.reference.band) (T : TargetChart D s h n i) {N : ℕ} {α κ : ℝ} (C : D.controls N α κ) (hstrip : D.strip = CorrectionStep.ParticularParameters.nativeStrip s) {I : ℕ} (hcover : i + gap n = I) (Href : PhysicalParticularWave.ReferenceChart D h (ChartScales.Q D.reference.band) I) {U : Set Parameter} (hU : IsOpen U) (R : ∀ j ∈ ParticularWaveAssembly.modes N, PhysicalParticularWave.ReferenceODE D j U) {delta : ℝ} (hdelta : 0 < delta) (chart : PolarCharts.Index) : Set.EqOn (SpatialCurl.spatialCurl (PhysicalParticularWave.labelPotential D h (ChartScales.Q D.reference.band) I delta N)) ((CyclePhysicalPrefixes.polarVelocityMap delta chart) ((CyclePhysicalPrefixes.velocityMap (PhysicalResidualBridge.commonGraph (ChartScales.Q n) h i)) ((cycleBlock D s h gap N).oscillation n))) (physicalDomain D h n i (gap n) U delta chart)

theorem NavierStokes.ActualParticularRealization.cycle_pressure_eqOn (D : ParticularWaveAssembly.AssemblyData Parameter) (s : WeightedClasses.StripData Associated) (h : ℝ) (gap : ℕ → ℕ) (n i : ℕ) (H : PhysicalResidualNaturality.BandCoherence D h ⋯ ⋯ i (gap n) n) (hn : PhysicalResidualNaturality.PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput n) (hr : PhysicalResidualNaturality.PositiveSupport D.carrierBlock D.gaussianInput D.aliasInput D.reference.band) {N : ℕ} {α κ : ℝ} (C : D.controls N α κ) {I : ℕ} (hcover : i + gap n = I) {U : Set Parameter} (R : ∀ j ∈ ParticularWaveAssembly.modes N, PhysicalParticularWave.ReferenceODE D j U) {delta : ℝ} (hdelta : 0 < delta) (chart : PolarCharts.Index) : Set.EqOn (PhysicalParticularWave.labelPressure D h (ChartScales.Q D.reference.band) I delta N) ((CyclePhysicalPrefixes.polarPressureMap delta chart) ((CyclePhysicalPrefixes.pressureMap (PhysicalResidualBridge.commonGraph (ChartScales.Q n) h i)) ((cycleBlock D s h gap N).oscillatoryPressure n))) (physicalDomain D h n i (gap n) U delta chart)