Quantitative bounds for actual current-band particular fields

The estimates use the actual current coefficient and phase on their open validity domains. No reference-field smoothness or auxiliary copy-family representation is assumed.

Uniform phase jets for the actual current-chart copies

The functions below are literal reindexings of the selected common phase. Positive jets have a fixed Q^(-2h) loss, uniformly before the label and band are selected. No bound on the unbounded phase value is asserted.

@[reducible, inline]

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

Label: an abbreviation for ActualPrimaryBounds.SignedLabel B N0.

Equations

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

@[reducible, inline]

abbrev NavierStokes.ActualCurrentCarrierJets.Native : Type

Native: an abbreviation for ActualParticularBackground.Native.

Equations

• NavierStokes.ActualCurrentCarrierJets.Native = NavierStokes.ActualParticularBackground.Native

@[reducible, inline]

abbrev NavierStokes.ActualCurrentCarrierJets.FullPoint : Type

Full point: an abbreviation for ActualPrimary.FullPoint.

Equations

• NavierStokes.ActualCurrentCarrierJets.FullPoint = NavierStokes.CorrectionInitialization.ActualPrimary.FullPoint

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

The actual common phase in the current free-angle native coordinates.

Equations

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

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

The same phase with the actual base carrier already included.

Equations

• NavierStokes.ActualCurrentCarrierJets.weightedPhase l n z = NavierStokes.ActualPhaseJetBounds.weightedPhase l n (NavierStokes.ActualParticularBackground.nativeToFull z)

theorem NavierStokes.ActualCurrentCarrierJets.weightedPhase_eq {B N0 : ℕ} (l : Label B N0) (n : ℕ) : weightedPhase l n = fun (z : Native) => ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n) * phase l n z

theorem NavierStokes.ActualCurrentCarrierJets.harmonic_carrier_eq {B N0 : ℕ} (l : Label B N0) (n : ℕ) (j : ℤ) : HarmonicCalculus.carrier (↑j * ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n)) (phase l n) = PhysicalGraphBounds.character ↑j ∘ weightedPhase l n

The oscillatory factor used by the actual harmonic copy is exactly the character of the carrier-weighted current phase.

theorem NavierStokes.ActualCurrentCarrierJets.actualCarrier_phase {B N0 : ℕ} (b : Label B N0 → CorrectionState.HarmonicBlock CorrectionStep.CyclePoint) (hb : ∀ (l : Label B N0), CorrectionStep.SameCarrier (b l) (ActualParticularBackground.primaryBlock l)) (j : ℤ) (l : Label B N0) (n : ℕ) : (ActualParticularBackground.carrier b j l).phase n = phase l n

theorem NavierStokes.ActualCurrentCarrierJets.actualCarrier_character {B N0 : ℕ} (b : Label B N0 → CorrectionState.HarmonicBlock CorrectionStep.CyclePoint) (hb : ∀ (l : Label B N0), CorrectionStep.SameCarrier (b l) (ActualParticularBackground.primaryBlock l)) (j : ℤ) (l : Label B N0) (n : ℕ) : HarmonicCalculus.carrier ((ActualParticularBackground.carrier b j l).frequency n) ((ActualParticularBackground.carrier b j l).phase n) = PhysicalGraphBounds.character ↑j ∘ weightedPhase l n

theorem NavierStokes.ActualCurrentCarrierJets.paddedCell_eq_phaseCell {B N0 : ℕ} (n : ℕ) (i : ActualPhaseJetBounds.CopyIndex B N0) : ParticularPaddedBackground.paddedCell n i = ActualPhaseJetBounds.phaseCell n i

theorem NavierStokes.ActualCurrentCarrierJets.mem_cells_iff {B N0 : ℕ} (n : ℕ) (i : ActualPhaseJetBounds.CopyIndex B N0) (z : Native) : z ∈ ParticularPaddedBackground.cells n i ↔ ActualParticularBackground.nativeToFull z ∈ ActualPhaseJetBounds.phaseCell n i

theorem NavierStokes.ActualCurrentCarrierJets.full_weightedPhase_smoothNear {B N0 n : ℕ} {i : ActualPhaseJetBounds.CopyIndex B N0} {x : FullPoint} (hx : x ∈ ActualPhaseJetBounds.phaseCell n i) : LocalPhysicalCopyBounds.SmoothNear (ActualPhaseJetBounds.weightedPhase i.1 n) x

The one open neighborhood is obtained from the actual analytic phase cell, then intersected with the genuine periodic-copy germ neighborhood.

theorem NavierStokes.ActualCurrentCarrierJets.weightedPhase_smoothNear {B N0 n : ℕ} {i : ActualPhaseJetBounds.CopyIndex B N0} {z : Native} (hz : z ∈ ParticularPaddedBackground.cells n i) : LocalPhysicalCopyBounds.SmoothNear (weightedPhase i.1 n) z

theorem NavierStokes.ActualCurrentCarrierJets.phase_smoothNear {B N0 n : ℕ} {i : ActualPhaseJetBounds.CopyIndex B N0} {z : Native} (hz : z ∈ ParticularPaddedBackground.cells n i) : LocalPhysicalCopyBounds.SmoothNear (phase i.1 n) z

theorem NavierStokes.ActualCurrentCarrierJets.weightedPhase_positive_jets {B N0 : ℕ} (m : ℕ) : ∃ (C : ℝ), 1 ≤ C ∧ ∃ (p : ℕ), ∀ (n : ℕ) (i : ActualPhaseJetBounds.CopyIndex B N0), ∀ z ∈ ParticularPaddedBackground.cells n i, ∀ (r : ℕ), 1 ≤ r → r ≤ m → ‖iteratedFDeriv ℝ r (weightedPhase i.1 n) z‖ ≤ C * ChartScales.S n ^ p * ChartScales.Q n ^ (-(2 * CorrectionInitialization.ActualPrimary.h))

Constants are chosen before the active label, band, copy, point, and positive derivative order. Reindexing is an isometry and adds no loss.

theorem NavierStokes.ActualCurrentCarrierJets.phase_positive_jets {B N0 : ℕ} (m : ℕ) : ∃ (C : ℝ), 1 ≤ C ∧ ∃ (p : ℕ), ∀ (n : ℕ) (i : ActualPhaseJetBounds.CopyIndex B N0), ∀ z ∈ ParticularPaddedBackground.cells n i, ∀ (r : ℕ), 1 ≤ r → r ≤ m → ‖iteratedFDeriv ℝ r (phase i.1 n) z‖ ≤ C * ChartScales.S n ^ p * ChartScales.Q n ^ (-(2 * CorrectionInitialization.ActualPrimary.h))

theorem NavierStokes.ActualCurrentCarrierJets.weightedPhase_positive_jets_epsilon {B N0 : ℕ} (m : ℕ) : ∃ (C : ℝ), 1 ≤ C ∧ ∃ (p : ℕ), ∀ (n : ℕ) (i : ActualPhaseJetBounds.CopyIndex B N0), ∀ z ∈ ParticularPaddedBackground.cells n i, ∀ (r : ℕ), 1 ≤ r → r ≤ m → ‖iteratedFDeriv ℝ r (weightedPhase i.1 n) z‖ ≤ C * ChartScales.S n ^ p * (ChartScales.epsilon CorrectionInitialization.ActualPrimary.h n)⁻¹ ^ 2

The displayed physical loss is exactly two inverse powers of epsilon.

theorem NavierStokes.ActualCurrentCarrierJets.weightedPhase_smoothNear_controlPatch {B N0 : ℕ} (l : Label B N0) (n : ℕ) (k : TorusInverse.Frequency) {z : Native} (hz : z ∈ ActualParticularStageControls.controlPatch l n k) : LocalPhysicalCopyBounds.SmoothNear (weightedPhase l n) z

theorem NavierStokes.ActualCurrentCarrierJets.phase_smoothNear_controlPatch {B N0 : ℕ} (l : Label B N0) (n : ℕ) (k : TorusInverse.Frequency) {z : Native} (hz : z ∈ ActualParticularStageControls.controlPatch l n k) : LocalPhysicalCopyBounds.SmoothNear (phase l n) z

theorem NavierStokes.ActualCurrentCarrierJets.weightedPhase_positive_jets_controlPatch {B N0 : ℕ} (m : ℕ) : ∃ (C : ℝ), 1 ≤ C ∧ ∃ (p : ℕ), ∀ (l : Label B N0) (n : ℕ) (k : TorusInverse.Frequency), ∀ z ∈ ActualParticularStageControls.controlPatch l n k, ∀ (r : ℕ), 1 ≤ r → r ≤ m → ‖iteratedFDeriv ℝ r (weightedPhase l n) z‖ ≤ C * ChartScales.S n ^ p * ChartScales.Q n ^ (-(2 * CorrectionInitialization.ActualPrimary.h))

The quantitative statement on the actual retained current-copy cells. The cell hypothesis already supplies activeness; no native-band interior or separate phase-jet assumption is added.

theorem NavierStokes.ActualCurrentCarrierJets.phase_positive_jets_controlPatch {B N0 : ℕ} (m : ℕ) : ∃ (C : ℝ), 1 ≤ C ∧ ∃ (p : ℕ), ∀ (l : Label B N0) (n : ℕ) (k : TorusInverse.Frequency), ∀ z ∈ ActualParticularStageControls.controlPatch l n k, ∀ (r : ℕ), 1 ≤ r → r ≤ m → ‖iteratedFDeriv ℝ r (phase l n) z‖ ≤ C * ChartScales.S n ^ p * ChartScales.Q n ^ (-(2 * CorrectionInitialization.ActualPrimary.h))

The literal native potential coefficient

theorem NavierStokes.ActualCurrentParticularBounds.potential_local_class {E : Type u_1} {I : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData E} {cells : ℕ → I → Set E} {envelope : ℕ → I → E → ℝ} {α κ : ℝ} {d : LinearWaveBounds.GraphDirections E} {a : LocalizedWaveBounds.WaveFamily E I} (hin : LocalizedWaveBounds.InputBounds s cells envelope α κ d a) {b M : ℝ} (hb : 0 < b) (hlower : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ cells n i → b ≤ ‖a.normal s d n i x‖) (hupper : ∀ (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ cells n i → ‖a.normal s d n i x‖ ≤ M) (hfreq : LocalizedWaveBounds.LocalUnweighted s cells (1 / 2) fun (n : ℕ) (i : I) (x : E) => 1 / a.frequency n i) : LocalizedWaveBounds.LocalWave s cells envelope (α + 1 / 2) fun (n : ℕ) (i : I) (x : E) => CurlClassBounds.inverseCarrier (a.frequency n i) • CurlClassBounds.normalCoefficient (a.normal s d n i x) (a.amplitude n i x)

noncomputable def NavierStokes.ActualCurrentParticularBounds.strippedPotential {E I : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (a : PeriodizedWaveBounds.CopyData E I) (s : WeightedClasses.StripData E) (d : LinearWaveBounds.GraphDirections E) (n : ℕ) (x : E) : HarmonicCalculus.ComplexVector

Stripped potential, constructed using CurlClassBounds.inverseCarrier.

Equations

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

theorem NavierStokes.ActualCurrentParticularBounds.common_potential_class {E L I : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (a : L → PeriodizedWaveBounds.CopyData E I) (K : L → PeriodizedWaveBounds.Cells E I) (hs : ∀ (l : L) (n : ℕ) (i : I), Function.support ((a l).cutoff n i) ⊆ (K l).carrier n i) (C : L → ℕ → I → Set E) {s : WeightedClasses.StripData E} {d : LinearWaveBounds.GraphDirections E} {W : L → ℕ → E → ℝ} {α κ : ℝ} (hW : ∀ (l : L) (n : ℕ), ∀ x ∈ s.domain, 0 ≤ W l n x) (hin : LocalizedWaveBounds.InputBounds s (fun (n : ℕ) (i : L × I) => C i.1 n i.2) (fun (n : ℕ) (i : L × I) (x : E) => W i.1 n x) α κ d (LocalizedWaveBounds.jointNativeFamily a)) {b M : ℝ} (hb : 0 < b) (hlower : ∀ (l : L) (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ C l n i → b ≤ ‖(a l).background.normal s d n x‖) (hupper : ∀ (l : L) (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ C l n i → ‖(a l).background.normal s d n x‖ ≤ M) (hfreq : LocalizedWaveBounds.LocalUnweighted s (fun (n : ℕ) (i : L × I) => C i.1 n i.2) (1 / 2) fun (n : ℕ) (i : L × I) (x : E) => 1 / (a i.1).background.frequency n) (hcover : ∀ (l : L) (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ (K l).carrier n i → x ∈ C l n i ∨ ((a l).localized i).amplitude n =ᶠ[nhds x] fun (x : E) => 0) : LabelSumBounds.UniformWaveClass s W (α + 1 / 2) fun (l : L) => strippedPotential (a l) s d

The actual common potential coefficient inherits the inverse-carrier gain. The native normal estimates are used only on their control cells; the remaining portions are handled by actual amplitude zero germs.

The supplied source below is the actual current harmonic residual. The normal-inverse and periodization estimates are derived here.

@[reducible, inline]

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

Label: an abbreviation for ActualParticularStageControls.Label B N0.

Equations

• NavierStokes.ActualCurrentParticularBounds.Label B N0 = NavierStokes.ActualParticularStageControls.Label B N0

@[reducible, inline]

abbrev NavierStokes.ActualCurrentParticularBounds.Native : Type

Native: an abbreviation for ActualParticularStageControls.Native.

Equations

• NavierStokes.ActualCurrentParticularBounds.Native = NavierStokes.ActualParticularStageControls.Native

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

Native strip, given by CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip ActualParticularStageControls.slowStrip).

Equations

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

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

Potential coefficient, given by strippedPotential (ActualParticularStageControls.data x l j) nativeStrip (ActualParticularStageControls.directions (B := B)).

Equations

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

theorem NavierStokes.ActualCurrentParticularBounds.actual_potential_coefficient_class {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (hx : ActualParticularStageControls.PreservesCarriers x) (hs : ActualParticularStageControls.InputSupport x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) {α : ℝ} (j : ℤ) (hj : j ≠ 0) (H : LabelSumBounds.UniformWaveClass nativeStrip ActualParticularStageControls.nativeEnvelope α (ActualParticularStageControls.currentSource x j)) : LabelSumBounds.UniformWaveClass nativeStrip ActualParticularStageControls.nativeEnvelope (α + 1 / 2) fun (l : ActualParticularStageControls.Label B N0) => potentialCoefficient x l j

theorem NavierStokes.ActualCurrentParticularBounds.actual_pressure_coefficient_class {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (hx : ActualParticularStageControls.PreservesCarriers x) (hs : ActualParticularStageControls.InputSupport x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) {α : ℝ} (j : ℤ) (hj : j ≠ 0) (H : LabelSumBounds.UniformWaveClass nativeStrip ActualParticularStageControls.nativeEnvelope α (ActualParticularStageControls.currentSource x j)) : LabelSumBounds.UniformWaveClass nativeStrip ActualParticularStageControls.nativeEnvelope (α + 1 / 2) fun (l : ActualParticularStageControls.Label B N0) => (ActualParticularStageControls.data x l j).common.pressure

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

theorem NavierStokes.ActualCurrentParticularBounds.native_flat_geometry : ∃ (cL : ℝ) (cR : ℝ) (L : ℝ) (ρ : Native → ℝ), PhysicalClassBounds.FlatGeometry nativeStrip cL cR L ρ

theorem NavierStokes.ActualCurrentParticularBounds.native_source_bounds {B N0 : ℕ} {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {α : ℝ} {f : Label B N0 → ℕ → Native → E} (hf : LabelSumBounds.UniformWaveClass nativeStrip ActualParticularStageControls.nativeEnvelope α f) : LocalPhysicalCopyBounds.LocalSourceBounds nativeStrip CorrectionInitialization.ActualPrimary.h α (fun (l : ActualParticularStageControls.Label B N0) (n : ℕ) (z : Native) => √(nativeStrip.zeta z) * ActualParticularStageControls.nativeEnvelope l n z) f

The actual moving flat weight removes every inverse-edge power before passing to the physical graph.

theorem NavierStokes.ActualCurrentParticularBounds.common_control_or_zero {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (hs : ActualParticularStageControls.InputSupport x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (l : Label B N0) (j : ℤ) (n : ℕ) {z : Native} (hz : z ∈ nativeStrip.domain) : (∃ (k : TorusInverse.Frequency), z ∈ ActualParticularStageControls.controlPatch l n k) ∨ (potentialCoefficient x l j n =ᶠ[nhds z] fun (x : Native) => 0) ∧ (ActualParticularStageControls.data x l j).common.pressure n =ᶠ[nhds z] fun (x : Native) => 0

Local finite jets of the actual oscillatory exponential

theorem NavierStokes.ActualCurrentParticularBounds.character_comp_positive_jets {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Φ : E → ℝ} (hΦ : ContDiff ℝ (↑⊤) Φ) (x : E) (m : ℕ) {c B M : ℝ} (hB : 1 ≤ B) (hM : 1 ≤ M) (hc : |c| ≤ M) (hΦb : ∀ (i : ℕ), 1 ≤ i → i ≤ m → ‖iteratedFDeriv ℝ i Φ x‖ ≤ B) (k : ℕ) : k ≤ m → ‖iteratedFDeriv ℝ k (PhysicalGraphBounds.character c ∘ Φ) x‖ ≤ ↑m.factorial * M ^ m * B ^ m

theorem NavierStokes.ActualCurrentParticularBounds.mode_jet_bound_local {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {a : E → ℂ} {Φ : E → ℝ} {x : E} (ha : LocalPhysicalCopyBounds.SmoothNear a x) (hΦ : LocalPhysicalCopyBounds.SmoothNear Φ x) (m : ℕ) {c A B M : ℝ} (hA : 0 ≤ A) (hB : 1 ≤ B) (hM : 1 ≤ M) (hc : |c| ≤ M) (hab : ∀ i ≤ m, ‖iteratedFDeriv ℝ i a x‖ ≤ A) (hΦb : ∀ (i : ℕ), 1 ≤ i → i ≤ m → ‖iteratedFDeriv ℝ i Φ x‖ ≤ B) (k : ℕ) : k ≤ m → ‖iteratedFDeriv ℝ k (fun (y : E) => a y * PhysicalGraphBounds.character c (Φ y)) x‖ ≤ 2 ^ m * A * (↑m.factorial * M ^ m * B ^ m)

theorem NavierStokes.ActualCurrentParticularBounds.smul_mode_jet_bound_local {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedSpace ℂ V] [IsScalarTower ℝ ℂ V] {a : E → V} {Φ : E → ℝ} {x : E} (ha : LocalPhysicalCopyBounds.SmoothNear a x) (hΦ : LocalPhysicalCopyBounds.SmoothNear Φ x) (m : ℕ) {c A B M : ℝ} (hA : 0 ≤ A) (hB : 1 ≤ B) (hM : 1 ≤ M) (hc : |c| ≤ M) (hab : ∀ i ≤ m, ‖iteratedFDeriv ℝ i a x‖ ≤ A) (hΦb : ∀ (i : ℕ), 1 ≤ i → i ≤ m → ‖iteratedFDeriv ℝ i Φ x‖ ≤ B) (k : ℕ) : k ≤ m → ‖iteratedFDeriv ℝ k (fun (y : E) => PhysicalGraphBounds.character c (Φ y) • a y) x‖ ≤ 2 ^ m * A * (↑m.factorial * M ^ m * B ^ m)

theorem NavierStokes.ActualCurrentParticularBounds.smoothNear_mode {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a : E → ℂ} {Φ : E → ℝ} {x : E} (ha : LocalPhysicalCopyBounds.SmoothNear a x) (hΦ : LocalPhysicalCopyBounds.SmoothNear Φ x) (c : ℝ) : LocalPhysicalCopyBounds.SmoothNear (fun (y : E) => a y * PhysicalGraphBounds.character c (Φ y)) x

The current physical graph, with no copy-family premise

noncomputable def NavierStokes.ActualCurrentParticularBounds.currentLoss (degree ρ : ℝ) (m : ℕ) : ℝ

Current loss, given by degree + ρ * m + PhysicalGraphBounds.graphLoss m + 1.

Equations

• NavierStokes.ActualCurrentParticularBounds.currentLoss degree ρ m = degree + ρ * ↑m + NavierStokes.PhysicalGraphBounds.graphLoss m + 1

theorem NavierStokes.ActualCurrentParticularBounds.native_modulated_smoothNear {B N0 : ℕ} {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedSpace ℂ V] [IsScalarTower ℝ ℂ V] {α : ℝ} {f : Label B N0 → ℕ → Native → V} (hf : LabelSumBounds.UniformWaveClass nativeStrip ActualParticularStageControls.nativeEnvelope α f) (hzero : ∀ (l : ActualParticularStageControls.Label B N0) (n : ℕ), ∀ z ∈ nativeStrip.domain, (∃ (k : TorusInverse.Frequency), z ∈ ActualParticularStageControls.controlPatch l n k) ∨ f l n =ᶠ[nhds z] fun (x : Native) => 0) (j : ℤ) (l : Label B N0) (n : ℕ) {z : Native} (hz : z ∈ nativeStrip.domain) : LocalPhysicalCopyBounds.SmoothNear (fun (y : ActualCurrentCarrierJets.Native) => PhysicalGraphBounds.character (↑j) (ActualCurrentCarrierJets.weightedPhase l n y) • f l n y) z

theorem NavierStokes.ActualCurrentParticularBounds.native_modulated_bound {B N0 : ℕ} {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedSpace ℂ V] [IsScalarTower ℝ ℂ V] {α : ℝ} {f : Label B N0 → ℕ → Native → V} (hf : LabelSumBounds.UniformWaveClass nativeStrip ActualParticularStageControls.nativeEnvelope α f) (hzero : ∀ (l : ActualParticularStageControls.Label B N0) (n : ℕ), ∀ z ∈ nativeStrip.domain, (∃ (k : TorusInverse.Frequency), z ∈ ActualParticularStageControls.controlPatch l n k) ∨ f l n =ᶠ[nhds z] fun (x : Native) => 0) (j : ℤ) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∃ (p : ℕ), ∀ (l : ActualCurrentCarrierJets.Label B N0) (n : ℕ), 4 ≤ n → ∀ z ∈ nativeStrip.domain, ∀ i ≤ m, ‖iteratedFDeriv ℝ i (fun (y : ActualCurrentCarrierJets.Native) => PhysicalGraphBounds.character (↑j) (ActualCurrentCarrierJets.weightedPhase l n y) • f l n y) z‖ ≤ C * ChartScales.Q n ^ (CorrectionInitialization.ActualPrimary.h * α - 2 * CorrectionInitialization.ActualPrimary.h * ↑m) * ChartScales.S n ^ p

Uniform full native jets of the literal current oscillation. The actual periodic phase is used only where the native control cell applies; outside those cells the cut coefficient has a zero germ.

theorem NavierStokes.ActualCurrentParticularBounds.actual_nativePotential_eq_character {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (hx : ActualParticularStageControls.PreservesCarriers x) (l : Label B N0) (j : ℤ) (n : ℕ) : ActualCurrentParticularPhysical.nativePotential x l j n = fun (y : ActualCurrentCarrierJets.Native) => PhysicalGraphBounds.character (↑j) (ActualCurrentCarrierJets.weightedPhase l n y) • potentialCoefficient x l j n y

theorem NavierStokes.ActualCurrentParticularBounds.actual_nativePressure_eq_character {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (hx : ActualParticularStageControls.PreservesCarriers x) (l : Label B N0) (j : ℤ) (n : ℕ) : ActualCurrentParticularPhysical.nativePressure x l j n = fun (y : ActualCurrentCarrierJets.Native) => PhysicalGraphBounds.character (↑j) (ActualCurrentCarrierJets.weightedPhase l n y) • (ActualParticularStageControls.data x l j).common.pressure n y

theorem NavierStokes.ActualCurrentParticularBounds.actual_native_potential_bound {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (hx : ActualParticularStageControls.PreservesCarriers x) (hs : ActualParticularStageControls.InputSupport x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) {α : ℝ} (j : ℤ) (hj : j ≠ 0) (H : LabelSumBounds.UniformWaveClass nativeStrip ActualParticularStageControls.nativeEnvelope α (ActualParticularStageControls.currentSource x j)) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∃ (p : ℕ), ∀ (l : ActualCurrentParticularPhysical.Label B N0) (n : ℕ), 4 ≤ n → ∀ z ∈ nativeStrip.domain, ∀ i ≤ m, ‖iteratedFDeriv ℝ i (ActualCurrentParticularPhysical.nativePotential x l j n) z‖ ≤ C * ChartScales.Q n ^ (CorrectionInitialization.ActualPrimary.h * (α + 1 / 2) - 2 * CorrectionInitialization.ActualPrimary.h * ↑m) * ChartScales.S n ^ p

theorem NavierStokes.ActualCurrentParticularBounds.actual_native_pressure_bound {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (hx : ActualParticularStageControls.PreservesCarriers x) (hs : ActualParticularStageControls.InputSupport x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) {α : ℝ} (j : ℤ) (hj : j ≠ 0) (H : LabelSumBounds.UniformWaveClass nativeStrip ActualParticularStageControls.nativeEnvelope α (ActualParticularStageControls.currentSource x j)) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∃ (p : ℕ), ∀ (l : ActualCurrentParticularPhysical.Label B N0) (n : ℕ), 4 ≤ n → ∀ z ∈ nativeStrip.domain, ∀ i ≤ m, ‖iteratedFDeriv ℝ i (ActualCurrentParticularPhysical.nativePressure x l j n) z‖ ≤ C * ChartScales.Q n ^ (CorrectionInitialization.ActualPrimary.h * (α + 1 / 2) - 2 * CorrectionInitialization.ActualPrimary.h * ↑m) * ChartScales.S n ^ p

theorem NavierStokes.ActualCurrentParticularBounds.actual_native_potential_smoothNear {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (hx : ActualParticularStageControls.PreservesCarriers x) (hs : ActualParticularStageControls.InputSupport x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) {α : ℝ} (j : ℤ) (hj : j ≠ 0) (H : LabelSumBounds.UniformWaveClass nativeStrip ActualParticularStageControls.nativeEnvelope α (ActualParticularStageControls.currentSource x j)) (l : Label B N0) (n : ℕ) {z : Native} (hz : z ∈ nativeStrip.domain) : LocalPhysicalCopyBounds.SmoothNear (ActualCurrentParticularPhysical.nativePotential x l j n) z

theorem NavierStokes.ActualCurrentParticularBounds.actual_native_pressure_smoothNear {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (hx : ActualParticularStageControls.PreservesCarriers x) (hs : ActualParticularStageControls.InputSupport x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) {α : ℝ} (j : ℤ) (hj : j ≠ 0) (H : LabelSumBounds.UniformWaveClass nativeStrip ActualParticularStageControls.nativeEnvelope α (ActualParticularStageControls.currentSource x j)) (l : Label B N0) (n : ℕ) {z : Native} (hz : z ∈ nativeStrip.domain) : LocalPhysicalCopyBounds.SmoothNear (ActualCurrentParticularPhysical.nativePressure x l j n) z

theorem NavierStokes.ActualCurrentParticularBounds.actual_native_pressure_re_bound {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (hx : ActualParticularStageControls.PreservesCarriers x) (hs : ActualParticularStageControls.InputSupport x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) {α : ℝ} (j : ℤ) (hj : j ≠ 0) (H : LabelSumBounds.UniformWaveClass nativeStrip ActualParticularStageControls.nativeEnvelope α (ActualParticularStageControls.currentSource x j)) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∃ (p : ℕ), ∀ (l : ActualCurrentParticularPhysical.Label B N0) (n : ℕ), 4 ≤ n → ∀ z ∈ nativeStrip.domain, ∀ i ≤ m, ‖iteratedFDeriv ℝ i (fun (y : ActualCurrentParticularPhysical.Native) => (ActualCurrentParticularPhysical.nativePressure x l j n y).re) z‖ ≤ C * ChartScales.Q n ^ (CorrectionInitialization.ActualPrimary.h * (α + 1 / 2) - 2 * CorrectionInitialization.ActualPrimary.h * ↑m) * ChartScales.S n ^ p

theorem NavierStokes.ActualCurrentParticularBounds.native_closed_mem_closure {z : Native} (hz : z ∈ ActualCurrentParticularPhysical.nativeDomain) (hr : ActualWaveRegularityData.radius (ActualWaveRegularity.particularChart.symm z) ∈ Set.Icc (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal)) : z ∈ closure nativeStrip.domain

The closed moving annulus is the closure of the genuine open native strip within each positive-time slow fiber.

theorem NavierStokes.ActualCurrentParticularBounds.native_bound_on_closed {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : Native → E} (hf : ContDiffOn ℝ (↑⊤) f ActualCurrentParticularPhysical.nativeDomain) {C : ℝ} (m : ℕ) (hb : ∀ z ∈ nativeStrip.domain, ‖iteratedFDeriv ℝ m f z‖ ≤ C) {z : Native} (hz : z ∈ ActualCurrentParticularPhysical.nativeDomain) (hr : ActualWaveRegularityData.radius (ActualWaveRegularity.particularChart.symm z) ∈ Set.Icc (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal)) : ‖iteratedFDeriv ℝ m f z‖ ≤ C

theorem NavierStokes.ActualCurrentParticularBounds.scaled_common_bound {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {h a b : ℝ} (hh : 0 ≤ h) (hh1 : h ≤ 1 / 2) (ha : 0 < a) (Δ m : ℕ) (gain degree A : ℝ) (p : ℕ) (hA : 0 ≤ A) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (n : ℕ), 4 ≤ n → ∀ d ≤ Δ, ∀ (w : ProblemStatement.SpaceTime), (PhysicalGraphBounds.scaledRadial n) w ∈ PhysicalGraphBounds.annulus a b → |w.1| ≤ 1 → ∀ (q : ℝ), 0 < q → q / 2 ≤ ChartScales.Q n → ChartScales.Q n ≤ 2 * q → ∀ (F : PhysicalWaveSum.LiftPoint → E), LocalPhysicalCopyBounds.SmoothNear F (PhysicalWaveSum.commonLift h n d w) → (∀ i ≤ m, ‖iteratedFDeriv ℝ i F (PhysicalWaveSum.commonLift h n d w)‖ ≤ A * ChartScales.Q n ^ gain * ChartScales.S n ^ p) → ‖iteratedFDeriv ℝ m (fun (y : ProblemStatement.SpaceTime) => ChartScales.Q n ^ (-degree) • F (PhysicalWaveSum.commonLift h n d y)) w‖ ≤ C * q ^ (gain - degree - (PhysicalGraphBounds.graphLoss m + 1))

A frozen physical power is included before applying the proved jets of the actual common graph.

theorem NavierStokes.ActualCurrentParticularBounds.scalar_chart_physical_bound {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {h a b : ℝ} (hh : 0 ≤ h) (hh1 : h ≤ 1 / 2) (ha : 0 < a) (Δ m : ℕ) (gain degree A : ℝ) (p : ℕ) (hA : 0 ≤ A) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (n : ℕ), 4 ≤ n → ∀ d ≤ Δ, ∀ (w : ProblemStatement.SpaceTime), (PhysicalGraphBounds.scaledRadial n) w ∈ PhysicalGraphBounds.annulus a b → |w.1| ≤ 1 → ∀ (q : ℝ), 0 < q → q / 2 ≤ ChartScales.Q n → ChartScales.Q n ≤ 2 * q → ∀ (chart : PolarCharts.Index) (f : Native → E), LocalPhysicalCopyBounds.SmoothNear f (CurrentPhysicalChartJets.chartMap a chart (PhysicalWaveSum.commonLift h n d w)) → (∀ i ≤ m, ‖iteratedFDeriv ℝ i f (CurrentPhysicalChartJets.chartMap a chart (PhysicalWaveSum.commonLift h n d w))‖ ≤ A * ChartScales.Q n ^ gain * ChartScales.S n ^ p) → ‖iteratedFDeriv ℝ m (fun (y : ProblemStatement.SpaceTime) => ChartScales.Q n ^ (-degree) • f (CurrentPhysicalChartJets.chartMap a chart (PhysicalWaveSum.commonLift h n d y))) w‖ ≤ C * q ^ (gain - degree - (PhysicalGraphBounds.graphLoss m + 1))

theorem NavierStokes.ActualCurrentParticularBounds.vector_chart_physical_bound {h a b : ℝ} (hh : 0 ≤ h) (hh1 : h ≤ 1 / 2) (ha : 0 < a) (Δ m : ℕ) (gain degree A : ℝ) (p : ℕ) (hA : 0 ≤ A) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (n : ℕ), 4 ≤ n → ∀ d ≤ Δ, ∀ (w : ProblemStatement.SpaceTime), (PhysicalGraphBounds.scaledRadial n) w ∈ PhysicalGraphBounds.annulus a b → |w.1| ≤ 1 → ∀ (q : ℝ), 0 < q → q / 2 ≤ ChartScales.Q n → ChartScales.Q n ≤ 2 * q → ∀ (chart : PolarCharts.Index) (f : Native → HarmonicCalculus.ComplexVector), LocalPhysicalCopyBounds.SmoothNear f (CurrentPhysicalChartJets.chartMap a chart (PhysicalWaveSum.commonLift h n d w)) → (∀ i ≤ m, ‖iteratedFDeriv ℝ i f (CurrentPhysicalChartJets.chartMap a chart (PhysicalWaveSum.commonLift h n d w))‖ ≤ A * ChartScales.Q n ^ gain * ChartScales.S n ^ p) → ‖iteratedFDeriv ℝ m (fun (y : ProblemStatement.SpaceTime) => ChartScales.Q n ^ (-degree) • PhysicalCurlCovariance.realVector (CurrentPhysicalChartJets.rotated a chart f (PhysicalWaveSum.commonLift h n d y))) w‖ ≤ C * q ^ (gain - degree - (PhysicalGraphBounds.graphLoss m + 1))

theorem NavierStokes.ActualCurrentParticularBounds.current_mode_physical_bound {h a b : ℝ} (hh : 0 ≤ h) (hh1 : h ≤ 1 / 2) (ha : 0 < a) (Δ m : ℕ) (gain degree ρ A B H : ℝ) (p r : ℕ) (hρ : 0 ≤ ρ) (hA : 0 ≤ A) (hB : 1 ≤ B) (hH : 0 ≤ H) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (n : ℕ), 4 ≤ n → ∀ d ≤ Δ, ∀ (w : ProblemStatement.SpaceTime), (PhysicalGraphBounds.scaledRadial n) w ∈ PhysicalGraphBounds.annulus a b → |w.1| ≤ 1 → ∀ (q : ℝ), 0 < q → q / 2 ≤ ChartScales.Q n → ChartScales.Q n ≤ 2 * q → ∀ (amp : PhysicalWaveSum.LiftPoint → ℂ) (Φ : PhysicalWaveSum.LiftPoint → ℝ) (c : ℝ), |c| ≤ H → LocalPhysicalCopyBounds.SmoothNear amp (PhysicalWaveSum.commonLift h n d w) → LocalPhysicalCopyBounds.SmoothNear Φ (PhysicalWaveSum.commonLift h n d w) → (∀ i ≤ m, ‖iteratedFDeriv ℝ i amp (PhysicalWaveSum.commonLift h n d w)‖ ≤ A * ChartScales.Q n ^ gain * ChartScales.S n ^ p) → (∀ (i : ℕ), 1 ≤ i → i ≤ m → ‖iteratedFDeriv ℝ i Φ (PhysicalWaveSum.commonLift h n d w)‖ ≤ B * ChartScales.Q n ^ (-ρ) * ChartScales.S n ^ r) → ‖iteratedFDeriv ℝ m (fun (y : ProblemStatement.SpaceTime) => ChartScales.Q n ^ (-degree) • (amp (PhysicalWaveSum.commonLift h n d y) * PhysicalGraphBounds.character c (Φ (PhysicalWaveSum.commonLift h n d y)))) w‖ ≤ C * q ^ (gain - currentLoss degree ρ m)

A physical estimate for the literal current-band oscillatory formula. The scalar phase may already include the rounded carrier. Its positive derivatives alone are needed, so no bound on the free angular coordinate is introduced.

theorem NavierStokes.ActualCurrentParticularBounds.current_potential_mode_bound {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (ActualInitialization.Index B N0)} (H : ActualParticularCycleData.Invariant σ x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (j : ℤ) (hj : j ≠ 0) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (l : Label B N0) (n : ℕ), 4 ≤ n → ∀ w ∈ ValidDyadicBandCover.band CorrectionInitialization.ActualPrimary.h n, PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w ≤ 1 → ‖iteratedFDeriv ℝ m (ActualCurrentParticularPhysical.localPotentialMode (ActualCycleParameters.particularState x) l j n) w‖ ≤ C * PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w ^ (CorrectionInitialization.ActualPrimary.h * (1 / 2 + σ + 1 / 2) - currentLoss CorrectionInitialization.ActualPrimary.h (2 * CorrectionInitialization.ActualPrimary.h) m)

All physical jets of the actual current particular potential mode. The constant is chosen before the label, current band, and physical point. Only the literal incoming analytic invariant is required.

theorem NavierStokes.ActualCurrentParticularBounds.current_pressure_mode_bound {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (ActualInitialization.Index B N0)} (H : ActualParticularCycleData.Invariant σ x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (j : ℤ) (hj : j ≠ 0) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (l : Label B N0) (n : ℕ), 4 ≤ n → ∀ w ∈ ValidDyadicBandCover.band CorrectionInitialization.ActualPrimary.h n, PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w ≤ 1 → ‖iteratedFDeriv ℝ m (ActualCurrentParticularPhysical.localPressureMode (ActualCycleParameters.particularState x) l j n) w‖ ≤ C * PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w ^ (CorrectionInitialization.ActualPrimary.h * (1 / 2 + σ + 1 / 2) - currentLoss (2 * CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h) (2 * CorrectionInitialization.ActualPrimary.h) m)

The matching full physical-jet estimate for the literal current particular pressure mode, with its actual quadratic physical scale.