Actual particular-wave data on the active label-band pairs

The reference phase and native slot are those of the existing initializer choice. The forced fields use the literal current harmonic residual. Active pair estimates do not impose polynomial clock bounds on inactive bands. The actual source support and transported cutoff then globalize the native estimates. The final theorems give uniform bounds for the literal common and finite-harmonic fields from the current analytic invariant.

Actual particular background on the full retained carrier

The retained source mask gives the padded native scale interval (1/4,4). The cells below use its phase carrier and closed clock core without adding the narrower dyadic mask of the original primary coefficient support.

Local background bounds for the actual particular harmonics

The fixed harmonic changes the frequency. Its phase is the same primary phase, including the free angular variable. All primitive bounds are pulled from the actual primary inputs on the same closed support cells.

theorem NavierStokes.ActualParticularBackground.localClass_reindex {D E V I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (e : D ≃ₗᵢ[ℝ] E) {s : WeightedClasses.StripData E} {K : ℕ → I → Set E} {w : ℕ → I → E → ℝ} {α : ℝ} {f : ℕ → I → E → V} (hf : LocalizedWaveBounds.LocalClass s K w α f) : LocalizedWaveBounds.LocalClass (ParticularWaveBounds.reindexStrip e s) (fun (n : ℕ) (i : I) => ⇑e ⁻¹' K n i) (fun (n : ℕ) (i : I) (x : D) => w n i (e x)) α fun (n : ℕ) (i : I) (x : D) => f n i (e x)

The same jet constants work after the native coordinate isometry.

noncomputable def NavierStokes.ActualParticularBackground.reindexFamily {D E I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (a : LocalizedWaveBounds.WaveFamily E I) : LocalizedWaveBounds.WaveFamily D I

Reindex family, given by WaveFamily.ofCoefficients (fun i => ParticularWaveBounds.reindexCoefficients e (a.coefficients i)).

Equations

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

theorem NavierStokes.ActualParticularBackground.normal_reindex {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (a : LinearWaveBounds.WaveCoefficients E) (s : WeightedClasses.StripData E) (d : LinearWaveBounds.GraphDirections E) (n : ℕ) (x : D) : (ParticularWaveBounds.reindexCoefficients e a).normal (ParticularWaveBounds.reindexStrip e s) (ParticularWaveBounds.reindexDirections e d) n x = a.normal s d n (e x)

theorem NavierStokes.ActualParticularBackground.defect_reindex {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (a : LinearWaveBounds.WaveCoefficients E) (s : WeightedClasses.StripData E) (d : LinearWaveBounds.GraphDirections E) (n : ℕ) (x : D) : (ParticularWaveBounds.reindexCoefficients e a).defect (ParticularWaveBounds.reindexStrip e s) (ParticularWaveBounds.reindexDirections e d) n x = a.defect s d n (e x)

theorem NavierStokes.ActualParticularBackground.auxiliary_reindex {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) {f : E → ℝ} (d : E) {x : D} (h : (fun (y : E) => (fderiv ℝ f y) d) =ᶠ[nhds (e x)] fun (x : E) => 0) : (fun (y : D) => (fderiv ℝ (fun (z : D) => f (e z)) y) (e.symm d)) =ᶠ[nhds x] fun (x : D) => 0

theorem NavierStokes.ActualParticularBackground.inputBounds_reindex {D E I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) {s : WeightedClasses.StripData E} {K : ℕ → I → Set E} {P : ℕ → I → E → ℝ} {α κ : ℝ} {d : LinearWaveBounds.GraphDirections E} {a : LocalizedWaveBounds.WaveFamily E I} (h : LocalizedWaveBounds.InputBounds s K P α κ d a) : LocalizedWaveBounds.InputBounds (ParticularWaveBounds.reindexStrip e s) (fun (n : ℕ) (i : I) => ⇑e ⁻¹' K n i) (fun (n : ℕ) (i : I) (x : D) => P n i (e x)) α κ (ParticularWaveBounds.reindexDirections e d) (reindexFamily e a)

noncomputable def NavierStokes.ActualParticularBackground.zeroRescale {D I : Type} (q : ℝ) (a : LocalizedWaveBounds.WaveFamily D I) : LocalizedWaveBounds.WaveFamily D I

This operation changes only the harmonic frequency and sets the two unknown coefficients to zero. In particular its actual normal and defect are unchanged.

Equations

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

theorem NavierStokes.ActualParticularBackground.zeroRescale_normal {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (q : ℝ) (a : LocalizedWaveBounds.WaveFamily D I) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) : (zeroRescale q a).normal s d = a.normal s d

theorem NavierStokes.ActualParticularBackground.zeroRescale_defect {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (q : ℝ) (a : LocalizedWaveBounds.WaveFamily D I) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) : (zeroRescale q a).defect s d = a.defect s d

theorem NavierStokes.ActualParticularBackground.inputBounds_zeroRescale {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {K : ℕ → I → Set D} {P : ℕ → I → D → ℝ} {α κ : ℝ} {d : LinearWaveBounds.GraphDirections D} {a : LocalizedWaveBounds.WaveFamily D I} (h : LocalizedWaveBounds.InputBounds s K P α κ d a) (q : ℝ) (W : ℕ → I → D → ℝ) (hW : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, 0 ≤ W n i x) (β : ℝ) : LocalizedWaveBounds.InputBounds s K W β κ d (zeroRescale q a)

theorem NavierStokes.ActualParticularBackground.coefficients_ext {D : Type} {a b : LinearWaveBounds.WaveCoefficients D} (hR : a.radius = b.radius) (hr : a.radialBase = b.radialBase) (hF : a.frequencyBase = b.frequencyBase) (hG : a.axialBase = b.axialBase) (hΦ : a.phase = b.phase) (hA : a.amplitude = b.amplitude) (hp : a.pressure = b.pressure) (hk : a.frequency = b.frequency) : a = b

The same primary choice in native/free-angle coordinates

@[reducible, inline]

abbrev NavierStokes.ActualParticularBackground.Label (B N0 : ℕ) : Type

Label: an abbreviation for ActualPrimaryBounds.SignedLabel B N0.

Equations

• NavierStokes.ActualParticularBackground.Label B N0 = NavierStokes.ActualPrimaryBounds.SignedLabel B N0

@[reducible, inline]

abbrev NavierStokes.ActualParticularBackground.CopyIndex (B N0 : ℕ) : Type

Copy index: an abbreviation for ActualPrimaryBounds.CopyIndex B N0.

Equations

• NavierStokes.ActualParticularBackground.CopyIndex B N0 = NavierStokes.ActualPrimaryBounds.CopyIndex B N0

@[reducible, inline]

abbrev NavierStokes.ActualParticularBackground.Parameter : Type

Parameter: an abbreviation for CorrectionStep.CycleSlow.

Equations

• NavierStokes.ActualParticularBackground.Parameter = NavierStokes.CorrectionStep.CycleSlow

@[reducible, inline]

abbrev NavierStokes.ActualParticularBackground.Native : Type

Native: an abbreviation for (Parameter × ℝ) × TorusInverse.Plane.

Equations

• NavierStokes.ActualParticularBackground.Native = ((NavierStokes.ActualParticularBackground.Parameter × ℝ) × NavierStokes.TorusInverse.Plane)

noncomputable def NavierStokes.ActualParticularBackground.nativeToFull : Native ≃ₗᵢ[ℝ] CorrectionInitialization.ActualPrimary.FullPoint

Native to full, given by ParticularWaveAssembly.angleShuffle.symm.trans (StateReindex.cylinder cycleAssoc.symm).

Equations

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

noncomputable def NavierStokes.ActualParticularBackground.nativeStrip : WeightedClasses.StripData Native

Native strip, given by ParticularWaveBounds.reindexStrip nativeToFull ActualPrimaryBounds.fullStrip.

Equations

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

noncomputable def NavierStokes.ActualParticularBackground.cells {B N0 : ℕ} (n : ℕ) (i : CopyIndex B N0) : Set Native

Cells, given by nativeToFull ⁻¹' ActualPrimaryBounds.controlCell n i.

Equations

• NavierStokes.ActualParticularBackground.cells n i = ⇑NavierStokes.ActualParticularBackground.nativeToFull ⁻¹' NavierStokes.ActualPrimaryBounds.controlCell n i

noncomputable def NavierStokes.ActualParticularBackground.directions (B : ℕ) : LinearWaveBounds.GraphDirections Native

Directions, given by ParticularWaveBounds.reindexDirections nativeToFull (ActualPrimaryBounds.directions B).

Equations

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

noncomputable def NavierStokes.ActualParticularBackground.primaryBlock {B N0 : ℕ} (l : Label B N0) : CorrectionState.HarmonicBlock CorrectionStep.CyclePoint

Primary block as an element of HarmonicBlock CyclePoint.

Equations

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

noncomputable def NavierStokes.ActualParticularBackground.carrier {B N0 : ℕ} (b : Label B N0 → CorrectionState.HarmonicBlock CorrectionStep.CyclePoint) (j : ℤ) (l : Label B N0) : LinearWaveBounds.WaveCoefficients Native

Carrier, constructed using ParticularWaveAssembly.actualCarrier.

Equations

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

noncomputable def NavierStokes.ActualParticularBackground.backgroundFamily {B N0 : ℕ} (b : Label B N0 → CorrectionState.HarmonicBlock CorrectionStep.CyclePoint) (j : ℤ) : LocalizedWaveBounds.WaveFamily Native (CopyIndex B N0)

Background family, given by WaveFamily.ofCoefficients (fun i => ParticularWaveBounds.zeroAmplitudes (carrier b j i.1)).

Equations

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

theorem NavierStokes.ActualParticularBackground.primary_phase_affine {B N0 : ℕ} (l : Label B N0) (n : ℕ) (x : CorrectionStep.CyclePoint) (θ : ℝ) : (CorrectionInitialization.ActualPrimary.chartCoefficients l.1 l.2).phase n (x, θ) = (primaryBlock l).phase n x + ↑((primaryBlock l).angularFrequency n) / (primaryBlock l).frequency n * θ

theorem NavierStokes.ActualParticularBackground.carrier_phase {B N0 : ℕ} (b : Label B N0 → CorrectionState.HarmonicBlock CorrectionStep.CyclePoint) (hb : ∀ (l : Label B N0), CorrectionStep.SameCarrier (b l) (primaryBlock l)) (j : ℤ) (l : Label B N0) : (carrier b j l).phase = fun (n : ℕ) (z : Native) => (CorrectionInitialization.ActualPrimary.chartCoefficients l.1 l.2).phase n (nativeToFull z)

theorem NavierStokes.ActualParticularBackground.carrier_frequency {B N0 : ℕ} (b : Label B N0 → CorrectionState.HarmonicBlock CorrectionStep.CyclePoint) (hb : ∀ (l : Label B N0), CorrectionStep.SameCarrier (b l) (primaryBlock l)) (j : ℤ) (l : Label B N0) : (carrier b j l).frequency = fun (n : ℕ) => ↑j * ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n)

theorem NavierStokes.ActualParticularBackground.backgroundFamily_eq {B N0 : ℕ} (b : Label B N0 → CorrectionState.HarmonicBlock CorrectionStep.CyclePoint) (hb : ∀ (l : Label B N0), CorrectionStep.SameCarrier (b l) (primaryBlock l)) (j : ℤ) : backgroundFamily b j = reindexFamily nativeToFull (zeroRescale (↑j) ActualPrimaryBounds.actualFamily)

theorem NavierStokes.ActualParticularBackground.actual_background_inputs {B N0 : ℕ} (b : Label B N0 → CorrectionState.HarmonicBlock CorrectionStep.CyclePoint) (hb : ∀ (l : Label B N0), CorrectionStep.SameCarrier (b l) (primaryBlock l)) (j : ℤ) (W : ℕ → CopyIndex B N0 → Native → ℝ) (hW : ∀ (n : ℕ) (i : CopyIndex B N0), ∀ x ∈ nativeStrip.domain, 0 ≤ W n i x) : LocalizedWaveBounds.InputBounds nativeStrip cells W 0 ChartScales.kappa (directions B) (backgroundFamily b j)

All order-zero background classes, at every derivative order, are derived from the primary inputs. The envelope can be any nonnegative one because the velocity and pressure slots are zero. Constants remain uniform in the spatial label and lattice copy.

theorem NavierStokes.ActualParticularBackground.background_normal {B N0 : ℕ} (b : Label B N0 → CorrectionState.HarmonicBlock CorrectionStep.CyclePoint) (hb : ∀ (l : Label B N0), CorrectionStep.SameCarrier (b l) (primaryBlock l)) (j : ℤ) (n : ℕ) (i : CopyIndex B N0) (x : Native) : (backgroundFamily b j).normal nativeStrip (directions B) n i x = ActualPrimaryBounds.chartNormal i.1 n (nativeToFull x)

theorem NavierStokes.ActualParticularBackground.background_normal_range {B N0 : ℕ} (b : Label B N0 → CorrectionState.HarmonicBlock CorrectionStep.CyclePoint) (hb : ∀ (l : Label B N0), CorrectionStep.SameCarrier (b l) (primaryBlock l)) (j : ℤ) {n : ℕ} {i : CopyIndex B N0} {x : Native} (hx : x ∈ nativeStrip.domain) (hi : x ∈ cells n i) : ActualPrimaryBounds.normalFloor B N0 ≤ ‖(backgroundFamily b j).normal nativeStrip (directions B) n i x‖ ∧ ‖(backgroundFamily b j).normal nativeStrip (directions B) n i x‖ ≤ ActualPrimaryBounds.normalCeiling B N0

theorem NavierStokes.ActualParticularBackground.background_defect {B N0 : ℕ} (b : Label B N0 → CorrectionState.HarmonicBlock CorrectionStep.CyclePoint) (hb : ∀ (l : Label B N0), CorrectionStep.SameCarrier (b l) (primaryBlock l)) (j : ℤ) (n : ℕ) (i : CopyIndex B N0) (x : Native) : (backgroundFamily b j).defect nativeStrip (directions B) n i x = ActualPhaseDefect.defect i.1.1 i.1.2 n (nativeToFull x)

theorem NavierStokes.ActualParticularBackground.background_inverse_frequency {B N0 : ℕ} (b : Label B N0 → CorrectionState.HarmonicBlock CorrectionStep.CyclePoint) (hb : ∀ (l : Label B N0), CorrectionStep.SameCarrier (b l) (primaryBlock l)) (j : ℤ) : LocalizedWaveBounds.LocalUnweighted nativeStrip cells (1 / 2) fun (n : ℕ) (i : CopyIndex B N0) (x : Native) => 1 / (backgroundFamily b j).frequency n i

theorem NavierStokes.ActualParticularBackground.background_frequency_ne {B N0 : ℕ} (b : Label B N0 → CorrectionState.HarmonicBlock CorrectionStep.CyclePoint) (hb : ∀ (l : Label B N0), CorrectionStep.SameCarrier (b l) (primaryBlock l)) {j : ℤ} (hj : j ≠ 0) (n : ℕ) (i : CopyIndex B N0) : (backgroundFamily b j).frequency n i ≠ 0

noncomputable def NavierStokes.ParticularPaddedBackground.paddedCell {B N0 : ℕ} (n : ℕ) (i : ActualPrimaryBounds.CopyIndex B N0) : Set CorrectionInitialization.ActualPrimary.FullPoint

Padded cell as an element of Set ActualPrimary.FullPoint.

Equations

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

noncomputable def NavierStokes.ParticularPaddedBackground.cells {B N0 : ℕ} (n : ℕ) (i : ActualPrimaryBounds.CopyIndex B N0) : Set ActualParticularBackground.Native

Cells, given by ActualParticularBackground.nativeToFull ⁻¹' paddedCell n i.

Equations

• NavierStokes.ParticularPaddedBackground.cells n i = ⇑NavierStokes.ActualParticularBackground.nativeToFull ⁻¹' NavierStokes.ParticularPaddedBackground.paddedCell n i

theorem NavierStokes.ParticularPaddedBackground.primary_control_subset_padded {B N0 : ℕ} (n : ℕ) (i : ActualPrimaryBounds.CopyIndex B N0) : ActualPrimaryBounds.controlCell n i ⊆ paddedCell n i

theorem NavierStokes.ParticularPaddedBackground.padded_q {B N0 : ℕ} (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) {n : ℕ} {i : ActualPrimaryBounds.CopyIndex B N0} {x : CorrectionInitialization.ActualPrimary.FullPoint} (hc : x ∈ paddedCell n i) : SimilarityHomogeneity.chartQ CorrectionInitialization.ActualPrimary.h (ActualPrimaryBounds.fullCopy i.1 n i.2 x).1 ∈ Set.Ioo (1 / 4) 4

theorem NavierStokes.ParticularPaddedBackground.padded_maps {B N0 : ℕ} (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) {n : ℕ} {i : ActualPrimaryBounds.CopyIndex B N0} {x : CorrectionInitialization.ActualPrimary.FullPoint} (hx : x ∈ ActualPrimaryBounds.fullStrip.domain) (hc : x ∈ paddedCell n i) : ((ActualPrimaryBounds.fullCopy i.1 n i.2 x).1, (ActualPrimaryBounds.fullCopy i.1 n i.2 x).2.2) ∈ (ActualPhaseDefect.reducedJetDomain ActualPhaseDefect.paddedRegion).carrier i.1

theorem NavierStokes.ParticularPaddedBackground.polynomial_on_padded {B N0 : ℕ} (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ActualPrimaryBounds.SignedLabel B N0 → PhaseCalculus.Slow × ℝ → E} (hf : PhaseJetBounds.PolynomialJets (ActualPhaseDefect.reducedJetDomain ActualPhaseDefect.paddedRegion) f) : LocalizedWaveBounds.LocalUnweighted ActualPrimaryBounds.fullStrip paddedCell 0 fun (n : ℕ) (i : ActualPrimaryBounds.CopyIndex B N0) (x : CorrectionInitialization.ActualPrimary.FullPoint) => f i.1 ((ActualPrimaryBounds.fullCopy i.1 n i.2 x).1, (ActualPrimaryBounds.fullCopy i.1 n i.2 x).2.2)

The actual normal and material defect on the larger cells

theorem NavierStokes.ParticularPaddedBackground.padded_normal_germ {B N0 : ℕ} {i : ActualPrimaryBounds.CopyIndex B N0} {n : ℕ} {x : CorrectionInitialization.ActualPrimary.FullPoint} (hx : x ∈ ActualPrimaryBounds.fullStrip.domain) (hc : x ∈ paddedCell n i) : ActualPrimaryBounds.chartNormal i.1 n =ᶠ[nhds x] fun (y : CorrectionInitialization.ActualPrimary.FullPoint) => ActualPrimaryBounds.normalScale i.1 n • ActualPrimaryBounds.jointPhase.normal i.1 ((ActualPrimaryBounds.fullCopy i.1 n i.2 y).1, (ActualPrimaryBounds.fullCopy i.1 n i.2 y).2.2)

theorem NavierStokes.ParticularPaddedBackground.padded_normalScale_local {B N0 : ℕ} : LocalizedWaveBounds.LocalUnweighted ActualPrimaryBounds.fullStrip paddedCell 0 fun (n : ℕ) (i : ActualPrimaryBounds.CopyIndex B N0) (x : CorrectionInitialization.ActualPrimary.FullPoint) => ActualPrimaryBounds.normalScale i.1 n

theorem NavierStokes.ParticularPaddedBackground.padded_normal_local {B N0 : ℕ} (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) : LocalizedWaveBounds.LocalUnweighted ActualPrimaryBounds.fullStrip paddedCell 0 fun (n : ℕ) (i : ActualPrimaryBounds.CopyIndex B N0) => ActualPrimaryBounds.chartNormal i.1 n

theorem NavierStokes.ParticularPaddedBackground.padded_normal_range {B N0 : ℕ} {i : ActualPrimaryBounds.CopyIndex B N0} {n : ℕ} {x : CorrectionInitialization.ActualPrimary.FullPoint} (hx : x ∈ ActualPrimaryBounds.fullStrip.domain) (hc : x ∈ paddedCell n i) : ActualPrimaryBounds.normalFloor B N0 ≤ ‖ActualPrimaryBounds.chartNormal i.1 n x‖ ∧ ‖ActualPrimaryBounds.chartNormal i.1 n x‖ ≤ ActualPrimaryBounds.normalCeiling B N0

theorem NavierStokes.ParticularPaddedBackground.padded_defect_local {B N0 : ℕ} (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) : LocalizedWaveBounds.LocalUnweighted ActualPrimaryBounds.fullStrip paddedCell 1 fun (n : ℕ) (i : ActualPrimaryBounds.CopyIndex B N0) => ActualPhaseDefect.defect i.1.1 i.1.2 n

Zero input slots and the unchanged native carrier

theorem NavierStokes.ParticularPaddedBackground.full_background_inputs {B N0 : ℕ} (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (j : ℤ) (W : ℕ → ActualPrimaryBounds.CopyIndex B N0 → CorrectionInitialization.ActualPrimary.FullPoint → ℝ) (hW : ∀ (n : ℕ) (i : ActualPrimaryBounds.CopyIndex B N0), ∀ x ∈ ActualPrimaryBounds.fullStrip.domain, 0 ≤ W n i x) : LocalizedWaveBounds.InputBounds ActualPrimaryBounds.fullStrip paddedCell W 0 ChartScales.kappa (ActualPrimaryBounds.directions B) (ActualParticularBackground.zeroRescale (↑j) ActualPrimaryBounds.actualFamily)

theorem NavierStokes.ParticularPaddedBackground.actual_background_inputs {B N0 : ℕ} (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (b : ActualPrimaryBounds.SignedLabel B N0 → CorrectionState.HarmonicBlock CorrectionStep.CyclePoint) (hb : ∀ (l : ActualPrimaryBounds.SignedLabel B N0), CorrectionStep.SameCarrier (b l) (ActualParticularBackground.primaryBlock l)) (j : ℤ) (W : ℕ → ActualPrimaryBounds.CopyIndex B N0 → ActualParticularBackground.Native → ℝ) (hW : ∀ (n : ℕ) (i : ActualPrimaryBounds.CopyIndex B N0), ∀ x ∈ ActualParticularBackground.nativeStrip.domain, 0 ≤ W n i x) : LocalizedWaveBounds.InputBounds ActualParticularBackground.nativeStrip cells W 0 ChartScales.kappa (ActualParticularBackground.directions B) (ActualParticularBackground.backgroundFamily b j)

The literal actualCarrier, now controlled on every retained padded cell. No dyadic mask or additional support hypothesis is imposed.

theorem NavierStokes.ParticularPaddedBackground.background_normal_range {B N0 : ℕ} (b : ActualPrimaryBounds.SignedLabel B N0 → CorrectionState.HarmonicBlock CorrectionStep.CyclePoint) (hb : ∀ (l : ActualPrimaryBounds.SignedLabel B N0), CorrectionStep.SameCarrier (b l) (ActualParticularBackground.primaryBlock l)) (j : ℤ) {n : ℕ} {i : ActualPrimaryBounds.CopyIndex B N0} {x : ActualParticularBackground.Native} (hx : x ∈ ActualParticularBackground.nativeStrip.domain) (hi : x ∈ cells n i) : ActualPrimaryBounds.normalFloor B N0 ≤ ‖(ActualParticularBackground.backgroundFamily b j).normal ActualParticularBackground.nativeStrip (ActualParticularBackground.directions B) n i x‖ ∧ ‖(ActualParticularBackground.backgroundFamily b j).normal ActualParticularBackground.nativeStrip (ActualParticularBackground.directions B) n i x‖ ≤ ActualPrimaryBounds.normalCeiling B N0

theorem NavierStokes.ParticularPaddedBackground.background_inverse_frequency {B N0 : ℕ} (b : ActualPrimaryBounds.SignedLabel B N0 → CorrectionState.HarmonicBlock CorrectionStep.CyclePoint) (hb : ∀ (l : ActualPrimaryBounds.SignedLabel B N0), CorrectionStep.SameCarrier (b l) (ActualParticularBackground.primaryBlock l)) (j : ℤ) : LocalizedWaveBounds.LocalUnweighted ActualParticularBackground.nativeStrip cells (1 / 2) fun (n : ℕ) (i : ActualPrimaryBounds.CopyIndex B N0) (x : ActualParticularBackground.Native) => 1 / (ActualParticularBackground.backgroundFamily b j).frequency n i

Geometric jets for the actual scaled particular inverse

The normal, its native time derivative, and the action operator are computed from the selected transported frame. Their native-copy jets follow from the selected phase construction and the polynomial coordinate cost, without estimates on a solved velocity or pressure as hypotheses.

@[reducible, inline]

abbrev NavierStokes.ScaledParticularFrameJets.Slow : Type

Slow: an abbreviation for PhaseCalculus.Slow.

Equations

• NavierStokes.ScaledParticularFrameJets.Slow = NavierStokes.PhaseCalculus.Slow

@[reducible, inline]

abbrev NavierStokes.ScaledParticularFrameJets.Space : Type

Space: an abbreviation for ProblemStatement.Space.

Equations

• NavierStokes.ScaledParticularFrameJets.Space = NavierStokes.ProblemStatement.Space

@[reducible, inline]

abbrev NavierStokes.ScaledParticularFrameJets.Plane : Type

Plane: an abbreviation for TorusInverse.Plane.

Equations

• NavierStokes.ScaledParticularFrameJets.Plane = NavierStokes.TorusInverse.Plane

theorem NavierStokes.ScaledParticularFrameJets.frame_normal_jets {ι Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] {U : PhaseJetBounds.Domain ι (Q × ℝ)} {d : ι → PrimaryODE.FrameData Q} (h : PhaseJetBounds.FrameJets U d) : PhaseJetBounds.PolynomialJets U fun (i : ι) => (d i).normal

theorem NavierStokes.ScaledParticularFrameJets.frame_motion_jets {ι Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] {U : PhaseJetBounds.Domain ι (Q × ℝ)} {d : ι → PrimaryODE.FrameData Q} (h : PhaseJetBounds.FrameJets U d) : PhaseJetBounds.PolynomialJets U fun (i : ι) => (d i).normalMotion

theorem NavierStokes.ScaledParticularFrameJets.frame_action_jets {ι Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] {U : PhaseJetBounds.Domain ι (Q × ℝ)} {d : ι → PrimaryODE.FrameData Q} (h : PhaseJetBounds.FrameJets U d) : PhaseJetBounds.PolynomialJets U fun (i : ι) (z : Q × ℝ) => PrimaryCopyBridge.baseOperator ((d i).F z) ((d i).shear z)

theorem NavierStokes.ScaledParticularFrameJets.polynomial_native_jets {Label I X Q E : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Q] [NormedSpace ℝ Q] [NormedAddCommGroup E] [NormedSpace ℝ E] (s : WeightedClasses.StripData X) {U : PhaseJetBounds.Domain (Label × ℕ) Q} {f : Label × ℕ → Q → E} (hf : PhaseJetBounds.PolynomialJets U f) (C : Label → ℕ → I → Set X) (L : Label → ℕ → X →L[ℝ] Q) (b : Label → ℕ → I → Q) (hscale : ∀ (l : Label) (n : ℕ), U.scale (l, n) = s.slow n) {A : ℝ} {a : ℕ} (hA : 1 ≤ A) (hL : ∀ (l : Label) (n : ℕ), ‖L l n‖ ≤ A * s.slow n ^ a) (hmap : ∀ (l : Label) (n : ℕ) (k : I), ∀ x ∈ s.domain, x ∈ C l n k → (L l n) x + b l n k ∈ U.carrier (l, n)) : PeriodizedWaveBounds.UniformLocalJets s (fun (x : Label) (x_1 : ℕ) (x_2 : X) => 1) 0 C fun (l : Label) (n : ℕ) (k : I) (x : X) => f (l, n) ((L l n) x + b l n k)

The translation may depend on the lattice copy; its size never enters a derivative bound.

noncomputable def NavierStokes.ScaledParticularFrameJets.argument {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (χ : P →L[ℝ] Slow) (g : CommonCoverSolve.Geometry) (k : TorusInverse.Frequency) (x : P × Plane) : Slow × ℝ

Argument, given by (χ x.1, (g.coordinates k x.2).2).

Equations

• NavierStokes.ScaledParticularFrameJets.argument χ g k x = (χ x.1, (g.coordinates k x.2).2)

noncomputable def NavierStokes.ScaledParticularFrameJets.argumentLinear {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (χ : P →L[ℝ] Slow) (g : CommonCoverSolve.Geometry) : P × Plane →L[ℝ] Slow × ℝ

Argument linear as an element of (P × Plane) →L[ℝ] (Slow × ℝ).

Equations

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

theorem NavierStokes.ScaledParticularFrameJets.argument_affine {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (χ : P →L[ℝ] Slow) (g : CommonCoverSolve.Geometry) (k : TorusInverse.Frequency) (x : P × Plane) : argument χ g k x = (argumentLinear χ g) x + (0, (g.coordinates k 0).2)

theorem NavierStokes.ScaledParticularFrameJets.argumentLinear_norm {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (χ : P →L[ℝ] Slow) (g : CommonCoverSolve.Geometry) : ‖argumentLinear χ g‖ ≤ ‖χ‖ + CommonCoverClass.argumentCost g

theorem NavierStokes.ScaledParticularFrameJets.argument_smooth {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (χ : P →L[ℝ] Slow) (g : CommonCoverSolve.Geometry) (k : TorusInverse.Frequency) : ContDiff ℝ (↑⊤) (argument χ g k)

noncomputable def NavierStokes.ScaledParticularFrameJets.tangent {Label P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : PhaseJetBounds.Domain (Label × ℕ) Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (χ : P →L[ℝ] Slow) (φ : Label × ℕ → Slow →L[ℝ] Slow) (clock normal : ActualSignedControl.PositiveScale Label) (source : Label → ℕ → P × Plane → Space) (j : ℤ) (l : Label) (n : ℕ) : CommonCoverSolve.TangentData P Space

Tangent, given by PrimaryCopyBridge.frameTangentData (nativeFrame (ScaledActualParticularControl.frame F φ clock normal (l,n)) χ) j (source l n).

Equations

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

theorem NavierStokes.ScaledParticularFrameJets.argument_mem {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} {x : P × Plane} (hx : x ∈ ScaledActualParticularControl.patch s F χ φ clock g r l n k) : argument χ (g l n) k x ∈ ((ScaledActualParticularControl.targetDomain s φ).slot (ScaledActualParticularControl.interval F clock) ⋯).carrier (l, n)

theorem NavierStokes.ScaledParticularFrameJets.frame_field_native_jets {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 → ℕ → ℝ) {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : Label × ℕ → Slow × ℝ → E} (hf : PhaseJetBounds.PolynomialJets ((ScaledActualParticularControl.targetDomain s φ).slot (ScaledActualParticularControl.interval F clock) ⋯) f) {C : ℝ} {a : ℕ} (hC : 1 ≤ C) (hgeometry : ∀ (l : Label) (n : ℕ), CommonCoverClass.argumentCost (g l n) ≤ C * s.slow n ^ a) : PeriodizedWaveBounds.UniformLocalJets (CommonCoverClass.sourceStrip s) (fun (x : Label) (x_1 : ℕ) (x_2 : P × TorusInverse.Plane) => 1) 0 (ScaledActualParticularControl.patch s F χ φ clock g r) fun (l : Label) (n : ℕ) (k : TorusInverse.Frequency) (x : P × TorusInverse.Plane) => f (l, n) (argument χ (g l n) k x)

theorem NavierStokes.ScaledParticularFrameJets.native_normal_eq {Label P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : PhaseJetBounds.Domain (Label × ℕ) Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (χ : P →L[ℝ] Slow) (φ : Label × ℕ → Slow →L[ℝ] Slow) (clock normal : ActualSignedControl.PositiveScale Label) (g : Label → ℕ → CommonCoverSolve.Geometry) (source : Label → ℕ → P × Plane → Space) (j : ℤ) (l : Label) (n : ℕ) (k : TorusInverse.Frequency) (x : P × Plane) : (tangent F χ φ clock normal source j l n).normal (ParticularWaveBounds.nativePoint (g l n) k x) = (ScaledActualParticularControl.frame F φ clock normal (l, n)).normal (argument χ (g l n) k x)

theorem NavierStokes.ScaledParticularFrameJets.native_motion_eq {Label P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : PhaseJetBounds.Domain (Label × ℕ) Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (χ : P →L[ℝ] Slow) (φ : Label × ℕ → Slow →L[ℝ] Slow) (clock normal : ActualSignedControl.PositiveScale Label) (g : Label → ℕ → CommonCoverSolve.Geometry) (source : Label → ℕ → P × Plane → Space) (j : ℤ) (l : Label) (n : ℕ) (k : TorusInverse.Frequency) (x : P × Plane) : (tangent F χ φ clock normal source j l n).normalDot (ParticularWaveBounds.nativePoint (g l n) k x) = (ScaledActualParticularControl.frame F φ clock normal (l, n)).normalMotion (argument χ (g l n) k x)

theorem NavierStokes.ScaledParticularFrameJets.native_action_eq {Label P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : PhaseJetBounds.Domain (Label × ℕ) Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (χ : P →L[ℝ] Slow) (φ : Label × ℕ → Slow →L[ℝ] Slow) (clock normal : ActualSignedControl.PositiveScale Label) (g : Label → ℕ → CommonCoverSolve.Geometry) (source : Label → ℕ → P × Plane → Space) (j : ℤ) (l : Label) (n : ℕ) (k : TorusInverse.Frequency) (x : P × Plane) : (tangent F χ φ clock normal source j l n).action (ParticularWaveBounds.nativePoint (g l n) k x) = PrimaryCopyBridge.baseOperator ((ScaledActualParticularControl.frame F φ clock normal (l, n)).F (argument χ (g l n) k x)) ((ScaledActualParticularControl.frame F φ clock normal (l, n)).shear (argument χ (g l n) k x))

theorem NavierStokes.ScaledParticularFrameJets.native_geometry_jets {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) (g : Label → ℕ → CommonCoverSolve.Geometry) (r : Label → ℕ → ℝ) (source : Label → ℕ → P × Plane → Space) (j : ℤ) {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) (hgeometry : ∀ (l : Label) (n : ℕ), CommonCoverClass.argumentCost (g l n) ≤ C * s.slow n ^ a) : (PeriodizedWaveBounds.UniformLocalJets (CommonCoverClass.sourceStrip s) (fun (x : Label) (x_1 : ℕ) (x_2 : P × TorusInverse.Plane) => 1) 0 (ScaledActualParticularControl.patch s F χ φ clock g r) fun (l : Label) (n : ℕ) (k : TorusInverse.Frequency) (x : P × TorusInverse.Plane) => (tangent F χ φ clock normal source j l n).normal (ParticularWaveBounds.nativePoint (g l n) k x)) ∧ (PeriodizedWaveBounds.UniformLocalJets (CommonCoverClass.sourceStrip s) (fun (x : Label) (x_1 : ℕ) (x_2 : P × TorusInverse.Plane) => 1) 0 (ScaledActualParticularControl.patch s F χ φ clock g r) fun (l : Label) (n : ℕ) (k : TorusInverse.Frequency) (x : P × TorusInverse.Plane) => (tangent F χ φ clock normal source j l n).normalDot (ParticularWaveBounds.nativePoint (g l n) k x)) ∧ PeriodizedWaveBounds.UniformLocalJets (CommonCoverClass.sourceStrip s) (fun (x : Label) (x_1 : ℕ) (x_2 : P × TorusInverse.Plane) => 1) 0 (ScaledActualParticularControl.patch s F χ φ clock g r) fun (l : Label) (n : ℕ) (k : TorusInverse.Frequency) (x : P × TorusInverse.Plane) => (tangent F χ φ clock normal source j l n).action (ParticularWaveBounds.nativePoint (g l n) k x)

These are the three actual geometric inputs needed by the pressure estimate in ParticularCopyBounds.uniform_coefficients_jets.

theorem NavierStokes.ScaledParticularFrameJets.selected_frame_normal_eq {Label : Type} {D : PhaseJetBounds.Domain (Label × ℕ) Slow} (F : PrimaryPulseBounds.PhaseConstruction D) {i : Label × ℕ} {z : Slow × ℝ} (hz : z ∈ (D.slot F.V ⋯).carrier i) : (F.frame i).normal z = F.phase.normal i z

The frame reconstructed from the selected actual phase has exactly that phase's normal; the nonzero transverse normal follows from its proved reference comparison.

theorem NavierStokes.ScaledParticularFrameJets.native_normal_eq_scaled {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) (g : Label → ℕ → CommonCoverSolve.Geometry) (r : Label → ℕ → ℝ) (source : Label → ℕ → P × Plane → Space) (j : ℤ) {l : Label} {n : ℕ} {k : TorusInverse.Frequency} {x : P × Plane} (hx : x ∈ ScaledActualParticularControl.patch s F χ φ clock g r l n k) : (tangent F χ φ clock normal source j l n).normal (ParticularWaveBounds.nativePoint (g l n) k x) = normal.value l n • F.phase.normal (l, n) ((φ (l, n)) (χ x.1), clock.value l n * ((g l n).coordinates k x.2).2)

theorem NavierStokes.ScaledParticularFrameJets.normal_lower_pos {Label : Type} {D : PhaseJetBounds.Domain (Label × ℕ) Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (normal : ActualSignedControl.PositiveScale Label) : 0 < normal.lower * F.b

theorem NavierStokes.ScaledParticularFrameJets.native_normal_bounds {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) (g : Label → ℕ → CommonCoverSolve.Geometry) (r : Label → ℕ → ℝ) (source : Label → ℕ → P × Plane → Space) (j : ℤ) {l : Label} {n : ℕ} {k : TorusInverse.Frequency} {x : P × Plane} (hx : x ∈ ScaledActualParticularControl.patch s F χ φ clock g r l n k) : normal.lower * F.b ≤ ‖(tangent F χ φ clock normal source j l n).normal (ParticularWaveBounds.nativePoint (g l n) k x)‖ ∧ ‖(tangent F χ φ clock normal source j l n).normal (ParticularWaveBounds.nativePoint (g l n) k x)‖ ≤ normal.upper * (F.M ^ 2 + 3 * F.M)

Both range constants precede every label, band, native copy and evaluation point. There is no inverse dependence on the clock rate.

The actual broad carrier in the canonical particular coordinates

Only the selected geometry and its closed source support occur here. No property of a solved particular or signed field is assumed.

@[reducible, inline]

abbrev NavierStokes.ActualCarrierTransportBase.Point : Type

Point: an abbreviation for LocalSignedRequest.Point.

Equations

• NavierStokes.ActualCarrierTransportBase.Point = NavierStokes.LocalSignedRequest.Point

@[reducible, inline]

abbrev NavierStokes.ActualCarrierTransportBase.Parameter : Type

Parameter: an abbreviation for CorrectionStep.CycleSlow.

Equations

• NavierStokes.ActualCarrierTransportBase.Parameter = NavierStokes.CorrectionStep.CycleSlow

@[reducible, inline]

abbrev NavierStokes.ActualCarrierTransportBase.Plane : Type

Plane: an abbreviation for TorusInverse.Plane.

Equations

• NavierStokes.ActualCarrierTransportBase.Plane = NavierStokes.TorusInverse.Plane

@[reducible, inline]

abbrev NavierStokes.ActualCarrierTransportBase.Index (B N0 : ℕ) : Type

Index: an abbreviation for ActualPrimary.Label B N0 × Fin 2.

Equations

• NavierStokes.ActualCarrierTransportBase.Index B N0 = (NavierStokes.CorrectionInitialization.ActualPrimary.Label B N0 × Fin 2)

noncomputable def NavierStokes.ActualCarrierTransportBase.domain : Set Point

Domain, given by PhysicalMeanDomain.slowDomain standardRegion.carrier.

Equations

• NavierStokes.ActualCarrierTransportBase.domain = NavierStokes.PhysicalMeanDomain.slowDomain NavierStokes.CorrectionInitialization.ActualPrimary.standardRegion.carrier

noncomputable def NavierStokes.ActualCarrierTransportBase.labelCarrier {B N0 : ℕ} (l : Index B N0) (n : ℕ) : Set Point

Label carrier, given by ActualInitialExcluded.labelCarrier (l.2,l.1) n.

Equations

• NavierStokes.ActualCarrierTransportBase.labelCarrier l n = NavierStokes.ActualInitialExcluded.labelCarrier (l.2, l.1) n

noncomputable def NavierStokes.ActualCarrierTransportBase.associatedPoint (p : Parameter) (Y : Plane) : Point

Associated point, given by CorrectionStep.cycleAssoc.symm (p, Y).

Equations

• NavierStokes.ActualCarrierTransportBase.associatedPoint p Y = NavierStokes.CorrectionStep.cycleAssoc.symm (p, Y)

noncomputable def NavierStokes.ActualCarrierTransportBase.parameterDomain : Set Parameter

Parameter domain, given by {p | p.2 ∈ standardRegion.carrier}.

Equations

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

theorem NavierStokes.ActualCarrierTransportBase.associatedPoint_mem_domain (p : Parameter) (Y : Plane) : associatedPoint p Y ∈ domain ↔ p ∈ parameterDomain

noncomputable def NavierStokes.ActualCarrierTransportBase.Ordered {B N0 : ℕ} (l : Index B N0) (n : ℕ) : Prop

Ordered, given by CommonWindow.index h n ≤ ChartScales.nativeIndex h (BaseChartJets.cellBand l.1).

Equations

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

noncomputable def NavierStokes.ActualCarrierTransportBase.slowMap {B N0 : ℕ} (l : Index B N0) (n : ℕ) (p : Parameter) : PhaseCalculus.Slow

Slow map, given by nativeSlow l.1 (toAbsolute n (associatedPoint p 0)).

Equations

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

theorem NavierStokes.ActualCarrierTransportBase.slowMap_eq {B N0 : ℕ} (l : Index B N0) (n : ℕ) (p : Parameter) (Y : Plane) : slowMap l n p = CorrectionInitialization.ActualPrimary.nativeSlow l.1 (CorrectionInitialization.ActualPrimary.toAbsolute n (associatedPoint p Y))

theorem NavierStokes.ActualCarrierTransportBase.slowMap_continuous {B N0 : ℕ} (l : Index B N0) (n : ℕ) : Continuous (slowMap l n)

noncomputable def NavierStokes.ActualCarrierTransportBase.slowCore {B N0 : ℕ} (l : Index B N0) (n : ℕ) : Set Parameter

Slow core, given by slowMap l n ⁻¹' ActualGaussianCoverage.actualSlowCore certificate modulation (choice B N0).prepared l.1.

Equations

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

theorem NavierStokes.ActualCarrierTransportBase.slowCore_closed {B N0 : ℕ} (l : Index B N0) (n : ℕ) : IsClosed (slowCore l n)

noncomputable def NavierStokes.ActualCarrierTransportBase.referenceLength {B N0 : ℕ} (l : Index B N0) : ℝ

Reference length, given by (phases B N0 l.2).L l.1.

Equations

• NavierStokes.ActualCarrierTransportBase.referenceLength l = (NavierStokes.CorrectionInitialization.ActualPrimary.phases B N0 l.2).L l.1

theorem NavierStokes.ActualCarrierTransportBase.referenceLength_pos {B N0 : ℕ} (l : Index B N0) : 0 < referenceLength l

noncomputable def NavierStokes.ActualCarrierTransportBase.clock {B N0 : ℕ} (l : Index B N0) (n : ℕ) : ℝ

Clock, given by PhysicalParticularWave.clockWeight h (ChartScales.Q n) (ChartScales.Q (BaseChartJets.cellBand l.1)).

Equations

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

theorem NavierStokes.ActualCarrierTransportBase.clock_pos {B N0 : ℕ} (l : Index B N0) (n : ℕ) : 0 < clock l n

noncomputable def NavierStokes.ActualCarrierTransportBase.spatialLabel {B N0 : ℕ} (l : Index B N0) : SlotColoring.Label

Spatial label, given by PartitionedCovariance.signedLabel (PrimaryGeometryAssembly.label nominal l.1) l.2.

Equations

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

noncomputable def NavierStokes.ActualCarrierTransportBase.referenceGeometry {B N0 : ℕ} (l : Index B N0) : CommonCoverSolve.Geometry

Reference geometry, given by ActualSignedGeometry.slotGeometry slots vectors_det (spatialLabel l) 0.

Equations

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

noncomputable def NavierStokes.ActualCarrierTransportBase.gap {B N0 : ℕ} (l : Index B N0) (n : ℕ) : ℕ

Gap, given by ChartScales.nativeIndex h (BaseChartJets.cellBand l.1) - CommonWindow.index h n.

Equations

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

noncomputable def NavierStokes.ActualCarrierTransportBase.geometry {B N0 : ℕ} (l : Index B N0) (n : ℕ) : CommonCoverSolve.Geometry

Geometry, given by CopySolveCompatibility.transportGeometry (referenceGeometry l) (gap l n) 0 (clock l n) (clock_pos l n).ne'.

Equations

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

theorem NavierStokes.ActualCarrierTransportBase.reference_refine {B N0 : ℕ} (l : Index B N0) (n : ℕ) : CopySolveCompatibility.refineGeometry (referenceGeometry l) (gap l n) = CorrectionInitialization.ActualPrimary.chartGeometry n l.2 l.1

noncomputable def NavierStokes.ActualCarrierTransportBase.sourceRegion {B N0 : ℕ} (l : Index B N0) (n : ℕ) : Set (Parameter × Plane)

Source region, given by ActualGaussianCoverage.sourceRegion (slowCore l n) (geometry l n) slots.radius (referenceLength l) (clock l n).

Equations

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

theorem NavierStokes.ActualCarrierTransportBase.sourceRegion_closed {B N0 : ℕ} (l : Index B N0) (n : ℕ) : IsClosed (sourceRegion l n)

theorem NavierStokes.ActualCarrierTransportBase.domain_log_band (n : ℕ) {x : Point} (hx : x ∈ domain) : SquaredPartition.logCoordinate (CorrectionInitialization.ActualPrimary.physicalScale n x) ∈ Set.Icc (↑n - 1) (↑n + 1)

The common-band logarithmic range holds on the full slow domain, without any restriction on the radial variable.

theorem NavierStokes.ActualCarrierTransportBase.carrier_band_distance {B N0 : ℕ} (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (l : Index B N0) (n : ℕ) {x : Point} (hx : x ∈ domain) (hc : x ∈ labelCarrier l n) : n ≤ BaseChartJets.cellBand l.1 + 2 ∧ BaseChartJets.cellBand l.1 ≤ n + 2

Broad carrier support forces the same finite band distance on the entire slow domain, including radii outside the analytic strip.

theorem NavierStokes.ActualCarrierTransportBase.ordered_of_carrier {B N0 : ℕ} (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (l : Index B N0) (n : ℕ) {x : Point} (hx : x ∈ domain) (hc : x ∈ labelCarrier l n) : Ordered l n

theorem NavierStokes.ActualCarrierTransportBase.carrier_empty_of_not_ordered {B N0 : ℕ} (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (l : Index B N0) (n : ℕ) (hn : ¬Ordered l n) : Disjoint domain (labelCarrier l n)

The canonical geometry rescales time after the same native refinement.

theorem NavierStokes.ActualCarrierTransportBase.coordinates_clock {B N0 : ℕ} (l : Index B N0) (n : ℕ) (k : TorusInverse.Frequency) (Y : Plane) : CopySolveCompatibility.nativeTimeMap 0 (clock l n) ((geometry l n).coordinates k Y) = (CorrectionInitialization.ActualPrimary.chartGeometry n l.2 l.1).coordinates k Y

theorem NavierStokes.ActualCarrierTransportBase.native_coordinates {B N0 : ℕ} (l : Index B N0) (n : ℕ) (hn : Ordered l n) (p : Parameter) (Y : Plane) (k : TorusInverse.Frequency) : (CorrectionInitialization.ActualPrimary.geometry l.2 l.1).coordinates k (CorrectionInitialization.ActualPrimary.toAbsolute n (associatedPoint p Y)).2 = CopySolveCompatibility.nativeTimeMap 0 (clock l n) ((geometry l n).coordinates k Y)

theorem NavierStokes.ActualCarrierTransportBase.mem_sourceRegion {B N0 : ℕ} (l : Index B N0) (n : ℕ) (p : Parameter) (Y : Plane) : (p, Y) ∈ sourceRegion l n ↔ p ∈ slowCore l n ∧ ∃ (k : TorusInverse.Frequency), (geometry l n).coordinates k Y ∈ ActualGaussianCoverage.sourceCell CorrectionInitialization.ActualPrimary.slots.radius (referenceLength l) (clock l n)

theorem NavierStokes.ActualCarrierTransportBase.labelCarrier_iff_sourceRegion {B N0 : ℕ} (l : Index B N0) (n : ℕ) (hn : Ordered l n) (p : Parameter) (Y : Plane) : associatedPoint p Y ∈ labelCarrier l n ↔ (p, Y) ∈ sourceRegion l n

Under the actual index ordering, the broad primary carrier is exactly the source region of the canonical particular geometry.

noncomputable def NavierStokes.ActualCarrierTransportBase.activeSlowCore {B N0 : ℕ} (l : Index B N0) (n : ℕ) : Set Parameter

The unordered branch is empty. This makes the same source-region description valid on the full slow domain for every band.

Equations

• NavierStokes.ActualCarrierTransportBase.activeSlowCore l n = if NavierStokes.ActualCarrierTransportBase.Ordered l n then NavierStokes.ActualCarrierTransportBase.slowCore l n else ∅

theorem NavierStokes.ActualCarrierTransportBase.activeSlowCore_closed {B N0 : ℕ} (l : Index B N0) (n : ℕ) : IsClosed (activeSlowCore l n)

noncomputable def NavierStokes.ActualCarrierTransportBase.canonicalSourceRegion {B N0 : ℕ} (l : Index B N0) (n : ℕ) : Set (Parameter × Plane)

Canonical source region, given by ActualGaussianCoverage.sourceRegion (activeSlowCore l n) (geometry l n) slots.radius (referenceLength l) (clock l n).

Equations

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

theorem NavierStokes.ActualCarrierTransportBase.canonicalSourceRegion_closed {B N0 : ℕ} (l : Index B N0) (n : ℕ) : IsClosed (canonicalSourceRegion l n)

theorem NavierStokes.ActualCarrierTransportBase.labelCarrier_iff_canonicalSourceRegion {B N0 : ℕ} (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (l : Index B N0) (n : ℕ) {p : Parameter} (hp : p ∈ parameterDomain) (Y : Plane) : associatedPoint p Y ∈ labelCarrier l n ↔ (p, Y) ∈ canonicalSourceRegion l n

noncomputable def NavierStokes.ActualCarrierTransportBase.cutoff {B N0 : ℕ} (l : Index B N0) (n : ℕ) : Plane → ℝ

Cutoff as an element of Plane → ℝ.

Equations

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

theorem NavierStokes.ActualCarrierTransportBase.cutoff_eq_native {B N0 : ℕ} (l : Index B N0) (n : ℕ) : cutoff l n = ActualGaussianCoverage.nativeCutoff CorrectionInitialization.ActualPrimary.slots.radius (referenceLength l) ⋯ ⋯ (clock l n)

theorem NavierStokes.ActualCarrierTransportBase.reference_outer_injective {B N0 : ℕ} (l : Index B N0) : Set.InjOn TorusAverages.quotientPoint ((fun (z : TorusInverse.Plane) => (referenceGeometry l).center + (referenceGeometry l).basis z) '' (ActualGaussianCoverage.referenceWindow CorrectionInitialization.ActualPrimary.slots.radius (referenceLength l) ⋯ ⋯).outer)

theorem NavierStokes.ActualCarrierTransportBase.geometry_outer_injective {B N0 : ℕ} (l : Index B N0) (n : ℕ) : Set.InjOn TorusAverages.quotientPoint ((fun (z : TorusInverse.Plane) => (geometry l n).center + (geometry l n).basis z) '' ActualGaussianCoverage.outerCell CorrectionInitialization.ActualPrimary.slots.radius (referenceLength l) (clock l n))

Scalar-clock support of the actual particular solve

This support argument uses the literal complex Volterra solve and the Gaussian-times-padding cutoff. Clock factors only need to be positive at each band; no uniform range for the complete clock family is assumed.

noncomputable def NavierStokes.ScalarParticularSupport.scalarData {P : Type} (base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)) (t : ℕ → CommonCoverSolve.TangentData (P × ℝ) ProblemStatement.Space) (f : ℕ → (P × ℝ) × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (g : ℕ → CommonCoverSolve.Geometry) (r L rate : ℕ → ℝ) (hr : ∀ (n : ℕ), 0 < r n) (hL : ∀ (n : ℕ), 0 < L n) (hc : ∀ (n : ℕ), 0 < rate n) : PeriodizedWaveBounds.CopyData ((P × ℝ) × TorusInverse.Plane) TorusInverse.Frequency

The literal complex Volterra solve and its separately transported Gaussian/outer cutoff, without uniform bounds on the clock scalars.

Equations

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

theorem NavierStokes.ScalarParticularSupport.scalarData_amplitude {P : Type} (base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)) (t : ℕ → CommonCoverSolve.TangentData (P × ℝ) ProblemStatement.Space) (f : ℕ → (P × ℝ) × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (g : ℕ → CommonCoverSolve.Geometry) (r L rate : ℕ → ℝ) (hr : ∀ (n : ℕ), 0 < r n) (hL : ∀ (n : ℕ), 0 < L n) (hc : ∀ (n : ℕ), 0 < rate n) (n : ℕ) (k : TorusInverse.Frequency) : (scalarData base t f g r L rate hr hL hc).amplitude n k = ParticularWaveBounds.complexCopyVelocity (t n) (f n) (g n) ⋯ k

theorem NavierStokes.ScalarParticularSupport.scalarData_pressure {P : Type} (base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)) (t : ℕ → CommonCoverSolve.TangentData (P × ℝ) ProblemStatement.Space) (f : ℕ → (P × ℝ) × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (g : ℕ → CommonCoverSolve.Geometry) (r L rate : ℕ → ℝ) (hr : ∀ (n : ℕ), 0 < r n) (hL : ∀ (n : ℕ), 0 < L n) (hc : ∀ (n : ℕ), 0 < rate n) (n : ℕ) (k : TorusInverse.Frequency) : (scalarData base t f g r L rate hr hL hc).pressure n k = ParticularWaveBounds.complexCopyPressure (t n) (f n) (g n) ⋯ k (base.frequency n)

noncomputable def NavierStokes.ScalarParticularSupport.scalarCells {P : Type} [NormedAddCommGroup P] (g : ℕ → CommonCoverSolve.Geometry) (r L rate : ℕ → ℝ) (hinj : ∀ (n : ℕ), Set.InjOn TorusAverages.quotientPoint ((fun (z : TorusInverse.Plane) => (g n).center + (g n).basis z) '' ActualGaussianCoverage.outerCell (r n) (L n) (rate n))) : PeriodizedWaveBounds.Cells ((P × ℝ) × TorusInverse.Plane) TorusInverse.Frequency

Scalar cells, constructed using nativeCells.

Equations

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

theorem NavierStokes.ScalarParticularSupport.scalarData_cutoff_support {P : Type} [NormedAddCommGroup P] (base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)) (t : ℕ → CommonCoverSolve.TangentData (P × ℝ) ProblemStatement.Space) (f : ℕ → (P × ℝ) × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (g : ℕ → CommonCoverSolve.Geometry) (r L rate : ℕ → ℝ) (hr : ∀ (n : ℕ), 0 < r n) (hL : ∀ (n : ℕ), 0 < L n) (hc : ∀ (n : ℕ), 0 < rate n) (hinj : ∀ (n : ℕ), Set.InjOn TorusAverages.quotientPoint ((fun (z : TorusInverse.Plane) => (g n).center + (g n).basis z) '' ActualGaussianCoverage.outerCell (r n) (L n) (rate n))) (n : ℕ) (k : TorusInverse.Frequency) : Function.support ((scalarData base t f g r L rate hr hL hc).cutoff n k) ⊆ (scalarCells g r L rate hinj).carrier n k

theorem NavierStokes.ScalarParticularSupport.scalarData_native_zero_alternative {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)) (t : ℕ → CommonCoverSolve.TangentData (P × ℝ) ProblemStatement.Space) (f : ℕ → (P × ℝ) × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (g : ℕ → CommonCoverSolve.Geometry) (r L rate : ℕ → ℝ) (hr : ∀ (n : ℕ), 0 < r n) (hL : ∀ (n : ℕ), 0 < L n) (hc : ∀ (n : ℕ), 0 < rate n) (hinj : ∀ (n : ℕ), Set.InjOn TorusAverages.quotientPoint ((fun (z : TorusInverse.Plane) => (g n).center + (g n).basis z) '' ActualGaussianCoverage.outerCell (r n) (L n) (rate n))) (U : Set P) (S : ℕ → Set P) (hf : ∀ (n : ℕ) (x : (P × ℝ) × TorusInverse.Plane), x.1.1 ∈ U → (x.1.1, x.2) ∉ ActualGaussianCoverage.sourceRegion (S n) (g n) (r n) (L n) (rate n) → f n =ᶠ[nhds x] fun (x : (P × ℝ) × TorusInverse.Plane) => 0) (n : ℕ) (k : TorusInverse.Frequency) {x : (P × ℝ) × TorusInverse.Plane} (hx : x.1.1 ∈ U) (hk : x ∈ (scalarCells g r L rate hinj).carrier n k) (hn : (x.1.1, x.2) ∉ ActualGaussianCoverage.sourceRegion (S n) (g n) (r n) (L n) (rate n)) : ((scalarData base t f g r L rate hr hL hc).cutoff n k =ᶠ[nhds x] fun (x : (P × ℝ) × TorusInverse.Plane) => 0) ∨ ((scalarData base t f g r L rate hr hL hc).amplitude n k =ᶠ[nhds x] fun (x : (P × ℝ) × TorusInverse.Plane) => 0) ∧ (scalarData base t f g r L rate hr hL hc).pressure n k =ᶠ[nhds x] fun (x : (P × ℝ) × TorusInverse.Plane) => 0

Outside the source carrier, each padded native cell has a zero cutoff or a zero whole-path Volterra solve.

theorem NavierStokes.ScalarParticularSupport.scalarData_zero_germs {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)) (t : ℕ → CommonCoverSolve.TangentData (P × ℝ) ProblemStatement.Space) (f : ℕ → (P × ℝ) × TorusInverse.Plane → HarmonicCalculus.ComplexVector) (g : ℕ → CommonCoverSolve.Geometry) (r L rate : ℕ → ℝ) (hr : ∀ (n : ℕ), 0 < r n) (hL : ∀ (n : ℕ), 0 < L n) (hc : ∀ (n : ℕ), 0 < rate n) (hinj : ∀ (n : ℕ), Set.InjOn TorusAverages.quotientPoint ((fun (z : TorusInverse.Plane) => (g n).center + (g n).basis z) '' ActualGaussianCoverage.outerCell (r n) (L n) (rate n))) (U : Set P) (S : ℕ → Set P) (hf : ∀ (n : ℕ) (x : (P × ℝ) × TorusInverse.Plane), x.1.1 ∈ U → (x.1.1, x.2) ∉ ActualGaussianCoverage.sourceRegion (S n) (g n) (r n) (L n) (rate n) → f n =ᶠ[nhds x] fun (x : (P × ℝ) × TorusInverse.Plane) => 0) (s : WeightedClasses.StripData ((P × ℝ) × TorusInverse.Plane)) (d : LinearWaveBounds.GraphDirections ((P × ℝ) × TorusInverse.Plane)) (n : ℕ) {x : (P × ℝ) × TorusInverse.Plane} (hx : x.1.1 ∈ U) (hn : (x.1.1, x.2) ∉ ActualGaussianCoverage.sourceRegion (S n) (g n) (r n) (L n) (rate n)) : have a := scalarData base t f g r L rate hr hL hc; ((a.commonCorrected s d).amplitude n =ᶠ[nhds x] fun (x : (P × ℝ) × TorusInverse.Plane) => 0) ∧ (a.common.pressure n =ᶠ[nhds x] fun (x : (P × ℝ) × TorusInverse.Plane) => 0) ∧ a.globalGaussian d n =ᶠ[nhds x] fun (x : (P × ℝ) × TorusInverse.Plane) => 0

Jets of the literal transported native cutoff

The product consists of the padded reference window and the separate Gaussian slot cutoff. On the analytic patch the window equals one on an ambient neighborhood, including at the closed transverse endpoints. Its exact germ therefore transfers the Gaussian clock estimates without assumptions about a source, correction state, or modal-control output.

noncomputable def NavierStokes.NativeCutoffJets.literalCutoff {Label P : Type} {D : PhaseJetBounds.Domain (Label × ℕ) PhaseCalculus.Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (clock : ActualSignedControl.PositiveScale Label) (g : Label → ℕ → CommonCoverSolve.Geometry) (r : Label → ℕ → ℝ) (hr : ∀ (l : Label) (n : ℕ), 0 < r l n) (l : Label) (n : ℕ) (k : TorusInverse.Frequency) (x : P × TorusInverse.Plane) : ℝ

The literal cutoff, before placing it in any particular-solve record.

Equations

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

theorem NavierStokes.NativeCutoffJets.literalCutoff_eq_referenceTransport {Label P : Type} {D : PhaseJetBounds.Domain (Label × ℕ) PhaseCalculus.Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (clock : ActualSignedControl.PositiveScale Label) (g : Label → ℕ → CommonCoverSolve.Geometry) (r : Label → ℕ → ℝ) (hr : ∀ (l : Label) (n : ℕ), 0 < r l n) (l : Label) (n : ℕ) (k : TorusInverse.Frequency) : literalCutoff F clock g r hr l n k = fun (x : P × TorusInverse.Plane) => ActualGaussianCoverage.referenceCutoff (r l n) (F.L (l, n)) ⋯ ⋯ (CopySolveCompatibility.nativeTimeMap 0 (clock.value l n) ((g l n).coordinates k x.2))

theorem NavierStokes.NativeCutoffJets.nativeTime_mem_core {Label P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : PhaseJetBounds.Domain (Label × ℕ) PhaseCalculus.Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (clock : ActualSignedControl.PositiveScale Label) (g : Label → ℕ → CommonCoverSolve.Geometry) (r : Label → ℕ → ℝ) (hr : ∀ (l : Label) (n : ℕ), 0 < r l n) (s : WeightedClasses.StripData P) (χ : P →L[ℝ] PhaseCalculus.Slow) (φ : Label × ℕ → PhaseCalculus.Slow →L[ℝ] PhaseCalculus.Slow) (l : Label) (n : ℕ) (k : TorusInverse.Frequency) {x : P × TorusInverse.Plane} (hx : x ∈ ScaledActualParticularControl.patch s F χ φ clock g r l n k) : CopySolveCompatibility.nativeTimeMap 0 (clock.value l n) ((g l n).coordinates k x.2) ∈ (ActualGaussianCoverage.referenceWindow (r l n) (F.L (l, n)) ⋯ ⋯).core

Patch membership supplies the actual closed-core hypothesis of the reference window's neighborhood theorem.

theorem NavierStokes.NativeCutoffJets.literalCutoff_gaussian_germ {Label P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : PhaseJetBounds.Domain (Label × ℕ) PhaseCalculus.Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (clock : ActualSignedControl.PositiveScale Label) (g : Label → ℕ → CommonCoverSolve.Geometry) (r : Label → ℕ → ℝ) (hr : ∀ (l : Label) (n : ℕ), 0 < r l n) (s : WeightedClasses.StripData P) (χ : P →L[ℝ] PhaseCalculus.Slow) (φ : Label × ℕ → PhaseCalculus.Slow →L[ℝ] PhaseCalculus.Slow) (l : Label) (n : ℕ) (k : TorusInverse.Frequency) {x : P × TorusInverse.Plane} (hx : x ∈ ScaledActualParticularControl.patch s F χ φ clock g r l n k) : literalCutoff F clock g r hr l n k =ᶠ[nhds x] fun (y : P × TorusInverse.Plane) => GaussianTailFlat.profile (ActualGaussianCoverage.theta F clock l n ((g l n).coordinates k y.2).2)

This is an ambient germ, obtained from the padded window's exact cutoff_germ theorem rather than from its value at the boundary point.

theorem NavierStokes.NativeCutoffJets.literalCutoff_uniformLocalJets {Label P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : PhaseJetBounds.Domain (Label × ℕ) PhaseCalculus.Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (clock : ActualSignedControl.PositiveScale Label) (g : Label → ℕ → CommonCoverSolve.Geometry) (r : Label → ℕ → ℝ) (hr : ∀ (l : Label) (n : ℕ), 0 < r l n) (s : WeightedClasses.StripData P) (χ : P →L[ℝ] PhaseCalculus.Slow) (φ : Label × ℕ → PhaseCalculus.Slow →L[ℝ] PhaseCalculus.Slow) {u0 : ℝ} (hu0 : 0 < u0) (hu : ∀ (l : Label) (n : ℕ), F.u (l, n) = u0) (hcost : ∃ (K : ℝ), 1 ≤ K ∧ ∃ (p : ℕ), ∀ (l : Label) (n : ℕ), CommonCoverClass.argumentCost (g l n) ≤ K * s.slow n ^ p) : PeriodizedWaveBounds.UniformLocalJets (CommonCoverClass.sourceStrip s) (fun (x : Label) (x_1 : ℕ) (x_2 : P × TorusInverse.Plane) => 1) 0 (ScaledActualParticularControl.patch s F χ φ clock g r) (literalCutoff F clock g r hr)

All finite jets are uniform in the label, band, and lifted copy. The only quantitative input beyond the primitive phase and clock is the polynomial bound for the actual affine geometry.

@[reducible, inline]

abbrev NavierStokes.ActualParticularStageControls.Slow : Type

Slow: an abbreviation for PhaseCalculus.Slow.

Equations

• NavierStokes.ActualParticularStageControls.Slow = NavierStokes.PhaseCalculus.Slow

@[reducible, inline]

abbrev NavierStokes.ActualParticularStageControls.Parameter : Type

Parameter: an abbreviation for PhysicalParticularWave.Parameter.

Equations

• NavierStokes.ActualParticularStageControls.Parameter = NavierStokes.PhysicalParticularWave.Parameter

@[reducible, inline]

abbrev NavierStokes.ActualParticularStageControls.Plane : Type

Plane: an abbreviation for TorusInverse.Plane.

Equations

• NavierStokes.ActualParticularStageControls.Plane = NavierStokes.TorusInverse.Plane

@[reducible, inline]

abbrev NavierStokes.ActualParticularStageControls.Native : Type

Native: an abbreviation for (Parameter × ℝ) × Plane.

Equations

• NavierStokes.ActualParticularStageControls.Native = ((NavierStokes.ActualParticularStageControls.Parameter × ℝ) × NavierStokes.ActualParticularStageControls.Plane)

@[reducible, inline]

abbrev NavierStokes.ActualParticularStageControls.AP : Type

AP: an abbreviation for CorrectionInitialization.ActualPrimary.FullPoint.

Equations

• NavierStokes.ActualParticularStageControls.AP = NavierStokes.CorrectionInitialization.ActualPrimary.FullPoint

@[reducible, inline]

abbrev NavierStokes.ActualParticularStageControls.Label (B N0 : ℕ) : Type

Label: an abbreviation for Fin 2 × CorrectionInitialization.ActualPrimary.Label B N0 /-! Reindexing retains the selected phase, its frame, and all uniform constants. -/.

Equations

• NavierStokes.ActualParticularStageControls.Label B N0 = (Fin 2 × NavierStokes.CorrectionInitialization.ActualPrimary.Label B N0)

Reindexing retains the selected phase, its frame, and all uniform constants.

noncomputable def NavierStokes.ActualParticularStageControls.reindexDomain {ι κ : Type} (D : PhaseJetBounds.Domain ι Slow) (e : κ → ι) : PhaseJetBounds.Domain κ Slow

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

Equations

• NavierStokes.ActualParticularStageControls.reindexDomain D e = { scale := fun (i : κ) => D.scale (e i), carrier := fun (i : κ) => D.carrier (e i), isOpen := ⋯, one_le_scale := ⋯ }

noncomputable def NavierStokes.ActualParticularStageControls.reindexPhase {ι κ : Type} (F : PhaseJetBounds.PhaseFamily ι) (e : κ → ι) : PhaseJetBounds.PhaseFamily κ

Reindex phase, bundling epsilon, p, pz, x0 and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.ActualParticularStageControls.reindexConstruction {ι κ : Type} {D : PhaseJetBounds.Domain ι Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (e : κ → ι) : PrimaryPulseBounds.PhaseConstruction (reindexDomain D e)

Reindex construction, bundling phase, V, openV, lam and the required compatibility proofs.

Equations

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

@[simp]

theorem NavierStokes.ActualParticularStageControls.reindex_frame {ι κ : Type} {D : PhaseJetBounds.Domain ι Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (e : κ → ι) (i : κ) : (reindexConstruction F e).frame i = F.frame (e i)

The original physical slot, Gaussian cutoff, and actual current-state data.

noncomputable def NavierStokes.ActualParticularStageControls.spatialLabel {B N0 : ℕ} (l : Label B N0) : SlotColoring.Label

Spatial label, given by PartitionedCovariance.signedLabel (PrimaryGeometryAssembly.label nominal l.2) l.1.

Equations

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

noncomputable def NavierStokes.ActualParticularStageControls.referenceGeometry {B N0 : ℕ} (l : Label B N0) : CommonCoverSolve.Geometry

Reference geometry, given by ActualSignedGeometry.slotGeometry slots vectors_det (spatialLabel l) 0.

Equations

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

noncomputable def NavierStokes.ActualParticularStageControls.gap {B N0 : ℕ} (l : Label B N0) (n : ℕ) : ℕ

Gap, given by ChartScales.nativeIndex h (BaseChartJets.cellBand l.2) - CommonWindow.index h n.

Equations

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

theorem NavierStokes.ActualParticularStageControls.reference_refine {B N0 : ℕ} (l : Label B N0) (n : ℕ) : CopySolveCompatibility.refineGeometry (referenceGeometry l) (gap l n) = CorrectionInitialization.ActualPrimary.chartGeometry n l.1 l.2

noncomputable def NavierStokes.ActualParticularStageControls.referenceCutoff {B N0 : ℕ} (l : Label B N0) (z : Plane) : ℝ

Reference cutoff, given by (clockWindow l.2).cutoff z * GaussianTailFlat.slotCutoff ((phases B N0 l.1).L l.2) z.2.

Equations

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

theorem NavierStokes.ActualParticularStageControls.referenceCutoff_compact {B N0 : ℕ} (l : Label B N0) : HasCompactSupport (referenceCutoff l)

noncomputable def NavierStokes.ActualParticularStageControls.reference {B N0 : ℕ} (l : Label B N0) : ParticularWaveAssembly.Reference Parameter

Reference, bundling band, geometry, length, length_pos and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.ActualParticularStageControls.nativeToFull : Native ≃ₗᵢ[ℝ] AP

Native to full, given by ParticularWaveAssembly.angleShuffle.symm.trans (StateReindex.cylinder cycleAssoc.symm).

Equations

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

noncomputable def NavierStokes.ActualParticularStageControls.background {B N0 : ℕ} (l : Label B N0) : LinearWaveBounds.WaveCoefficients Native

Background, given by ParticularWaveBounds.reindexCoefficients nativeToFull (chartCoefficients l.1 l.2).

Equations

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

noncomputable def NavierStokes.ActualParticularStageControls.directions {B : ℕ} : LinearWaveBounds.GraphDirections Native

Directions, given by ParticularWaveBounds.reindexDirections nativeToFull (PrimaryResidualClass.directions (commonContext B)).

Equations

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

noncomputable def NavierStokes.ActualParticularStageControls.associatedContext {B : ℕ} : CorrectionState.Context (Parameter × Plane)

Associated context, given by StateReindex.context cycleAssoc.symm (commonContext B).

Equations

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

noncomputable def NavierStokes.ActualParticularStageControls.associatedStrip : WeightedClasses.StripData (Parameter × Plane)

Associated strip, given by ParticularWaveBounds.reindexStrip cycleAssoc.symm (BaseContextAssembly.nativeStrip nominal standardRegion).

Equations

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

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

Assembly, bundling reference, charts, parameter, gap and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.ActualParticularStageControls.parameters {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) : CorrectionStep.ParticularParameters Parameter

Parameters, given by ParticularParameters.fromReference (assembly x l) h (gap l).

Equations

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

theorem NavierStokes.ActualParticularStageControls.parameters_source {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (j : ℤ) : ((parameters x l).copyData (assembly x l).context (assembly x l).state (assembly x l).carrierBlock (assembly x l).gaussianInput (assembly x l).aliasInput j).source = ParticularWaveAssembly.sourceFamily (assembly x l).context (assembly x l).state (assembly x l).carrierBlock (assembly x l).gaussianInput (assembly x l).aliasInput j

theorem NavierStokes.ActualParticularStageControls.parameters_length {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (n : ℕ) : (parameters x l).length n = (CorrectionInitialization.ActualPrimary.phases B N0 l.1).L l.2 / PhysicalParticularWave.clockWeight CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (ChartScales.Q (BaseChartJets.cellBand l.2))

noncomputable def NavierStokes.ActualParticularStageControls.canonicalParameters {B N0 : ℕ} (l : Label B N0) : CorrectionStep.ParticularParameters Parameter

Fixed primitive data for all iterations of the same labeled construction.

Equations

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

theorem NavierStokes.ActualParticularStageControls.parameters_eq_canonical {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (hfrequency : ∀ (n : ℕ), (x.coefficients.blocks l).frequency n = ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n)) : parameters x l = canonicalParameters l

The sign combination is proved before specializing the constructed profile.

noncomputable def NavierStokes.ActualParticularStageControls.signedPhase {ι : Type} {D : PhaseJetBounds.Domain ι Slow} (F : Fin 2 → PrimaryPulseBounds.PhaseConstruction D) : PhaseJetBounds.PhaseFamily (Fin 2 × ι)

Signed phase, bundling epsilon, p, pz, x0 and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.ActualParticularStageControls.signedConstruction {ι : Type} {D : PhaseJetBounds.Domain ι Slow} (F : Fin 2 → PrimaryPulseBounds.PhaseConstruction D) (hr : ∀ (j : Fin 2), (F j).r = (F 0).r) (hb : ∀ (j : Fin 2), (F j).b = (F 0).b) (hM : ∀ (j : Fin 2), (F j).M = (F 0).M) (hC : ∀ (j : Fin 2), (F j).C = (F 0).C) (hE : ∀ (j : Fin 2), (F j).E = (F 0).E) (hF : ∀ (j : Fin 2), (F j).phase.F = (F 0).phase.F) (hG : ∀ (j : Fin 2), (F j).phase.G = (F 0).phase.G) : PrimaryPulseBounds.PhaseConstruction (reindexDomain D Prod.snd)

Signed construction, bundling phase, V, openV, lam and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.ActualParticularStageControls.jointDomain {B N0 : ℕ} : PhaseJetBounds.Domain (Label B N0) Slow

Joint domain, given by reindexDomain (PrimaryGeometryAssembly.domain nominal (choice B N0).prepared.N) Prod.snd.

Equations

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

noncomputable def NavierStokes.ActualParticularStageControls.jointPhase {B N0 : ℕ} : PhaseJetBounds.PhaseFamily (Label B N0)

Joint phase, given by signedPhase (phases B N0).

Equations

• NavierStokes.ActualParticularStageControls.jointPhase = NavierStokes.ActualParticularStageControls.signedPhase (NavierStokes.CorrectionInitialization.ActualPrimary.phases B N0)

theorem NavierStokes.ActualParticularStageControls.phase_common_bounds {B N0 : ℕ} (j : Fin 2) : (CorrectionInitialization.ActualPrimary.phases B N0 j).r = (CorrectionInitialization.ActualPrimary.phases B N0 0).r ∧ (CorrectionInitialization.ActualPrimary.phases B N0 j).b = (CorrectionInitialization.ActualPrimary.phases B N0 0).b ∧ (CorrectionInitialization.ActualPrimary.phases B N0 j).M = (CorrectionInitialization.ActualPrimary.phases B N0 0).M ∧ (CorrectionInitialization.ActualPrimary.phases B N0 j).C = (CorrectionInitialization.ActualPrimary.phases B N0 0).C ∧ (CorrectionInitialization.ActualPrimary.phases B N0 j).E = (CorrectionInitialization.ActualPrimary.phases B N0 0).E

theorem NavierStokes.ActualParticularStageControls.phase_frequency_eq {B N0 : ℕ} (j : Fin 2) : (CorrectionInitialization.ActualPrimary.phases B N0 j).phase.F = (CorrectionInitialization.ActualPrimary.phases B N0 0).phase.F

theorem NavierStokes.ActualParticularStageControls.phase_axial_eq {B N0 : ℕ} (j : Fin 2) : (CorrectionInitialization.ActualPrimary.phases B N0 j).phase.G = (CorrectionInitialization.ActualPrimary.phases B N0 0).phase.G

noncomputable def NavierStokes.ActualParticularStageControls.jointConstruction {B N0 : ℕ} : PrimaryPulseBounds.PhaseConstruction jointDomain

Joint construction, constructed using signedConstruction.

Equations

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

@[simp]

theorem NavierStokes.ActualParticularStageControls.joint_frame {B N0 : ℕ} (l : Label B N0) : jointConstruction.frame l = (CorrectionInitialization.ActualPrimary.phases B N0 l.1).frame l.2

Changing the native clock preserves the same grouped Gaussian exactly.

theorem NavierStokes.ActualParticularStageControls.copyEnvelope_time (g : CommonCoverSolve.Geometry) (r L rate : ℝ) (hrate : 0 < rate) (W : ℝ → ℝ) (Y : Plane) : WaveEnvelopeTransport.copyEnvelope (CopySolveCompatibility.timeGeometry g 0 rate ⋯) r (L / rate) (fun (t : ℝ) => W (rate * t)) Y = WaveEnvelopeTransport.copyEnvelope g r L W Y

theorem NavierStokes.ActualParticularStageControls.copyEnvelope_transport (g : CommonCoverSolve.Geometry) (gap : ℕ) (r L rate : ℝ) (hrate : 0 < rate) (W : ℝ → ℝ) (Y : Plane) : WaveEnvelopeTransport.copyEnvelope (CopySolveCompatibility.transportGeometry g gap 0 rate ⋯) r (L / rate) (fun (t : ℝ) => W (rate * t)) Y = WaveEnvelopeTransport.copyEnvelope (CopySolveCompatibility.refineGeometry g gap) r L W Y

The slow/fast association keeps the full moving weight unchanged.

noncomputable def NavierStokes.ActualParticularStageControls.slowInsert : Parameter →L[ℝ] CorrectionStep.CyclePoint

Slow insert, bundling toFun, map_add, map_smul, cont.

Equations

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

noncomputable def NavierStokes.ActualParticularStageControls.slowStrip : WeightedClasses.StripData Parameter

Slow strip, given by HarmonicWaveInteraction.pullbackStrip (BaseContextAssembly.nativeStrip nominal standardRegion) slowInsert.

Equations

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

theorem NavierStokes.ActualParticularStageControls.sourceStrip_eq : CommonCoverClass.sourceStrip slowStrip = associatedStrip

theorem NavierStokes.ActualParticularStageControls.nativeStrip_eq : CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip slowStrip) = CorrectionStep.ParticularParameters.nativeStrip associatedStrip

noncomputable def NavierStokes.ActualParticularStageControls.pulseEnvelope {B N0 : ℕ} (l : Label B N0) : ℝ → ℝ

Pulse envelope, given by PrimaryPulseBounds.referenceP ((phases B N0 l.1).lam l.2) ((phases B N0 l.1).u l.2) ((phases B N0 l.1).L l.2).

Equations

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

noncomputable def NavierStokes.ActualParticularStageControls.envelope {B N0 : ℕ} (l : Label B N0) (n : ℕ) (z : Parameter × Plane) : ℝ

Envelope, given by WaveEnvelopeTransport.copyEnvelope (chartGeometry n l.1 l.2) slots.radius ((phases B N0 l.1).L l.2) (pulseEnvelope l) z.2.

Equations

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

noncomputable def NavierStokes.ActualParticularStageControls.meanEnvelope {B N0 : ℕ} (l : Label B N0) (n : ℕ) (z : CorrectionStep.CyclePoint) : ℝ

Mean envelope, given by envelope l n (cycleAssoc z).

Equations

• NavierStokes.ActualParticularStageControls.meanEnvelope l n z = NavierStokes.ActualParticularStageControls.envelope l n (NavierStokes.CorrectionStep.cycleAssoc z)

noncomputable def NavierStokes.ActualParticularStageControls.nativeEnvelope {B N0 : ℕ} (l : Label B N0) (n : ℕ) (z : Native) : ℝ

Native envelope, given by envelope l n (z.1.1,z.2).

Equations

• NavierStokes.ActualParticularStageControls.nativeEnvelope l n z = NavierStokes.ActualParticularStageControls.envelope l n (z.1.1, z.2)

theorem NavierStokes.ActualParticularStageControls.envelope_nonneg {B N0 : ℕ} (l : Label B N0) (n : ℕ) (z : Parameter × Plane) : 0 ≤ envelope l n z

noncomputable def NavierStokes.ActualParticularStageControls.Active {B N0 : ℕ} (l : Label B N0) (n : ℕ) : Prop

Active, given by 1 ≤ n ∧ BaseChartJets.cellBand l.2 ∈ CommonWindow.levels n.

Equations

• NavierStokes.ActualParticularStageControls.Active l n = (1 ≤ n ∧ NavierStokes.BaseChartJets.cellBand l.2 ∈ NavierStokes.CorrectionInitialization.CommonWindow.levels n)

@[reducible, inline]

abbrev NavierStokes.ActualParticularStageControls.ActivePair (B N0 : ℕ) : Type

Active pair: an abbreviation for {i : Label B N0 × ℕ // Active i.1 i.2}.

Equations

• NavierStokes.ActualParticularStageControls.ActivePair B N0 = { i : NavierStokes.ActualParticularStageControls.Label B N0 × ℕ // NavierStokes.ActualParticularStageControls.Active i.1 i.2 }

noncomputable def NavierStokes.ActualParticularStageControls.selectedLabel {B N0 : ℕ} (e : ℕ → ActivePair B N0) (n : ℕ) : Label B N0

Selected label, given by (e n).val.1.

Equations

• NavierStokes.ActualParticularStageControls.selectedLabel e n = (↑(e n)).1

noncomputable def NavierStokes.ActualParticularStageControls.selectedBand {B N0 : ℕ} (e : ℕ → ActivePair B N0) (n : ℕ) : ℕ

Selected band, given by (e n).val.2.

Equations

• NavierStokes.ActualParticularStageControls.selectedBand e n = (↑(e n)).2

noncomputable def NavierStokes.ActualParticularStageControls.selectedConstruction {B N0 : ℕ} (e : ℕ → ActivePair B N0) : PrimaryPulseBounds.PhaseConstruction (reindexDomain jointDomain fun (i : Unit × ℕ) => selectedLabel e i.2)

Selected construction, given by reindexConstruction (jointConstruction (B := B) (N0 := N0)) (fun i : Unit × ℕ => selectedLabel e i.2).

Equations

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

noncomputable def NavierStokes.ActualParticularStageControls.selectedStrip {B N0 : ℕ} (e : ℕ → ActivePair B N0) : WeightedClasses.StripData Parameter

Selected strip, given by UniformPrimaryWeights.reindexedStrip slowStrip (fun n => (selectedBand e n, ())).

Equations

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

noncomputable def NavierStokes.ActualParticularStageControls.selectedSlot {B N0 : ℕ} (e : ℕ → ActivePair B N0) : Unit → (n : ℕ) → SlotColoring.Label

Selected slot, given by spatialLabel (selectedLabel e n).

Equations

• NavierStokes.ActualParticularStageControls.selectedSlot e x✝ n = NavierStokes.ActualParticularStageControls.spatialLabel (NavierStokes.ActualParticularStageControls.selectedLabel e n)

theorem NavierStokes.ActualParticularStageControls.selected_near {B N0 : ℕ} (e : ℕ → ActivePair B N0) (u : Unit) (n : ℕ) : selectedBand e n ≤ (selectedSlot e u n).1 + 4 ∧ (selectedSlot e u n).1 ≤ selectedBand e n + 4

noncomputable def NavierStokes.ActualParticularStageControls.selectedClock {B N0 : ℕ} (e : ℕ → ActivePair B N0) : ActualSignedControl.PositiveScale Unit

Selected clock, given by ActualSignedGeometry.clockScale (selectedBand e) (fun u n => (selectedSlot e u n).1) (selected_near e) h.

Equations

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

noncomputable def NavierStokes.ActualParticularStageControls.selectedNormal {B N0 : ℕ} (e : ℕ → ActivePair B N0) : ActualSignedControl.PositiveScale Unit

Selected normal, given by ActualSignedGeometry.normalScale (selectedBand e) (fun u n => (selectedSlot e u n).1) (selected_near e) outgoing.data.h_pos.le.

Equations

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

noncomputable def NavierStokes.ActualParticularStageControls.selectedGap {B N0 : ℕ} (e : ℕ → ActivePair B N0) : Unit → (n : ℕ) → ℕ

Selected gap, given by gap (selectedLabel e n) (selectedBand e n).

Equations

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

noncomputable def NavierStokes.ActualParticularStageControls.selectedGeometry {B N0 : ℕ} (e : ℕ → ActivePair B N0) (l : Unit) (n : ℕ) : CommonCoverSolve.Geometry

Selected geometry, constructed using ScaledActualParticularControl.geometry.

Equations

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

noncomputable def NavierStokes.ActualParticularStageControls.selectedLength {B N0 : ℕ} (e : ℕ → ActivePair B N0) (l : Unit) (n : ℕ) : ℝ

Selected length, given by ScaledActualParticularControl.length (selectedConstruction e) (selectedClock e).

Equations

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

noncomputable def NavierStokes.ActualParticularStageControls.selectedPulseEnvelope {B N0 : ℕ} (e : ℕ → ActivePair B N0) (l : Unit) (n : ℕ) (v : ℝ) : ℝ

Selected pulse envelope, given by ScaledActualParticularControl.envelope (selectedConstruction e) (selectedClock e).

Equations

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

theorem NavierStokes.ActualParticularStageControls.selected_geometry_eq {B N0 : ℕ} (e : ℕ → ActivePair B N0) (x : CorrectionStep.CycleState (Label B N0)) (n : ℕ) : selectedGeometry e () n = (parameters x (selectedLabel e n)).geometry (selectedBand e n)

theorem NavierStokes.ActualParticularStageControls.selected_length_eq {B N0 : ℕ} (e : ℕ → ActivePair B N0) (x : CorrectionStep.CycleState (Label B N0)) (n : ℕ) : selectedLength e () n = (parameters x (selectedLabel e n)).length (selectedBand e n)

theorem NavierStokes.ActualParticularStageControls.selected_gap_bound {B N0 : ℕ} (e : ℕ → ActivePair B N0) (u : Unit) (n : ℕ) : selectedGap e u n ≤ CorrectionInitialization.CommonWindow.gap CorrectionInitialization.ActualPrimary.h + SlotColoring.nativeGap CorrectionInitialization.ActualPrimary.h

theorem NavierStokes.ActualParticularStageControls.selected_slot_large {B N0 : ℕ} (e : ℕ → ActivePair B N0) (u : Unit) (n : ℕ) : 4 ≤ (selectedSlot e u n).1

theorem NavierStokes.ActualParticularStageControls.selected_scale {B N0 : ℕ} (e : ℕ → ActivePair B N0) (i : Unit × ℕ) : (reindexDomain jointDomain fun (z : Unit × ℕ) => selectedLabel e z.2).scale i = ChartScales.S (selectedSlot e i.1 i.2).1

theorem NavierStokes.ActualParticularStageControls.selected_length {B N0 : ℕ} (e : ℕ → ActivePair B N0) (i : Unit × ℕ) : (selectedConstruction e).L i = ChartScales.slotLength CorrectionInitialization.ActualPrimary.slots.radius CorrectionInitialization.ActualPrimary.h (selectedSlot e i.1 i.2).1

theorem NavierStokes.ActualParticularStageControls.selected_envelope_eq {B N0 : ℕ} (e : ℕ → ActivePair B N0) (n : ℕ) (z : Parameter × Plane) : ActualParticularControl.groupedEnvelope (selectedGeometry e) (fun (x : Unit) (x_1 : ℕ) => CorrectionInitialization.ActualPrimary.slots.radius) (selectedLength e) (selectedPulseEnvelope e) () n z = envelope (selectedLabel e n) (selectedBand e n) z

The input class is exactly the residual component of the cycle invariant.

theorem NavierStokes.ActualParticularStageControls.select_uniform {ι X E : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData X} {w : ι → ℕ → X → ℝ} {f : ι → ℕ → X → E} {α : ℝ} (hf : LabelSumBounds.UniformClass s w α f) (e : ℕ → ι × ℕ) : LabelSumBounds.UniformClass (UniformPrimaryWeights.reindexedStrip s fun (n : ℕ) => ((e n).2, ())) (fun (x : Unit) (n : ℕ) => w (e n).1 (e n).2) α fun (x : Unit) (n : ℕ) => f (e n).1 (e n).2

theorem NavierStokes.ActualParticularStageControls.associated_residual_class {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) {α : ℝ} (H : UniformHarmonicInteraction.UniformVelocity (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion) meanEnvelope α fun (l : Label B N0) => HarmonicResidual.residualBlock (CorrectionInitialization.ActualPrimary.commonContext B) x.state (x.coefficients.blocks l) (x.coefficients.gaussian l) (x.coefficients.aliasCoefficients l)) : UniformHarmonicInteraction.UniformVelocity associatedStrip envelope α fun (l : Label B N0) => HarmonicResidual.residualBlock (assembly x l).context (assembly x l).state (assembly x l).carrierBlock (assembly x l).gaussianInput (assembly x l).aliasInput

noncomputable def NavierStokes.ActualParticularStageControls.currentSource {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (j : ℤ) (l : Label B N0) : ℕ → Native → HarmonicCalculus.ComplexVector

Current source, constructed using ParticularWaveAssembly.sourceFamily.

Equations

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

theorem NavierStokes.ActualParticularStageControls.current_source_class {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) {α : ℝ} (H : UniformHarmonicInteraction.UniformVelocity (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion) meanEnvelope α fun (l : Label B N0) => HarmonicResidual.residualBlock (CorrectionInitialization.ActualPrimary.commonContext B) x.state (x.coefficients.blocks l) (x.coefficients.gaussian l) (x.coefficients.aliasCoefficients l)) (j : ℤ) (hj : j ≠ 0) : LabelSumBounds.UniformWaveClass (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip slowStrip)) nativeEnvelope α (currentSource x j)

theorem NavierStokes.ActualParticularStageControls.invariant_current_source_class {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) {G : SignedMeanGain.Geometry} {primary : Label B N0 → CorrectionState.HarmonicBlock CorrectionStep.CyclePoint} {σ : ℝ} {labelCarrier : Label B N0 → ℕ → Set CorrectionStep.CyclePoint} (H : CorrectionStep.CycleAnalyticInvariant G (CorrectionInitialization.ActualPrimary.commonContext B) primary meanEnvelope labelCarrier σ x) (hstrip : G.strip = BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion) (j : ℤ) (hj : j ≠ 0) : LabelSumBounds.UniformWaveClass (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip slowStrip)) nativeEnvelope (1 / 2 + σ) (currentSource x j)

theorem NavierStokes.ActualParticularStageControls.source_angle_reindex (s : WeightedClasses.StripData Parameter) (index : ℕ → ℕ) : CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip (UniformPrimaryWeights.reindexedStrip s fun (n : ℕ) => (index n, ()))) = UniformPrimaryWeights.reindexedStrip (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip s)) fun (n : ℕ) => (index n, ())

theorem NavierStokes.ActualParticularStageControls.selected_source_class {B N0 : ℕ} {j : ℤ} (x : CorrectionStep.CycleState (Label B N0)) {α : ℝ} (H : LabelSumBounds.UniformWaveClass (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip slowStrip)) nativeEnvelope α (currentSource x j)) (e : ℕ → ActivePair B N0) : LabelSumBounds.UniformWaveClass (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip (selectedStrip e))) (ActualParticularControl.groupedEnvelope (selectedGeometry e) (fun (x : Unit) (x_1 : ℕ) => CorrectionInitialization.ActualPrimary.slots.radius) (selectedLength e) (selectedPulseEnvelope e)) α fun (x_1 : Unit) (n : ℕ) => currentSource x j (selectedLabel e n) (selectedBand e n)

noncomputable def NavierStokes.ActualParticularStageControls.selectedPhi {B N0 : ℕ} (e : ℕ → ActivePair B N0) (i : Unit × ℕ) : ScaledActualParticularControl.Slow →L[ℝ] ScaledActualParticularControl.Slow

Selected phi, given by ScaledActualParticularControl.physicalPhi h (selectedBand e) (fun u n => (selectedSlot e u n).1).

Equations

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

noncomputable def NavierStokes.ActualParticularStageControls.selectedChi : Parameter × ℝ →L[ℝ] Slow

Selected chi, given by ActualSignedGeometry.swapParameter.toContinuousLinearEquiv.toContinuousLinearMap.comp (ContinuousLinearMap.fst ℝ Parameter ℝ).

Equations

• NavierStokes.ActualParticularStageControls.selectedChi = ↑↑NavierStokes.ActualSignedGeometry.swapParameter ∘SL ContinuousLinearMap.fst ℝ NavierStokes.ActualParticularStageControls.Parameter ℝ

noncomputable def NavierStokes.ActualParticularStageControls.selectedFrame {B N0 : ℕ} (e : ℕ → ActivePair B N0) (n : ℕ) : PrimaryODE.FrameData ((Parameter × ℝ) × ℝ)

Selected frame, constructed using ActualParticularControl.nativeFrame.

Equations

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

noncomputable def NavierStokes.ActualParticularStageControls.selectedPatch {B N0 : ℕ} (e : ℕ → ActivePair B N0) : Unit → ℕ → TorusInverse.Frequency → Set Native

Selected patch, constructed using ScaledActualParticularControl.patch.

Equations

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

theorem NavierStokes.ActualParticularStageControls.selected_scale_le {B N0 : ℕ} (e : ℕ → ActivePair B N0) (i : Unit × ℕ) : (reindexDomain jointDomain fun (z : Unit × ℕ) => selectedLabel e z.2).scale i ≤ 25 * (selectedStrip e).slow i.2

theorem NavierStokes.ActualParticularStageControls.selected_geometry_bound {B N0 : ℕ} (e : ℕ → ActivePair B N0) (u : Unit) (n : ℕ) : CommonCoverClass.argumentCost (selectedGeometry e u n) ≤ ScaledActualParticularControl.slotCost CorrectionInitialization.ActualPrimary.vectors_det (selectedClock e) (CorrectionInitialization.CommonWindow.gap CorrectionInitialization.ActualPrimary.h + SlotColoring.nativeGap CorrectionInitialization.ActualPrimary.h) * (selectedStrip e).slow n ^ 2

noncomputable def NavierStokes.ActualParticularStageControls.selectedControl {B N0 : ℕ} (e : ℕ → ActivePair B N0) (x : CorrectionStep.CycleState (Label B N0)) {α : ℝ} (j : ℤ) (hj : j ≠ 0) (H : LabelSumBounds.UniformWaveClass (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip slowStrip)) nativeEnvelope α (currentSource x j)) (part : HarmonicCalculus.ComplexVector →L[ℝ] ProblemStatement.Space) : ParticularCopyBounds.UniformModalControl (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip (selectedStrip e))) α (fun (l : Unit) (n : ℕ) => ActualParticularControl.nativeFrame (ScaledActualParticularControl.frame (selectedConstruction e) (selectedPhi e) (selectedClock e) (selectedNormal e) (l, n)) selectedChi) (fun (l : Unit) (n : ℕ) => PrimaryCopyBridge.frameTangentData (ActualParticularControl.nativeFrame (ScaledActualParticularControl.frame (selectedConstruction e) (selectedPhi e) (selectedClock e) (selectedNormal e) (l, n)) selectedChi) j fun (z : (Parameter × ℝ) × ScaledActualParticularControl.Plane) => part (currentSource x j (selectedLabel e n) (selectedBand e n) z)) j (ScaledActualParticularControl.geometry (ScaledActualParticularControl.slotReference CorrectionInitialization.ActualPrimary.slots CorrectionInitialization.ActualPrimary.vectors_det (selectedSlot e)) (selectedGap e) (selectedClock e)) (ScaledActualParticularControl.length (selectedConstruction e) (selectedClock e)) (ScaledActualParticularControl.envelope (selectedConstruction e) (selectedClock e)) (ScaledActualParticularControl.patch (ActualParticularControl.angleStrip (selectedStrip e)) (selectedConstruction e) selectedChi (selectedPhi e) (selectedClock e) (ScaledActualParticularControl.geometry (ScaledActualParticularControl.slotReference CorrectionInitialization.ActualPrimary.slots CorrectionInitialization.ActualPrimary.vectors_det (selectedSlot e)) (selectedGap e) (selectedClock e)) fun (x : Unit) (x_1 : ℕ) => CorrectionInitialization.ActualPrimary.slots.radius)

The real or imaginary control is constructed from the selected phase, the exact clock and slot geometry, and the current residual class.

Equations

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

theorem NavierStokes.ActualParticularStageControls.selected_tangent_eq {B N0 : ℕ} (e : ℕ → ActivePair B N0) (x : CorrectionStep.CycleState (Label B N0)) (hfrequency : ∀ (l : Label B N0) (n : ℕ), (x.coefficients.blocks l).frequency n = ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n)) (j : ℤ) (hj : j ≠ 0) (n : ℕ) (f : Native → ProblemStatement.Space) : ScaledActualParticularControl.withSource ((parameters x (selectedLabel e n)).nativeTangent j (selectedBand e n)) f = PrimaryCopyBridge.frameTangentData (selectedFrame e n) j f

noncomputable def NavierStokes.ActualParticularStageControls.selectedSource {B N0 : ℕ} (e : ℕ → ActivePair B N0) (x : CorrectionStep.CycleState (Label B N0)) (j : ℤ) : Unit → (n : ℕ) → Native → HarmonicCalculus.ComplexVector

Selected source, given by currentSource x j (selectedLabel e n) (selectedBand e n).

Equations

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

noncomputable def NavierStokes.ActualParticularStageControls.selectedTangent {B N0 : ℕ} (e : ℕ → ActivePair B N0) (x : CorrectionStep.CycleState (Label B N0)) (j : ℤ) : Unit → (n : ℕ) → CommonCoverSolve.TangentData (Parameter × ℝ) ProblemStatement.Space

Selected tangent, given by (parameters x (selectedLabel e n)).nativeTangent j (selectedBand e n).

Equations

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

noncomputable def NavierStokes.ActualParticularStageControls.selectedBackground {B N0 : ℕ} (e : ℕ → ActivePair B N0) (x : CorrectionStep.CycleState (Label B N0)) (j : ℤ) : Unit → LinearWaveBounds.WaveCoefficients ((Parameter × ℝ) × TorusInverse.Plane)

Selected background, constructed using ParticularCopyBounds.reindexedBase.

Equations

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

noncomputable def NavierStokes.ActualParticularStageControls.selectedActualControl {B N0 : ℕ} (e : ℕ → ActivePair B N0) (x : CorrectionStep.CycleState (Label B N0)) (hfrequency : ∀ (l : Label B N0) (n : ℕ), (x.coefficients.blocks l).frequency n = ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n)) {α : ℝ} (j : ℤ) (hj : j ≠ 0) (H : LabelSumBounds.UniformWaveClass (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip slowStrip)) nativeEnvelope α (currentSource x j)) (part : HarmonicCalculus.ComplexVector →L[ℝ] ProblemStatement.Space) : ParticularCopyBounds.UniformModalControl (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip (selectedStrip e))) α (fun (x : Unit) (n : ℕ) => selectedFrame e n) (fun (u : Unit) (n : ℕ) => ScaledActualParticularControl.withSource (selectedTangent e x j u n) fun (z : (Parameter × ℝ) × ScaledActualParticularControl.Plane) => part (selectedSource e x j u n z)) j (selectedGeometry e) (selectedLength e) (selectedPulseEnvelope e) (selectedPatch e)

This is the control of the literal selected fromReference tangent, after its source is overwritten by the corresponding part of the current HR source.

Equations

• NavierStokes.ActualParticularStageControls.selectedActualControl e x hfrequency j hj H part = ⋯.mpr (NavierStokes.ActualParticularStageControls.selectedControl e x j hj H part)

theorem NavierStokes.ActualParticularStageControls.selected_inverse_frequency {B N0 : ℕ} (e : ℕ → ActivePair B N0) (x : CorrectionStep.CycleState (Label B N0)) (hfrequency : ∀ (l : Label B N0) (n : ℕ), (x.coefficients.blocks l).frequency n = ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n)) (j : ℤ) (hj : j ≠ 0) : UniformPrimaryWeights.UniformBandBound (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip (selectedStrip e))) (1 / 2) fun (u : Unit) (n : ℕ) => 1 / (selectedBackground e x j u).frequency n

theorem NavierStokes.ActualParticularStageControls.uniform_to_local {ι I X E : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData X} {w : ι → ℕ → X → ℝ} {f : ι → ℕ → X → E} {α : ℝ} (hf : LabelSumBounds.UniformClass s w α f) (C : ι → ℕ → I → Set X) : PeriodizedWaveBounds.UniformLocalJets s w α C fun (l : ι) (n : ℕ) (x : I) => f l n

noncomputable def NavierStokes.ActualParticularStageControls.data {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (j : ℤ) : PeriodizedWaveBounds.CopyData ((Parameter × ℝ) × TorusInverse.Plane) TorusInverse.Frequency

The actual computed copy data, with the current residual as source.

Equations

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

noncomputable def NavierStokes.ActualParticularStageControls.controlPatch {B N0 : ℕ} (l : Label B N0) (n : ℕ) (k : TorusInverse.Frequency) : Set Native

The active phase patch includes the transverse boundary. Its time coordinate is the actual transported clock.

Equations

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

theorem NavierStokes.ActualParticularStageControls.selected_controlPatch {B N0 : ℕ} (e : ℕ → ActivePair B N0) (u : Unit) (q : ℕ) (k : TorusInverse.Frequency) : controlPatch (selectedLabel e q) (selectedBand e q) k = selectedPatch e u q k

theorem NavierStokes.ActualParticularStageControls.selected_data_amplitude {B N0 : ℕ} (e : ℕ → ActivePair B N0) (x : CorrectionStep.CycleState (Label B N0)) (j : ℤ) (u : Unit) (q : ℕ) (k : TorusInverse.Frequency) : (data x (selectedLabel e q) j).amplitude (selectedBand e q) k = (ParticularWaveBounds.complexCopyCoefficients (selectedBackground e x j u) (selectedTangent e x j u) (selectedSource e x j u) (selectedGeometry e u) (fun (x : ℕ) => k) (selectedLength e u) ⋯).amplitude q

theorem NavierStokes.ActualParticularStageControls.selected_data_pressure {B N0 : ℕ} (e : ℕ → ActivePair B N0) (x : CorrectionStep.CycleState (Label B N0)) (j : ℤ) (u : Unit) (q : ℕ) (k : TorusInverse.Frequency) : (data x (selectedLabel e q) j).pressure (selectedBand e q) k = (ParticularWaveBounds.complexCopyCoefficients (selectedBackground e x j u) (selectedTangent e x j u) (selectedSource e x j u) (selectedGeometry e u) (fun (x : ℕ) => k) (selectedLength e u) ⋯).pressure q

noncomputable def NavierStokes.ActualParticularStageControls.selectedWeight {B N0 : ℕ} (e : ℕ → ActivePair B N0) : Unit → ℕ → Native → ℝ

Selected weight, constructed using ActualParticularControl.groupedEnvelope.

Equations

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

theorem NavierStokes.ActualParticularStageControls.selectedWeight_nonneg {B N0 : ℕ} (e : ℕ → ActivePair B N0) (u : Unit) (n : ℕ) (z : Native) : 0 ≤ selectedWeight e u n z

theorem NavierStokes.ActualParticularStageControls.selectedWeight_eq {B N0 : ℕ} (e : ℕ → ActivePair B N0) (u : Unit) (n : ℕ) (k : TorusInverse.Frequency) {z : Native} (hz : z ∈ selectedPatch e u n k) : selectedWeight e u n z = selectedPulseEnvelope e u n ((selectedGeometry e u n).coordinates k z.2).2

theorem NavierStokes.ActualParticularStageControls.selected_raw_jets {B N0 : ℕ} (e : ℕ → ActivePair B N0) (x : CorrectionStep.CycleState (Label B N0)) (hfrequency : ∀ (l : Label B N0) (n : ℕ), (x.coefficients.blocks l).frequency n = ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n)) {α : ℝ} (j : ℤ) (hj : j ≠ 0) (H : LabelSumBounds.UniformWaveClass (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip slowStrip)) nativeEnvelope α (currentSource x j)) : (PeriodizedWaveBounds.UniformLocalJets (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip (selectedStrip e))) (fun (u : Unit) (n : ℕ) (z : (Parameter × ℝ) × TorusInverse.Plane) => √((CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip (selectedStrip e))).zeta z) * selectedWeight e u n z) α (selectedPatch e) fun (u : Unit) (n : ℕ) (k : TorusInverse.Frequency) => (ParticularWaveBounds.complexCopyCoefficients (selectedBackground e x j u) (selectedTangent e x j u) (selectedSource e x j u) (selectedGeometry e u) (fun (x : ℕ) => k) (selectedLength e u) ⋯).amplitude n) ∧ PeriodizedWaveBounds.UniformLocalJets (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip (selectedStrip e))) (fun (u : Unit) (n : ℕ) (z : (Parameter × ℝ) × TorusInverse.Plane) => √((CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip (selectedStrip e))).zeta z) * selectedWeight e u n z) (α + 1 / 2) (selectedPatch e) fun (u : Unit) (n : ℕ) (k : TorusInverse.Frequency) => (ParticularWaveBounds.complexCopyCoefficients (selectedBackground e x j u) (selectedTangent e x j u) (selectedSource e x j u) (selectedGeometry e u) (fun (x : ℕ) => k) (selectedLength e u) ⋯).pressure n

theorem NavierStokes.ActualParticularStageControls.raw_jets {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (hfrequency : ∀ (l : Label B N0) (n : ℕ), (x.coefficients.blocks l).frequency n = ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n)) {α : ℝ} (j : ℤ) (hj : j ≠ 0) (H : LabelSumBounds.UniformWaveClass (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip slowStrip)) nativeEnvelope α (currentSource x j)) : (PeriodizedWaveBounds.UniformLocalJets (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip slowStrip)) (fun (l : Label B N0) (n : ℕ) (z : (Parameter × ℝ) × TorusInverse.Plane) => √((CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip slowStrip)).zeta z) * nativeEnvelope l n z) α controlPatch fun (l : Label B N0) => (data x l j).amplitude) ∧ PeriodizedWaveBounds.UniformLocalJets (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip slowStrip)) (fun (l : Label B N0) (n : ℕ) (z : (Parameter × ℝ) × TorusInverse.Plane) => √((CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip slowStrip)).zeta z) * nativeEnvelope l n z) (α + 1 / 2) controlPatch fun (l : Label B N0) => (data x l j).pressure

The selector is only an indexing device. Both actual raw fields have one bound before the original spatial label, active band, and lattice copy.

The support geometry is the same canonical scalar-clock geometry.

noncomputable def NavierStokes.ActualParticularStageControls.supportLabel {B N0 : ℕ} (l : Label B N0) : ActualCarrierTransportBase.Index B N0

Support label, given by (l.2,l.1).

Equations

• NavierStokes.ActualParticularStageControls.supportLabel l = (l.2, l.1)

theorem NavierStokes.ActualParticularStageControls.support_geometry_eq {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (n : ℕ) : ActualCarrierTransportBase.geometry (supportLabel l) n = (parameters x l).geometry n

theorem NavierStokes.ActualParticularStageControls.support_length_eq {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (n : ℕ) : ActualCarrierTransportBase.referenceLength (supportLabel l) / ActualCarrierTransportBase.clock (supportLabel l) n = (parameters x l).length n

theorem NavierStokes.ActualParticularStageControls.support_cutoff_eq {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (n : ℕ) : ActualCarrierTransportBase.cutoff (supportLabel l) n = (parameters x l).cutoff n

theorem NavierStokes.ActualParticularStageControls.copyData_ext {D I : Type} {a b : PeriodizedWaveBounds.CopyData D I} (hb : a.background = b.background) (ha : a.amplitude = b.amplitude) (hp : a.pressure = b.pressure) (hc : a.cutoff = b.cutoff) (hs : a.source = b.source) : a = b

theorem NavierStokes.ActualParticularStageControls.data_scalar_eq {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (j : ℤ) : data x l j = ScalarParticularSupport.scalarData (data x l j).background ((parameters x l).nativeTangent j) (currentSource x j l) (ActualCarrierTransportBase.geometry (supportLabel l)) (fun (x : ℕ) => CorrectionInitialization.ActualPrimary.slots.radius) (fun (x : ℕ) => ActualCarrierTransportBase.referenceLength (supportLabel l)) (ActualCarrierTransportBase.clock (supportLabel l)) ⋯ ⋯ ⋯

noncomputable def NavierStokes.ActualParticularStageControls.carrierCells {B N0 : ℕ} (l : Label B N0) : PeriodizedWaveBounds.Cells Native TorusInverse.Frequency

Carrier cells, constructed using ScalarParticularSupport.scalarCells.

Equations

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

theorem NavierStokes.ActualParticularStageControls.data_cutoff_support {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (j : ℤ) (n : ℕ) (k : TorusInverse.Frequency) : Function.support ((data x l j).cutoff n k) ⊆ (carrierCells l).carrier n k

@[reducible, inline]

abbrev NavierStokes.ActualParticularStageControls.InputSupport {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) : Prop

Input support type used in actual particular stage controls.

Equations

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

theorem NavierStokes.ActualParticularStageControls.currentSource_pull {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (j : ℤ) (n : ℕ) : currentSource x j l n = fun (z : Native) => ParticularWaveAssembly.residualSource (CorrectionInitialization.ActualPrimary.commonContext B) x.state (x.coefficients.blocks l) (x.coefficients.gaussian l) (x.coefficients.aliasCoefficients l) j n (nativeToFull z).1

theorem NavierStokes.ActualParticularStageControls.currentSource_zero_germ {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (hs : InputSupport x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (l : Label B N0) (j : ℤ) (n : ℕ) {z : Native} (hz : z.1.1 ∈ ActualCarrierTransportBase.parameterDomain) (hout : (z.1.1, z.2) ∉ ActualCarrierTransportBase.canonicalSourceRegion (supportLabel l) n) : currentSource x j l n =ᶠ[nhds z] fun (x : Native) => 0

Actual incoming coefficient support supplies the source's zero germ on the full slow domain; no zero-germ conclusion about the solved field is assumed.

Actual source-carrier coverage of the analytic patch.

theorem NavierStokes.ActualParticularStageControls.native_parameter_domain {z : Native} (hz : z ∈ (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip slowStrip)).domain) : z.1.1 ∈ ActualCarrierTransportBase.parameterDomain

theorem NavierStokes.ActualParticularStageControls.sourceRegion_mem_controlPatch {B N0 : ℕ} (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (l : Label B N0) (n : ℕ) (k : TorusInverse.Frequency) {z : Native} (hz : z ∈ (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip slowStrip)).domain) (hk : z ∈ (carrierCells l).carrier n k) (hs : (z.1.1, z.2) ∈ ActualCarrierTransportBase.canonicalSourceRegion (supportLabel l) n) : z ∈ controlPatch l n k

theorem NavierStokes.ActualParticularStageControls.data_control_alternative {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (hs : InputSupport x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (l : Label B N0) (j : ℤ) (n : ℕ) (k : TorusInverse.Frequency) {z : Native} (hz : z ∈ (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip slowStrip)).domain) (hk : z ∈ (carrierCells l).carrier n k) : z ∈ controlPatch l n k ∨ ((data x l j).cutoff n k =ᶠ[nhds z] fun (x : Native) => 0) ∨ ((data x l j).amplitude n k =ᶠ[nhds z] fun (x : Native) => 0) ∧ ((data x l j).pressure n k =ᶠ[nhds z] fun (x : Native) => 0) ∧ (data x l j).source n =ᶠ[nhds z] fun (x : Native) => 0

Every native cell is either controlled, killed by the actual cutoff, or has both a zero raw solve and a zero current forcing germ.

theorem NavierStokes.ActualParticularStageControls.data_control_cover {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (hs : InputSupport x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (l : Label B N0) (j : ℤ) (n : ℕ) (k : TorusInverse.Frequency) {z : Native} (hz : z ∈ (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip slowStrip)).domain) (hk : z ∈ (carrierCells l).carrier n k) : z ∈ controlPatch l n k ∨ (((data x l j).localized k).amplitude n =ᶠ[nhds z] fun (x : Native) => 0) ∧ ((data x l j).localized k).pressure n =ᶠ[nhds z] fun (x : Native) => 0

The literal transported window/Gaussian product has uniform jets.

theorem NavierStokes.ActualParticularStageControls.selected_u {B N0 : ℕ} (e : ℕ → ActivePair B N0) (u : Unit) (n : ℕ) : (selectedConstruction e).u (u, n) = (CorrectionInitialization.ActualPrimary.choice B N0).prepared.u

theorem NavierStokes.ActualParticularStageControls.selected_cutoff_eq {B N0 : ℕ} (e : ℕ → ActivePair B N0) (x : CorrectionStep.CycleState (Label B N0)) (j : ℤ) (u : Unit) (n : ℕ) (k : TorusInverse.Frequency) : (data x (selectedLabel e n) j).cutoff (selectedBand e n) k = NativeCutoffJets.literalCutoff (selectedConstruction e) (selectedClock e) (selectedGeometry e) (fun (x : Unit) (x_1 : ℕ) => CorrectionInitialization.ActualPrimary.slots.radius) ⋯ u n k

theorem NavierStokes.ActualParticularStageControls.selected_cutoff_jets {B N0 : ℕ} (e : ℕ → ActivePair B N0) (x : CorrectionStep.CycleState (Label B N0)) (j : ℤ) : PeriodizedWaveBounds.UniformLocalJets (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip (selectedStrip e))) (fun (x : Unit) (x_1 : ℕ) (x_2 : (Parameter × ℝ) × TorusInverse.Plane) => 1) 0 (selectedPatch e) fun (x_1 : Unit) (n : ℕ) (k : TorusInverse.Frequency) => (data x (selectedLabel e n) j).cutoff (selectedBand e n) k

theorem NavierStokes.ActualParticularStageControls.cutoff_jets {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (j : ℤ) : PeriodizedWaveBounds.UniformLocalJets (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip slowStrip)) (fun (x : Label B N0) (x_1 : ℕ) (x_2 : (Parameter × ℝ) × TorusInverse.Plane) => 1) 0 controlPatch fun (l : Label B N0) => (data x l j).cutoff

Derived local background bounds and actual common-field estimates.

theorem NavierStokes.ActualParticularStageControls.canonical_geometry_eq {B N0 : ℕ} (l : Label B N0) (n : ℕ) : (canonicalParameters l).geometry n = ActualCarrierTransportBase.geometry (supportLabel l) n

theorem NavierStokes.ActualParticularStageControls.control_clock {B N0 : ℕ} (l : Label B N0) (n : ℕ) (k : TorusInverse.Frequency) (Y : Plane) : CopySolveCompatibility.nativeTimeMap 0 (ActualCarrierTransportBase.clock (supportLabel l) n) (((canonicalParameters l).geometry n).coordinates k Y) = (CorrectionInitialization.ActualPrimary.chartGeometry n l.1 l.2).coordinates k Y

theorem NavierStokes.ActualParticularStageControls.controlPatch_subset_padded {B N0 : ℕ} (l : Label B N0) (n : ℕ) (k : TorusInverse.Frequency) : controlPatch l n k ⊆ ParticularPaddedBackground.cells n (l, k)

theorem NavierStokes.ActualParticularStageControls.local_restrict {D I E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {C K : ℕ → I → Set D} {w : ℕ → I → D → ℝ} {α : ℝ} {f : ℕ → I → D → E} (hf : LocalizedWaveBounds.LocalClass s C w α f) (hsub : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K n i → x ∈ C n i) : LocalizedWaveBounds.LocalClass s K w α f

theorem NavierStokes.ActualParticularStageControls.inputs_restrict {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {C K : ℕ → I → Set D} {W : ℕ → I → D → ℝ} {α κ : ℝ} {d : LinearWaveBounds.GraphDirections D} {a : LocalizedWaveBounds.WaveFamily D I} (hf : LocalizedWaveBounds.InputBounds s C W α κ d a) (hsub : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K n i → x ∈ C n i) : LocalizedWaveBounds.InputBounds s K W α κ d a

@[reducible, inline]

abbrev NavierStokes.ActualParticularStageControls.PreservesCarriers {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) : Prop

Preserves carriers: an abbreviation for ∀ l, SameCarrier (x.coefficients.blocks l) (ActualParticularBackground.primaryBlock l).

Equations

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

theorem NavierStokes.ActualParticularStageControls.preserves_frequency {B N0 : ℕ} {x : CorrectionStep.CycleState (Label B N0)} (hx : PreservesCarriers x) (l : Label B N0) (n : ℕ) : (x.coefficients.blocks l).frequency n = ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n)

theorem NavierStokes.ActualParticularStageControls.data_background_eq {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (j : ℤ) : (data x l j).background = ActualParticularBackground.carrier (fun (l : ActualParticularBackground.Label B N0) => x.coefficients.blocks l) j l

theorem NavierStokes.ActualParticularStageControls.native_background_eq {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (j : ℤ) : (CorrectionStep.jointRawBackground fun (l : Label B N0) => data x l j) = ActualParticularBackground.backgroundFamily (fun (l : ActualParticularBackground.Label B N0) => x.coefficients.blocks l) j

theorem NavierStokes.ActualParticularStageControls.actual_background_inputs {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (hx : PreservesCarriers x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (j : ℤ) : LocalizedWaveBounds.InputBounds (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip slowStrip)) (fun (n : ℕ) (i : Label B N0 × TorusInverse.Frequency) => controlPatch i.1 n i.2) (fun (n : ℕ) (i : Label B N0 × TorusInverse.Frequency) (z : (Parameter × ℝ) × TorusInverse.Plane) => nativeEnvelope i.1 n z) 0 ChartScales.kappa directions (CorrectionStep.jointRawBackground fun (l : Label B N0) => data x l j)

theorem NavierStokes.ActualParticularStageControls.actual_normal_range {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (hx : PreservesCarriers x) (l : Label B N0) (j : ℤ) (n : ℕ) (k : TorusInverse.Frequency) {z : Native} (hz : z ∈ (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip slowStrip)).domain) (hk : z ∈ controlPatch l n k) : ActualPrimaryBounds.normalFloor B N0 ≤ ‖(data x l j).background.normal (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip slowStrip)) directions n z‖ ∧ ‖(data x l j).background.normal (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip slowStrip)) directions n z‖ ≤ ActualPrimaryBounds.normalCeiling B N0

theorem NavierStokes.ActualParticularStageControls.actual_inverse_frequency {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (hx : PreservesCarriers x) (j : ℤ) : LocalizedWaveBounds.LocalUnweighted (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip slowStrip)) (fun (n : ℕ) (i : Label B N0 × TorusInverse.Frequency) => controlPatch i.1 n i.2) (1 / 2) fun (n : ℕ) (i : Label B N0 × TorusInverse.Frequency) (x_1 : Native) => 1 / (data x i.1 j).background.frequency n

theorem NavierStokes.ActualParticularStageControls.common_bounds {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (hx : PreservesCarriers x) (hs : InputSupport x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) {α : ℝ} (j : ℤ) (hj : j ≠ 0) (H : LabelSumBounds.UniformWaveClass (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip slowStrip)) nativeEnvelope α (currentSource x j)) : have s := CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip slowStrip); (LabelSumBounds.UniformWaveClass s nativeEnvelope α fun (l : Label B N0) => (data x l j).common.amplitude) ∧ (LabelSumBounds.UniformWaveClass s nativeEnvelope α fun (l : Label B N0) => ((data x l j).commonCorrected s directions).amplitude) ∧ (LabelSumBounds.UniformWaveClass s nativeEnvelope (α + 1 / 2) fun (l : Label B N0) => (data x l j).common.pressure) ∧ (LabelSumBounds.UniformWaveClass s nativeEnvelope (α + 1 / 2 - ChartScales.kappa) fun (l : Label B N0) => (data x l j).common.curlCorrection s directions) ∧ LabelSumBounds.UniformWaveClass s nativeEnvelope (α + 1 / 2 - 3 * ChartScales.kappa) fun (l : Label B N0) => (data x l j).globalGood s directions

The exact moving weight, finite harmonic assembly, and invariant interface.

theorem NavierStokes.ActualParticularStageControls.meanEnvelope_eq_primary {B N0 : ℕ} (l : Label B N0) (n : ℕ) (z : CorrectionStep.CyclePoint) : meanEnvelope l n z = ActualPrimaryBounds.meanEnvelope l n z

theorem NavierStokes.ActualParticularStageControls.nativeEnvelope_le_one {B N0 : ℕ} (l : Label B N0) (n : ℕ) (z : Native) : nativeEnvelope l n z ≤ 1

theorem NavierStokes.ActualParticularStageControls.native_wave_to_weighted {B N0 : ℕ} {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {α : ℝ} {f : Label B N0 → ℕ → Native → E} (hf : LabelSumBounds.UniformWaveClass (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip slowStrip)) nativeEnvelope α f) : LabelSumBounds.UniformClass (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip slowStrip)) (fun (x : Label B N0) (x_1 : ℕ) (z : (Parameter × ℝ) × TorusInverse.Plane) => √((CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip slowStrip)).zeta z)) α f

@[reducible, inline]

abbrev NavierStokes.ActualParticularStageControls.ResidualBounds {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (α : ℝ) : Prop

Residual bounds type used in actual particular stage controls.

Equations

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

noncomputable def NavierStokes.ActualParticularStageControls.associatedUpdate {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (N : ℕ) (l : Label B N0) : CorrectionState.HarmonicBlock (Parameter × Plane)

Associated update as an element of HarmonicBlock (Parameter × Plane).

Equations

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

noncomputable def NavierStokes.ActualParticularStageControls.associatedGood {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (N : ℕ) (l : Label B N0) : CorrectionState.HarmonicBlock (Parameter × Plane)

Associated good as an element of HarmonicBlock (Parameter × Plane).

Equations

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

theorem NavierStokes.ActualParticularStageControls.associated_assembled_bounds {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (hx : PreservesCarriers x) (hs : InputSupport x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) {α : ℝ} (H : ResidualBounds x α) (N : ℕ) : (∀ (i : Fin 3) (j : ℤ), LabelSumBounds.UniformWaveClass associatedStrip envelope α fun (l : Label B N0) (n : ℕ) (z : Parameter × Plane) => ((associatedUpdate x N l).velocity n i).coeff j z) ∧ (∀ (j : ℤ), LabelSumBounds.UniformWaveClass associatedStrip envelope (α + 1 / 2) fun (l : Label B N0) (n : ℕ) (z : Parameter × Plane) => ((associatedUpdate x N l).pressure n).coeff j z) ∧ ∀ (i : Fin 3) (j : ℤ), LabelSumBounds.UniformWaveClass associatedStrip envelope (α + 1 / 2 - 3 * ChartScales.kappa) fun (l : Label B N0) (n : ℕ) (z : Parameter × Plane) => ((associatedGood x N l).velocity n i).coeff j z

noncomputable def NavierStokes.ActualParticularStageControls.outputBlock {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (N : ℕ) (l : Label B N0) : CorrectionState.HarmonicBlock CorrectionStep.CyclePoint

Output block, given by StateReindex.block cycleAssoc (associatedUpdate x N l).

Equations

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

noncomputable def NavierStokes.ActualParticularStageControls.outputGood {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (N : ℕ) (l : Label B N0) : CorrectionState.HarmonicBlock CorrectionStep.CyclePoint

Output good, given by StateReindex.block cycleAssoc (associatedGood x N l).

Equations

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

theorem NavierStokes.ActualParticularStageControls.associated_wave_return {B N0 : ℕ} {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {α : ℝ} {f : Label B N0 → ℕ → Parameter × Plane → E} (hf : LabelSumBounds.UniformWaveClass associatedStrip envelope α f) : LabelSumBounds.UniformWaveClass (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion) meanEnvelope α fun (l : Label B N0) (n : ℕ) (z : BaseContextAssembly.Point) => f l n (CorrectionStep.cycleAssoc z)

theorem NavierStokes.ActualParticularStageControls.assembled_bounds {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (hx : PreservesCarriers x) (hs : InputSupport x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) {α : ℝ} (H : ResidualBounds x α) (N : ℕ) : (∀ (i : Fin 3) (j : ℤ), LabelSumBounds.UniformWaveClass (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion) meanEnvelope α fun (l : Label B N0) (n : ℕ) (z : BaseContextAssembly.Point) => ((outputBlock x N l).velocity n i).coeff j z) ∧ (∀ (j : ℤ), LabelSumBounds.UniformWaveClass (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion) meanEnvelope (α + 1 / 2) fun (l : Label B N0) (n : ℕ) (z : BaseContextAssembly.Point) => ((outputBlock x N l).pressure n).coeff j z) ∧ ∀ (i : Fin 3) (j : ℤ), LabelSumBounds.UniformWaveClass (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion) meanEnvelope (α + 1 / 2 - 3 * ChartScales.kappa) fun (l : Label B N0) (n : ℕ) (z : BaseContextAssembly.Point) => ((outputGood x N l).velocity n i).coeff j z

The finite harmonic assembly and coordinate association retain constants chosen before the spatial label and band.

theorem NavierStokes.ActualParticularStageControls.invariant_assembled_bounds {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) {G : SignedMeanGain.Geometry} {σ : ℝ} (H : CorrectionStep.CycleAnalyticInvariant G (CorrectionInitialization.ActualPrimary.commonContext B) ActualParticularBackground.primaryBlock meanEnvelope (fun (l : ActualParticularBackground.Label B N0) => ActualCarrierTransportBase.labelCarrier (supportLabel l)) σ x) (hstrip : G.strip = BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion) (hdomain : G.domain = ActualCarrierTransportBase.domain) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) : (∀ (i : Fin 3) (j : ℤ), LabelSumBounds.UniformWaveClass G.strip meanEnvelope (1 / 2 + σ) fun (l : Label B N0) (n : ℕ) (z : SignedMeanGain.Point) => ((outputBlock x x.coefficients.residualBand l).velocity n i).coeff j z) ∧ (∀ (j : ℤ), LabelSumBounds.UniformWaveClass G.strip meanEnvelope (1 + σ) fun (l : Label B N0) (n : ℕ) (z : SignedMeanGain.Point) => ((outputBlock x x.coefficients.residualBand l).pressure n).coeff j z) ∧ ∀ (i : Fin 3) (j : ℤ), LabelSumBounds.UniformWaveClass G.strip meanEnvelope (1 + σ - 3 * ChartScales.kappa) fun (l : Label B N0) (n : ℕ) (z : SignedMeanGain.Point) => ((outputGood x x.coefficients.residualBand l).velocity n i).coeff j z

The quantitative inputs are precisely fields of the current analytic invariant. The geometric equalities identify its actual strip and carrier.