Native reference data from the actual common-cover state

The current state at the reference band still uses that band's common cover. The reference Volterra geometry, on the other hand, uses the native cover. This file changes the free auxiliary coordinate before forming the reference source. The change acts on the entire current residual, including its Gaussian and alias inputs.

A single deck shift of the actual particular solve

Only invariance under the specified lattice vector is assumed. Equality of the actual anchored coefficient and forcing paths gives equality of the Volterra solves, and a bijective copy reindexing gives the same symmetry of the periodized velocity and pressure.

theorem NavierStokes.SubcoverPeriodicity.forcingAlong_shift {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] (d : CommonCoverSolve.LinearData P V E) (g : CommonCoverSolve.Geometry) (j K : TorusInverse.Frequency) (p : P) (hf : ∀ (Y : TorusInverse.Plane), d.source (p, Y + TorusAverages.latticePoint K) = d.source (p, Y)) (Y : TorusInverse.Plane) (s : ℝ) : d.forcingAlong g (j + CommonCoverSolve.coverIndex g.gap K) ((p, Y + TorusAverages.latticePoint K), s) = d.forcingAlong g j ((p, Y), s)

theorem NavierStokes.SubcoverPeriodicity.forcingPath_shift {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] (d : CommonCoverSolve.LinearData P V E) (g : CommonCoverSolve.Geometry) {a b : ℝ} (j K : TorusInverse.Frequency) (p : P) (hf : ∀ (Y : TorusInverse.Plane), d.source (p, Y + TorusAverages.latticePoint K) = d.source (p, Y)) (Y : TorusInverse.Plane) : d.forcingPath g (j + CommonCoverSolve.coverIndex g.gap K) (p, Y + TorusAverages.latticePoint K) = d.forcingPath g j (p, Y)

theorem NavierStokes.SubcoverPeriodicity.anchoredSolve_shift {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (d : CommonCoverSolve.LinearData P V E) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (j K : TorusInverse.Frequency) (p : P) (hf : ∀ (Y : TorusInverse.Plane), d.source (p, Y + TorusAverages.latticePoint K) = d.source (p, Y)) (Y : TorusInverse.Plane) (s : ℝ) : d.anchoredSolve g hab (j + CommonCoverSolve.coverIndex g.gap K) (p, Y + TorusAverages.latticePoint K) s = d.anchoredSolve g hab j (p, Y) s

theorem NavierStokes.SubcoverPeriodicity.copySolve_shift {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (d : CommonCoverSolve.LinearData P V E) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (j K : TorusInverse.Frequency) (p : P) (hf : ∀ (Y : TorusInverse.Plane), d.source (p, Y + TorusAverages.latticePoint K) = d.source (p, Y)) (Y : TorusInverse.Plane) : d.copySolve g hab (j + CommonCoverSolve.coverIndex g.gap K) (p, Y + TorusAverages.latticePoint K) = d.copySolve g hab j (p, Y)

theorem NavierStokes.SubcoverPeriodicity.copyVelocity_shift {P : Type} (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (j K : TorusInverse.Frequency) (p : P) (hf : ∀ (Y : TorusInverse.Plane), t.source (p, Y + TorusAverages.latticePoint K) = t.source (p, Y)) (Y : TorusInverse.Plane) : ParticularWaveBounds.copyVelocity t g hab (j + CommonCoverSolve.coverIndex g.gap K) (p, Y + TorusAverages.latticePoint K) = ParticularWaveBounds.copyVelocity t g hab j (p, Y)

theorem NavierStokes.SubcoverPeriodicity.copyPressure_shift {P : Type} (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (j K : TorusInverse.Frequency) (frequency : ℝ) (p : P) (hf : ∀ (Y : TorusInverse.Plane), t.source (p, Y + TorusAverages.latticePoint K) = t.source (p, Y)) (Y : TorusInverse.Plane) : ParticularWaveBounds.copyPressure t g hab (j + CommonCoverSolve.coverIndex g.gap K) frequency (p, Y + TorusAverages.latticePoint K) = ParticularWaveBounds.copyPressure t g hab j frequency (p, Y)

theorem NavierStokes.SubcoverPeriodicity.complexCopyVelocity_shift {P : Type} (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (f : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (j K : TorusInverse.Frequency) (p : P) (hf : ∀ (Y : TorusInverse.Plane), f (p, Y + TorusAverages.latticePoint K) = f (p, Y)) (Y : TorusInverse.Plane) : ParticularWaveBounds.complexCopyVelocity t f g hab (j + CommonCoverSolve.coverIndex g.gap K) (p, Y + TorusAverages.latticePoint K) = ParticularWaveBounds.complexCopyVelocity t f g hab j (p, Y)

theorem NavierStokes.SubcoverPeriodicity.complexCopyPressure_shift {P : Type} (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (f : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (j K : TorusInverse.Frequency) (frequency : ℝ) (p : P) (hf : ∀ (Y : TorusInverse.Plane), f (p, Y + TorusAverages.latticePoint K) = f (p, Y)) (Y : TorusInverse.Plane) : ParticularWaveBounds.complexCopyPressure t f g hab (j + CommonCoverSolve.coverIndex g.gap K) frequency (p, Y + TorusAverages.latticePoint K) = ParticularWaveBounds.complexCopyPressure t f g hab j frequency (p, Y)

theorem NavierStokes.SubcoverPeriodicity.complexCopyVelocity_shift_of_gap_zero {P : Type} (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (f : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (g : CommonCoverSolve.Geometry) (hg : g.gap = 0) {a b : ℝ} (hab : a ≤ b) (j K : TorusInverse.Frequency) (p : P) (hf : ∀ (Y : TorusInverse.Plane), f (p, Y + TorusAverages.latticePoint K) = f (p, Y)) (Y : TorusInverse.Plane) : ParticularWaveBounds.complexCopyVelocity t f g hab (j + K) (p, Y + TorusAverages.latticePoint K) = ParticularWaveBounds.complexCopyVelocity t f g hab j (p, Y)

theorem NavierStokes.SubcoverPeriodicity.complexCopyPressure_shift_of_gap_zero {P : Type} (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (f : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (g : CommonCoverSolve.Geometry) (hg : g.gap = 0) {a b : ℝ} (hab : a ≤ b) (j K : TorusInverse.Frequency) (frequency : ℝ) (p : P) (hf : ∀ (Y : TorusInverse.Plane), f (p, Y + TorusAverages.latticePoint K) = f (p, Y)) (Y : TorusInverse.Plane) : ParticularWaveBounds.complexCopyPressure t f g hab (j + K) frequency (p, Y + TorusAverages.latticePoint K) = ParticularWaveBounds.complexCopyPressure t f g hab j frequency (p, Y)

theorem NavierStokes.SubcoverPeriodicity.periodizedCopies_shift {P H : Type} [NormedAddCommGroup H] [NormedSpace ℝ H] (g : CommonCoverSolve.Geometry) (κ : TorusInverse.Plane → ℝ) (F : TorusInverse.Frequency → P × TorusInverse.Plane → H) (K : TorusInverse.Frequency) (p : P) (hF : ∀ (j : TorusInverse.Frequency) (Y : TorusInverse.Plane), F (j + CommonCoverSolve.coverIndex g.gap K) (p, Y + TorusAverages.latticePoint K) = F j (p, Y)) (Y : TorusInverse.Plane) : ParticularWaveBounds.periodizedCopies g κ F (p, Y + TorusAverages.latticePoint K) = ParticularWaveBounds.periodizedCopies g κ F (p, Y)

Translation of the copy index is a bijection; there is no multiplicity factor when passing from the individual solves to the common field.

theorem NavierStokes.SubcoverPeriodicity.commonVelocity_shift {P : Type} (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (f : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (κ : TorusInverse.Plane → ℝ) (K : TorusInverse.Frequency) (p : P) (hf : ∀ (Y : TorusInverse.Plane), f (p, Y + TorusAverages.latticePoint K) = f (p, Y)) (Y : TorusInverse.Plane) : ParticularWaveBounds.commonVelocity t f g hab κ (p, Y + TorusAverages.latticePoint K) = ParticularWaveBounds.commonVelocity t f g hab κ (p, Y)

theorem NavierStokes.SubcoverPeriodicity.commonPressure_shift {P : Type} (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (f : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (κ : TorusInverse.Plane → ℝ) (frequency : ℝ) (K : TorusInverse.Frequency) (p : P) (hf : ∀ (Y : TorusInverse.Plane), f (p, Y + TorusAverages.latticePoint K) = f (p, Y)) (Y : TorusInverse.Plane) : ParticularWaveBounds.commonPressure t f g hab κ frequency (p, Y + TorusAverages.latticePoint K) = ParticularWaveBounds.commonPressure t f g hab κ frequency (p, Y)

theorem NavierStokes.SubcoverPeriodicity.commonFields_finite_sum {P : Type} (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (f : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (κ : TorusInverse.Plane → ℝ) (hκ : HasCompactSupport κ) (frequency : ℝ) (p : P) (Y : TorusInverse.Plane) : ∃ (I : Finset TorusInverse.Frequency), ParticularWaveBounds.commonVelocity t f g hab κ (p, Y) = ∑ j ∈ I, κ (g.coordinates j Y) • ParticularWaveBounds.complexCopyVelocity t f g hab j (p, Y) ∧ ParticularWaveBounds.commonPressure t f g hab κ frequency (p, Y) = ∑ j ∈ I, κ (g.coordinates j Y) • ParticularWaveBounds.complexCopyPressure t f g hab j frequency (p, Y)

With a compact cutoff, both fields are genuine finite sums over the same copy set at the specified point.

The inherited sublattice, without a unit-lattice assertion

def NavierStokes.SubcoverPeriodicity.SubcoverPeriodicAt {P V : Type} (d : ℕ) (f : P × TorusInverse.Plane → V) (p : P) : Prop

Periodicity on the image of the integer lattice under the d-fold cover. The parameter is fixed throughout the statement.

Equations

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

noncomputable def NavierStokes.SubcoverPeriodicity.inverseCoverSource {P V : Type} (d : ℕ) (f : P × TorusInverse.Plane → V) : P × TorusInverse.Plane → V

The actual inverse-cover pullback of a source.

Equations

• NavierStokes.SubcoverPeriodicity.inverseCoverSource d f x = f (x.1, (NavierStokes.CommonCoverSolve.coverPower d).symm x.2)

theorem NavierStokes.SubcoverPeriodicity.inverseCoverSource_shift {P V : Type} (d : ℕ) (f : P × TorusInverse.Plane → V) (p : P) (k : TorusInverse.Frequency) (hf : ∀ (Y : TorusInverse.Plane), f (p, Y + TorusAverages.latticePoint k) = f (p, Y)) (Y : TorusInverse.Plane) : inverseCoverSource d f (p, Y + TorusAverages.latticePoint (CommonCoverSolve.coverIndex d k)) = inverseCoverSource d f (p, Y)

theorem NavierStokes.SubcoverPeriodicity.inverseCoverSource_subcoverPeriodic {P V : Type} (d : ℕ) (f : P × TorusInverse.Plane → V) (p : P) (hf : CommonCoverSolve.PeriodicAt f p) : SubcoverPeriodicAt d (inverseCoverSource d f) p

theorem NavierStokes.SubcoverPeriodicity.cover_pullback_shift {P V : Type} (d : ℕ) (f : P × TorusInverse.Plane → V) (p : P) (k : TorusInverse.Frequency) (hf : ∀ (Y : TorusInverse.Plane), f (p, Y + TorusAverages.latticePoint (CommonCoverSolve.coverIndex d k)) = f (p, Y)) (Y : TorusInverse.Plane) : f (p, (CommonCoverSolve.coverPower d) (Y + TorusAverages.latticePoint k)) = f (p, (CommonCoverSolve.coverPower d) Y)

Pushing a sublattice-periodic field back through the same cover recovers the corresponding unit-lattice shift.

theorem NavierStokes.SubcoverPeriodicity.commonVelocity_subcover_shift {P : Type} (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (f : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (κ : TorusInverse.Plane → ℝ) (d : ℕ) (k : TorusInverse.Frequency) (p : P) (hf : ∀ (Y : TorusInverse.Plane), f (p, Y + TorusAverages.latticePoint (CommonCoverSolve.coverIndex d k)) = f (p, Y)) (Y : TorusInverse.Plane) : ParticularWaveBounds.commonVelocity t f g hab κ (p, Y + TorusAverages.latticePoint (CommonCoverSolve.coverIndex d k)) = ParticularWaveBounds.commonVelocity t f g hab κ (p, Y)

theorem NavierStokes.SubcoverPeriodicity.commonPressure_subcover_shift {P : Type} (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (f : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (κ : TorusInverse.Plane → ℝ) (frequency : ℝ) (d : ℕ) (k : TorusInverse.Frequency) (p : P) (hf : ∀ (Y : TorusInverse.Plane), f (p, Y + TorusAverages.latticePoint (CommonCoverSolve.coverIndex d k)) = f (p, Y)) (Y : TorusInverse.Plane) : ParticularWaveBounds.commonPressure t f g hab κ frequency (p, Y + TorusAverages.latticePoint (CommonCoverSolve.coverIndex d k)) = ParticularWaveBounds.commonPressure t f g hab κ frequency (p, Y)

theorem NavierStokes.SubcoverPeriodicity.commonVelocity_subcoverPeriodic {P : Type} (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (f : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (κ : TorusInverse.Plane → ℝ) (d : ℕ) (p : P) (hf : SubcoverPeriodicAt d f p) : SubcoverPeriodicAt d (ParticularWaveBounds.commonVelocity t f g hab κ) p

theorem NavierStokes.SubcoverPeriodicity.commonPressure_subcoverPeriodic {P : Type} (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (f : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (κ : TorusInverse.Plane → ℝ) (frequency : ℝ) (d : ℕ) (p : P) (hf : SubcoverPeriodicAt d f p) : SubcoverPeriodicAt d (ParticularWaveBounds.commonPressure t f g hab κ frequency) p

theorem NavierStokes.SubcoverPeriodicity.commonVelocity_inverseCoverSource_shift {P : Type} (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (f : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (κ : TorusInverse.Plane → ℝ) (d : ℕ) (k : TorusInverse.Frequency) (p : P) (hf : ∀ (Y : TorusInverse.Plane), f (p, Y + TorusAverages.latticePoint k) = f (p, Y)) (Y : TorusInverse.Plane) : ParticularWaveBounds.commonVelocity t (inverseCoverSource d f) g hab κ (p, Y + TorusAverages.latticePoint (CommonCoverSolve.coverIndex d k)) = ParticularWaveBounds.commonVelocity t (inverseCoverSource d f) g hab κ (p, Y)

A single symmetry of the original source yields precisely the transported symmetry of the solved inverse-cover source.

theorem NavierStokes.SubcoverPeriodicity.commonPressure_inverseCoverSource_shift {P : Type} (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (f : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (κ : TorusInverse.Plane → ℝ) (frequency : ℝ) (d : ℕ) (k : TorusInverse.Frequency) (p : P) (hf : ∀ (Y : TorusInverse.Plane), f (p, Y + TorusAverages.latticePoint k) = f (p, Y)) (Y : TorusInverse.Plane) : ParticularWaveBounds.commonPressure t (inverseCoverSource d f) g hab κ frequency (p, Y + TorusAverages.latticePoint (CommonCoverSolve.coverIndex d k)) = ParticularWaveBounds.commonPressure t (inverseCoverSource d f) g hab κ frequency (p, Y)

Pullback of the actual state through an invertible linear map

noncomputable def NavierStokes.ActualReferenceRebase.pullField {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃L[ℝ] E) (f : MeanIncrementBounds.Field E) : MeanIncrementBounds.Field D

Pull field, defined pointwise by f n (e x).

Equations

• NavierStokes.ActualReferenceRebase.pullField e f n x = f n (e x)

noncomputable def NavierStokes.ActualReferenceRebase.pullTriple {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃L[ℝ] E) (v : MeanIncrementBounds.Triple E) : MeanIncrementBounds.Triple D

Pull triple, given by ⟨pullField e v.radial, pullField e v.angular, pullField e v.axial⟩.

Equations

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

noncomputable def NavierStokes.ActualReferenceRebase.pullOperators {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃L[ℝ] E) (o : MeanIncrementBounds.Operators E) : MeanIncrementBounds.Operators D

Pull operators, bundling epsilon, radialFrequency, fastCoefficient, radius and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.ActualReferenceRebase.pullContext {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃L[ℝ] E) (c : CorrectionState.Context E) : CorrectionState.Context D

Pull context, bundling operators, base, virtualTheta, virtualAxial.

Equations

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

noncomputable def NavierStokes.ActualReferenceRebase.pullOscillation {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃L[ℝ] E) (u : CorrectionState.Oscillation E) : CorrectionState.Oscillation D

Pull oscillation, defined pointwise by u n (e x.1, x.2).

Equations

• NavierStokes.ActualReferenceRebase.pullOscillation e u n x = u n (e x.1, x.2)

noncomputable def NavierStokes.ActualReferenceRebase.pullErrors {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃L[ℝ] E) (u : CorrectionState.ExcludedErrors E) : CorrectionState.ExcludedErrors D

Pull errors, given by ⟨pullOscillation e u.base, pullOscillation e u.gaussian, pullOscillation e u.aliasError⟩.

Equations

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

noncomputable def NavierStokes.ActualReferenceRebase.pullState {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃L[ℝ] E) (u : CorrectionState.State E) : CorrectionState.State D

Pull state, bundling mean, pressure, oscillation, oscillatoryPressure and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.ActualReferenceRebase.pullCoefficients {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃L[ℝ] E) (a : HarmonicFields.Coefficients E) : HarmonicFields.Coefficients D

Pull coefficients, given by AddMonoidAlgebra.ofCoeff (Finsupp.mapRange (fun f : E → ℂ => fun x => f (e x)) rfl a.coeff).

Equations

• NavierStokes.ActualReferenceRebase.pullCoefficients e a = AddMonoidAlgebra.ofCoeff (Finsupp.mapRange (fun (f : E → ℂ) (x : D) => f (e x)) ⋯ a.coeff)

@[simp]

theorem NavierStokes.ActualReferenceRebase.pullCoefficients_apply {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃L[ℝ] E) (a : HarmonicFields.Coefficients E) (j : ℤ) (x : D) : (pullCoefficients e a).coeff j x = a.coeff j (e x)

theorem NavierStokes.ActualReferenceRebase.pullCoefficients_support {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃L[ℝ] E) (a : HarmonicFields.Coefficients E) : (pullCoefficients e a).support = a.support

theorem NavierStokes.ActualReferenceRebase.pullCoefficients_field {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃L[ℝ] E) (a : HarmonicFields.Coefficients E) (K : ℝ) (Phi : E → ℝ) (kp : ℤ) (x : D × ℝ) : HarmonicFields.field (pullCoefficients e a) K (fun (y : D) => Phi (e y)) kp x = HarmonicFields.field a K Phi kp (e x.1, x.2)

noncomputable def NavierStokes.ActualReferenceRebase.pullBlock {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃L[ℝ] E) (b : CorrectionState.HarmonicBlock E) : CorrectionState.HarmonicBlock D

Pull block, bundling velocity, pressure, frequency, phase and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.ActualReferenceRebase.pullBlockCoefficients {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃L[ℝ] E) (a : HarmonicResidual.BlockCoefficients E) : HarmonicResidual.BlockCoefficients D

Pull block coefficients, defined pointwise by pullCoefficients e (a n i).

Equations

• NavierStokes.ActualReferenceRebase.pullBlockCoefficients e a n i = NavierStokes.ActualReferenceRebase.pullCoefficients e (a n i)

theorem NavierStokes.ActualReferenceRebase.pullBlock_oscillation {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃L[ℝ] E) (b : CorrectionState.HarmonicBlock E) (n : ℕ) (x : D × ℝ) : (pullBlock e b).oscillation n x = b.oscillation n (e x.1, x.2)

theorem NavierStokes.ActualReferenceRebase.pullBlock_pressure {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃L[ℝ] E) (b : CorrectionState.HarmonicBlock E) (n : ℕ) (x : D × ℝ) : (pullBlock e b).oscillatoryPressure n x = b.oscillatoryPressure n (e x.1, x.2)

noncomputable def NavierStokes.ActualReferenceRebase.pullFrame {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃L[ℝ] E) (g : HarmonicResidual.Frame E) : HarmonicResidual.Frame D

Pull frame, bundling radius, radial, axial, time and the required compatibility proofs.

Equations

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

theorem NavierStokes.ActualReferenceRebase.pullContext_frame {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃L[ℝ] E) (c : CorrectionState.Context E) (n : ℕ) : HarmonicResidual.contextFrame (pullContext e c) n = pullFrame e (HarmonicResidual.contextFrame c n)

theorem NavierStokes.ActualReferenceRebase.pullFrame_on {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃L[ℝ] E) (g : HarmonicResidual.Frame E) : PhysicalResidualNaturality.FrameOn Set.univ e 1 1 (pullFrame e g) g

theorem NavierStokes.ActualReferenceRebase.pull_residualSource {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃L[ℝ] E) (c : CorrectionState.Context E) (u : CorrectionState.State E) (b : CorrectionState.HarmonicBlock E) (G A : HarmonicResidual.BlockCoefficients E) (j : ℤ) (n : ℕ) (x : D) : ParticularWaveAssembly.residualSource (pullContext e c) (pullState e u) (pullBlock e b) (pullBlockCoefficients e G) (pullBlockCoefficients e A) j n x = ParticularWaveAssembly.residualSource c u b G A j n (e x)

The full residual, rather than only its on-graph values, is pulled back. No carrier nondegeneracy or differentiability premise is needed.

noncomputable def NavierStokes.ActualReferenceRebase.pullStrip {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃L[ℝ] E) (s : WeightedClasses.StripData E) : WeightedClasses.StripData D

Pull strip, bundling domain, isOpen_domain, epsilon, epsilon_pos and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.ActualReferenceRebase.pullWave {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃L[ℝ] E) (a : LinearWaveBounds.WaveCoefficients E) : LinearWaveBounds.WaveCoefficients D

Pull wave, bundling radius, radialBase, frequencyBase, axialBase and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.ActualReferenceRebase.pullDirections {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃L[ℝ] E) (d : LinearWaveBounds.GraphDirections E) : LinearWaveBounds.GraphDirections D

Pull directions, bundling radial, auxiliary, axial, angular and the required compatibility proofs.

Equations

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

theorem NavierStokes.ActualReferenceRebase.pullDirections_radial {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃L[ℝ] E) (d : LinearWaveBounds.GraphDirections E) (n : ℕ) (x : D) : (pullDirections e d).radialField n x = e.symm (d.radialField n (e x))

theorem NavierStokes.ActualReferenceRebase.pullDirections_axial {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃L[ℝ] E) (d : LinearWaveBounds.GraphDirections E) (s : WeightedClasses.StripData E) (n : ℕ) (x : D) : (pullDirections e d).axialField (pullStrip e s) n x = e.symm (d.axialField s n (e x))

A separate, genuine native-reference assembly

noncomputable def NavierStokes.ActualReferenceRebase.inverseCover {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (k : ℕ) : (P × TorusInverse.Plane) ≃L[ℝ] P × TorusInverse.Plane

Inverse cover, given by (ContinuousLinearEquiv.refl ℝ P).prodCongr (coverPower k).symm.

Equations

• NavierStokes.ActualReferenceRebase.inverseCover k = (ContinuousLinearEquiv.refl ℝ P).prodCongr (NavierStokes.CommonCoverSolve.coverPower k).symm

@[simp]

theorem NavierStokes.ActualReferenceRebase.inverseCover_apply {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (k : ℕ) (x : P × TorusInverse.Plane) : (inverseCover k) x = (x.1, (CommonCoverSolve.coverPower k).symm x.2)

@[simp]

theorem NavierStokes.ActualReferenceRebase.inverseCover_symm_apply {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (k : ℕ) (x : P × TorusInverse.Plane) : (inverseCover k).symm x = (x.1, (CommonCoverSolve.coverPower k) x.2)

noncomputable def NavierStokes.ActualReferenceRebase.rebaseAssembly {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (D : ParticularWaveAssembly.AssemblyData P) (k : ℕ) : ParticularWaveAssembly.AssemblyData P

All fields, all directions and the complete source are expressed in the native fast coordinate. This assembly is only a reference view; the target solver keeps its original common-cover data.

Equations

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

theorem NavierStokes.ActualReferenceRebase.rebaseAssembly_source {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (D : ParticularWaveAssembly.AssemblyData P) (k : ℕ) (j : ℤ) (n : ℕ) (x : P × TorusInverse.Plane) : ParticularWaveAssembly.residualSource (rebaseAssembly D k).context (rebaseAssembly D k).state (rebaseAssembly D k).carrierBlock (rebaseAssembly D k).gaussianInput (rebaseAssembly D k).aliasInput j n x = ParticularWaveAssembly.residualSource D.context D.state D.carrierBlock D.gaussianInput D.aliasInput j n (x.1, (CommonCoverSolve.coverPower k).symm x.2)

theorem NavierStokes.ActualReferenceRebase.rebaseAssembly_referenceIdentity (D : ParticularWaveAssembly.AssemblyData PhysicalParticularWave.Parameter) (k : ℕ) : PhysicalParticularWave.ReferenceIdentity (rebaseAssembly D k)

Binding to the one actual initializer choice and current cycle state

noncomputable def NavierStokes.ActualReferenceRebase.referenceResidualSource {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (l : ActualParticularStageControls.Label B N0) (j : ℤ) : PhysicalResidualNaturality.Associated → HarmonicCalculus.ComplexVector

Reference residual source as an element of PhysicalResidualNaturality.Associated → ComplexVector.

Equations

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

noncomputable def NavierStokes.ActualReferenceRebase.nativeAssembly {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (l : ActualParticularStageControls.Label B N0) : ParticularWaveAssembly.AssemblyData PhysicalParticularWave.Parameter

Native assembly, given by rebaseAssembly (ActualParticularStageControls.assembly x l) (ActualParticularStageControls.gap l (BaseChartJets.cellBand l.2)).

Equations

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

theorem NavierStokes.ActualReferenceRebase.nativeAssembly_reference {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (l : ActualParticularStageControls.Label B N0) : (nativeAssembly x l).reference = ActualParticularStageControls.reference l

theorem NavierStokes.ActualReferenceRebase.nativeAssembly_source {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (l : ActualParticularStageControls.Label B N0) (j : ℤ) : PhysicalParticularWave.referenceSource (nativeAssembly x l) j = referenceResidualSource x l j

theorem NavierStokes.ActualReferenceRebase.nativeAssembly_identity {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (l : ActualParticularStageControls.Label B N0) : PhysicalParticularWave.ReferenceIdentity (nativeAssembly x l)

theorem NavierStokes.ActualReferenceRebase.nativeAssembly_raw {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (l : ActualParticularStageControls.Label B N0) (j : ℤ) : PhysicalParticularWave.referenceRaw (nativeAssembly x l) j = ParticularWaveAssembly.angleLift (ParticularWaveBounds.commonVelocity ((ActualParticularStageControls.reference l).tangent j) (referenceResidualSource x l j) (ActualParticularStageControls.reference l).geometry ⋯ (ActualParticularStageControls.reference l).cutoff)

theorem NavierStokes.ActualReferenceRebase.nativeAssembly_rawPressure {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (l : ActualParticularStageControls.Label B N0) (j : ℤ) : PhysicalParticularWave.referenceRawPressure (nativeAssembly x l) j = ParticularWaveAssembly.angleLift (ParticularWaveBounds.commonPressure ((ActualParticularStageControls.reference l).tangent j) (referenceResidualSource x l j) (ActualParticularStageControls.reference l).geometry ⋯ (ActualParticularStageControls.reference l).cutoff (↑j * (x.coefficients.blocks l).frequency (BaseChartJets.cellBand l.2)))

The native reference has its own actual frame and phase.

@[simp]

theorem NavierStokes.ActualReferenceRebase.associatedToLift_symm_apply (z : PhysicalResidualNaturality.Lift) : PhysicalResidualNaturality.associatedToLift.symm z = ((z.1, z.2.1.2, z.2.1.1), z.2.2)

@[simp]

theorem NavierStokes.ActualReferenceRebase.cycleAssoc_apply (z : CorrectionStep.CyclePoint) : CorrectionStep.cycleAssoc z = ((z.1, z.2.1), z.2.2)

@[simp]

theorem NavierStokes.ActualReferenceRebase.cycleAssoc_symm_apply (z : PhysicalResidualNaturality.Associated) : CorrectionStep.cycleAssoc.symm z = (z.1.1, z.1.2, z.2)

theorem NavierStokes.ActualReferenceRebase.inverseCover_associatedFrame (h Q : ℝ) (i k : ℕ) : pullFrame (inverseCover k) (PhysicalResidualNaturality.associatedFrame h Q i) = PhysicalResidualNaturality.associatedFrame h Q (i + k)

theorem NavierStokes.ActualReferenceRebase.associatedContext_frame (B n : ℕ) : HarmonicResidual.contextFrame ActualParticularStageControls.associatedContext n = PhysicalResidualNaturality.associatedFrame CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n)

theorem NavierStokes.ActualReferenceRebase.nativeAssembly_frame {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (l : ActualParticularStageControls.Label B N0) : HarmonicResidual.contextFrame (nativeAssembly x l).context (BaseChartJets.cellBand l.2) = PhysicalResidualNaturality.associatedFrame CorrectionInitialization.ActualPrimary.h (ChartScales.Q (BaseChartJets.cellBand l.2)) (ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2))

theorem NavierStokes.ActualReferenceRebase.rebaseAssembly_phase (D : ParticularWaveAssembly.AssemblyData PhysicalParticularWave.Parameter) (k : ℕ) (j : ℤ) (z : PhysicalParticularWave.WaveSpace) : PhysicalParticularWave.referencePhase (rebaseAssembly D k) j z = PhysicalParticularWave.referencePhase D j ((inverseCover k) z)

theorem NavierStokes.ActualReferenceRebase.rebaseAssembly_frequency (D : ParticularWaveAssembly.AssemblyData PhysicalParticularWave.Parameter) (k : ℕ) (j : ℤ) : PhysicalParticularWave.referenceFrequency (rebaseAssembly D k) j = PhysicalParticularWave.referenceFrequency D j

theorem NavierStokes.ActualReferenceRebase.ratioPower_self {Q : ℝ} (hQ : 0 < Q) (a : ℝ) : PhysicalParticularWave.ratioPower Q Q a = 1

theorem NavierStokes.ActualReferenceRebase.cylinderChange_inverseCover (h : ℝ) {Q : ℝ} (hQ : 0 < Q) (k : ℕ) (z : PhysicalParticularWave.WaveSpace) : (PhysicalParticularWave.cylinderChange h Q Q k) (PhysicalParticularWave.waveEquiv.symm ((inverseCover k) z)) = PhysicalParticularWave.waveEquiv.symm z

theorem NavierStokes.ActualReferenceRebase.nativeAssembly_background_phase {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (l : ActualParticularStageControls.Label B N0) (z : PhysicalParticularWave.WaveSpace) : (nativeAssembly x l).background.phase (BaseChartJets.cellBand l.2) z = ActualSignedGeometry.preparedPhase CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation CorrectionInitialization.ActualPrimary.slots (CorrectionInitialization.ActualPrimary.choice B N0).prepared l.1 l.2 (PhysicalParticularWave.waveEquiv.symm z)

Dependence of a copy solve on one complete parameter fiber

theorem NavierStokes.ActualReferenceRebase.real_copySolve_source_congr {Q : Type} (t : CommonCoverSolve.TangentData Q ProblemStatement.Space) (f g : Q × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (G : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (q : Q) (hf : ∀ (Y : TorusInverse.Plane), f (q, Y) = g (q, Y)) (copy : TorusInverse.Frequency) (Y : TorusInverse.Plane) : (ParticularWaveBounds.realData t f).linearData.copySolve G hab copy (q, Y) = (ParticularWaveBounds.realData t g).linearData.copySolve G hab copy (q, Y)

theorem NavierStokes.ActualReferenceRebase.imag_copySolve_source_congr {Q : Type} (t : CommonCoverSolve.TangentData Q ProblemStatement.Space) (f g : Q × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (G : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (q : Q) (hf : ∀ (Y : TorusInverse.Plane), f (q, Y) = g (q, Y)) (copy : TorusInverse.Frequency) (Y : TorusInverse.Plane) : (ParticularWaveBounds.imagData t f).linearData.copySolve G hab copy (q, Y) = (ParticularWaveBounds.imagData t g).linearData.copySolve G hab copy (q, Y)

theorem NavierStokes.ActualReferenceRebase.copyVelocity_source_congr {Q : Type} (t : CommonCoverSolve.TangentData Q ProblemStatement.Space) (f g : Q × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (G : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (q : Q) (hf : ∀ (Y : TorusInverse.Plane), f (q, Y) = g (q, Y)) (copy : TorusInverse.Frequency) (Y : TorusInverse.Plane) : ParticularWaveBounds.complexCopyVelocity t f G hab copy (q, Y) = ParticularWaveBounds.complexCopyVelocity t g G hab copy (q, Y)

theorem NavierStokes.ActualReferenceRebase.copyPressure_source_congr {Q : Type} (t : CommonCoverSolve.TangentData Q ProblemStatement.Space) (f g : Q × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (G : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (q : Q) (hf : ∀ (Y : TorusInverse.Plane), f (q, Y) = g (q, Y)) (copy : TorusInverse.Frequency) (K : ℝ) (Y : TorusInverse.Plane) : ParticularWaveBounds.complexCopyPressure t f G hab copy K (q, Y) = ParticularWaveBounds.complexCopyPressure t g G hab copy K (q, Y)

theorem NavierStokes.ActualReferenceRebase.commonVelocity_source_congr {Q : Type} (t : CommonCoverSolve.TangentData Q ProblemStatement.Space) (f g : Q × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (G : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (cutoff : TorusInverse.Plane → ℝ) (q : Q) (hf : ∀ (Y : TorusInverse.Plane), f (q, Y) = g (q, Y)) (Y : TorusInverse.Plane) : ParticularWaveBounds.commonVelocity t f G hab cutoff (q, Y) = ParticularWaveBounds.commonVelocity t g G hab cutoff (q, Y)

theorem NavierStokes.ActualReferenceRebase.commonPressure_source_congr {Q : Type} (t : CommonCoverSolve.TangentData Q ProblemStatement.Space) (f g : Q × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (G : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (cutoff : TorusInverse.Plane → ℝ) (K : ℝ) (q : Q) (hf : ∀ (Y : TorusInverse.Plane), f (q, Y) = g (q, Y)) (Y : TorusInverse.Plane) : ParticularWaveBounds.commonPressure t f G hab cutoff K (q, Y) = ParticularWaveBounds.commonPressure t g G hab cutoff K (q, Y)

Actual common-band comparison, without truncated reverse gaps

noncomputable def NavierStokes.ActualReferenceRebase.commonReferenceChart {B N0 : ℕ} (l : ActualParticularStageControls.Label B N0) (n : ℕ) : PhysicalResidualNaturality.Associated ≃L[ℝ] PhysicalResidualNaturality.Associated

Common reference chart as an element of PhysicalResidualNaturality.Associated ≃L[ℝ] PhysicalResidualNaturality.Associated.

Equations

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

@[simp]

theorem NavierStokes.ActualReferenceRebase.commonReferenceChart_apply {B N0 : ℕ} (l : ActualParticularStageControls.Label B N0) (n : ℕ) (z : PhysicalResidualNaturality.Associated) : (commonReferenceChart l n) z = (PhysicalParticularWave.parameterChange CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (ChartScales.Q (BaseChartJets.cellBand l.2)) z.1, (CommonCoverSolve.coverPower (ActualParticularStageControls.gap l (BaseChartJets.cellBand l.2))).symm ((CommonCoverSolve.coverPower (ActualParticularStageControls.gap l n)) z.2))

theorem NavierStokes.ActualReferenceRebase.associatedChart_stateChart (n m k : ℕ) (z : PhysicalResidualNaturality.Associated) : CorrectionStep.cycleAssoc.symm ((PhysicalResidualNaturality.associatedChart CorrectionInitialization.ActualPrimary.h ⋯ ⋯ k) z) = (GaugeStateCoherence.bandChartEquiv CorrectionInitialization.ActualPrimary.h n m k) (CorrectionStep.cycleAssoc.symm z)

theorem NavierStokes.ActualReferenceRebase.commonReferenceChart_forward {B N0 : ℕ} (l : ActualParticularStageControls.Label B N0) (n k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2)) (z : PhysicalResidualNaturality.Associated) : CorrectionStep.cycleAssoc.symm ((commonReferenceChart l n) z) = (GaugeStateCoherence.bandChartEquiv CorrectionInitialization.ActualPrimary.h n (BaseChartJets.cellBand l.2) k) (CorrectionStep.cycleAssoc.symm z)

theorem NavierStokes.ActualReferenceRebase.assembly_source {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (l : ActualParticularStageControls.Label B N0) (j : ℤ) (n : ℕ) (z : PhysicalResidualNaturality.Associated) : ParticularWaveAssembly.residualSource (ActualParticularStageControls.assembly x l).context (ActualParticularStageControls.assembly x l).state (ActualParticularStageControls.assembly x l).carrierBlock (ActualParticularStageControls.assembly x l).gaussianInput (ActualParticularStageControls.assembly x l).aliasInput j n z = ParticularWaveAssembly.residualSource (CorrectionInitialization.ActualPrimary.commonContext B) x.state (x.coefficients.blocks l) (x.coefficients.gaussian l) (x.coefficients.aliasCoefficients l) j n (CorrectionStep.cycleAssoc.symm z)

theorem NavierStokes.ActualReferenceRebase.transportedSource_eq_commonReference {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (l : ActualParticularStageControls.Label B N0) (j : ℤ) (n : ℕ) (z : PhysicalResidualNaturality.Associated) : PhysicalParticularWave.transportedResidualSource (nativeAssembly x l) CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (ChartScales.Q (BaseChartJets.cellBand l.2)) (ActualParticularStageControls.gap l n) j z = PhysicalParticularWave.sourceWeight CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (ChartScales.Q (BaseChartJets.cellBand l.2)) • ParticularWaveAssembly.residualSource (CorrectionInitialization.ActualPrimary.commonContext B) x.state (x.coefficients.blocks l) (x.coefficients.gaussian l) (x.coefficients.aliasCoefficients l) j (BaseChartJets.cellBand l.2) (CorrectionStep.cycleAssoc.symm ((commonReferenceChart l n) z))

theorem NavierStokes.ActualReferenceRebase.state_sourceWeight (n m : ℕ) : GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m * GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m * GaugeStateCoherence.bandScale n m = PhysicalParticularWave.sourceWeight CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (ChartScales.Q m)

theorem NavierStokes.ActualReferenceRebase.source_forward {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (l : ActualParticularStageControls.Label B N0) {V : Set TorusInverse.Plane} (hV : IsOpen V) (htime : ∀ s ∈ V, 0 < s.1) (n k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2)) (HS : PhysicalResidualNaturality.StateOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.bandChartEquiv CorrectionInitialization.ActualPrimary.h n (BaseChartJets.cellBand l.2) k) (GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n (BaseChartJets.cellBand l.2)) (GaugeStateCoherence.bandScale n (BaseChartJets.cellBand l.2)) x.state x.state n (BaseChartJets.cellBand l.2)) (HB : PhysicalResidualNaturality.BlockFieldsOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.bandChartEquiv CorrectionInitialization.ActualPrimary.h n (BaseChartJets.cellBand l.2) k) (GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n (BaseChartJets.cellBand l.2)) (GaugeStateCoherence.bandScale n (BaseChartJets.cellBand l.2)) (x.coefficients.blocks l) (x.coefficients.blocks l) (x.coefficients.gaussian l) (x.coefficients.aliasCoefficients l) (x.coefficients.gaussian l) (x.coefficients.aliasCoefficients l) n (BaseChartJets.cellBand l.2)) (j : ℤ) (z : PhysicalResidualNaturality.Associated) (hz : z.1.2 ∈ V) : ParticularWaveAssembly.residualSource (ActualParticularStageControls.assembly x l).context (ActualParticularStageControls.assembly x l).state (ActualParticularStageControls.assembly x l).carrierBlock (ActualParticularStageControls.assembly x l).gaussianInput (ActualParticularStageControls.assembly x l).aliasInput j n z = PhysicalParticularWave.transportedResidualSource (nativeAssembly x l) CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (ChartScales.Q (BaseChartJets.cellBand l.2)) (ActualParticularStageControls.gap l n) j z

This consumes exactly the full-fiber state and block conclusions of the physical recurrence. It does not assume source or solved-wave coherence.

The reference operator identities hold on the entire free lift.

noncomputable def NavierStokes.ActualReferenceRebase.angleEmbed (v : PhysicalResidualNaturality.Associated) : PhysicalParticularWave.WaveSpace

Angle embed, given by ((v.1, 0), v.2).

Equations

• NavierStokes.ActualReferenceRebase.angleEmbed v = ((v.1, 0), v.2)

theorem NavierStokes.ActualReferenceRebase.associatedDirections_radial (B n : ℕ) (z : PhysicalParticularWave.WaveSpace) : ActualParticularStageControls.directions.radialField n z = angleEmbed ((HarmonicResidual.contextFrame ActualParticularStageControls.associatedContext n).radial (z.1.1, z.2))

theorem NavierStokes.ActualReferenceRebase.associatedDirections_axial (B n : ℕ) (z : PhysicalParticularWave.WaveSpace) : ActualParticularStageControls.directions.axialField (CorrectionStep.ParticularParameters.nativeStrip ActualParticularStageControls.associatedStrip) n z = angleEmbed ((HarmonicResidual.contextFrame ActualParticularStageControls.associatedContext n).axial (z.1.1, z.2))

theorem NavierStokes.ActualReferenceRebase.nativeDirections_radial {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (l : ActualParticularStageControls.Label B N0) (n : ℕ) (z : PhysicalParticularWave.WaveSpace) : (nativeAssembly x l).directions.radialField n z = angleEmbed ((HarmonicResidual.contextFrame (nativeAssembly x l).context n).radial (z.1.1, z.2))

theorem NavierStokes.ActualReferenceRebase.nativeDirections_axial {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (l : ActualParticularStageControls.Label B N0) (n : ℕ) (z : PhysicalParticularWave.WaveSpace) : (nativeAssembly x l).directions.axialField (nativeAssembly x l).strip n z = angleEmbed ((HarmonicResidual.contextFrame (nativeAssembly x l).context n).axial (z.1.1, z.2))

theorem NavierStokes.ActualReferenceRebase.nativeDirections_angular {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (l : ActualParticularStageControls.Label B N0) : (nativeAssembly x l).directions.angular = ((0, 1), 0)

theorem NavierStokes.ActualReferenceRebase.nativeAssembly_referenceChart {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (l : ActualParticularStageControls.Label B N0) : PhysicalParticularWave.ReferenceChart (nativeAssembly x l) CorrectionInitialization.ActualPrimary.h (ChartScales.Q (BaseChartJets.cellBand l.2)) (ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2))

Reverse index order and the original recurrence interface

theorem NavierStokes.ActualReferenceRebase.ratioPower_reverse_mul {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (a : ℝ) : PhysicalParticularWave.ratioPower Q Qr a * PhysicalParticularWave.ratioPower Qr Q a = 1

theorem NavierStokes.ActualReferenceRebase.parameterChange_inverse (h : ℝ) {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (p : PhysicalParticularWave.Parameter) : PhysicalParticularWave.parameterChange h Qr Q (PhysicalParticularWave.parameterChange h Q Qr p) = p

theorem NavierStokes.ActualReferenceRebase.commonReferenceChart_backward {B N0 : ℕ} (l : ActualParticularStageControls.Label B N0) (n k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2) + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n) (hn : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n ≤ ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2)) (z : PhysicalResidualNaturality.Associated) : (GaugeStateCoherence.bandChartEquiv CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2) n k) (CorrectionStep.cycleAssoc.symm ((commonReferenceChart l n) z)) = CorrectionStep.cycleAssoc.symm z

@[reducible, inline]

abbrev NavierStokes.ActualReferenceRebase.StateComparison {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (V : Set TorusInverse.Plane) (n m k : ℕ) : Prop

State comparison type used in actual reference rebase.

Equations

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

@[reducible, inline]

abbrev NavierStokes.ActualReferenceRebase.BlockComparison {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (l : ActualParticularStageControls.Label B N0) (V : Set TorusInverse.Plane) (n m k : ℕ) : Prop

Block comparison type used in actual reference rebase.

Equations

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

theorem NavierStokes.ActualReferenceRebase.source_backward {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (l : ActualParticularStageControls.Label B N0) {V : Set TorusInverse.Plane} (hV : IsOpen V) (htime : ∀ s ∈ V, 0 < s.1) (n k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2) + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n) (hn : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n ≤ ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2)) (HS : StateComparison x V (BaseChartJets.cellBand l.2) n k) (HB : BlockComparison x l V (BaseChartJets.cellBand l.2) n k) (j : ℤ) (z : PhysicalResidualNaturality.Associated) (hz : ((commonReferenceChart l n) z).1.2 ∈ V) : ParticularWaveAssembly.residualSource (ActualParticularStageControls.assembly x l).context (ActualParticularStageControls.assembly x l).state (ActualParticularStageControls.assembly x l).carrierBlock (ActualParticularStageControls.assembly x l).gaussianInput (ActualParticularStageControls.assembly x l).aliasInput j n z = PhysicalParticularWave.transportedResidualSource (nativeAssembly x l) CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (ChartScales.Q (BaseChartJets.cellBand l.2)) (ActualParticularStageControls.gap l n) j z

Regularity and support are transported, not postulated anew

theorem NavierStokes.ActualReferenceRebase.referenceResidualSource_smooth {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (l : ActualParticularStageControls.Label B N0) (j : ℤ) (V : Set PhysicalParticularWave.Parameter) (hf : ContDiffOn ℝ (↑⊤) (ParticularWaveAssembly.residualSource (ActualParticularStageControls.assembly x l).context (ActualParticularStageControls.assembly x l).state (ActualParticularStageControls.assembly x l).carrierBlock (ActualParticularStageControls.assembly x l).gaussianInput (ActualParticularStageControls.assembly x l).aliasInput j (BaseChartJets.cellBand l.2)) (V ×ˢ Set.univ)) : ContDiffOn ℝ (↑⊤) (referenceResidualSource x l j) (V ×ˢ Set.univ)

theorem NavierStokes.ActualReferenceRebase.referenceResidualSource_support {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (l : ActualParticularStageControls.Label B N0) (j : ℤ) : Function.support (referenceResidualSource x l j) = ⇑(inverseCover (ActualParticularStageControls.gap l (BaseChartJets.cellBand l.2))) ⁻¹' Function.support (ParticularWaveAssembly.residualSource (ActualParticularStageControls.assembly x l).context (ActualParticularStageControls.assembly x l).state (ActualParticularStageControls.assembly x l).carrierBlock (ActualParticularStageControls.assembly x l).gaussianInput (ActualParticularStageControls.assembly x l).aliasInput j (BaseChartJets.cellBand l.2))

The unchanged target solve uses this native reference

theorem NavierStokes.ActualReferenceRebase.residualBandAmplitude_rebase_at (D : ParticularWaveAssembly.AssemblyData PhysicalParticularWave.Parameter) (h : ℝ) {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (kr gap : ℕ) (K : ℝ) (j : ℤ) (n : ℕ) (p : PhysicalParticularWave.Parameter) (hf : ∀ (Y : TorusInverse.Plane), ParticularWaveAssembly.residualSource D.context D.state D.carrierBlock D.gaussianInput D.aliasInput j n (p, Y) = PhysicalParticularWave.transportedResidualSource (rebaseAssembly D kr) h Q Qr gap j (p, Y)) (Y : TorusInverse.Plane) : PhysicalParticularWave.residualBandAmplitude D h hQ hQr gap K j n (p, Y) = PhysicalParticularWave.bandAmplitude (rebaseAssembly D kr) h hQ hQr gap K j (p, Y)

theorem NavierStokes.ActualReferenceRebase.residualBandPressure_rebase_at (D : ParticularWaveAssembly.AssemblyData PhysicalParticularWave.Parameter) (h : ℝ) {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (kr gap : ℕ) (K : ℝ) (j : ℤ) (n : ℕ) (p : PhysicalParticularWave.Parameter) (hf : ∀ (Y : TorusInverse.Plane), ParticularWaveAssembly.residualSource D.context D.state D.carrierBlock D.gaussianInput D.aliasInput j n (p, Y) = PhysicalParticularWave.transportedResidualSource (rebaseAssembly D kr) h Q Qr gap j (p, Y)) (Y : TorusInverse.Plane) : PhysicalParticularWave.residualBandPressure D h hQ hQr gap K j n (p, Y) = PhysicalParticularWave.bandPressure (rebaseAssembly D kr) h hQ hQr gap K j (p, Y)

noncomputable def NavierStokes.ActualReferenceRebase.actualCoefficients {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (l : ActualParticularStageControls.Label B N0) (j : ℤ) : LinearWaveBounds.WaveCoefficients PhysicalParticularWave.WaveSpace

The literal current-source common coefficient in the actual stage.

Equations

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

theorem NavierStokes.ActualReferenceRebase.actualAmplitude_rebase_at {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (l : ActualParticularStageControls.Label B N0) (j : ℤ) (n : ℕ) (p : PhysicalParticularWave.Parameter) (hf : ∀ (Y : TorusInverse.Plane), ParticularWaveAssembly.residualSource (ActualParticularStageControls.assembly x l).context (ActualParticularStageControls.assembly x l).state (ActualParticularStageControls.assembly x l).carrierBlock (ActualParticularStageControls.assembly x l).gaussianInput (ActualParticularStageControls.assembly x l).aliasInput j n (p, Y) = PhysicalParticularWave.transportedResidualSource (nativeAssembly x l) CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (ChartScales.Q (BaseChartJets.cellBand l.2)) (ActualParticularStageControls.gap l n) j (p, Y)) (theta : ℝ) (Y : TorusInverse.Plane) : (actualCoefficients x l j).amplitude n ((p, theta), Y) = PhysicalParticularWave.bandAmplitude (nativeAssembly x l) CorrectionInitialization.ActualPrimary.h ⋯ ⋯ (ActualParticularStageControls.gap l n) (↑j * (x.coefficients.blocks l).frequency n) j (p, Y)

theorem NavierStokes.ActualReferenceRebase.actualPressure_rebase_at {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (l : ActualParticularStageControls.Label B N0) (j : ℤ) (n : ℕ) (p : PhysicalParticularWave.Parameter) (hK : ↑j * (x.coefficients.blocks l).frequency n ≠ 0) (hf : ∀ (Y : TorusInverse.Plane), ParticularWaveAssembly.residualSource (ActualParticularStageControls.assembly x l).context (ActualParticularStageControls.assembly x l).state (ActualParticularStageControls.assembly x l).carrierBlock (ActualParticularStageControls.assembly x l).gaussianInput (ActualParticularStageControls.assembly x l).aliasInput j n (p, Y) = PhysicalParticularWave.transportedResidualSource (nativeAssembly x l) CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (ChartScales.Q (BaseChartJets.cellBand l.2)) (ActualParticularStageControls.gap l n) j (p, Y)) (theta : ℝ) (Y : TorusInverse.Plane) : (actualCoefficients x l j).pressure n ((p, theta), Y) = PhysicalParticularWave.bandPressure (nativeAssembly x l) CorrectionInitialization.ActualPrimary.h ⋯ ⋯ (ActualParticularStageControls.gap l n) (↑j * (x.coefficients.blocks l).frequency n) j (p, Y)

theorem NavierStokes.ActualReferenceRebase.actualAmplitude_forward {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (l : ActualParticularStageControls.Label B N0) {V : Set TorusInverse.Plane} (hV : IsOpen V) (htime : ∀ s ∈ V, 0 < s.1) (n k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2)) (HS : StateComparison x V n (BaseChartJets.cellBand l.2) k) (HB : BlockComparison x l V n (BaseChartJets.cellBand l.2) k) (j : ℤ) (p : PhysicalParticularWave.Parameter) (hp : p.2 ∈ V) (theta : ℝ) (Y : TorusInverse.Plane) : (actualCoefficients x l j).amplitude n ((p, theta), Y) = PhysicalParticularWave.bandAmplitude (nativeAssembly x l) CorrectionInitialization.ActualPrimary.h ⋯ ⋯ (ActualParticularStageControls.gap l n) (↑j * (x.coefficients.blocks l).frequency n) j (p, Y)

theorem NavierStokes.ActualReferenceRebase.actualPressure_forward {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (l : ActualParticularStageControls.Label B N0) {V : Set TorusInverse.Plane} (hV : IsOpen V) (htime : ∀ s ∈ V, 0 < s.1) (n k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2)) (HS : StateComparison x V n (BaseChartJets.cellBand l.2) k) (HB : BlockComparison x l V n (BaseChartJets.cellBand l.2) k) (j : ℤ) (hK : ↑j * (x.coefficients.blocks l).frequency n ≠ 0) (p : PhysicalParticularWave.Parameter) (hp : p.2 ∈ V) (theta : ℝ) (Y : TorusInverse.Plane) : (actualCoefficients x l j).pressure n ((p, theta), Y) = PhysicalParticularWave.bandPressure (nativeAssembly x l) CorrectionInitialization.ActualPrimary.h ⋯ ⋯ (ActualParticularStageControls.gap l n) (↑j * (x.coefficients.blocks l).frequency n) j (p, Y)

theorem NavierStokes.ActualReferenceRebase.actualAmplitude_backward {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (l : ActualParticularStageControls.Label B N0) {V : Set TorusInverse.Plane} (hV : IsOpen V) (htime : ∀ s ∈ V, 0 < s.1) (n k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2) + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n) (hn : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n ≤ ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2)) (HS : StateComparison x V (BaseChartJets.cellBand l.2) n k) (HB : BlockComparison x l V (BaseChartJets.cellBand l.2) n k) (j : ℤ) (p : PhysicalParticularWave.Parameter) (hp : (PhysicalParticularWave.parameterChange CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (ChartScales.Q (BaseChartJets.cellBand l.2)) p).2 ∈ V) (theta : ℝ) (Y : TorusInverse.Plane) : (actualCoefficients x l j).amplitude n ((p, theta), Y) = PhysicalParticularWave.bandAmplitude (nativeAssembly x l) CorrectionInitialization.ActualPrimary.h ⋯ ⋯ (ActualParticularStageControls.gap l n) (↑j * (x.coefficients.blocks l).frequency n) j (p, Y)

theorem NavierStokes.ActualReferenceRebase.actualPressure_backward {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (l : ActualParticularStageControls.Label B N0) {V : Set TorusInverse.Plane} (hV : IsOpen V) (htime : ∀ s ∈ V, 0 < s.1) (n k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2) + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n) (hn : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n ≤ ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2)) (HS : StateComparison x V (BaseChartJets.cellBand l.2) n k) (HB : BlockComparison x l V (BaseChartJets.cellBand l.2) n k) (j : ℤ) (hK : ↑j * (x.coefficients.blocks l).frequency n ≠ 0) (p : PhysicalParticularWave.Parameter) (hp : (PhysicalParticularWave.parameterChange CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (ChartScales.Q (BaseChartJets.cellBand l.2)) p).2 ∈ V) (theta : ℝ) (Y : TorusInverse.Plane) : (actualCoefficients x l j).pressure n ((p, theta), Y) = PhysicalParticularWave.bandPressure (nativeAssembly x l) CorrectionInitialization.ActualPrimary.h ⋯ ⋯ (ActualParticularStageControls.gap l n) (↑j * (x.coefficients.blocks l).frequency n) j (p, Y)

The full carrier uses the same rebase, including the angular integer.

theorem NavierStokes.ActualReferenceRebase.carrier_phase_rebase {K Kr J a theta phi psi : ℝ} (hK : K ≠ 0) (hKr : Kr ≠ 0) (hJ : J ≠ 0) (hphi : K * phi = Kr * psi) : J * Kr / (J * K) * (psi + a / Kr * theta) = phi + a / K * theta

theorem NavierStokes.ActualReferenceRebase.actualPhase_rebase_at {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (l : ActualParticularStageControls.Label B N0) (j : ℤ) (hj : j ≠ 0) (n : ℕ) (hn : (x.coefficients.blocks l).frequency n ≠ 0) (hm : (x.coefficients.blocks l).frequency (BaseChartJets.cellBand l.2) ≠ 0) (p : PhysicalParticularWave.Parameter) (Y : TorusInverse.Plane) (hp : (x.coefficients.blocks l).frequency n * (x.coefficients.blocks l).phase n (CorrectionStep.cycleAssoc.symm (p, Y)) = (x.coefficients.blocks l).frequency (BaseChartJets.cellBand l.2) * (x.coefficients.blocks l).phase (BaseChartJets.cellBand l.2) (CorrectionStep.cycleAssoc.symm ((commonReferenceChart l n) (p, Y)))) (ha : (x.coefficients.blocks l).angularFrequency n = (x.coefficients.blocks l).angularFrequency (BaseChartJets.cellBand l.2)) (theta : ℝ) : PhysicalParticularWave.bandPhase (nativeAssembly x l) CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (ChartScales.Q (BaseChartJets.cellBand l.2)) (ActualParticularStageControls.gap l n) (↑j * (x.coefficients.blocks l).frequency n) j (PhysicalParticularWave.waveEquiv.symm ((p, theta), Y)) = (actualCoefficients x l j).phase n ((p, theta), Y)

theorem NavierStokes.ActualReferenceRebase.actualPhase_forward {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (l : ActualParticularStageControls.Label B N0) (V : Set TorusInverse.Plane) (n k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2)) (HB : BlockComparison x l V n (BaseChartJets.cellBand l.2) k) (j : ℤ) (hj : j ≠ 0) (hn : (x.coefficients.blocks l).frequency n ≠ 0) (hm : (x.coefficients.blocks l).frequency (BaseChartJets.cellBand l.2) ≠ 0) (p : PhysicalParticularWave.Parameter) (hp : p.2 ∈ V) (theta : ℝ) (Y : TorusInverse.Plane) : PhysicalParticularWave.bandPhase (nativeAssembly x l) CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (ChartScales.Q (BaseChartJets.cellBand l.2)) (ActualParticularStageControls.gap l n) (↑j * (x.coefficients.blocks l).frequency n) j (PhysicalParticularWave.waveEquiv.symm ((p, theta), Y)) = (actualCoefficients x l j).phase n ((p, theta), Y)

theorem NavierStokes.ActualReferenceRebase.actualPhase_backward {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (l : ActualParticularStageControls.Label B N0) (V : Set TorusInverse.Plane) (n k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2) + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n) (hcover : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n ≤ ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2)) (HB : BlockComparison x l V (BaseChartJets.cellBand l.2) n k) (j : ℤ) (hj : j ≠ 0) (hn : (x.coefficients.blocks l).frequency n ≠ 0) (hm : (x.coefficients.blocks l).frequency (BaseChartJets.cellBand l.2) ≠ 0) (p : PhysicalParticularWave.Parameter) (hp : (PhysicalParticularWave.parameterChange CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (ChartScales.Q (BaseChartJets.cellBand l.2)) p).2 ∈ V) (theta : ℝ) (Y : TorusInverse.Plane) : PhysicalParticularWave.bandPhase (nativeAssembly x l) CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (ChartScales.Q (BaseChartJets.cellBand l.2)) (ActualParticularStageControls.gap l n) (↑j * (x.coefficients.blocks l).frequency n) j (PhysicalParticularWave.waveEquiv.symm ((p, theta), Y)) = (actualCoefficients x l j).phase n ((p, theta), Y)

Precisely the inherited lattice is retained.

theorem NavierStokes.ActualReferenceRebase.referenceResidualSource_subcoverPeriodic {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (l : ActualParticularStageControls.Label B N0) (j : ℤ) (p : PhysicalParticularWave.Parameter) (hf : CommonCoverSolve.PeriodicAt (ParticularWaveAssembly.residualSource (ActualParticularStageControls.assembly x l).context (ActualParticularStageControls.assembly x l).state (ActualParticularStageControls.assembly x l).carrierBlock (ActualParticularStageControls.assembly x l).gaussianInput (ActualParticularStageControls.assembly x l).aliasInput j (BaseChartJets.cellBand l.2)) p) : SubcoverPeriodicity.SubcoverPeriodicAt (ActualParticularStageControls.gap l (BaseChartJets.cellBand l.2)) (referenceResidualSource x l j) p

theorem NavierStokes.ActualReferenceRebase.nativeRaw_subcoverPeriodic {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (l : ActualParticularStageControls.Label B N0) (j : ℤ) (p : PhysicalParticularWave.Parameter) (hf : CommonCoverSolve.PeriodicAt (ParticularWaveAssembly.residualSource (ActualParticularStageControls.assembly x l).context (ActualParticularStageControls.assembly x l).state (ActualParticularStageControls.assembly x l).carrierBlock (ActualParticularStageControls.assembly x l).gaussianInput (ActualParticularStageControls.assembly x l).aliasInput j (BaseChartJets.cellBand l.2)) p) : SubcoverPeriodicity.SubcoverPeriodicAt (ActualParticularStageControls.gap l (BaseChartJets.cellBand l.2)) (ParticularWaveBounds.commonVelocity ((ActualParticularStageControls.reference l).tangent j) (referenceResidualSource x l j) (ActualParticularStageControls.reference l).geometry ⋯ (ActualParticularStageControls.reference l).cutoff) p

theorem NavierStokes.ActualReferenceRebase.nativePressure_subcoverPeriodic {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (l : ActualParticularStageControls.Label B N0) (j : ℤ) (p : PhysicalParticularWave.Parameter) (hf : CommonCoverSolve.PeriodicAt (ParticularWaveAssembly.residualSource (ActualParticularStageControls.assembly x l).context (ActualParticularStageControls.assembly x l).state (ActualParticularStageControls.assembly x l).carrierBlock (ActualParticularStageControls.assembly x l).gaussianInput (ActualParticularStageControls.assembly x l).aliasInput j (BaseChartJets.cellBand l.2)) p) : SubcoverPeriodicity.SubcoverPeriodicAt (ActualParticularStageControls.gap l (BaseChartJets.cellBand l.2)) (ParticularWaveBounds.commonPressure ((ActualParticularStageControls.reference l).tangent j) (referenceResidualSource x l j) (ActualParticularStageControls.reference l).geometry ⋯ (ActualParticularStageControls.reference l).cutoff (PhysicalParticularWave.referenceFrequency (nativeAssembly x l) j)) p