Complete controls for the scaled actual particular inverse

The clock, normal, integration interval and native geometry are transported together. The forcing is the current target residual, with no source naturality assumption and no supplied modal-control record.

Modal inputs for the actual residual inverse

The frame is the selected PhaseConstruction.frame. Its modal energy estimate is derived from FrameData.energy_bound, including every nonzero harmonic. The source is differentiated along the genuine shifted copy path; geometric separation identifies its grouped Gaussian at every integration time. All finite-jet constants precede the external label and lattice copy.

@[reducible, inline]

abbrev NavierStokes.ActualParticularControl.Plane : Type

Plane: an abbreviation for TorusInverse.Plane.

Equations

• NavierStokes.ActualParticularControl.Plane = NavierStokes.TorusInverse.Plane

theorem NavierStokes.ActualParticularControl.selected_frame_jets {ι : Type u_1} {D : PhaseJetBounds.Domain ι PhaseCalculus.Slow} (F : PrimaryPulseBounds.PhaseConstruction D) : PhaseJetBounds.FrameJets (D.slot F.V ⋯) F.frame

Actual frame jets, directly from the base and phase data of the selected construction. No regularity of a solved amplitude is an input.

theorem NavierStokes.ActualParticularControl.selected_energy {ι : Type u_1} {D : PhaseJetBounds.Domain ι PhaseCalculus.Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (i : ι) {p : PhaseCalculus.Slow} (hp : p ∈ D.carrier i) {v : ℝ} (hv : v ∈ Set.Icc 0 (F.L i)) {j : ℤ} (hj : j ≠ 0) (z : PrimaryODE.State) : inner ℝ z (((F.frame i).coefficient j (p, v)) z) ≤ (GaussianEnvelope.referenceRate (F.lam i) (F.u i) (F.L i) v + (F.E + 4 * F.C) / D.scale i) * ‖z‖ ^ 2

The extra j² damping is dissipative. The same Gaussian rate and error constant work for all nonzero harmonics, without a bound on j.

theorem NavierStokes.ActualParticularControl.selected_kinematics {ι : Type u_1} {D : PhaseJetBounds.Domain ι PhaseCalculus.Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (i : ι) {p : PhaseCalculus.Slow} (hp : p ∈ D.carrier i) : (F.frame i).Kinematics p (Set.Icc 0 (F.L i))

The same selected frame satisfies its actual slot kinematics.

theorem NavierStokes.ActualParticularControl.frame_coefficient_jets_bounded {ι : Type u_1} {Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] {U : PhaseJetBounds.Domain ι (Q × ℝ)} {d : ι → PrimaryODE.FrameData Q} (hd : PhaseJetBounds.FrameJets U d) (j : ι → ℤ) {J : ℝ} (hJ : 1 ≤ J) (hj : ∀ (i : ι), |↑(j i)| ≤ J) : PhaseJetBounds.PolynomialJets U fun (i : ι) => (d i).coefficient (j i)

A finite harmonic range introduces only a finite coefficient constant; the index type may already include every spatial label and band.

theorem NavierStokes.ActualParticularControl.frame_forcingLinear_jets {ι : Type u_1} {Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] {U : PhaseJetBounds.Domain ι (Q × ℝ)} {d : ι → PrimaryODE.FrameData Q} (hd : PhaseJetBounds.FrameJets U d) : PhaseJetBounds.PolynomialJets U fun (i : ι) => ParticularWaveBounds.frameForcingLinear (d i)

The source projection is built from its three actual frame columns.

noncomputable def NavierStokes.ActualParticularControl.nativeFrame {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (d : PrimaryODE.FrameData PhaseCalculus.Slow) (χ : P →L[ℝ] PhaseCalculus.Slow) : PrimaryODE.FrameData (P × ℝ)

The transverse copy coordinate is not a slow variable of the selected frame. The linear map also permits forgetting the auxiliary angle.

Equations

• NavierStokes.ActualParticularControl.nativeFrame d χ = NavierStokes.PrimaryCopyBridge.reindex d fun (q : P × ℝ) => χ q.1

noncomputable def NavierStokes.ActualParticularControl.frameArgument {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (χ : P →L[ℝ] PhaseCalculus.Slow) : (P × Plane) × ℝ →L[ℝ] PhaseCalculus.Slow × ℝ

Frame argument as an element of ((P × Plane) × ℝ) →L[ℝ] (PhaseCalculus.Slow × ℝ).

Equations

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

@[simp]

theorem NavierStokes.ActualParticularControl.frameArgument_apply {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (χ : P →L[ℝ] PhaseCalculus.Slow) (z : (P × Plane) × ℝ) : (frameArgument χ) z = (χ z.1.1, z.2)

@[simp]

theorem NavierStokes.ActualParticularControl.copyFrame_coefficient {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (d : PrimaryODE.FrameData PhaseCalculus.Slow) (χ : P →L[ℝ] PhaseCalculus.Slow) (g : CommonCoverSolve.Geometry) (k : TorusInverse.Frequency) (j : ℤ) (z : (P × Plane) × ℝ) : (PrimaryCopyBridge.copyFrame (nativeFrame d χ) g k).coefficient j z = d.coefficient j ((frameArgument χ) z)

@[simp]

theorem NavierStokes.ActualParticularControl.copyFrame_synthesis {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (d : PrimaryODE.FrameData PhaseCalculus.Slow) (χ : P →L[ℝ] PhaseCalculus.Slow) (g : CommonCoverSolve.Geometry) (k : TorusInverse.Frequency) (i : Fin 2) (z : (P × Plane) × ℝ) : PrimaryPulseBounds.synthesisColumn (PrimaryCopyBridge.copyFrame (nativeFrame d χ) g k) i z = PrimaryPulseBounds.synthesisColumn d i ((frameArgument χ) z)

@[simp]

theorem NavierStokes.ActualParticularControl.copyFrame_forcingLinear {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (d : PrimaryODE.FrameData PhaseCalculus.Slow) (χ : P →L[ℝ] PhaseCalculus.Slow) (g : CommonCoverSolve.Geometry) (k : TorusInverse.Frequency) (z : (P × Plane) × ℝ) : ParticularWaveBounds.frameForcingLinear (PrimaryCopyBridge.copyFrame (nativeFrame d χ) g k) z = ParticularWaveBounds.frameForcingLinear d ((frameArgument χ) z)

noncomputable def NavierStokes.ActualParticularControl.frameDomain {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {ι : Type u_1} (U : PhaseJetBounds.Domain ι (PhaseCalculus.Slow × ℝ)) (χ : P →L[ℝ] PhaseCalculus.Slow) : PhaseJetBounds.Domain ι ((P × Plane) × ℝ)

Frame domain, bundling scale, carrier, isOpen, one_le_scale.

Equations

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

theorem NavierStokes.ActualParticularControl.pull_frame_jets {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {ι : Type u_1} {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] {U : PhaseJetBounds.Domain ι (PhaseCalculus.Slow × ℝ)} {f : ι → PhaseCalculus.Slow × ℝ → V} (hf : PhaseJetBounds.PolynomialJets U f) (χ : P →L[ℝ] PhaseCalculus.Slow) : PhaseJetBounds.PolynomialJets (frameDomain U χ) fun (i : ι) (z : (P × Plane) × ℝ) => f i ((frameArgument χ) z)

noncomputable def NavierStokes.ActualParticularControl.groupedEnvelope {Label : Type u_1} {P : Type} (g : Label → ℕ → CommonCoverSolve.Geometry) (r L : Label → ℕ → ℝ) (W : Label → ℕ → ℝ → ℝ) : Label → ℕ → P × Plane → ℝ

The grouped Gaussian of this label, built from its actual copy geometry and its full padded integration rectangle.

Equations

• NavierStokes.ActualParticularControl.groupedEnvelope g r L W l n x = NavierStokes.WaveEnvelopeTransport.copyEnvelope (g l n) (r l n) (L l n) (W l n) x.2

theorem NavierStokes.ActualParticularControl.source_path_bounds {Label : Type u_1} {P V : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] (s : WeightedClasses.StripData P) (g : Label → ℕ → CommonCoverSolve.Geometry) (r L : Label → ℕ → ℝ) (W : Label → ℕ → ℝ → ℝ) (hW : ∀ (l : Label) (n : ℕ) (v : ℝ), 0 ≤ W l n v) (hsep : ∀ (l : Label) (n : ℕ), WaveEnvelopeTransport.Separated (g l n) (r l n) (L l n)) {A : ℝ} {a : ℕ} (hA : 1 ≤ A) (hgeometry : ∀ (l : Label) (n : ℕ), CommonCoverClass.argumentCost (g l n) ≤ A * s.slow n ^ a) {α : ℝ} {f : Label → ℕ → P × Plane → V} (hf : LabelSumBounds.UniformWaveClass (CommonCoverClass.sourceStrip s) (groupedEnvelope g r L W) α f) (N : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∃ (m : ℕ), ∀ (l : Label) (n : ℕ) (k : TorusInverse.Frequency) (x : P × Plane), x.1 ∈ s.domain → ((g l n).coordinates k x.2).1 ∈ Set.Icc (-r l n) (r l n) → ∀ v ∈ Set.Icc 0 (L l n), ∀ j ≤ N, ‖iteratedFDeriv ℝ j (fun (z : (P × Plane) × ℝ) => f l n (CommonCoverClass.sourceArgument (g l n) k z)) (x, v)‖ ≤ C * s.growth n x.1 ^ m * (s.epsilon n ^ α * √(s.zeta x.1)) * W l n v

Uniform full jets of the actual shifted source. The source class is an input on the current residual, not on the solution or projected forcing. The Gaussian at an earlier integration time is derived by separation.

theorem NavierStokes.ActualParticularControl.frame_input_jets {Label : Type u_1} {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : PhaseJetBounds.Domain (Label × ℕ) PhaseCalculus.Slow} (s : WeightedClasses.StripData P) (V : Label × ℕ → Set ℝ) (hV : ∀ (i : Label × ℕ), IsOpen (V i)) (d : Label × ℕ → PrimaryODE.FrameData PhaseCalculus.Slow) (L : Label × ℕ → ℝ) (W : Label → ℕ → ℝ → ℝ) (hd : PhaseJetBounds.FrameJets (D.slot V hV) d) (hinterval : ∀ (i : Label × ℕ), Set.Icc 0 (L i) ⊆ V i) (hW : ∀ (l : Label) (n : ℕ) (v : ℝ), 0 ≤ W l n v) (χ : P →L[ℝ] PhaseCalculus.Slow) (g : Label → ℕ → CommonCoverSolve.Geometry) (r : Label → ℕ → ℝ) (hscale : ∀ (l : Label) (n : ℕ), D.scale (l, n) = s.slow n) (hsep : ∀ (l : Label) (n : ℕ), WaveEnvelopeTransport.Separated (g l n) (r l n) (L (l, n))) {A : ℝ} {a : ℕ} (hA : 1 ≤ A) (hgeometry : ∀ (l : Label) (n : ℕ), CommonCoverClass.argumentCost (g l n) ≤ A * s.slow n ^ a) (harmonic : Label → ℤ) {J : ℝ} (hJ : 1 ≤ J) (hj : ∀ (l : Label), |↑(harmonic l)| ≤ J) {α : ℝ} {f : Label → ℕ → P × Plane → ProblemStatement.Space} (hf : LabelSumBounds.UniformWaveClass (CommonCoverClass.sourceStrip s) (groupedEnvelope g r (fun (l : Label) (n : ℕ) => L (l, n)) fun (l : Label) (n : ℕ) => W l n) α f) (N : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∃ (m : ℕ), ∀ (l : Label) (n : ℕ) (k : TorusInverse.Frequency) (x : P × Plane), x.1 ∈ s.domain → χ x.1 ∈ D.carrier (l, n) → ((g l n).coordinates k x.2).1 ∈ Set.Icc (-r l n) (r l n) → ∀ j ≤ N, ∀ v ∈ Set.Icc 0 (L (l, n)), ‖iteratedFDeriv ℝ j ((PrimaryCopyBridge.copyFrame (nativeFrame (d (l, n)) χ) (g l n) k).coefficient (harmonic l)) (x, v)‖ ≤ C * s.growth n x.1 ^ m ∧ ‖iteratedFDeriv ℝ j ((PrimaryCopyBridge.copyFrame (nativeFrame (d (l, n)) χ) (g l n) k).forcing (PrimaryCopyBridge.copySource (f l n) (g l n) k)) (x, v)‖ ≤ s.epsilon n ^ α * √(s.zeta x.1) * C * s.growth n x.1 ^ m * W l n v ∧ ∀ (i : Fin 2), ‖iteratedFDeriv ℝ j (PrimaryPulseBounds.synthesisColumn (PrimaryCopyBridge.copyFrame (nativeFrame (d (l, n)) χ) (g l n) k) i) (x, v)‖ ≤ C * s.growth n x.1 ^ m

Joint coefficient, source-projection, and synthesis bounds of the literal copy frame. The full source path is used at every derivative order. No modal energy or projected forcing bound is supplied.

theorem NavierStokes.ActualParticularControl.selected_input_jets {Label : Type u_1} {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : PhaseJetBounds.Domain (Label × ℕ) PhaseCalculus.Slow} (s : WeightedClasses.StripData P) (F : PrimaryPulseBounds.PhaseConstruction D) (χ : P →L[ℝ] PhaseCalculus.Slow) (g : Label → ℕ → CommonCoverSolve.Geometry) (r : Label → ℕ → ℝ) (hscale : ∀ (l : Label) (n : ℕ), D.scale (l, n) = s.slow n) (hsep : ∀ (l : Label) (n : ℕ), WaveEnvelopeTransport.Separated (g l n) (r l n) (F.L (l, n))) {A : ℝ} {a : ℕ} (hA : 1 ≤ A) (hgeometry : ∀ (l : Label) (n : ℕ), CommonCoverClass.argumentCost (g l n) ≤ A * s.slow n ^ a) (harmonic : Label → ℤ) {J : ℝ} (hJ : 1 ≤ J) (hj : ∀ (l : Label), |↑(harmonic l)| ≤ J) {α : ℝ} {f : Label → ℕ → P × Plane → ProblemStatement.Space} (hf : LabelSumBounds.UniformWaveClass (CommonCoverClass.sourceStrip s) (groupedEnvelope g r (fun (l : Label) (n : ℕ) => F.L (l, n)) fun (l : Label) (n : ℕ) => PrimaryPulseBounds.referenceP (F.lam (l, n)) (F.u (l, n)) (F.L (l, n))) α f) (N : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∃ (m : ℕ), ∀ (l : Label) (n : ℕ) (k : TorusInverse.Frequency) (x : P × Plane), x.1 ∈ s.domain → χ x.1 ∈ D.carrier (l, n) → ((g l n).coordinates k x.2).1 ∈ Set.Icc (-r l n) (r l n) → ∀ j ≤ N, ∀ v ∈ Set.Icc 0 (F.L (l, n)), ‖iteratedFDeriv ℝ j ((PrimaryCopyBridge.copyFrame (nativeFrame (F.frame (l, n)) χ) (g l n) k).coefficient (harmonic l)) (x, v)‖ ≤ C * s.growth n x.1 ^ m ∧ ‖iteratedFDeriv ℝ j ((PrimaryCopyBridge.copyFrame (nativeFrame (F.frame (l, n)) χ) (g l n) k).forcing (PrimaryCopyBridge.copySource (f l n) (g l n) k)) (x, v)‖ ≤ s.epsilon n ^ α * √(s.zeta x.1) * C * s.growth n x.1 ^ m * PrimaryPulseBounds.referenceP (F.lam (l, n)) (F.u (l, n)) (F.L (l, n)) v ∧ ∀ (i : Fin 2), ‖iteratedFDeriv ℝ j (PrimaryPulseBounds.synthesisColumn (PrimaryCopyBridge.copyFrame (nativeFrame (F.frame (l, n)) χ) (g l n) k) i) (x, v)‖ ≤ C * s.growth n x.1 ^ m

Instantiation of the input bound for the selected actual phase.

theorem NavierStokes.ActualParticularControl.uniform_parameter_pull {Label : Type u_1} {P E V : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {s : WeightedClasses.StripData P} {w : Label → ℕ → P → ℝ} {α : ℝ} {f : Label → ℕ → P → V} (hf : LabelSumBounds.UniformClass s w α f) (L : E →L[ℝ] P) : LabelSumBounds.UniformClass (CommonCoverClass.parameterStrip s L) (fun (l : Label) (n : ℕ) (x : E) => w l n (L x)) α fun (l : Label) (n : ℕ) (x : E) => f l n (L x)

A fixed linear pullback preserves the order of all uniform quantifiers.

theorem NavierStokes.ActualParticularControl.residualSource_uniform {Label : Type u_1} {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (s : WeightedClasses.StripData (P × Plane)) (W : Label → ℕ → P × Plane → ℝ) (α : ℝ) (c : CorrectionState.Context (P × Plane)) (u : CorrectionState.State (P × Plane)) (b : Label → CorrectionState.HarmonicBlock (P × Plane)) (G A : Label → HarmonicResidual.BlockCoefficients (P × Plane)) (j : Label → ℤ) (h : ∀ (i : Fin 3), LabelSumBounds.UniformWaveClass s W α fun (l : Label) (n : ℕ) (x : P × Plane) => ((HarmonicResidual.residualBlock c u (b l) (G l) (A l)).velocity n i).coeff (j l) x) : LabelSumBounds.UniformWaveClass s W α fun (l : Label) (n : ℕ) => ParticularWaveAssembly.residualSource c u (b l) (G l) (A l) (j l) n

The actual three residual coefficients form one uniformly bounded source vector. No property of the inverse is assumed here.

noncomputable def NavierStokes.ActualParticularControl.angleStrip {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (s : WeightedClasses.StripData P) : WeightedClasses.StripData (P × ℝ)

Angle strip, given by CommonCoverClass.parameterStrip s (ContinuousLinearMap.fst ℝ P ℝ).

Equations

• NavierStokes.ActualParticularControl.angleStrip s = NavierStokes.CommonCoverClass.parameterStrip s (ContinuousLinearMap.fst ℝ P ℝ)

noncomputable def NavierStokes.ActualParticularControl.forgetAngle {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] : (P × ℝ) × Plane →L[ℝ] P × Plane

Forget angle, given by ((ContinuousLinearMap.fst ℝ P ℝ).comp (ContinuousLinearMap.fst ℝ (P × ℝ) Plane)).prod (ContinuousLinearMap.snd ℝ (P × ℝ) Plane).

Equations

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

theorem NavierStokes.ActualParticularControl.sourceFamily_uniform {Label : Type u_1} {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (s : WeightedClasses.StripData P) (g : Label → ℕ → CommonCoverSolve.Geometry) (r L : Label → ℕ → ℝ) (W : Label → ℕ → ℝ → ℝ) (α : ℝ) (c : CorrectionState.Context (P × Plane)) (u : CorrectionState.State (P × Plane)) (b : Label → CorrectionState.HarmonicBlock (P × Plane)) (G A : Label → HarmonicResidual.BlockCoefficients (P × Plane)) (j : Label → ℤ) (h : ∀ (i : Fin 3), LabelSumBounds.UniformWaveClass (CommonCoverClass.sourceStrip s) (groupedEnvelope g r L W) α fun (l : Label) (n : ℕ) (x : P × TorusInverse.Plane) => ((HarmonicResidual.residualBlock c u (b l) (G l) (A l)).velocity n i).coeff (j l) x) : LabelSumBounds.UniformWaveClass (CommonCoverClass.sourceStrip (angleStrip s)) (groupedEnvelope g r L W) α fun (l : Label) => ParticularWaveAssembly.sourceFamily c u (b l) (G l) (A l) (j l)

The additional angular variable is genuinely absent from the current source. Its introduction preserves the same moving strip weight.

theorem NavierStokes.ActualParticularControl.finite_harmonic_uniform {Label : Type u_1} {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (s : WeightedClasses.StripData E) (w : Label → ℕ → E → ℝ) (α : ℝ) (H : Finset ℤ) (f : ℤ → Label → ℕ → E → V) (hf : ∀ j ∈ H, LabelSumBounds.UniformClass s w α (f j)) : LabelSumBounds.UniformClass s (fun (l : Label × ↥H) => w l.1) α fun (l : Label × ↥H) => f (↑l.2) l.1

A stage's finite harmonic range can be folded into the external label with one constant before both. This never infers uniformity over an unbounded harmonic family from separate class memberships.

theorem NavierStokes.ActualParticularControl.frame_smooth_mono {Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] {d : PrimaryODE.FrameData Q} {U V : Set (Q × ℝ)} (h : d.SmoothOn U) (hVU : V ⊆ U) : d.SmoothOn V

noncomputable def NavierStokes.ActualParticularControl.phaseNeighborhood {Label P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : PhaseJetBounds.Domain (Label × ℕ) PhaseCalculus.Slow} (s : WeightedClasses.StripData P) (F : PrimaryPulseBounds.PhaseConstruction D) (χ : P →L[ℝ] PhaseCalculus.Slow) (g : Label → ℕ → CommonCoverSolve.Geometry) (l : Label) (n : ℕ) (k : TorusInverse.Frequency) : Set (P × Plane)

Phase neighborhood, given by {x | x.1 ∈ s.domain ∧ χ x.1 ∈ D.carrier (l,n) ∧ ((g l n).coordinates k x.2).2 ∈ Ioo 0 (F.L (l,n))}.

Equations

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

noncomputable def NavierStokes.ActualParticularControl.phasePatch {Label P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : PhaseJetBounds.Domain (Label × ℕ) PhaseCalculus.Slow} (s : WeightedClasses.StripData P) (F : PrimaryPulseBounds.PhaseConstruction D) (χ : P →L[ℝ] PhaseCalculus.Slow) (g : Label → ℕ → CommonCoverSolve.Geometry) (r : Label → ℕ → ℝ) (l : Label) (n : ℕ) (k : TorusInverse.Frequency) : Set (P × Plane)

Phase patch, given by phaseNeighborhood s F χ g l n k ∩ {x | ((g l n).coordinates k x.2).1 ∈ Icc (-(r l n)) (r l n)}.

Equations

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

theorem NavierStokes.ActualParticularControl.phaseNeighborhood_open {Label P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : PhaseJetBounds.Domain (Label × ℕ) PhaseCalculus.Slow} (s : WeightedClasses.StripData P) (F : PrimaryPulseBounds.PhaseConstruction D) (χ : P →L[ℝ] PhaseCalculus.Slow) (g : Label → ℕ → CommonCoverSolve.Geometry) (l : Label) (n : ℕ) (k : TorusInverse.Frequency) : IsOpen (phaseNeighborhood s F χ g l n k)

theorem NavierStokes.ActualParticularControl.phasePatch_envelope {Label P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : PhaseJetBounds.Domain (Label × ℕ) PhaseCalculus.Slow} (s : WeightedClasses.StripData P) (F : PrimaryPulseBounds.PhaseConstruction D) (χ : P →L[ℝ] PhaseCalculus.Slow) (g : Label → ℕ → CommonCoverSolve.Geometry) (r : Label → ℕ → ℝ) (hsep : ∀ (l : Label) (n : ℕ), WaveEnvelopeTransport.Separated (g l n) (r l n) (F.L (l, n))) {l : Label} {n : ℕ} {k : TorusInverse.Frequency} {x : P × Plane} (hx : x ∈ phasePatch s F χ g r l n k) : groupedEnvelope g r (fun (l : Label) (n : ℕ) => F.L (l, n)) (fun (l : Label) (n : ℕ) => PrimaryPulseBounds.referenceP (F.lam (l, n)) (F.u (l, n)) (F.L (l, n))) l n x = PrimaryPulseBounds.referenceP (F.lam (l, n)) (F.u (l, n)) (F.L (l, n)) ((g l n).coordinates k x.2).2

The output majorant is this same native Gaussian on the phase patch; there is no replacement by an unweighted bound.

theorem NavierStokes.ActualParticularControl.selected_copy_smooth {Label P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : PhaseJetBounds.Domain (Label × ℕ) PhaseCalculus.Slow} (s : WeightedClasses.StripData P) (F : PrimaryPulseBounds.PhaseConstruction D) (χ : P →L[ℝ] PhaseCalculus.Slow) (g : Label → ℕ → CommonCoverSolve.Geometry) (l : Label) (n : ℕ) (k : TorusInverse.Frequency) : (PrimaryCopyBridge.copyFrame (nativeFrame (F.frame (l, n)) χ) (g l n) k).SmoothOn (phaseNeighborhood s F χ g l n k ×ˢ F.V (l, n))

noncomputable def NavierStokes.ActualParticularControl.referenceControl {Label P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : PhaseJetBounds.Domain (Label × ℕ) PhaseCalculus.Slow} (s : WeightedClasses.StripData P) (F : PrimaryPulseBounds.PhaseConstruction D) (χ : P →L[ℝ] PhaseCalculus.Slow) (g : Label → ℕ → CommonCoverSolve.Geometry) (r : Label → ℕ → ℝ) (hscale : ∀ (l : Label) (n : ℕ), D.scale (l, n) = s.slow n) (hsep : ∀ (l : Label) (n : ℕ), WaveEnvelopeTransport.Separated (g l n) (r l n) (F.L (l, n))) {A : ℝ} {a : ℕ} (hA : 1 ≤ A) (hgeometry : ∀ (l : Label) (n : ℕ), CommonCoverClass.argumentCost (g l n) ≤ A * s.slow n ^ a) (j : ℤ) (hj : j ≠ 0) {α : ℝ} (f : Label → ℕ → P × Plane → ProblemStatement.Space) (hf : LabelSumBounds.UniformWaveClass (CommonCoverClass.sourceStrip s) (groupedEnvelope g r (fun (l : Label) (n : ℕ) => F.L (l, n)) fun (l : Label) (n : ℕ) => PrimaryPulseBounds.referenceP (F.lam (l, n)) (F.u (l, n)) (F.L (l, n))) α f) : ParticularCopyBounds.UniformModalControl (CommonCoverClass.sourceStrip s) α (fun (l : Label) (n : ℕ) => nativeFrame (F.frame (l, n)) χ) (fun (l : Label) (n : ℕ) => PrimaryCopyBridge.frameTangentData (nativeFrame (F.frame (l, n)) χ) j (f l n)) j g (fun (l : Label) (n : ℕ) => F.L (l, n)) (fun (l : Label) (n : ℕ) => PrimaryPulseBounds.referenceP (F.lam (l, n)) (F.u (l, n)) (F.L (l, n))) (phasePatch s F χ g r)

The reference/native control is assembled from the selected phase and the current source class. Its energy and all input jets are conclusions. Only the geometric separation and scale comparison remain geometric inputs.

Equations

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

noncomputable def NavierStokes.ActualParticularControl.actualSourceControl {Label P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : PhaseJetBounds.Domain (Label × ℕ) PhaseCalculus.Slow} (s : WeightedClasses.StripData P) (F : PrimaryPulseBounds.PhaseConstruction D) (χ : P →L[ℝ] PhaseCalculus.Slow) (g : Label → ℕ → CommonCoverSolve.Geometry) (r : Label → ℕ → ℝ) (hscale : ∀ (l : Label) (n : ℕ), D.scale (l, n) = s.slow n) (hsep : ∀ (l : Label) (n : ℕ), WaveEnvelopeTransport.Separated (g l n) (r l n) (F.L (l, n))) {K : ℝ} {a : ℕ} (hK : 1 ≤ K) (hgeometry : ∀ (l : Label) (n : ℕ), CommonCoverClass.argumentCost (g l n) ≤ K * s.slow n ^ a) (c : CorrectionState.Context (P × Plane)) (u : CorrectionState.State (P × Plane)) (b : Label → CorrectionState.HarmonicBlock (P × Plane)) (G A : Label → HarmonicResidual.BlockCoefficients (P × Plane)) (j : ℤ) (hj : j ≠ 0) {α : ℝ} (h : ∀ (i : Fin 3), LabelSumBounds.UniformWaveClass (CommonCoverClass.sourceStrip s) (groupedEnvelope g r (fun (l : Label) (n : ℕ) => F.L (l, n)) fun (l : Label) (n : ℕ) => PrimaryPulseBounds.referenceP (F.lam (l, n)) (F.u (l, n)) (F.L (l, n))) α fun (l : Label) (n : ℕ) (x : P × TorusInverse.Plane) => ((HarmonicResidual.residualBlock c u (b l) (G l) (A l)).velocity n i).coeff j x) (part : HarmonicCalculus.ComplexVector →L[ℝ] ProblemStatement.Space) : ParticularCopyBounds.UniformModalControl (CommonCoverClass.sourceStrip (angleStrip s)) α (fun (l : Label) (n : ℕ) => nativeFrame (F.frame (l, n)) (χ ∘SL ContinuousLinearMap.fst ℝ P ℝ)) (fun (l : Label) (n : ℕ) => PrimaryCopyBridge.frameTangentData (nativeFrame (F.frame (l, n)) (χ ∘SL ContinuousLinearMap.fst ℝ P ℝ)) j fun (x : (P × ℝ) × PrimaryCopyBridge.Plane) => part (ParticularWaveAssembly.sourceFamily c u (b l) (G l) (A l) j n x)) j g (fun (l : Label) (n : ℕ) => F.L (l, n)) (fun (l : Label) (n : ℕ) => PrimaryPulseBounds.referenceP (F.lam (l, n)) (F.u (l, n)) (F.L (l, n))) (phasePatch (angleStrip s) F (χ ∘SL ContinuousLinearMap.fst ℝ P ℝ) g r)

The actual HR-source control, with an arbitrary fixed real projection. The two applications part = realPart and part = imagPart are the two literal Volterra solves in complexCopyCoefficients.

Equations

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

noncomputable def NavierStokes.ActualParticularControl.transportArgument {P Q : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup Q] [NormedSpace ℝ Q] (φ : Q →L[ℝ] P) (rate : ℝ) : Q × ℝ →L[ℝ] P × ℝ

Transport argument, given by (φ.comp (ContinuousLinearMap.fst ℝ Q ℝ)).prod (rate • ContinuousLinearMap.snd ℝ Q ℝ).

Equations

• NavierStokes.ActualParticularControl.transportArgument φ rate = (φ ∘SL ContinuousLinearMap.fst ℝ Q ℝ).prod (rate • ContinuousLinearMap.snd ℝ Q ℝ)

@[simp]

theorem NavierStokes.ActualParticularControl.transportArgument_apply {P Q : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup Q] [NormedSpace ℝ Q] (φ : Q →L[ℝ] P) (rate : ℝ) (z : Q × ℝ) : (transportArgument φ rate) z = (φ z.1, rate * z.2)

theorem NavierStokes.ActualParticularControl.norm_transportArgument_le {P Q : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup Q] [NormedSpace ℝ Q] (φ : Q →L[ℝ] P) (rate : ℝ) : ‖transportArgument φ rate‖ ≤ ‖φ‖ + |rate|

theorem NavierStokes.ActualParticularControl.polynomial_affine_family {P : Type} {ι : Type u_1} {E : Type u_2} {V : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {U : PhaseJetBounds.Domain ι P} {T : PhaseJetBounds.Domain ι E} {f : ι → P → V} (hf : PhaseJetBounds.PolynomialJets U f) (L : ι → E →L[ℝ] P) (c : ι → P) {A B : ℝ} {a b : ℕ} (hA : 1 ≤ A) (hB : 1 ≤ B) (hlin : ∀ (i : ι), ‖L i‖ ≤ A * T.scale i ^ a) (hscale : ∀ (i : ι), U.scale i ≤ B * T.scale i ^ b) (hmap : ∀ (i : ι), Set.MapsTo (fun (x : E) => (L i) x + c i) (T.carrier i) (U.carrier i)) : PhaseJetBounds.PolynomialJets T fun (i : ι) (x : E) => f i ((L i) x + c i)

Indexed affine parameter/clock changes, with a single polynomial cost before every label. Translation centers have no derivative cost.

noncomputable def NavierStokes.ActualParticularControl.transportedFrame {P Q : Type} (d : PrimaryODE.FrameData P) (φ : Q → P) (shift rate normalScale : ℝ) : PrimaryODE.FrameData Q

Transport all primitive frame fields with the same clock and normal factors as ScaledTangentTransport.transportTangent.

Equations

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

theorem NavierStokes.ActualParticularControl.transported_frame_jets {P Q : Type} {ι : Type u_1} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup Q] [NormedSpace ℝ Q] {U : PhaseJetBounds.Domain ι (P × ℝ)} {T : PhaseJetBounds.Domain ι (Q × ℝ)} {d : ι → PrimaryODE.FrameData P} (hd : PhaseJetBounds.FrameJets U d) (φ : ι → Q →L[ℝ] P) (c : ι → P) (shift rate normalScale : ι → ℝ) {A B R : ℝ} {a b : ℕ} (hA : 1 ≤ A) (hB : 1 ≤ B) (hR : 1 ≤ R) (hrate : ∀ (i : ι), |rate i| ≤ R) (hnormal : ∀ (i : ι), |normalScale i| ≤ R) (hlin : ∀ (i : ι), ‖transportArgument (φ i) (rate i)‖ ≤ A * T.scale i ^ a) (hscale : ∀ (i : ι), U.scale i ≤ B * T.scale i ^ b) (hmap : ∀ (i : ι), Set.MapsTo (fun (z : Q × ℝ) => ((φ i) z.1 + c i, shift i + rate i * z.2)) (T.carrier i) (U.carrier i)) : PhaseJetBounds.FrameJets T fun (i : ι) => transportedFrame (d i) (fun (q : Q) => (φ i) q + c i) (shift i) (rate i) (normalScale i)

Actual primitive jets after the same affine parameter and clock transport. The scalar bounds precede every index; the normal multiplier appears only in the two normal-scale fields.

theorem NavierStokes.ActualParticularControl.transported_errors {P Q : Type} (d : PrimaryODE.FrameData P) (φ : Q → P) (shift rate normalScale : ℝ) (z : Q × ℝ) : (transportedFrame d φ shift rate normalScale).error11 z = rate * d.error11 (φ z.1, shift + rate * z.2) ∧ (transportedFrame d φ shift rate normalScale).error12 z = rate * d.error12 (φ z.1, shift + rate * z.2) ∧ (transportedFrame d φ shift rate normalScale).error21 z = rate * d.error21 (φ z.1, shift + rate * z.2) ∧ (transportedFrame d φ shift rate normalScale).error22 z = rate * d.error22 (φ z.1, shift + rate * z.2)

theorem NavierStokes.ActualParticularControl.transported_coefficient {P Q : Type} (d : PrimaryODE.FrameData P) (φ : Q → P) (shift rate normalScale : ℝ) (j : ℤ) (z : Q × ℝ) : (transportedFrame d φ shift rate normalScale).coefficient j z = rate • d.coefficient j (φ z.1, shift + rate * z.2)

theorem NavierStokes.ActualParticularControl.transported_energy {Q : Type} {ι : Type u_1} {D : PhaseJetBounds.Domain ι PhaseCalculus.Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (i : ι) (φ : Q → PhaseCalculus.Slow) (shift rate normalScale : ℝ) (hrate : 0 ≤ rate) {q : Q} (hq : φ q ∈ D.carrier i) {v : ℝ} (hv : shift + rate * v ∈ Set.Icc 0 (F.L i)) {j : ℤ} (hj : j ≠ 0) (z : PrimaryODE.State) : inner ℝ z (((transportedFrame (F.frame i) φ shift rate normalScale).coefficient j (q, v)) z) ≤ (rate * GaussianEnvelope.referenceRate (F.lam i) (F.u i) (F.L i) (shift + rate * v) + rate * ((F.E + 4 * F.C) / D.scale i)) * ‖z‖ ^ 2

theorem NavierStokes.ActualParticularControl.transported_envelope_deriv (lam u L shift rate v : ℝ) : HasDerivAt (fun (t : ℝ) => PrimaryPulseBounds.referenceP lam u L (shift + rate * t)) (rate * GaussianEnvelope.referenceRate lam u L (shift + rate * v) * PrimaryPulseBounds.referenceP lam u L (shift + rate * v)) v

theorem NavierStokes.ActualParticularControl.transported_exponential (rate mu L : ℝ) (hrate : rate ≠ 0) : Real.exp (rate * mu * (L / rate)) = Real.exp (mu * L)

Clock shortening exactly compensates the rescaling of the modal error rate. No lower bound on the clock rate is lost inside the exponential.

@[simp]

theorem NavierStokes.ActualParticularControl.transported_synthesis {P Q : Type} (d : PrimaryODE.FrameData P) (φ : Q → P) (shift rate normalScale : ℝ) (i : Fin 2) (z : Q × ℝ) : PrimaryPulseBounds.synthesisColumn (transportedFrame d φ shift rate normalScale) i z = PrimaryPulseBounds.synthesisColumn d i (φ z.1, shift + rate * z.2)

theorem NavierStokes.ActualParticularControl.transported_normal {P Q : Type} (d : PrimaryODE.FrameData P) (φ : Q → P) (shift rate normalScale : ℝ) (z : Q × ℝ) : (transportedFrame d φ shift rate normalScale).normal z = normalScale • d.normal (φ z.1, shift + rate * z.2)

theorem NavierStokes.ActualParticularControl.transported_normalMotion {P Q : Type} (d : PrimaryODE.FrameData P) (φ : Q → P) (shift rate normalScale : ℝ) (z : Q × ℝ) : (transportedFrame d φ shift rate normalScale).normalMotion z = (normalScale * rate) • d.normalMotion (φ z.1, shift + rate * z.2)

theorem NavierStokes.ActualParticularControl.transported_kinematics {P Q : Type} (d : PrimaryODE.FrameData P) (φ : Q → P) (shift rate normalScale : ℝ) (hnormal : normalScale ≠ 0) (q : Q) (I J : Set ℝ) (hmap : Set.MapsTo (fun (t : ℝ) => shift + rate * t) I J) (hd : d.Kinematics (φ q) J) : (transportedFrame d φ shift rate normalScale).Kinematics q I

theorem NavierStokes.ActualParticularControl.frameTangentData_transport {P Q : Type} (d : PrimaryODE.FrameData (P × ℝ)) (φ : Q → P) (f : P × Plane → ProblemStatement.Space) (j : ℤ) (gap : ℕ) (shift rate amplitude normalScale : ℝ) : (PrimaryCopyBridge.frameTangentData (transportedFrame d (fun (q : Q × ℝ) => (φ q.1, q.2)) shift rate normalScale) j fun (z : Q × PrimaryCopyBridge.Plane) => (rate * amplitude) • f (φ z.1, (CommonCoverSolve.coverPower gap) z.2)) = ScaledTangentTransport.transportTangent (PrimaryCopyBridge.frameTangentData d j f) φ gap shift rate amplitude normalScale

The transformed frame is precisely the tangent transport already used by the physical particular inverse, including its normal derivative.

theorem NavierStokes.ActualParticularControl.separated_transport {g : CommonCoverSolve.Geometry} {r L rate : ℝ} (hsep : WaveEnvelopeTransport.Separated g r L) (hrate : 0 < rate) (gap : ℕ) : WaveEnvelopeTransport.Separated (CopySolveCompatibility.transportGeometry g gap 0 rate ⋯) r (L / rate)

The complete integration rectangle remains separated after the actual clock shortening and any covering refinement.

noncomputable def NavierStokes.ActualParticularControl.scaledSelectedFrame {Label : Type} {D : PhaseJetBounds.Domain (Label × ℕ) PhaseCalculus.Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (φ : Label × ℕ → PhaseCalculus.Slow →L[ℝ] PhaseCalculus.Slow) (rate normalScale : Label × ℕ → ℝ) (i : Label × ℕ) : PrimaryODE.FrameData PhaseCalculus.Slow

The literal selected frame after the zero-entry physical clock change.

Equations

• NavierStokes.ActualParticularControl.scaledSelectedFrame F φ rate normalScale i = NavierStokes.ActualParticularControl.transportedFrame (F.frame i) (⇑(φ i)) 0 (rate i) (normalScale i)

theorem NavierStokes.ActualParticularControl.scaled_selected_copy_energy {Label P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : PhaseJetBounds.Domain (Label × ℕ) PhaseCalculus.Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (φ : Label × ℕ → PhaseCalculus.Slow →L[ℝ] PhaseCalculus.Slow) (rate normalScale : Label × ℕ → ℝ) (χ : P →L[ℝ] PhaseCalculus.Slow) (g : Label → ℕ → CommonCoverSolve.Geometry) (l : Label) (n : ℕ) (k : TorusInverse.Frequency) (hrate : 0 < rate (l, n)) (x : P × Plane) (hx : (φ (l, n)) (χ x.1) ∈ D.carrier (l, n)) {v : ℝ} (hv : v ∈ Set.Icc 0 (F.L (l, n) / rate (l, n))) {j : ℤ} (hj : j ≠ 0) (z : PrimaryODE.State) : inner ℝ z (((PrimaryCopyBridge.copyFrame (nativeFrame (scaledSelectedFrame F φ rate normalScale (l, n)) χ) (g l n) k).coefficient j (x, v)) z) ≤ (rate (l, n) * GaussianEnvelope.referenceRate (F.lam (l, n)) (F.u (l, n)) (F.L (l, n)) (rate (l, n) * v) + rate (l, n) * ((F.E + 4 * F.C) / D.scale (l, n))) * ‖z‖ ^ 2

theorem NavierStokes.ActualParticularControl.scaled_selected_input_jets {Label P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D T : PhaseJetBounds.Domain (Label × ℕ) PhaseCalculus.Slow} (s : WeightedClasses.StripData P) (F : PrimaryPulseBounds.PhaseConstruction D) (V : Label × ℕ → Set ℝ) (hV : ∀ (i : Label × ℕ), IsOpen (V i)) (φ : Label × ℕ → PhaseCalculus.Slow →L[ℝ] PhaseCalculus.Slow) (rate normalScale : Label × ℕ → ℝ) (χ : P →L[ℝ] PhaseCalculus.Slow) {A B R : ℝ} {a b : ℕ} (hA : 1 ≤ A) (hB : 1 ≤ B) (hR : 1 ≤ R) (hrateBound : ∀ (i : Label × ℕ), |rate i| ≤ R) (hnormal : ∀ (i : Label × ℕ), |normalScale i| ≤ R) (hlin : ∀ (i : Label × ℕ), ‖transportArgument (φ i) (rate i)‖ ≤ A * T.scale i ^ a) (hscale : ∀ (i : Label × ℕ), D.scale i ≤ B * T.scale i ^ b) (hmap : ∀ (i : Label × ℕ), Set.MapsTo (fun (z : PhaseCalculus.Slow × ℝ) => ((φ i) z.1, rate i * z.2)) ((T.slot V hV).carrier i) ((D.slot F.V ⋯).carrier i)) (hinterval : ∀ (i : Label × ℕ), Set.Icc 0 (F.L i / rate i) ⊆ V i) (g : Label → ℕ → CommonCoverSolve.Geometry) (r : Label → ℕ → ℝ) (hscaleTarget : ∀ (l : Label) (n : ℕ), T.scale (l, n) = s.slow n) (hsep : ∀ (l : Label) (n : ℕ), WaveEnvelopeTransport.Separated (g l n) (r l n) (F.L (l, n) / rate (l, n))) {C : ℝ} {c : ℕ} (hC : 1 ≤ C) (hgeometry : ∀ (l : Label) (n : ℕ), CommonCoverClass.argumentCost (g l n) ≤ C * s.slow n ^ c) (harmonic : Label → ℤ) {J : ℝ} (hJ : 1 ≤ J) (hj : ∀ (l : Label), |↑(harmonic l)| ≤ J) {α : ℝ} {f : Label → ℕ → P × Plane → ProblemStatement.Space} (hf : LabelSumBounds.UniformWaveClass (CommonCoverClass.sourceStrip s) (groupedEnvelope g r (fun (l : Label) (n : ℕ) => F.L (l, n) / rate (l, n)) fun (l : Label) (n : ℕ) (v : ℝ) => PrimaryPulseBounds.referenceP (F.lam (l, n)) (F.u (l, n)) (F.L (l, n)) (rate (l, n) * v)) α f) (N : ℕ) : ∃ (C0 : ℝ), 0 ≤ C0 ∧ ∃ (m : ℕ), ∀ (l : Label) (n : ℕ) (k : TorusInverse.Frequency) (x : P × Plane), x.1 ∈ s.domain → χ x.1 ∈ T.carrier (l, n) → ((g l n).coordinates k x.2).1 ∈ Set.Icc (-r l n) (r l n) → ∀ j ≤ N, ∀ v ∈ Set.Icc 0 (F.L (l, n) / rate (l, n)), ‖iteratedFDeriv ℝ j ((PrimaryCopyBridge.copyFrame (nativeFrame (scaledSelectedFrame F φ rate normalScale (l, n)) χ) (g l n) k).coefficient (harmonic l)) (x, v)‖ ≤ C0 * s.growth n x.1 ^ m ∧ ‖iteratedFDeriv ℝ j ((PrimaryCopyBridge.copyFrame (nativeFrame (scaledSelectedFrame F φ rate normalScale (l, n)) χ) (g l n) k).forcing (PrimaryCopyBridge.copySource (f l n) (g l n) k)) (x, v)‖ ≤ s.epsilon n ^ α * √(s.zeta x.1) * C0 * s.growth n x.1 ^ m * PrimaryPulseBounds.referenceP (F.lam (l, n)) (F.u (l, n)) (F.L (l, n)) (rate (l, n) * v) ∧ ∀ (i : Fin 2), ‖iteratedFDeriv ℝ j (PrimaryPulseBounds.synthesisColumn (PrimaryCopyBridge.copyFrame (nativeFrame (scaledSelectedFrame F φ rate normalScale (l, n)) χ) (g l n) k) i) (x, v)‖ ≤ C0 * s.growth n x.1 ^ m

All input jets at every target band are derived from the selected reference phase, bounded affine clock data, and the current residual source class on that target band. Neither transported modal energies nor transported output bounds are inputs.

@[reducible, inline]

abbrev NavierStokes.ScaledActualParticularControl.Plane : Type

Plane: an abbreviation for TorusInverse.Plane.

Equations

• NavierStokes.ScaledActualParticularControl.Plane = NavierStokes.TorusInverse.Plane

@[reducible, inline]

abbrev NavierStokes.ScaledActualParticularControl.Slow : Type

Slow: an abbreviation for PhaseCalculus.Slow.

Equations

• NavierStokes.ScaledActualParticularControl.Slow = NavierStokes.PhaseCalculus.Slow

noncomputable def NavierStokes.ScaledActualParticularControl.targetDomain {Label P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : PhaseJetBounds.Domain (Label × ℕ) Slow} (s : WeightedClasses.StripData P) (φ : Label × ℕ → Slow →L[ℝ] Slow) : PhaseJetBounds.Domain (Label × ℕ) Slow

Target domain, bundling scale, carrier, isOpen, one_le_scale.

Equations

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

noncomputable def NavierStokes.ScaledActualParticularControl.interval {Label : Type} {D : PhaseJetBounds.Domain (Label × ℕ) Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (clock : ActualSignedControl.PositiveScale Label) (i : Label × ℕ) : Set ℝ

Interval, given by (fun v => clock.value i.1 i.2*v) ⁻¹' F.V i.

Equations

• NavierStokes.ScaledActualParticularControl.interval F clock i = (fun (v : ℝ) => clock.value i.1 i.2 * v) ⁻¹' F.V i

theorem NavierStokes.ScaledActualParticularControl.interval_open {Label : Type} {D : PhaseJetBounds.Domain (Label × ℕ) Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (clock : ActualSignedControl.PositiveScale Label) (i : Label × ℕ) : IsOpen (interval F clock i)

noncomputable def NavierStokes.ScaledActualParticularControl.length {Label : Type} {D : PhaseJetBounds.Domain (Label × ℕ) Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (clock : ActualSignedControl.PositiveScale Label) (l : Label) (n : ℕ) : ℝ

Length, given by F.L (l,n)/clock.value l n.

Equations

• NavierStokes.ScaledActualParticularControl.length F clock l n = F.L (l, n) / clock.value l n

theorem NavierStokes.ScaledActualParticularControl.length_pos {Label : Type} {D : PhaseJetBounds.Domain (Label × ℕ) Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (clock : ActualSignedControl.PositiveScale Label) (l : Label) (n : ℕ) : 0 < length F clock l n

theorem NavierStokes.ScaledActualParticularControl.clock_mem {Label : Type} {D : PhaseJetBounds.Domain (Label × ℕ) Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (clock : ActualSignedControl.PositiveScale Label) {l : Label} {n : ℕ} {v : ℝ} (hv : v ∈ Set.Icc 0 (length F clock l n)) : clock.value l n * v ∈ Set.Icc 0 (F.L (l, n))

theorem NavierStokes.ScaledActualParticularControl.interval_contains {Label : Type} {D : PhaseJetBounds.Domain (Label × ℕ) Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (clock : ActualSignedControl.PositiveScale Label) (i : Label × ℕ) : Set.Icc 0 (length F clock i.1 i.2) ⊆ interval F clock i

noncomputable def NavierStokes.ScaledActualParticularControl.geometry {Label : Type} (reference : Label → ℕ → CommonCoverSolve.Geometry) (gap : Label → ℕ → ℕ) (clock : ActualSignedControl.PositiveScale Label) (l : Label) (n : ℕ) : CommonCoverSolve.Geometry

Geometry, given by CopySolveCompatibility.transportGeometry (reference l n) (gap l n) 0 (clock.value l n) (clock.value_pos l n).ne'.

Equations

• NavierStokes.ScaledActualParticularControl.geometry reference gap clock l n = NavierStokes.CopySolveCompatibility.transportGeometry (reference l n) (gap l n) 0 (clock.value l n) ⋯

noncomputable def NavierStokes.ScaledActualParticularControl.envelope {Label : Type} {D : PhaseJetBounds.Domain (Label × ℕ) Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (clock : ActualSignedControl.PositiveScale Label) (l : Label) (n : ℕ) (v : ℝ) : ℝ

Envelope, given by referenceP (F.lam (l,n)) (F.u (l,n)) (F.L (l,n)) (clock.value l n*v).

Equations

• NavierStokes.ScaledActualParticularControl.envelope F clock l n v = NavierStokes.PrimaryPulseBounds.referenceP (F.lam (l, n)) (F.u (l, n)) (F.L (l, n)) (clock.value l n * v)

noncomputable def NavierStokes.ScaledActualParticularControl.frame {Label : Type} {D : PhaseJetBounds.Domain (Label × ℕ) Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (φ : Label × ℕ → Slow →L[ℝ] Slow) (clock normal : ActualSignedControl.PositiveScale Label) (i : Label × ℕ) : PrimaryODE.FrameData Slow

Frame, given by scaledSelectedFrame F φ (fun i => clock.value i.1 i.2) (fun i => normal.value i.1 i.2) i.

Equations

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

noncomputable def NavierStokes.ScaledActualParticularControl.neighborhood {Label P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : PhaseJetBounds.Domain (Label × ℕ) Slow} (s : WeightedClasses.StripData P) (F : PrimaryPulseBounds.PhaseConstruction D) (χ : P →L[ℝ] Slow) (φ : Label × ℕ → Slow →L[ℝ] Slow) (clock : ActualSignedControl.PositiveScale Label) (g : Label → ℕ → CommonCoverSolve.Geometry) (l : Label) (n : ℕ) (k : TorusInverse.Frequency) : Set (P × Plane)

Neighborhood, given by {x | x.1 ∈ s.domain ∧ φ (l,n) (χ x.1) ∈ D.carrier (l,n) ∧ ((g l n).coordinates k x.2).2 ∈ Ioo 0 (length F clock l n)}.

Equations

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

noncomputable def NavierStokes.ScaledActualParticularControl.patch {Label P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : PhaseJetBounds.Domain (Label × ℕ) Slow} (s : WeightedClasses.StripData P) (F : PrimaryPulseBounds.PhaseConstruction D) (χ : P →L[ℝ] Slow) (φ : Label × ℕ → Slow →L[ℝ] Slow) (clock : ActualSignedControl.PositiveScale Label) (g : Label → ℕ → CommonCoverSolve.Geometry) (r : Label → ℕ → ℝ) (l : Label) (n : ℕ) (k : TorusInverse.Frequency) : Set (P × Plane)

Patch, given by neighborhood s F χ φ clock g l n k ∩ {x | ((g l n).coordinates k x.2).1 ∈ Icc (-(r l n)) (r l n)}.

Equations

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

theorem NavierStokes.ScaledActualParticularControl.neighborhood_open {Label P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : PhaseJetBounds.Domain (Label × ℕ) Slow} (s : WeightedClasses.StripData P) (F : PrimaryPulseBounds.PhaseConstruction D) (χ : P →L[ℝ] Slow) (φ : Label × ℕ → Slow →L[ℝ] Slow) (clock : ActualSignedControl.PositiveScale Label) (g : Label → ℕ → CommonCoverSolve.Geometry) (l : Label) (n : ℕ) (k : TorusInverse.Frequency) : IsOpen (neighborhood s F χ φ clock g l n k)

theorem NavierStokes.ScaledActualParticularControl.frame_jets {Label P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : PhaseJetBounds.Domain (Label × ℕ) Slow} (s : WeightedClasses.StripData P) (F : PrimaryPulseBounds.PhaseConstruction D) (φ : Label × ℕ → Slow →L[ℝ] Slow) (clock normal : ActualSignedControl.PositiveScale Label) {A B : ℝ} (hA : 1 ≤ A) (hB : 1 ≤ B) (hφ : ∀ (i : Label × ℕ), ‖φ i‖ ≤ A) (hscale : ∀ (i : Label × ℕ), D.scale i ≤ B * s.slow i.2) : PhaseJetBounds.FrameJets ((targetDomain s φ).slot (interval F clock) ⋯) (frame F φ clock normal)

Every frame jet follows from the selected reference phase and the existing bounded affine/positive-scale data.

noncomputable def NavierStokes.ScaledActualParticularControl.scaledControl {Label P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : PhaseJetBounds.Domain (Label × ℕ) Slow} (s : WeightedClasses.StripData P) (F : PrimaryPulseBounds.PhaseConstruction D) (χ : P →L[ℝ] Slow) (φ : Label × ℕ → Slow →L[ℝ] Slow) (clock normal : ActualSignedControl.PositiveScale Label) (reference : Label → ℕ → CommonCoverSolve.Geometry) (gap : Label → ℕ → ℕ) (r : Label → ℕ → ℝ) {A B C : ℝ} {a : ℕ} (hA : 1 ≤ A) (hB : 1 ≤ B) (hC : 1 ≤ C) (hφ : ∀ (i : Label × ℕ), ‖φ i‖ ≤ A) (hscale : ∀ (i : Label × ℕ), D.scale i ≤ B * s.slow i.2) (hsep : ∀ (l : Label) (n : ℕ), WaveEnvelopeTransport.Separated (reference l n) (r l n) (F.L (l, n))) (hgeometry : ∀ (l : Label) (n : ℕ), CommonCoverClass.argumentCost (geometry reference gap clock l n) ≤ C * s.slow n ^ a) (j : ℤ) (hj : j ≠ 0) {α : ℝ} (f : Label → ℕ → P × Plane → ProblemStatement.Space) (hf : LabelSumBounds.UniformWaveClass (CommonCoverClass.sourceStrip s) (ActualParticularControl.groupedEnvelope (geometry reference gap clock) r (length F clock) (envelope F clock)) α f) : ParticularCopyBounds.UniformModalControl (CommonCoverClass.sourceStrip s) α (fun (l : Label) (n : ℕ) => ActualParticularControl.nativeFrame (frame F φ clock normal (l, n)) χ) (fun (l : Label) (n : ℕ) => PrimaryCopyBridge.frameTangentData (ActualParticularControl.nativeFrame (frame F φ clock normal (l, n)) χ) j (f l n)) j (geometry reference gap clock) (length F clock) (envelope F clock) (patch s F χ φ clock (geometry reference gap clock) r)

All fields of the scaled modal control are derived. The remaining quantitative inputs are affine/scale/rectangle facts about the chosen geometry and the current source coefficient class.

Equations

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

noncomputable def NavierStokes.ScaledActualParticularControl.withSource {P : Type} (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (f : P × Plane → ProblemStatement.Space) : CommonCoverSolve.TangentData P ProblemStatement.Space

Overwrite only the source, exactly as realData and imagData do.

Equations

• NavierStokes.ScaledActualParticularControl.withSource t f = { normal := t.normal, normalDot := t.normalDot, action := t.action, damping := t.damping, source := f }

theorem NavierStokes.ScaledActualParticularControl.nativeFrame_transport {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (d : PrimaryODE.FrameData Slow) (χ : P →L[ℝ] Slow) (φ : Slow →L[ℝ] Slow) (ψ : P → P) (hχ : ∀ (p : P), χ (ψ p) = φ (χ p)) (rate normal : ℝ) : ActualParticularControl.transportedFrame (ActualParticularControl.nativeFrame d χ) (fun (q : P × ℝ) => (ψ q.1, q.2)) 0 rate normal = ActualParticularControl.nativeFrame (ActualParticularControl.transportedFrame d (⇑φ) 0 rate normal) χ

Normal and clock transport commute with the selected slow-coordinate map. The transverse coordinate remains an auxiliary parameter.

theorem NavierStokes.ScaledActualParticularControl.angle_transport_withSource {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (d : PrimaryODE.FrameData Slow) (χ : P →L[ℝ] Slow) (φ : Slow →L[ℝ] Slow) (ψ : P → P) (hχ : ∀ (p : P), χ (ψ p) = φ (χ p)) (referenceSource : P × Plane → ProblemStatement.Space) (targetSource : (P × ℝ) × Plane → ProblemStatement.Space) (j : ℤ) (gap : ℕ) (rate amplitude normal : ℝ) : withSource (ParticularWaveAssembly.angleTangent (ScaledTangentTransport.transportTangent (PrimaryCopyBridge.frameTangentData (ActualParticularControl.nativeFrame d χ) j referenceSource) ψ gap 0 rate amplitude normal)) targetSource = PrimaryCopyBridge.frameTangentData (ActualParticularControl.nativeFrame (ActualParticularControl.transportedFrame d (⇑φ) 0 rate normal) (χ ∘SL ContinuousLinearMap.fst ℝ P ℝ)) j targetSource

The selected transported frame gives the exact angle-lifted STT tangent after inserting the current target source. No equality between the current source and a transported old source is used.

@[simp]

theorem NavierStokes.ScaledActualParticularControl.withSource_real {P : Type} (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (f : P × Plane → HarmonicCalculus.ComplexVector) : (withSource t fun (x : P × Plane) => ParticularWaveBounds.realPart (f x)) = ParticularWaveBounds.realData t f

@[simp]

theorem NavierStokes.ScaledActualParticularControl.withSource_imag {P : Type} (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (f : P × Plane → HarmonicCalculus.ComplexVector) : (withSource t fun (x : P × Plane) => ParticularWaveBounds.imagPart (f x)) = ParticularWaveBounds.imagData t f

noncomputable def NavierStokes.ScaledActualParticularControl.transportedTangent {Label P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : PhaseJetBounds.Domain (Label × ℕ) Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (χ : P →L[ℝ] Slow) (ψ : Label × ℕ → P → P) (clock normal : ActualSignedControl.PositiveScale Label) (referenceSource : Label → ℕ → P × Plane → ProblemStatement.Space) (gap : Label → ℕ → ℕ) (amplitude : Label → ℕ → ℝ) (j : ℤ) (l : Label) (n : ℕ) : CommonCoverSolve.TangentData (P × ℝ) ProblemStatement.Space

Transported tangent, constructed using ParticularWaveAssembly.angleTangent.

Equations

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

noncomputable def NavierStokes.ScaledActualParticularControl.actualControl {Label P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : PhaseJetBounds.Domain (Label × ℕ) Slow} (s : WeightedClasses.StripData P) (F : PrimaryPulseBounds.PhaseConstruction D) (χ : P →L[ℝ] Slow) (φ : Label × ℕ → Slow →L[ℝ] Slow) (ψ : Label × ℕ → P → P) (hχ : ∀ (i : Label × ℕ) (p : P), χ (ψ i p) = (φ i) (χ p)) (clock normal : ActualSignedControl.PositiveScale Label) (reference : Label → ℕ → CommonCoverSolve.Geometry) (referenceSource : Label → ℕ → P × Plane → ProblemStatement.Space) (gap : Label → ℕ → ℕ) (amplitude r : Label → ℕ → ℝ) {A B C : ℝ} {a : ℕ} (hA : 1 ≤ A) (hB : 1 ≤ B) (hC : 1 ≤ C) (hφ : ∀ (i : Label × ℕ), ‖φ i‖ ≤ A) (hscale : ∀ (i : Label × ℕ), D.scale i ≤ B * s.slow i.2) (hsep : ∀ (l : Label) (n : ℕ), WaveEnvelopeTransport.Separated (reference l n) (r l n) (F.L (l, n))) (hgeometry : ∀ (l : Label) (n : ℕ), CommonCoverClass.argumentCost (geometry reference gap clock l n) ≤ C * s.slow n ^ a) (c : CorrectionState.Context (P × Plane)) (u : CorrectionState.State (P × Plane)) (b : Label → CorrectionState.HarmonicBlock (P × Plane)) (G A0 : Label → HarmonicResidual.BlockCoefficients (P × Plane)) (j : ℤ) (hj : j ≠ 0) {α : ℝ} (hsource : ∀ (i : Fin 3), LabelSumBounds.UniformWaveClass (CommonCoverClass.sourceStrip s) (ActualParticularControl.groupedEnvelope (geometry reference gap clock) r (length F clock) (envelope F clock)) α fun (l : Label) (n : ℕ) (x : P × TorusInverse.Plane) => ((HarmonicResidual.residualBlock c u (b l) (G l) (A0 l)).velocity n i).coeff j x) (part : HarmonicCalculus.ComplexVector →L[ℝ] ProblemStatement.Space) : ParticularCopyBounds.UniformModalControl (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip s)) α (fun (l : Label) (n : ℕ) => ActualParticularControl.nativeFrame (frame F φ clock normal (l, n)) (χ ∘SL ContinuousLinearMap.fst ℝ P ℝ)) (fun (l : Label) (n : ℕ) => withSource (transportedTangent F χ ψ clock normal referenceSource gap amplitude j l n) fun (x : (P × ℝ) × Plane) => part (ParticularWaveAssembly.sourceFamily c u (b l) (G l) (A0 l) j n x)) j (geometry reference gap clock) (length F clock) (envelope F clock) (patch (ActualParticularControl.angleStrip s) F (χ ∘SL ContinuousLinearMap.fst ℝ P ℝ) φ clock (geometry reference gap clock) r)

The full control for the literal target HR source and the exact angle-lifted ScaledTangentTransport datum. Inserting the current source does not require it to equal a scaled old source.

Equations

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

The clock change preserves the native Gaussian and polynomial geometry cost

theorem NavierStokes.ScaledActualParticularControl.patch_envelope {Label P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : PhaseJetBounds.Domain (Label × ℕ) Slow} (s : WeightedClasses.StripData P) (F : PrimaryPulseBounds.PhaseConstruction D) (χ : P →L[ℝ] Slow) (φ : Label × ℕ → Slow →L[ℝ] Slow) (clock : ActualSignedControl.PositiveScale Label) (reference : Label → ℕ → CommonCoverSolve.Geometry) (gap : Label → ℕ → ℕ) (r : Label → ℕ → ℝ) (hsep : ∀ (l : Label) (n : ℕ), WaveEnvelopeTransport.Separated (reference l n) (r l n) (F.L (l, n))) {l : Label} {n : ℕ} {k : TorusInverse.Frequency} {x : P × Plane} (hx : x ∈ patch s F χ φ clock (geometry reference gap clock) r l n k) : ActualParticularControl.groupedEnvelope (geometry reference gap clock) r (length F clock) (envelope F clock) l n x = envelope F clock l n ((geometry reference gap clock l n).coordinates k x.2).2

theorem NavierStokes.ScaledActualParticularControl.coordinateLinear_transport (g : CommonCoverSolve.Geometry) (gap : ℕ) (rate : ℝ) (hrate : rate ≠ 0) : (CopySolveCompatibility.transportGeometry g gap 0 rate hrate).coordinateLinear = ↑(TorusAverages.transverseChart rate hrate).symm ∘SL g.coordinateLinear ∘SL ↑(CommonCoverSolve.coverPower gap)

theorem NavierStokes.ScaledActualParticularControl.pointLinear_transport (g : CommonCoverSolve.Geometry) (gap : ℕ) (rate : ℝ) (hrate : rate ≠ 0) : (CopySolveCompatibility.transportGeometry g gap 0 rate hrate).pointLinear = ↑(CommonCoverSolve.coverPower gap).symm ∘SL g.pointLinear ∘SL ↑(TorusAverages.transverseChart rate hrate)

theorem NavierStokes.ScaledActualParticularControl.norm_timeChart_le (rate : ℝ) (hrate : rate ≠ 0) : ‖↑(TorusAverages.transverseChart rate hrate)‖ ≤ 1 + |rate|

noncomputable def NavierStokes.ScaledActualParticularControl.geometryFactor {Label : Type} (clock : ActualSignedControl.PositiveScale Label) (budget : ℕ) : ℝ

Geometry factor, given by 1 + coveringBound budget * (2+clock.upper+clock.lower⁻¹).

Equations

• NavierStokes.ScaledActualParticularControl.geometryFactor clock budget = 1 + NavierStokes.CommonCoverSolve.coveringBound budget * (2 + clock.upper + clock.lower⁻¹)

theorem NavierStokes.ScaledActualParticularControl.geometryFactor_one {Label : Type} (clock : ActualSignedControl.PositiveScale Label) (budget : ℕ) : 1 ≤ geometryFactor clock budget

theorem NavierStokes.ScaledActualParticularControl.geometry_cost {Label : Type} (clock : ActualSignedControl.PositiveScale Label) (g : CommonCoverSolve.Geometry) {l : Label} {n gap budget : ℕ} (hgap : gap ≤ budget) : CommonCoverClass.argumentCost (CopySolveCompatibility.transportGeometry g gap 0 (clock.value l n) ⋯) ≤ 4 * geometryFactor clock budget ^ 2 * CommonCoverClass.argumentCost g ^ 2

Refining the cover and scaling its time column has polynomial cost. The constant uses only the already selected scale bounds and gap budget.

theorem NavierStokes.ScaledActualParticularControl.geometry_cost_uniform {Label P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (s : WeightedClasses.StripData P) (clock : ActualSignedControl.PositiveScale Label) (reference : Label → ℕ → CommonCoverSolve.Geometry) (gap : Label → ℕ → ℕ) (budget : ℕ) {C : ℝ} {a : ℕ} (hgap : ∀ (l : Label) (n : ℕ), gap l n ≤ budget) (href : ∀ (l : Label) (n : ℕ), CommonCoverClass.argumentCost (reference l n) ≤ C * s.slow n ^ a) (l : Label) (n : ℕ) : CommonCoverClass.argumentCost (geometry reference gap clock l n) ≤ 4 * geometryFactor clock budget ^ 2 * C ^ 2 * s.slow n ^ (2 * a)

theorem NavierStokes.ScaledActualParticularControl.geometry_cost_constant_one {Label : Type} (clock : ActualSignedControl.PositiveScale Label) (budget : ℕ) {C : ℝ} (hC : 1 ≤ C) : 1 ≤ 4 * geometryFactor clock budget ^ 2 * C ^ 2

The actual active-window parameter and frequency scales

noncomputable def NavierStokes.ScaledActualParticularControl.physicalPhi {Label : Type} (h : ℝ) (chart : ℕ → ℕ) (reference : Label → ℕ → ℕ) (i : Label × ℕ) : Slow →L[ℝ] Slow

Physical phi, given by ActualSignedGeometry.slowChange h (ChartScales.Q (chart i.2)) (ChartScales.Q (reference i.1 i.2)).

Equations

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

noncomputable def NavierStokes.ScaledActualParticularControl.physicalPsi {Label : Type} (h : ℝ) (chart : ℕ → ℕ) (reference : Label → ℕ → ℕ) (i : Label × ℕ) : Slow → Slow

Physical psi, given by PhysicalParticularWave.parameterChange h (ChartScales.Q (chart i.2)) (ChartScales.Q (reference i.1 i.2)).

Equations

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

theorem NavierStokes.ScaledActualParticularControl.physical_commute {Label : Type} (h : ℝ) (chart : ℕ → ℕ) (reference : Label → ℕ → ℕ) (i : Label × ℕ) (p : Slow) : ActualSignedGeometry.swapParameter (physicalPsi h chart reference i p) = (physicalPhi h chart reference i) (ActualSignedGeometry.swapParameter p)

theorem NavierStokes.ScaledActualParticularControl.physicalPhi_bound {Label : Type} (h : ℝ) (chart : ℕ → ℕ) (reference : Label → ℕ → ℕ) (hnear : ∀ (l : Label) (n : ℕ), chart n ≤ reference l n + 4 ∧ reference l n ≤ chart n + 4) (i : Label × ℕ) : ‖physicalPhi h chart reference i‖ ≤ ActualSignedGeometry.slowChangeCost h

theorem NavierStokes.ScaledActualParticularControl.active_scale_bound {Label P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (s : WeightedClasses.StripData P) (chart : ℕ → ℕ) (reference : Label → ℕ → ℕ) (hchart : ∀ (n : ℕ), 1 ≤ chart n) (hnear : ∀ (l : Label) (n : ℕ), chart n ≤ reference l n + 4 ∧ reference l n ≤ chart n + 4) (hs : ∀ (n : ℕ), ChartScales.S (chart n) ≤ s.slow n) (l : Label) (n : ℕ) : ChartScales.S (reference l n) ≤ 25 * s.slow n

theorem NavierStokes.ScaledActualParticularControl.normalWeight_harmonic (Q Qr K Kr : ℝ) (j : ℤ) (hj : j ≠ 0) : PhysicalParticularWave.normalWeight Q Qr (↑j * K) (↑j * Kr) = PhysicalParticularWave.normalWeight Q Qr K Kr

The same nonzero harmonic appears in both physical frequencies, so normal scaling is independent of its sign and size.

theorem NavierStokes.ScaledActualParticularControl.normalScale_harmonic {Label : Type} {h : ℝ} (hh : 0 ≤ h) (chart : ℕ → ℕ) (reference : Label → ℕ → ℕ) (hnear : ∀ (l : Label) (n : ℕ), chart n ≤ reference l n + 4 ∧ reference l n ≤ chart n + 4) (j : ℤ) (hj : j ≠ 0) (l : Label) (n : ℕ) : (ActualSignedGeometry.normalScale chart reference hnear hh).value l n = PhysicalParticularWave.normalWeight (ChartScales.Q (chart n)) (ChartScales.Q (reference l n)) (↑j * ↑(ChartScales.carrier h (chart n))) (↑j * ↑(ChartScales.carrier h (reference l n)))

noncomputable def NavierStokes.ScaledActualParticularControl.slotReference {Label : Type} {h dimension : ℝ} {vr vt : Plane} (sys : PartitionedCovariance.SlotSystem dimension h vr vt) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (slot : Label → ℕ → SlotColoring.Label) (l : Label) (n : ℕ) : CommonCoverSolve.Geometry

Slot reference, given by ActualSignedGeometry.slotGeometry sys hdet (slot l n) 0.

Equations

• NavierStokes.ScaledActualParticularControl.slotReference sys hdet slot l n = NavierStokes.ActualSignedGeometry.slotGeometry sys hdet (slot l n) 0

noncomputable def NavierStokes.ScaledActualParticularControl.slotCost {Label : Type} {vr vt : Plane} (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (clock : ActualSignedControl.PositiveScale Label) (budget : ℕ) : ℝ

Slot cost, given by 4*(geometryFactor clock budget)^2 * (25*CommonCoverClass.bandArgumentCost (TorusAverages.slotChart vr vt hdet) 0)^2.

Equations

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

theorem NavierStokes.ScaledActualParticularControl.slotCost_one {Label : Type} {vr vt : Plane} (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (clock : ActualSignedControl.PositiveScale Label) (budget : ℕ) : 1 ≤ slotCost hdet clock budget

theorem NavierStokes.ScaledActualParticularControl.slot_geometry_cost {Label P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {h dimension : ℝ} {vr vt : Plane} (sys : PartitionedCovariance.SlotSystem dimension h vr vt) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (slot : Label → ℕ → SlotColoring.Label) (s : WeightedClasses.StripData P) (hh : 0 ≤ h) (clock : ActualSignedControl.PositiveScale Label) (gap : Label → ℕ → ℕ) (budget : ℕ) (hgap : ∀ (l : Label) (n : ℕ), gap l n ≤ budget) (hslot : ∀ (l : Label) (n : ℕ), 4 ≤ (slot l n).1) (hscale : ∀ (l : Label) (n : ℕ), ChartScales.S (slot l n).1 ≤ 25 * s.slow n) (l : Label) (n : ℕ) : CommonCoverClass.argumentCost (geometry (slotReference sys hdet slot) gap clock l n) ≤ slotCost hdet clock budget * s.slow n ^ 2

noncomputable def NavierStokes.ScaledActualParticularControl.actualSlotControl {Label : Type} {D : PhaseJetBounds.Domain (Label × ℕ) Slow} {h dimension : ℝ} {vr vt : Plane} (sys : PartitionedCovariance.SlotSystem dimension h vr vt) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (slot : Label → ℕ → SlotColoring.Label) (s : WeightedClasses.StripData Slow) (F : PrimaryPulseBounds.PhaseConstruction D) (hh : 0 ≤ h) (chart : ℕ → ℕ) (hchart : ∀ (n : ℕ), 1 ≤ chart n) (hnear : ∀ (l : Label) (n : ℕ), chart n ≤ (slot l n).1 + 4 ∧ (slot l n).1 ≤ chart n + 4) (hslot : ∀ (l : Label) (n : ℕ), 4 ≤ (slot l n).1) (hs : ∀ (n : ℕ), ChartScales.S (chart n) ≤ s.slow n) (hscale : ∀ (i : Label × ℕ), D.scale i = ChartScales.S (slot i.1 i.2).1) (hL : ∀ (i : Label × ℕ), F.L i = ChartScales.slotLength sys.radius h (slot i.1 i.2).1) (gap : Label → ℕ → ℕ) (budget : ℕ) (hgap : ∀ (l : Label) (n : ℕ), gap l n ≤ budget) (referenceSource : Label → ℕ → Slow × Plane → ProblemStatement.Space) (c : CorrectionState.Context (Slow × Plane)) (u : CorrectionState.State (Slow × Plane)) (b : Label → CorrectionState.HarmonicBlock (Slow × Plane)) (G A0 : Label → HarmonicResidual.BlockCoefficients (Slow × Plane)) (j : ℤ) (hj : j ≠ 0) {α : ℝ} (hsource : ∀ (i : Fin 3), LabelSumBounds.UniformWaveClass (CommonCoverClass.sourceStrip s) (ActualParticularControl.groupedEnvelope (geometry (slotReference sys hdet slot) gap (ActualSignedGeometry.clockScale chart (fun (l : Label) (n : ℕ) => (slot l n).1) hnear h)) (fun (x : Label) (x_1 : ℕ) => sys.radius) (length F (ActualSignedGeometry.clockScale chart (fun (l : Label) (n : ℕ) => (slot l n).1) hnear h)) (envelope F (ActualSignedGeometry.clockScale chart (fun (l : Label) (n : ℕ) => (slot l n).1) hnear h))) α fun (l : Label) (n : ℕ) (x : Slow × TorusInverse.Plane) => ((HarmonicResidual.residualBlock c u (b l) (G l) (A0 l)).velocity n i).coeff j x) (part : HarmonicCalculus.ComplexVector →L[ℝ] ProblemStatement.Space) : ParticularCopyBounds.UniformModalControl (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip s)) α (fun (l : Label) (n : ℕ) => ActualParticularControl.nativeFrame (frame F (physicalPhi h chart fun (l : Label) (n : ℕ) => (slot l n).1) (ActualSignedGeometry.clockScale chart (fun (l : Label) (n : ℕ) => (slot l n).1) hnear h) (ActualSignedGeometry.normalScale chart (fun (l : Label) (n : ℕ) => (slot l n).1) hnear hh) (l, n)) (↑↑ActualSignedGeometry.swapParameter ∘SL ContinuousLinearMap.fst ℝ Slow ℝ)) (fun (l : Label) (n : ℕ) => withSource (transportedTangent F (↑↑ActualSignedGeometry.swapParameter) (physicalPsi h chart fun (l : Label) (n : ℕ) => (slot l n).1) (ActualSignedGeometry.clockScale chart (fun (l : Label) (n : ℕ) => (slot l n).1) hnear h) (ActualSignedGeometry.normalScale chart (fun (l : Label) (n : ℕ) => (slot l n).1) hnear hh) referenceSource gap (fun (l : Label) (n : ℕ) => PhysicalParticularWave.velocityWeight h (ChartScales.Q (chart n)) (ChartScales.Q (slot l n).1)) j l n) fun (x : (Slow × ℝ) × Plane) => part (ParticularWaveAssembly.sourceFamily c u (b l) (G l) (A0 l) j n x)) j (geometry (slotReference sys hdet slot) gap (ActualSignedGeometry.clockScale chart (fun (l : Label) (n : ℕ) => (slot l n).1) hnear h)) (length F (ActualSignedGeometry.clockScale chart (fun (l : Label) (n : ℕ) => (slot l n).1) hnear h)) (envelope F (ActualSignedGeometry.clockScale chart (fun (l : Label) (n : ℕ) => (slot l n).1) hnear h)) (patch (ActualParticularControl.angleStrip s) F (↑↑ActualSignedGeometry.swapParameter ∘SL ContinuousLinearMap.fst ℝ Slow ℝ) (physicalPhi h chart fun (l : Label) (n : ℕ) => (slot l n).1) (ActualSignedGeometry.clockScale chart (fun (l : Label) (n : ℕ) => (slot l n).1) hnear h) (geometry (slotReference sys hdet slot) gap (ActualSignedGeometry.clockScale chart (fun (l : Label) (n : ℕ) => (slot l n).1) hnear h)) fun (x : Label) (x_1 : ℕ) => sys.radius)

A full target control built from the original slot system, the selected reference phase, active-band bounds, and current HR coefficient classes. All clock, normal, affine and geometry bounds are supplied by the concrete active-window constructions; no energy or output-control premise remains.

Equations

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

theorem NavierStokes.ScaledActualParticularControl.actualSlot_tangent_eq {Label : Type} {D : PhaseJetBounds.Domain (Label × ℕ) Slow} {h : ℝ} (slot : Label → ℕ → SlotColoring.Label) (F : PrimaryPulseBounds.PhaseConstruction D) (hh : 0 ≤ h) (chart : ℕ → ℕ) (hnear : ∀ (l : Label) (n : ℕ), chart n ≤ (slot l n).1 + 4 ∧ (slot l n).1 ≤ chart n + 4) (referenceSource : Label → ℕ → Slow × Plane → ProblemStatement.Space) (gap : Label → ℕ → ℕ) (j : ℤ) (hj : j ≠ 0) (l : Label) (n : ℕ) : transportedTangent F (↑↑ActualSignedGeometry.swapParameter) (physicalPsi h chart fun (l : Label) (n : ℕ) => (slot l n).1) (ActualSignedGeometry.clockScale chart (fun (l : Label) (n : ℕ) => (slot l n).1) hnear h) (ActualSignedGeometry.normalScale chart (fun (l : Label) (n : ℕ) => (slot l n).1) hnear hh) referenceSource gap (fun (l : Label) (n : ℕ) => PhysicalParticularWave.velocityWeight h (ChartScales.Q (chart n)) (ChartScales.Q (slot l n).1)) j l n = ParticularWaveAssembly.angleTangent (ScaledTangentTransport.transportTangent (PrimaryCopyBridge.frameTangentData (ActualParticularControl.nativeFrame (F.frame (l, n)) ↑↑ActualSignedGeometry.swapParameter) j (referenceSource l n)) (PhysicalParticularWave.parameterChange h (ChartScales.Q (chart n)) (ChartScales.Q (slot l n).1)) (gap l n) 0 (PhysicalParticularWave.clockWeight h (ChartScales.Q (chart n)) (ChartScales.Q (slot l n).1)) (PhysicalParticularWave.velocityWeight h (ChartScales.Q (chart n)) (ChartScales.Q (slot l n).1)) (PhysicalParticularWave.normalWeight (ChartScales.Q (chart n)) (ChartScales.Q (slot l n).1) (↑j * ↑(ChartScales.carrier h (chart n))) (↑j * ↑(ChartScales.carrier h (slot l n).1))))