Geometry of the actual prepared primary charts

The native variables are (p,(u,v)), with p=(R,(Z,T)). The pulse coordinate is exactly v/L, and the common-cover chart uses the chosen slot basis and the actual difference of covering indices.

Controls from the actual shared primary construction

The reference matrix, target, unit pulse, normal motion and action below are computed from the same prepared primary family. Their native-copy estimates have constants before all labels, bands and copies.

@[reducible, inline]

abbrev NavierStokes.ActualSignedControl.Mat2 : Type

Mat2: an abbreviation for SmoothCovariance.Mat2.

Equations

• NavierStokes.ActualSignedControl.Mat2 = NavierStokes.SmoothCovariance.Mat2

@[reducible, inline]

abbrev NavierStokes.ActualSignedControl.Vec2 : Type

Vec2: an abbreviation for SmoothCovariance.Vec2.

Equations

• NavierStokes.ActualSignedControl.Vec2 = NavierStokes.SmoothCovariance.Vec2

@[reducible, inline]

abbrev NavierStokes.ActualSignedControl.Space : Type

Space: an abbreviation for ProblemStatement.Space.

Equations

• NavierStokes.ActualSignedControl.Space = NavierStokes.ProblemStatement.Space

noncomputable def NavierStokes.ActualSignedControl.phaseNormal {ι D : Type} {U : PhaseJetBounds.Domain ι PhaseCalculus.Slow} (F : PrimaryPulseBounds.PhaseConstruction U) (χ : ι → D → PhaseCalculus.Slow × ℝ) : ι → D → Space

Phase normal, defined pointwise by F.phase.normal i (PrimaryCopyBounds.phasePoint F χ i x).

Equations

• NavierStokes.ActualSignedControl.phaseNormal F χ i x = F.phase.normal i (NavierStokes.PrimaryCopyBounds.phasePoint F χ i x)

noncomputable def NavierStokes.ActualSignedControl.phaseMotion {ι D : Type} {U : PhaseJetBounds.Domain ι PhaseCalculus.Slow} (F : PrimaryPulseBounds.PhaseConstruction U) (χ : ι → D → PhaseCalculus.Slow × ℝ) : ι → D → Space

Phase motion, defined pointwise by F.phase.velocity i (PrimaryCopyBounds.phasePoint F χ i x).

Equations

• NavierStokes.ActualSignedControl.phaseMotion F χ i x = F.phase.velocity i (NavierStokes.PrimaryCopyBounds.phasePoint F χ i x)

noncomputable def NavierStokes.ActualSignedControl.phaseAction {ι D : Type} {U : PhaseJetBounds.Domain ι PhaseCalculus.Slow} (F : PrimaryPulseBounds.PhaseConstruction U) (χ : ι → D → PhaseCalculus.Slow × ℝ) : ι → D → Space →L[ℝ] Space

Phase action, defined pointwise by PrimaryCopyBridge.baseOperator (F.phase.F i (χ i x).1) (F.phase.shear i (PrimaryCopyBounds.phasePoint F χ i x)).

Equations

• NavierStokes.ActualSignedControl.phaseAction F χ i x = NavierStokes.PrimaryCopyBridge.baseOperator (F.phase.F i (χ i x).1) (F.phase.shear i (NavierStokes.PrimaryCopyBounds.phasePoint F χ i x))

theorem NavierStokes.ActualSignedControl.pulseMatrix_eq_phaseMatrix {D : Type} {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (F : Fin 2 → PrimaryPulseBounds.PhaseConstruction U) (pref : Fin 2 → ℕ → ℝ) (χ : ℕ → D → PhaseCalculus.Slow × ℝ) : PrimaryCopyBounds.pulseMatrix F pref χ = SignedWaveUpdate.phaseMatrix F pref χ

theorem NavierStokes.ActualSignedControl.pulseVector_eq_phaseFundamental {D : Type} {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (F : Fin 2 → PrimaryPulseBounds.PhaseConstruction U) (χ : ℕ → D → PhaseCalculus.Slow × ℝ) (j : Fin 2) : PrimaryCopyBounds.pulseVector F χ j = SignedWaveUpdate.phaseFundamental F χ j

theorem NavierStokes.ActualSignedControl.phase_geometry_jets {ι D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {V : PrimaryCopyBounds.JetDomain ι D} {U : PhaseJetBounds.Domain ι PhaseCalculus.Slow} (F : PrimaryPulseBounds.PhaseConstruction U) (χ : ι → D → PhaseCalculus.Slow × ℝ) (hscale : ∀ (i : ι), U.scale i = V.scale i) (hχ : PhaseJetBounds.PolynomialJets V.toDomain χ) (hmap : ∀ (i : ι), ∀ x ∈ V.carrier i, χ i x ∈ U.carrier i ×ˢ Set.Ioo 0 1) : PhaseJetBounds.PolynomialJets V.toDomain (phaseNormal F χ) ∧ PhaseJetBounds.PolynomialJets V.toDomain (phaseMotion F χ) ∧ PhaseJetBounds.PolynomialJets V.toDomain (phaseAction F χ) ∧ (∀ (i : ι), ∀ x ∈ V.carrier i, F.b ≤ ‖phaseNormal F χ i x‖) ∧ ∀ (i : ι), ∀ x ∈ V.carrier i, ‖phaseNormal F χ i x‖ ≤ F.M ^ 2 + 3 * F.M

The three geometric jet estimates are obtained from the actual phase construction, rather than being supplied for the pressure output.

structure NavierStokes.ActualSignedControl.ReferenceBounds {ι D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (V : PrimaryCopyBounds.JetDomain ι D) (U : PhaseJetBounds.Domain ι PhaseCalculus.Slow) (F : Fin 2 → PrimaryPulseBounds.PhaseConstruction U) (pref : Fin 2 → ι → ℝ) (χ : ι → D → PhaseCalculus.Slow × ℝ) (T : ι → D → Vec2) (mask ζ : ι → D → ℝ) : Type

A proved reference certificate. The prepared-family constructor below derives its target and mask estimates and all three scalar margins.

• scale (i : ι) : U.scale i = V.scale i
• coordinate_jets : PhaseJetBounds.PolynomialJets V.toDomain χ
• coordinate_mem (i : ι) (x : D) : x ∈ V.carrier i → χ i x ∈ U.carrier i ×ˢ Set.Ioo 0 1
• prefactor_jets (j : Fin 2) : PhaseJetBounds.PolynomialJets U fun (i : ι) (x : PhaseCalculus.Slow) => pref j i
• target_jets (q : Fin 2) : PrimaryCopyBounds.NativeJets V ζ fun (i : ι) (x : D) => T i x q
• mask_jets : PhaseJetBounds.PolynomialJets V.toDomain mask
• weight_pos (i : ι) (x : D) : x ∈ V.carrier i → 0 < ζ i x
• determinantGap : ℝ

  Determinant gap of ReferenceBounds, of type ℝ.

• entryBound : ℝ

  Entry bound of ReferenceBounds, of type ℝ.

• primaryLower : ℝ

  Primary lower of ReferenceBounds, of type ℝ.

• gap_pos : 0 < self.determinantGap
• entry_one : 1 ≤ self.entryBound
• lower_pos : 0 < self.primaryLower
• zero_order (i : ι) (x : D) : x ∈ V.carrier i → PrimaryCovarianceBounds.ZeroOrderBounds (√(V.scale i)) self.determinantGap self.entryBound self.primaryLower (ζ i x) (PrimaryCopyBounds.pulseMatrix F pref χ i x) (T i x)

theorem NavierStokes.ActualSignedControl.ReferenceBounds.matrix_jets {ι D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {V : PrimaryCopyBounds.JetDomain ι D} {U : PhaseJetBounds.Domain ι PhaseCalculus.Slow} {F : Fin 2 → PrimaryPulseBounds.PhaseConstruction U} {pref : Fin 2 → ι → ℝ} {χ : ι → D → PhaseCalculus.Slow × ℝ} {T : ι → D → Vec2} {mask ζ : ι → D → ℝ} (h : ReferenceBounds V U F pref χ T mask ζ) (j k : Fin 2) : PhaseJetBounds.PolynomialJets V.toDomain fun (i : ι) (x : D) => PrimaryCopyBounds.pulseMatrix F pref χ i x j k

theorem NavierStokes.ActualSignedControl.ReferenceBounds.unit_jets {ι D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {V : PrimaryCopyBounds.JetDomain ι D} {U : PhaseJetBounds.Domain ι PhaseCalculus.Slow} {F : Fin 2 → PrimaryPulseBounds.PhaseConstruction U} {pref : Fin 2 → ι → ℝ} {χ : ι → D → PhaseCalculus.Slow × ℝ} {T : ι → D → Vec2} {mask ζ : ι → D → ℝ} (h : ReferenceBounds V U F pref χ T mask ζ) (j : Fin 2) : PrimaryCopyBounds.NativeJets V (PrimaryCopyBounds.pulseEnvelope F χ j) (PrimaryCopyBounds.pulseVector F χ j)

theorem NavierStokes.ActualSignedControl.ReferenceBounds.geometry_jets {ι D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {V : PrimaryCopyBounds.JetDomain ι D} {U : PhaseJetBounds.Domain ι PhaseCalculus.Slow} {F : Fin 2 → PrimaryPulseBounds.PhaseConstruction U} {pref : Fin 2 → ι → ℝ} {χ : ι → D → PhaseCalculus.Slow × ℝ} {T : ι → D → Vec2} {mask ζ : ι → D → ℝ} (h : ReferenceBounds V U F pref χ T mask ζ) (j : Fin 2) : PhaseJetBounds.PolynomialJets V.toDomain (phaseNormal (F j) χ) ∧ PhaseJetBounds.PolynomialJets V.toDomain (phaseMotion (F j) χ) ∧ PhaseJetBounds.PolynomialJets V.toDomain (phaseAction (F j) χ) ∧ (∀ (i : ι), ∀ x ∈ V.carrier i, (F j).b ≤ ‖phaseNormal (F j) χ i x‖) ∧ ∀ (i : ι), ∀ x ∈ V.carrier i, ‖phaseNormal (F j) χ i x‖ ≤ (F j).M ^ 2 + 3 * (F j).M

theorem NavierStokes.ActualSignedControl.ReferenceBounds.cutoff_jets {ι D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {V : PrimaryCopyBounds.JetDomain ι D} {U : PhaseJetBounds.Domain ι PhaseCalculus.Slow} {F : Fin 2 → PrimaryPulseBounds.PhaseConstruction U} {pref : Fin 2 → ι → ℝ} {χ : ι → D → PhaseCalculus.Slow × ℝ} {T : ι → D → Vec2} {mask ζ : ι → D → ℝ} (h : ReferenceBounds V U F pref χ T mask ζ) : PhaseJetBounds.PolynomialJets V.toDomain fun (i : ι) (x : D) => GaussianTailFlat.profile (χ i x).2

structure NavierStokes.ActualSignedControl.CopyChart {ι Λ I D X : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup X] [NormedSpace ℝ X] (s : WeightedClasses.StripData X) (V : PrimaryCopyBounds.JetDomain ι D) (ζ : ι → D → ℝ) (K : Λ → ℕ → I → Set X) : Type

Only affine coordinate geometry and weight/scale comparisons are stored here. No copied field or copied derivative bound is an input.

• index : Λ → ℕ → ι

  Index of CopyChart, of type Λ → ℕ → ι.

• linear : Λ → ℕ → I → X →L[ℝ] D

  Linear of CopyChart, of type Λ → ℕ → I → X →L[ℝ] D.

• shift : Λ → ℕ → I → D

  Shift of CopyChart, of type Λ → ℕ → I → D.

• maps (l : Λ) (n : ℕ) (i : I) (x : X) : x ∈ s.domain → x ∈ K l n i → (self.linear l n i) x + self.shift l n i ∈ V.carrier (self.index l n)
• growthConstant : ℝ

  Growth constant of CopyChart, of type ℝ.

• linearConstant : ℝ

  Linear constant of CopyChart, of type ℝ.

• growth_one : 1 ≤ self.growthConstant
• linear_one : 1 ≤ self.linearConstant
• growthDegree : ℕ

  Growth degree of CopyChart, of type ℕ.

• linearDegree : ℕ

  Linear degree of CopyChart, of type ℕ.

• growth_bound (l : Λ) (n : ℕ) (i : I) (x : X) : x ∈ s.domain → x ∈ K l n i → V.growth (self.index l n) ((self.linear l n i) x + self.shift l n i) ≤ self.growthConstant * s.growth n x ^ self.growthDegree
• linear_bound (l : Λ) (n : ℕ) (i : I) : ‖self.linear l n i‖ ≤ self.linearConstant * s.slow n ^ self.linearDegree
• weight_eq (l : Λ) (n : ℕ) (i : I) (x : X) : x ∈ s.domain → x ∈ K l n i → ζ (self.index l n) ((self.linear l n i) x + self.shift l n i) = s.zeta x
• ratioLower : ℝ

  Ratio lower of CopyChart, of type ℝ.

• ratioUpper : ℝ

  Ratio upper of CopyChart, of type ℝ.

• ratio_pos : 0 < self.ratioLower
• ratio_one : 1 ≤ self.ratioUpper
• scale_ratio (l : Λ) (n : ℕ) : self.ratioLower ≤ √(s.slow n) / √(V.scale (self.index l n)) ∧ √(s.slow n) / √(V.scale (self.index l n)) ≤ self.ratioUpper

noncomputable def NavierStokes.ActualSignedControl.CopyChart.pull {ι Λ I D X E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup X] [NormedSpace ℝ X] {s : WeightedClasses.StripData X} {V : PrimaryCopyBounds.JetDomain ι D} {ζ : ι → D → ℝ} {K : Λ → ℕ → I → Set X} (c : CopyChart s V ζ K) (f : ι → D → E) : Λ → ℕ → I → X → E

Pull, given by affineCopy f c.index c.linear c.shift.

Equations

• c.pull f = NavierStokes.PrimaryCopyBounds.affineCopy f c.index c.linear c.shift

theorem NavierStokes.ActualSignedControl.CopyChart.unweighted {ι Λ I D X E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData X} {V : PrimaryCopyBounds.JetDomain ι D} {ζ : ι → D → ℝ} {K : Λ → ℕ → I → Set X} (c : CopyChart s V ζ K) {f : ι → D → E} (hf : PhaseJetBounds.PolynomialJets V.toDomain f) : PeriodizedWaveBounds.UniformLocalJets s (fun (x : Λ) (x_1 : ℕ) (x_2 : X) => 1) 0 K (c.pull f)

theorem NavierStokes.ActualSignedControl.CopyChart.weighted {ι Λ I D X E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData X} {V : PrimaryCopyBounds.JetDomain ι D} {ζ : ι → D → ℝ} {K : Λ → ℕ → I → Set X} (c : CopyChart s V ζ K) {f : ι → D → E} (hf : PrimaryCopyBounds.NativeJets V ζ f) : PeriodizedWaveBounds.UniformLocalJets s (fun (x : Λ) (x_1 : ℕ) (x_2 : X) => s.zeta x_2) 0 K (c.pull f)

theorem NavierStokes.ActualSignedControl.CopyChart.envelope {ι Λ I D X E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData X} {V : PrimaryCopyBounds.JetDomain ι D} {ζ : ι → D → ℝ} {K : Λ → ℕ → I → Set X} (c : CopyChart s V ζ K) {w : ι → D → ℝ} {f : ι → D → E} (hf : PrimaryCopyBounds.NativeJets V w f) {W : Λ → ℕ → X → ℝ} (hW : ∀ (l : Λ) (n : ℕ), ∀ x ∈ s.domain, 0 ≤ W l n x) (hw : ∀ (l : Λ) (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K l n i → w (c.index l n) ((c.linear l n i) x + c.shift l n i) ≤ W l n x) : PeriodizedWaveBounds.UniformLocalJets s W 0 K (c.pull f)

The reference certificate is produced from the same actual profile

structure NavierStokes.ActualSignedControl.PreparedChart {F₀ : OutgoingProfile.Profile} {W₀ : NominalProfile.Witness F₀} (H₀ : NominalConeAssembly.Certificate W₀) {ld : ModulatedProfileAssembly.LoopData W₀} (v₀ : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H₀ v₀ upper B r0 N0) (D : Type) [NormedAddCommGroup D] [NormedSpace ℝ D] : Type

Primitive local chart geometry for a selected prepared family. The target, matrix, mask and pulse jets are not fields of this record.

• native : PrimaryCopyBounds.JetDomain (PrimaryGeometryAssembly.Index W₀ a.N) D

  Native of PreparedChart, of type JetDomain (PrimaryGeometryAssembly.Index W₀ a.N) D.

• slow : PrimaryCopyBounds.JetDomain (PrimaryGeometryAssembly.Index W₀ a.N) PhaseCalculus.Slow

  Slow of PreparedChart, of type JetDomain (PrimaryGeometryAssembly.Index W₀ a.N) PhaseCalculus.Slow.

• coordinate : PrimaryGeometryAssembly.Index W₀ a.N → D → PhaseCalculus.Slow × ℝ

  Coordinate of PreparedChart, of type PrimaryGeometryAssembly.Index W₀ a.N → D → PhaseCalculus.Slow × ℝ.

• scale (L : PrimaryGeometryAssembly.Index W₀ a.N) : (PrimaryGeometryAssembly.domain W₀ a.N).scale L = self.native.scale L
• coordinate_jets : PhaseJetBounds.PolynomialJets self.native.toDomain self.coordinate
• maps (L : PrimaryGeometryAssembly.Index W₀ a.N) (x : D) : x ∈ self.native.carrier L → self.coordinate L x ∈ (PrimaryGeometryAssembly.domain W₀ a.N).carrier L ×ˢ Set.Ioo 0 1
• positive (L : PrimaryGeometryAssembly.Index W₀ a.N) (x : D) : x ∈ self.native.carrier L → (self.coordinate L x).1 ∈ PositiveRepresentatives.positivePart (PrimaryGeometryAssembly.referenceSet W₀)
• slow_maps (L : PrimaryGeometryAssembly.Index W₀ a.N) (x : D) : x ∈ self.native.carrier L → (self.coordinate L x).1 ∈ self.slow.carrier L
• slow_growth (L : PrimaryGeometryAssembly.Index W₀ a.N) (x : D) : x ∈ self.native.carrier L → self.slow.growth L (self.coordinate L x).1 ≤ self.native.growth L x
• radiusLower : ℝ

  Radius lower of PreparedChart, of type ℝ.

• normUpper : ℝ

  Norm upper of PreparedChart, of type ℝ.

• qLower : ℝ

  Q lower of PreparedChart, of type ℝ.

• qUpper : ℝ

  Q upper of PreparedChart, of type ℝ.

• radius_pos : 0 < self.radiusLower
• q_pos : 0 < self.qLower
• geometry : BaseChartJets.GeometryBounds self.slow.toDomain F₀.data.h self.radiusLower self.normUpper self.qLower self.qUpper (NominalConeAssembly.activeLeft W₀) (NominalConeAssembly.activeRight W₀)
• inverse_edge (L : PrimaryGeometryAssembly.Index W₀ a.N) (p : PhaseCalculus.Slow) : p ∈ self.slow.carrier L → (FinalSlowBase.edgeDistance W₀ (BaseChartJets.normalizedCoordinates F₀.data.h p).2)⁻¹ ≤ self.slow.growth L p

noncomputable def NavierStokes.ActualSignedControl.PreparedChart.target {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {F₀ : OutgoingProfile.Profile} {W₀ : NominalProfile.Witness F₀} {H₀ : NominalConeAssembly.Certificate W₀} {ld : ModulatedProfileAssembly.LoopData W₀} {v₀ : ModulatedProfileAssembly.Witness ld} {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} {a : PrimaryGeometryAssembly.Prepared H₀ v₀ upper B r0 N0} (c : PreparedChart H₀ v₀ a D) : PrimaryGeometryAssembly.Index W₀ a.N → D → Vec2

Target, defined pointwise by PrimaryTargetBounds.actualTarget v₀ (c.coordinate L x).1 k.

Equations

• c.target L x k = (NavierStokes.PrimaryTargetBounds.actualTarget v₀ (c.coordinate L x).1).ofLp k

noncomputable def NavierStokes.ActualSignedControl.PreparedChart.weight {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {F₀ : OutgoingProfile.Profile} {W₀ : NominalProfile.Witness F₀} {H₀ : NominalConeAssembly.Certificate W₀} {ld : ModulatedProfileAssembly.LoopData W₀} {v₀ : ModulatedProfileAssembly.Witness ld} {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} {a : PrimaryGeometryAssembly.Prepared H₀ v₀ upper B r0 N0} (c : PreparedChart H₀ v₀ a D) : PrimaryGeometryAssembly.Index W₀ a.N → D → ℝ

Weight, defined pointwise by PrimaryTargetBounds.movingWeight W₀ (c.coordinate L x).1.

Equations

• c.weight L x = NavierStokes.PrimaryTargetBounds.movingWeight W₀ (c.coordinate L x).1

noncomputable def NavierStokes.ActualSignedControl.PreparedChart.mask {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {F₀ : OutgoingProfile.Profile} {W₀ : NominalProfile.Witness F₀} {H₀ : NominalConeAssembly.Certificate W₀} {ld : ModulatedProfileAssembly.LoopData W₀} {v₀ : ModulatedProfileAssembly.Witness ld} {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} {a : PrimaryGeometryAssembly.Prepared H₀ v₀ upper B r0 N0} (c : PreparedChart H₀ v₀ a D) : PrimaryGeometryAssembly.Index W₀ a.N → D → ℝ

Mask as an element of PrimaryGeometryAssembly.Index W₀ a.N → D → ℝ.

Equations

• c.mask L x = NavierStokes.PrimaryRepresentatives.nativeMask (NavierStokes.PrimaryGeometryAssembly.label W₀ L).1 (NavierStokes.PrimaryGeometryAssembly.label W₀ L).2 (c.coordinate L x).1

theorem NavierStokes.ActualSignedControl.PreparedChart.target_jets {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {F₀ : OutgoingProfile.Profile} {W₀ : NominalProfile.Witness F₀} {H₀ : NominalConeAssembly.Certificate W₀} {ld : ModulatedProfileAssembly.LoopData W₀} {v₀ : ModulatedProfileAssembly.Witness ld} {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} {a : PrimaryGeometryAssembly.Prepared H₀ v₀ upper B r0 N0} (c : PreparedChart H₀ v₀ a D) (hcone : LeadingStressWeights.FullTrueCone v₀) (k : Fin 2) : PrimaryCopyBounds.NativeJets c.native c.weight fun (L : PrimaryGeometryAssembly.Index W₀ a.N) (x : D) => c.target L x k

theorem NavierStokes.ActualSignedControl.PreparedChart.mask_jets {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {F₀ : OutgoingProfile.Profile} {W₀ : NominalProfile.Witness F₀} {H₀ : NominalConeAssembly.Certificate W₀} {ld : ModulatedProfileAssembly.LoopData W₀} {v₀ : ModulatedProfileAssembly.Witness ld} {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} {a : PrimaryGeometryAssembly.Prepared H₀ v₀ upper B r0 N0} (c : PreparedChart H₀ v₀ a D) : PhaseJetBounds.PolynomialJets c.native.toDomain c.mask

theorem NavierStokes.ActualSignedControl.PreparedChart.weight_pos {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {F₀ : OutgoingProfile.Profile} {W₀ : NominalProfile.Witness F₀} {H₀ : NominalConeAssembly.Certificate W₀} {ld : ModulatedProfileAssembly.LoopData W₀} {v₀ : ModulatedProfileAssembly.Witness ld} {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} {a : PrimaryGeometryAssembly.Prepared H₀ v₀ upper B r0 N0} (c : PreparedChart H₀ v₀ a D) (L : PrimaryGeometryAssembly.Index W₀ a.N) {x : D} (hx : x ∈ c.native.carrier L) : 0 < c.weight L x

noncomputable def NavierStokes.ActualSignedControl.PreparedChart.referenceBounds {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {F₀ : OutgoingProfile.Profile} {W₀ : NominalProfile.Witness F₀} {H₀ : NominalConeAssembly.Certificate W₀} {ld : ModulatedProfileAssembly.LoopData W₀} {v₀ : ModulatedProfileAssembly.Witness ld} {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} {a : PrimaryGeometryAssembly.Prepared H₀ v₀ upper B r0 N0} (c : PreparedChart H₀ v₀ a D) (hcone : LeadingStressWeights.FullTrueCone v₀) (hr0 : 0 < r0) (vr vt : TorusInverse.Plane) (dg eb il : ℝ) (hdg : 0 < dg) (heb : 1 ≤ eb) (hil : 0 < il) (hz : ∀ (L : PrimaryGeometryAssembly.Index W₀ a.N), ∀ p ∈ PositiveRepresentatives.positivePart (PrimaryGeometryAssembly.referenceSet W₀), p ∈ (PrimaryGeometryAssembly.domain W₀ a.N).carrier L → PrimaryCovarianceBounds.ZeroOrderBounds (√(ChartScales.S (BaseChartJets.cellBand L))) dg eb il (PrimaryTargetBounds.movingWeight W₀ p) (PrimaryTargetBounds.preparedCovariance H₀ v₀ a vr vt L p) fun (k : Fin 2) => (PrimaryTargetBounds.actualTarget v₀ p).ofLp k) : ReferenceBounds c.native (PrimaryGeometryAssembly.domain W₀ a.N) (PrimaryGeometryAssembly.construction H₀ v₀ a hr0) (PrimaryCopyBounds.preparedPrefactor r0 vr vt) c.coordinate c.target c.mask c.weight

Every jet field in this reference certificate is derived from the actual prepared phase, actual leading target and actual grid mask.

Equations

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

theorem NavierStokes.ActualSignedControl.exists_referenceBounds {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {F₀ : OutgoingProfile.Profile} {W₀ : NominalProfile.Witness F₀} (H₀ : NominalConeAssembly.Certificate W₀) {ld : ModulatedProfileAssembly.LoopData W₀} (v₀ : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H₀ v₀ upper B r0 N0) (hcone : LeadingStressWeights.FullTrueCone v₀) (hr0 : 0 < r0) (vr vt : TorusInverse.Plane) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) : ∃ (N : ℕ) (hN : a.N ≤ N), ∀ (c : PreparedChart H₀ v₀ (a.restrict N hN) D), Nonempty (ReferenceBounds c.native (PrimaryGeometryAssembly.domain W₀ N) (PrimaryGeometryAssembly.construction H₀ v₀ (a.restrict N hN) hr0) (PrimaryCopyBounds.preparedPrefactor r0 vr vt) c.coordinate c.target c.mask c.weight)

A supplied prepared family is only restricted to a later tail. Every surviving phase and representative is the same one used by the primary construction. No determinant or final control record is assumed.

Transport through the actual affine views

structure NavierStokes.ActualSignedControl.PositiveScale (Λ : Type) : Type

Positive band scalars with uniform primitive zeroth-order margins.

• value : Λ → ℕ → ℝ

  Value of PositiveScale, of type Λ → ℕ → ℝ.

• lower : ℝ

  Lower of PositiveScale, of type ℝ.

• upper : ℝ

  Upper of PositiveScale, of type ℝ.

• lower_pos : 0 < self.lower
• upper_one : 1 ≤ self.upper
• bounds (l : Λ) (n : ℕ) : self.lower ≤ self.value l n ∧ self.value l n ≤ self.upper

theorem NavierStokes.ActualSignedControl.PositiveScale.value_pos {Λ : Type} (a : PositiveScale Λ) (l : Λ) (n : ℕ) : 0 < a.value l n

theorem NavierStokes.ActualSignedControl.PositiveScale.bandBound {Λ X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] (a : PositiveScale Λ) (s : WeightedClasses.StripData X) : UniformPrimaryWeights.UniformBandBound s 0 a.value

theorem NavierStokes.ActualSignedControl.PositiveScale.square_bandBound {Λ X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] (a : PositiveScale Λ) (s : WeightedClasses.StripData X) : UniformPrimaryWeights.UniformBandBound s 0 fun (l : Λ) (n : ℕ) => a.value l n ^ 2

noncomputable def NavierStokes.ActualSignedControl.PositiveScale.mul {Λ : Type} (a b : PositiveScale Λ) : PositiveScale Λ

Mul, bundling value, lower, upper, lower_pos and the required compatibility proofs.

Equations

• a.mul b = { value := fun (l : Λ) (n : ℕ) => a.value l n * b.value l n, lower := a.lower * b.lower, upper := a.upper * b.upper, lower_pos := ⋯, upper_one := ⋯, bounds := ⋯ }

theorem NavierStokes.ActualSignedControl.uniform_band_smul {Λ I X E : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup E] [NormedSpace ℝ E] [Countable Λ] [Nonempty Λ] {s : WeightedClasses.StripData X} {K : Λ → ℕ → I → Set X} {w : Λ → ℕ → X → ℝ} {α β : ℝ} {f : Λ → ℕ → I → X → E} {r : Λ → ℕ → ℝ} (hf : PeriodizedWaveBounds.UniformLocalJets s w α K f) (hr : UniformPrimaryWeights.UniformBandBound s β r) (hw : ∀ (l : Λ) (n : ℕ), ∀ x ∈ s.domain, 0 ≤ w l n x) : PeriodizedWaveBounds.UniformLocalJets s w (α + β) K fun (l : Λ) (n : ℕ) (i : I) (x : X) => r l n • f l n i x

theorem NavierStokes.ActualSignedControl.uniform_local_congr {Λ I X E : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData X} {K : Λ → ℕ → I → Set X} {w : Λ → ℕ → X → ℝ} {α : ℝ} {f g : Λ → ℕ → I → X → E} (hf : PeriodizedWaveBounds.UniformLocalJets s w α K f) (he : ∀ (l : Λ) (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K l n i → f l n i =ᶠ[nhds x] g l n i) : PeriodizedWaveBounds.UniformLocalJets s w α K g

theorem NavierStokes.ActualSignedControl.rescale_margins {r R dg eb il ζ c clo rlo rhi : ℝ} {H : Mat2} {T : Vec2} (h : PrimaryCovarianceBounds.ZeroOrderBounds r dg eb il ζ H T) (hr : 1 ≤ r) (hdg : 0 ≤ dg) (hil : 0 ≤ il) (hζ : 0 ≤ ζ) (hclo : 0 < clo) (hc : clo ≤ c) (hrlo : 0 < rlo) (hlo : rlo ≤ R / r) (hhi : R / r ≤ rhi) : rlo ^ 2 * dg ≤ |Matrix.det (PrimaryPulseBounds.normalizedMatrix R H)| ∧ (∀ (i j : Fin 2), |R * H i j| ≤ rhi * eb) ∧ ∀ (j : Fin 2), clo ^ 2 * il * ζ ≤ SmoothCovariance.weights H (c ^ 2 • T) j

Changing the band's normalization and scaling the actual target preserves quantitative Cramer margins with explicit constants.

noncomputable def NavierStokes.ActualSignedControl.ReferenceBounds.nativeCovariance {ι Λ I D X : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup X] [NormedSpace ℝ X] [Countable Λ] [Nonempty Λ] {V : PrimaryCopyBounds.JetDomain ι D} {U : PhaseJetBounds.Domain ι PhaseCalculus.Slow} {F : Fin 2 → PrimaryPulseBounds.PhaseConstruction U} {pref : Fin 2 → ι → ℝ} {χ : ι → D → PhaseCalculus.Slow × ℝ} {T : ι → D → Vec2} {mask ζ : ι → D → ℝ} (h : ReferenceBounds V U F pref χ T mask ζ) {s : WeightedClasses.StripData X} {K : Λ → ℕ → I → Set X} (c : CopyChart s V ζ K) (scale : PositiveScale Λ) (hzeta : ∀ x ∈ s.domain, 0 < s.zeta x) : SignedCopyBounds.UniformNativeCovariance s K (fun (l : Λ) (i : I) (n : ℕ) => c.pull (PrimaryCopyBounds.pulseMatrix F pref χ) l n i) fun (l : Λ) (i : I) (n : ℕ) (x : X) => scale.value l n ^ 2 • c.pull T l n i x

Construct the actual uniform native covariance record from the derived reference jets and the primitive view geometry.

Equations

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

noncomputable def NavierStokes.ActualSignedControl.ReferenceBounds.nativeCovarianceAt {ι Λ I D X : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup X] [NormedSpace ℝ X] [Countable Λ] [Nonempty Λ] {V : PrimaryCopyBounds.JetDomain ι D} {U : PhaseJetBounds.Domain ι PhaseCalculus.Slow} {F : Fin 2 → PrimaryPulseBounds.PhaseConstruction U} {pref : Fin 2 → ι → ℝ} {χ : ι → D → PhaseCalculus.Slow × ℝ} {T : ι → D → Vec2} {mask ζ : ι → D → ℝ} (h : ReferenceBounds V U F pref χ T mask ζ) {s : WeightedClasses.StripData X} {K : Λ → ℕ → I → Set X} (c : CopyChart s V ζ K) (scale : PositiveScale Λ) (hzeta : ∀ x ∈ s.domain, 0 < s.zeta x) (l : Λ) : SignedCopyBounds.NativeCovariance s (K l) (fun (i : I) (n : ℕ) => c.pull (PrimaryCopyBounds.pulseMatrix F pref χ) l n i) fun (i : I) (n : ℕ) (x : X) => scale.value l n ^ 2 • c.pull T l n i x

The requested copy-level NativeCovariance is a projection of the jointly proved record, retaining the same numerical margins.

Equations

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

theorem NavierStokes.ActualSignedControl.ReferenceBounds.copied_unit_jets {ι Λ I D X : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup X] [NormedSpace ℝ X] {V : PrimaryCopyBounds.JetDomain ι D} {U : PhaseJetBounds.Domain ι PhaseCalculus.Slow} {F : Fin 2 → PrimaryPulseBounds.PhaseConstruction U} {pref : Fin 2 → ι → ℝ} {χ : ι → D → PhaseCalculus.Slow × ℝ} {T : ι → D → Vec2} {mask ζ : ι → D → ℝ} (h : ReferenceBounds V U F pref χ T mask ζ) {s : WeightedClasses.StripData X} {K : Λ → ℕ → I → Set X} (c : CopyChart s V ζ K) (j : Fin 2) {W : Λ → ℕ → X → ℝ} (hW : ∀ (l : Λ) (n : ℕ), ∀ x ∈ s.domain, 0 ≤ W l n x) (henv : ∀ (l : Λ) (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K l n i → c.pull (PrimaryCopyBounds.pulseEnvelope F χ j) l n i x ≤ W l n x) : PeriodizedWaveBounds.UniformLocalJets s W 0 K (c.pull (PrimaryCopyBounds.pulseVector F χ j))

theorem NavierStokes.ActualSignedControl.ReferenceBounds.copied_geometry_jets {ι Λ I D X : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup X] [NormedSpace ℝ X] [Countable Λ] [Nonempty Λ] {V : PrimaryCopyBounds.JetDomain ι D} {U : PhaseJetBounds.Domain ι PhaseCalculus.Slow} {F : Fin 2 → PrimaryPulseBounds.PhaseConstruction U} {pref : Fin 2 → ι → ℝ} {χ : ι → D → PhaseCalculus.Slow × ℝ} {T : ι → D → Vec2} {mask ζ : ι → D → ℝ} (h : ReferenceBounds V U F pref χ T mask ζ) {s : WeightedClasses.StripData X} {K : Λ → ℕ → I → Set X} (c : CopyChart s V ζ K) (normal clock : PositiveScale Λ) (j : Fin 2) : (PeriodizedWaveBounds.UniformLocalJets s (fun (x : Λ) (x_1 : ℕ) (x_2 : X) => 1) 0 K fun (l : Λ) (n : ℕ) (i : I) (x : X) => normal.value l n • c.pull (phaseNormal (F j) χ) l n i x) ∧ (PeriodizedWaveBounds.UniformLocalJets s (fun (x : Λ) (x_1 : ℕ) (x_2 : X) => 1) 0 K fun (l : Λ) (n : ℕ) (i : I) (x : X) => (normal.value l n * clock.value l n) • c.pull (phaseMotion (F j) χ) l n i x) ∧ PeriodizedWaveBounds.UniformLocalJets s (fun (x : Λ) (x_1 : ℕ) (x_2 : X) => 1) 0 K fun (l : Λ) (n : ℕ) (i : I) (x : X) => clock.value l n • c.pull (phaseAction (F j) χ) l n i x

The modeled normal, normal motion and action are the transported ones from the selected primary phase, with its actual clock factors.

theorem NavierStokes.ActualSignedControl.ReferenceBounds.copied_normal_bounds {ι Λ I D X : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup X] [NormedSpace ℝ X] {V : PrimaryCopyBounds.JetDomain ι D} {U : PhaseJetBounds.Domain ι PhaseCalculus.Slow} {F : Fin 2 → PrimaryPulseBounds.PhaseConstruction U} {pref : Fin 2 → ι → ℝ} {χ : ι → D → PhaseCalculus.Slow × ℝ} {T : ι → D → Vec2} {mask ζ : ι → D → ℝ} (h : ReferenceBounds V U F pref χ T mask ζ) {s : WeightedClasses.StripData X} {K : Λ → ℕ → I → Set X} (c : CopyChart s V ζ K) (normal : PositiveScale Λ) (j : Fin 2) (l : Λ) (n : ℕ) (i : I) {x : X} (hx : x ∈ s.domain) (hi : x ∈ K l n i) : normal.lower * (F j).b ≤ ‖normal.value l n • c.pull (phaseNormal (F j) χ) l n i x‖ ∧ ‖normal.value l n • c.pull (phaseNormal (F j) χ) l n i x‖ ≤ normal.upper * ((F j).M ^ 2 + 3 * (F j).M)

theorem NavierStokes.ActualSignedControl.harmonic_frequency_bound {Λ I X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] (s : WeightedClasses.StripData X) (base : Λ → I → LinearWaveBounds.WaveCoefficients X) (harmonic : Λ → ℕ → ℤ) (hn : ∀ (l : Λ) (n : ℕ), harmonic l n ≠ 0) (hf : ∀ (l : Λ) (i : I) (n : ℕ), (base l i).frequency n = CurlClassBounds.carrierFrequency s n * ↑(harmonic l n)) : UniformPrimaryWeights.UniformBandBound s (1 / 2) fun (li : Λ × I) (n : ℕ) => 1 / (base li.1 li.2).frequency n

The carrier bound is derived for any nonzero integral harmonic, with one constant before both the label and the copy.

noncomputable def NavierStokes.ActualSignedControl.ReferenceBounds.copiedCoefficients {ι Λ I D X : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup X] [NormedSpace ℝ X] {V : PrimaryCopyBounds.JetDomain ι D} {U : PhaseJetBounds.Domain ι PhaseCalculus.Slow} {F : Fin 2 → PrimaryPulseBounds.PhaseConstruction U} {pref : Fin 2 → ι → ℝ} {χ : ι → D → PhaseCalculus.Slow × ℝ} {T : ι → D → Vec2} {mask ζ : ι → D → ℝ} {s : WeightedClasses.StripData X} {K : Λ → ℕ → I → Set X} (c : CopyChart s V ζ K) (scale normal clock : PositiveScale Λ) (base : Λ → I → LinearWaveBounds.WaveCoefficients X) (dirs : Λ → I → LinearWaveBounds.GraphDirections X) (request : ℕ → X → Vec2) (j : Fin 2) (l : Λ) (i : I) : LinearWaveBounds.WaveCoefficients X

Exact functional form of the transported shared-reference signed constructor, including the target square and the pressure clock factors.

Equations

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

theorem NavierStokes.ActualSignedControl.ReferenceBounds.copied_coefficients_jets {ι Λ I D X : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup X] [NormedSpace ℝ X] [Countable Λ] [Nonempty Λ] {V : PrimaryCopyBounds.JetDomain ι D} {U : PhaseJetBounds.Domain ι PhaseCalculus.Slow} {F : Fin 2 → PrimaryPulseBounds.PhaseConstruction U} {pref : Fin 2 → ι → ℝ} {χ : ι → D → PhaseCalculus.Slow × ℝ} {T : ι → D → Vec2} {mask ζ : ι → D → ℝ} (h : ReferenceBounds V U F pref χ T mask ζ) {s : WeightedClasses.StripData X} {K : Λ → ℕ → I → Set X} (c : CopyChart s V ζ K) (scale normal clock : PositiveScale Λ) (base : Λ → I → LinearWaveBounds.WaveCoefficients X) (dirs : Λ → I → LinearWaveBounds.GraphDirections X) (request : ℕ → X → Vec2) {β : ℝ} {W : Λ → ℕ → X → ℝ} (hzeta : ∀ x ∈ s.domain, 0 < s.zeta x) (hR : ∀ (q : Fin 2), PeriodizedWaveBounds.UniformLocalJets s (fun (x : Λ) (x_1 : ℕ) (x_2 : X) => s.zeta x_2) β K fun (x : Λ) (n : ℕ) (x_1 : I) (x_2 : X) => request n x_2 q) (hW : ∀ (l : Λ) (n : ℕ), ∀ x ∈ s.domain, 0 ≤ W l n x) (j : Fin 2) (henv : ∀ (l : Λ) (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K l n i → c.pull (PrimaryCopyBounds.pulseEnvelope F χ j) l n i x ≤ W l n x) (hnormal : ∀ (l : Λ) (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K l n i → (fun (y : X) => normal.value l n • c.pull (phaseNormal (F j) χ) l n i y) =ᶠ[nhds x] (base l i).normal s (dirs l i) n) (hfrequency : UniformPrimaryWeights.UniformBandBound s (1 / 2) fun (li : Λ × I) (n : ℕ) => 1 / (base li.1 li.2).frequency n) : (PeriodizedWaveBounds.UniformLocalJets s (fun (l : Λ) (n : ℕ) (x : X) => √(s.zeta x) * W l n x) (β + 1 / 2) K fun (l : Λ) (n : ℕ) (i : I) => (copiedCoefficients c scale normal clock base dirs request j l i).amplitude n) ∧ PeriodizedWaveBounds.UniformLocalJets s (fun (l : Λ) (n : ℕ) (x : X) => √(s.zeta x) * W l n x) (β + 1) K fun (l : Λ) (n : ℕ) (i : I) => (copiedCoefficients c scale normal clock base dirs request j l i).pressure n

The native signed estimates are obtained from the constructed reference, without accepting a completed native covariance record.

The signed request is the measured current-state request

theorem NavierStokes.ActualSignedControl.uniformLocalJets_of_memClass {Λ I X E : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData X} {w : ℕ → X → ℝ} {α : ℝ} {f : ℕ → X → E} (hf : WeightedClasses.MemClass s w α f) (K : Λ → ℕ → I → Set X) : PeriodizedWaveBounds.UniformLocalJets s (fun (x : Λ) => w) α K fun (x : Λ) (n : ℕ) (x_1 : I) => f n

theorem NavierStokes.ActualSignedControl.fullRequest_localJets {Λ I : Type} (s : WeightedClasses.StripData LocalSignedRequest.Point) (P : SignedStressPrimitive.Patch) (coord : ℝ) (ctx : CorrectionState.Context LocalSignedRequest.Point) (u : CorrectionState.State LocalSignedRequest.Point) {β : ℝ} (h : ∀ (q : Fin 2), WeightedClasses.MeanClass s β fun (n : ℕ) (x : LocalSignedRequest.Point) => LocalSignedRequest.normalizedRequest s P coord ctx u n x q) (K : Λ → ℕ → I → Set (LocalSignedRequest.Point × ℝ)) (q : Fin 2) : PeriodizedWaveBounds.UniformLocalJets (HarmonicWaveInteraction.productStrip s) (fun (x : Λ) (x_1 : ℕ) (x_2 : LocalSignedRequest.Point × ℝ) => s.zeta x_2.1) β K fun (x : Λ) (n : ℕ) (x_1 : I) (x_2 : LocalSignedRequest.Point × ℝ) => LocalSignedRequest.fullRequest s P coord ctx u n x_2 q

theorem NavierStokes.ActualSignedControl.physical_fullRequest_localJets {Λ I : Type} {coord : ℝ} (U : LocalSignedRequest.SlowRegion coord) (P : SignedStressPrimitive.Patch) {cL cR : ℝ} (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (ctx : CorrectionState.Context LocalSignedRequest.Point) (u : CorrectionState.State LocalSignedRequest.Point) (α : ℝ) (hθ : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (u.thetaResidual ctx n) (PhysicalMeanDomain.slowDomain U.carrier)) (hz : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (u.axialResidual ctx n) (PhysicalMeanDomain.slowDomain U.carrier)) (hsθ : ∀ (n : ℕ), LocalSignedRequest.MovingSupport P.a P.b coord U.carrier (u.thetaResidual ctx n)) (hsz : ∀ (n : ℕ), LocalSignedRequest.MovingSupport P.a P.b coord U.carrier (u.axialResidual ctx n)) (hcθ : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U P.a P.b cL cR ⋯ hcL hcR ε L hε hεone hL) α (u.thetaResidual ctx)) (hcz : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U P.a P.b cL cR ⋯ hcL hcR ε L hε hεone hL) α (u.axialResidual ctx)) (K : Λ → ℕ → I → Set (LocalSignedRequest.Point × ℝ)) : have s := LocalSignedRequest.movingStripData U P.a P.b cL cR ⋯ hcL hcR ε L hε hεone hL; ∀ (q : Fin 2), PeriodizedWaveBounds.UniformLocalJets (HarmonicWaveInteraction.productStrip s) (fun (x : Λ) (x_1 : ℕ) (x_2 : LocalSignedRequest.Point × ℝ) => s.zeta x_2.1) (α - 1) K fun (x : Λ) (n : ℕ) (x_1 : I) (x_2 : LocalSignedRequest.Point × ℝ) => LocalSignedRequest.fullRequest s P coord ctx u n x_2 q

The actual residuals, their support, and their incoming mean classes give the complete copy-uniform request estimate. No request jet is assumed.

One selected reference family supplies the complete signed input

noncomputable def NavierStokes.ActualSignedControl.PreparedChart.copiedMatrix {Λ I D X : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup X] [NormedSpace ℝ X] {F₀ : OutgoingProfile.Profile} {W₀ : NominalProfile.Witness F₀} {H₀ : NominalConeAssembly.Certificate W₀} {ld : ModulatedProfileAssembly.LoopData W₀} {v₀ : ModulatedProfileAssembly.Witness ld} {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} {a : PrimaryGeometryAssembly.Prepared H₀ v₀ upper B r0 N0} (C : PreparedChart H₀ v₀ a D) (hr0 : 0 < r0) (vr vt : TorusInverse.Plane) {s : WeightedClasses.StripData X} {K : Λ → ℕ → I → Set X} (copy : CopyChart s C.native C.weight K) : Λ → I → ℕ → X → Mat2

Copied matrix, defined pointwise by copy.pull (pulseMatrix (PrimaryGeometryAssembly.construction H₀ v₀ a hr0) (preparedPrefactor r0 vr vt) C.coordinate) l n i.

Equations

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

noncomputable def NavierStokes.ActualSignedControl.PreparedChart.copiedTarget {Λ I D X : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup X] [NormedSpace ℝ X] {F₀ : OutgoingProfile.Profile} {W₀ : NominalProfile.Witness F₀} {H₀ : NominalConeAssembly.Certificate W₀} {ld : ModulatedProfileAssembly.LoopData W₀} {v₀ : ModulatedProfileAssembly.Witness ld} {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} {a : PrimaryGeometryAssembly.Prepared H₀ v₀ upper B r0 N0} (C : PreparedChart H₀ v₀ a D) {s : WeightedClasses.StripData X} {K : Λ → ℕ → I → Set X} (copy : CopyChart s C.native C.weight K) (scale : PositiveScale Λ) : Λ → I → ℕ → X → Vec2

Copied target, defined pointwise by scale.value l n ^ 2 • copy.pull C.target l n i x.

Equations

• C.copiedTarget copy scale l i n x = scale.value l n ^ 2 • copy.pull C.target l n i x

noncomputable def NavierStokes.ActualSignedControl.PreparedChart.copiedCoefficients {Λ I D X : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup X] [NormedSpace ℝ X] {F₀ : OutgoingProfile.Profile} {W₀ : NominalProfile.Witness F₀} {H₀ : NominalConeAssembly.Certificate W₀} {ld : ModulatedProfileAssembly.LoopData W₀} {v₀ : ModulatedProfileAssembly.Witness ld} {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} {a : PrimaryGeometryAssembly.Prepared H₀ v₀ upper B r0 N0} (C : PreparedChart H₀ v₀ a D) (hr0 : 0 < r0) (vr vt : TorusInverse.Plane) {s : WeightedClasses.StripData X} {K : Λ → ℕ → I → Set X} (copy : CopyChart s C.native C.weight K) (scale normal clock : PositiveScale Λ) (base : Λ → I → LinearWaveBounds.WaveCoefficients X) (dirs : Λ → I → LinearWaveBounds.GraphDirections X) (request : ℕ → X → Vec2) (j : Fin 2) : Λ → I → LinearWaveBounds.WaveCoefficients X

Copied coefficients, constructed using ReferenceBounds.copiedCoefficients.

Equations

• C.copiedCoefficients hr0 vr vt copy scale normal clock base dirs request j = NavierStokes.ActualSignedControl.ReferenceBounds.copiedCoefficients copy scale normal clock base dirs request j

theorem NavierStokes.ActualSignedControl.exists_actual_signed_control {Λ I D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [Countable Λ] [Nonempty Λ] {F₀ : OutgoingProfile.Profile} {W₀ : NominalProfile.Witness F₀} {H₀ : NominalConeAssembly.Certificate W₀} {ld : ModulatedProfileAssembly.LoopData W₀} {v₀ : ModulatedProfileAssembly.Witness ld} {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H₀ v₀ upper B r0 N0) (hcone : LeadingStressWeights.FullTrueCone v₀) (hr0 : 0 < r0) (vr vt : TorusInverse.Plane) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) : ∃ (N : ℕ) (hN : a.N ≤ N), ∀ (C : PreparedChart H₀ v₀ (a.restrict N hN) D) (s : WeightedClasses.StripData LocalSignedRequest.Point) (K : Λ → ℕ → I → Set (LocalSignedRequest.Point × ℝ)) (copy : CopyChart (HarmonicWaveInteraction.productStrip s) C.native C.weight K) (scale normal clock : PositiveScale Λ) (base : Λ → I → LinearWaveBounds.WaveCoefficients (LocalSignedRequest.Point × ℝ)) (dirs : Λ → I → LinearWaveBounds.GraphDirections (LocalSignedRequest.Point × ℝ)) (P : SignedStressPrimitive.Patch) (coord : ℝ) (ctx : CorrectionState.Context LocalSignedRequest.Point) (u : CorrectionState.State LocalSignedRequest.Point) (β : ℝ) (W : Λ → ℕ → LocalSignedRequest.Point × ℝ → ℝ) (j : Fin 2), (∀ x ∈ s.domain, 0 < s.zeta x) → (∀ (q : Fin 2), WeightedClasses.MeanClass s β fun (n : ℕ) (x : LocalSignedRequest.Point) => LocalSignedRequest.normalizedRequest s P coord ctx u n x q) → (∀ (l : Λ) (n : ℕ), ∀ x ∈ (HarmonicWaveInteraction.productStrip s).domain, 0 ≤ W l n x) → (∀ (l : Λ) (n : ℕ) (i : I), ∀ x ∈ (HarmonicWaveInteraction.productStrip s).domain, x ∈ K l n i → copy.pull (PrimaryCopyBounds.pulseEnvelope (PrimaryGeometryAssembly.construction H₀ v₀ (a.restrict N hN) hr0) C.coordinate j) l n i x ≤ W l n x) → (∀ (l : Λ) (n : ℕ) (i : I), ∀ x ∈ (HarmonicWaveInteraction.productStrip s).domain, x ∈ K l n i → (fun (y : LocalSignedRequest.Point × ℝ) => normal.value l n • copy.pull (phaseNormal (PrimaryGeometryAssembly.construction H₀ v₀ (a.restrict N hN) hr0 j) C.coordinate) l n i y) =ᶠ[nhds x] (base l i).normal (HarmonicWaveInteraction.productStrip s) (dirs l i) n) → (UniformPrimaryWeights.UniformBandBound (HarmonicWaveInteraction.productStrip s) (1 / 2) fun (li : Λ × I) (n : ℕ) => 1 / (base li.1 li.2).frequency n) → Nonempty (SignedCopyBounds.UniformNativeCovariance (HarmonicWaveInteraction.productStrip s) K (C.copiedMatrix hr0 vr vt copy) (C.copiedTarget copy scale)) ∧ (PeriodizedWaveBounds.UniformLocalJets (HarmonicWaveInteraction.productStrip s) (fun (l : Λ) (n : ℕ) (x : LocalSignedRequest.Point × ℝ) => √(s.zeta x.1) * W l n x) (β + 1 / 2) K fun (l : Λ) (n : ℕ) (i : I) => (C.copiedCoefficients hr0 vr vt copy scale normal clock base dirs (LocalSignedRequest.fullRequest s P coord ctx u) j l i).amplitude n) ∧ (PeriodizedWaveBounds.UniformLocalJets (HarmonicWaveInteraction.productStrip s) (fun (l : Λ) (n : ℕ) (x : LocalSignedRequest.Point × ℝ) => √(s.zeta x.1) * W l n x) (β + 1) K fun (l : Λ) (n : ℕ) (i : I) => (C.copiedCoefficients hr0 vr vt copy scale normal clock base dirs (LocalSignedRequest.fullRequest s P coord ctx u) j l i).pressure n) ∧ PeriodizedWaveBounds.UniformLocalJets (HarmonicWaveInteraction.productStrip s) (fun (x : Λ) (x_1 : ℕ) (x_2 : LocalSignedRequest.Point × ℝ) => 1) 0 K (copy.pull fun (L : PrimaryGeometryAssembly.Index W₀ (a.restrict N hN).N) (x : D) => GaussianTailFlat.profile (C.coordinate L x).2)

Starting with an already selected prepared primary, a common tail restriction gives actual uniform native covariance, request-driven signed amplitude/pressure bounds, and the actual cutoff jets. No finished control record, target jet, fundamental jet, or copied request jet is an input.

@[reducible, inline]

abbrev NavierStokes.ActualSignedGeometry.Slow : Type

Slow: an abbreviation for PhaseCalculus.Slow.

Equations

• NavierStokes.ActualSignedGeometry.Slow = NavierStokes.PhaseCalculus.Slow

@[reducible, inline]

abbrev NavierStokes.ActualSignedGeometry.Plane : Type

Plane: an abbreviation for TorusInverse.Plane.

Equations

• NavierStokes.ActualSignedGeometry.Plane = NavierStokes.TorusInverse.Plane

@[reducible, inline]

abbrev NavierStokes.ActualSignedGeometry.Native : Type

Native: an abbreviation for Slow × Plane.

Equations

• NavierStokes.ActualSignedGeometry.Native = (NavierStokes.ActualSignedGeometry.Slow × NavierStokes.ActualSignedGeometry.Plane)

The positive native annulus and the actual pulse coordinate

noncomputable def NavierStokes.ActualSignedGeometry.standardSlowRegion {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) : LocalSignedRequest.SlowRegion (2 * h)

Standard slow region, bundling carrier, isOpen, have, coord_pos and the required compatibility proofs.

Equations

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

@[reducible, inline]

abbrev NavierStokes.ActualSignedGeometry.Label {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) : Type

Label: an abbreviation for PrimaryGeometryAssembly.Index W a.N.

Equations

• NavierStokes.ActualSignedGeometry.Label H v a = NavierStokes.PrimaryGeometryAssembly.Index W a.N

noncomputable def NavierStokes.ActualSignedGeometry.nativeSlow {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) : PrimaryCopyBounds.JetDomain (Label H v a) Slow

Native slow, bundling scale, carrier, isOpen, one_le_scale and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.ActualSignedGeometry.nativeDomain {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) : PrimaryCopyBounds.JetDomain (Label H v a) Native

Native domain, bundling scale, carrier, isOpen, one_le_scale and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.ActualSignedGeometry.pulseCoordinates {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (L : Label H v a) (x : Native) : Slow × ℝ

Pulse coordinates, given by (x.1, x.2.2 / ChartScales.slotLength r0 F.data.h (BaseChartJets.cellBand L)).

Equations

• NavierStokes.ActualSignedGeometry.pulseCoordinates H v a L x = (x.1, x.2.2 / NavierStokes.ChartScales.slotLength r0 F.data.h (NavierStokes.BaseChartJets.cellBand L))

theorem NavierStokes.ActualSignedGeometry.nativeSlow_positive {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (L : Label H v a) {p : Slow} (hp : p ∈ (nativeSlow H v a).carrier L) : p ∈ PositiveRepresentatives.positivePart (PrimaryGeometryAssembly.referenceSet W)

theorem NavierStokes.ActualSignedGeometry.pulseCoordinates_jets {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (hr0 : 0 < r0) : PhaseJetBounds.PolynomialJets (nativeDomain H v a).toDomain (pulseCoordinates H v a)

theorem NavierStokes.ActualSignedGeometry.radialDelta_le_edge {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {r : ℝ} (hr : r ∈ Set.Ioo (PrimaryTargetBounds.leftRadius W) (PrimaryTargetBounds.rightRadius W)) (eta : ℝ) : WeightedRadialPrimitive.delta (WeightedRadialPrimitive.logLength (PrimaryTargetBounds.leftRadius W) (PrimaryTargetBounds.rightRadius W)) (WeightedRadialPrimitive.logPosition (PrimaryTargetBounds.leftRadius W) r) ≤ FinalSlowBase.edgeDistance W (r ^ 2 / 2, eta)

theorem NavierStokes.ActualSignedGeometry.nativeSlow_inverse_edge {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (L : Label H v a) {p : Slow} (hp : p ∈ (nativeSlow H v a).carrier L) : (FinalSlowBase.edgeDistance W (BaseChartJets.normalizedCoordinates F.data.h p).2)⁻¹ ≤ (nativeSlow H v a).growth L p

noncomputable def NavierStokes.ActualSignedGeometry.preparedChart {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (hr0 : 0 < r0) : ActualSignedControl.PreparedChart H v a Native

This is the native chart of the supplied prepared family. All its coordinate, growth, annular and positive-reference fields are proved.

Equations

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

@[simp]

theorem NavierStokes.ActualSignedGeometry.preparedChart_coordinate {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (hr0 : 0 < r0) (L : Label H v a) (x : Native) : (preparedChart H v a hr0).coordinate L x = (x.1, x.2.2 / (PrimaryGeometryAssembly.construction H v a hr0 0).L L)

Uniform comparisons on the actual four-level window

noncomputable def NavierStokes.ActualSignedGeometry.powerBound (exponent : ℝ) : ℝ

Power bound, given by (2 : ℝ) ^ (4 * |exponent|).

Equations

• NavierStokes.ActualSignedGeometry.powerBound exponent = 2 ^ (4 * |exponent|)

theorem NavierStokes.ActualSignedGeometry.powerBound_one (exponent : ℝ) : 1 ≤ powerBound exponent

theorem NavierStokes.ActualSignedGeometry.dyadic_ratioPower (n m : ℕ) (exponent : ℝ) : PhysicalParticularWave.ratioPower (ChartScales.Q n) (ChartScales.Q m) exponent = 2 ^ ((↑m - ↑n) * exponent)

theorem NavierStokes.ActualSignedGeometry.dyadic_ratioPower_le {n m : ℕ} (hnm : n ≤ m + 4) (hmn : m ≤ n + 4) (exponent : ℝ) : PhysicalParticularWave.ratioPower (ChartScales.Q n) (ChartScales.Q m) exponent ≤ powerBound exponent

theorem NavierStokes.ActualSignedGeometry.dyadic_ratioPower_lower {n m : ℕ} (hnm : n ≤ m + 4) (hmn : m ≤ n + 4) (exponent : ℝ) : 1 / powerBound exponent ≤ PhysicalParticularWave.ratioPower (ChartScales.Q n) (ChartScales.Q m) exponent

theorem NavierStokes.ActualSignedGeometry.S_window_le {n m : ℕ} (hn : 1 ≤ n) (hmn : m ≤ n + 4) : ChartScales.S m ≤ 25 * ChartScales.S n

theorem NavierStokes.ActualSignedGeometry.sqrt_S_window {n m : ℕ} (hn : 1 ≤ n) (hm : 1 ≤ m) (hnm : n ≤ m + 4) (hmn : m ≤ n + 4) : 1 / 5 ≤ √(ChartScales.S n) / √(ChartScales.S m) ∧ √(ChartScales.S n) / √(ChartScales.S m) ≤ 5

theorem NavierStokes.ActualSignedGeometry.common_native_gap {h : ℝ} (hh : 0 ≤ h) {index : ℕ → ℕ} {budget : ℕ} (hi : CommonBaseContext.IndexBounds h index budget) {n m : ℕ} (hn : 1 ≤ n) (hm : 1 ≤ m) (hnm : n ≤ m + 4) (hmn : m ≤ n + 4) : ChartScales.nativeIndex h m - index n ≤ budget + SlotColoring.nativeGap h

noncomputable def NavierStokes.ActualSignedGeometry.bandPowerScale {Λ : Type} (chart : ℕ → ℕ) (reference : Λ → ℕ → ℕ) (hnear : ∀ (l : Λ) (n : ℕ), chart n ≤ reference l n + 4 ∧ reference l n ≤ chart n + 4) (exponent : ℝ) : ActualSignedControl.PositiveScale Λ

Band power scale, bundling value, lower, upper, lower_pos and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.ActualSignedGeometry.velocityScale {Λ : Type} (chart : ℕ → ℕ) (reference : Λ → ℕ → ℕ) (hnear : ∀ (l : Λ) (n : ℕ), chart n ≤ reference l n + 4 ∧ reference l n ≤ chart n + 4) (h : ℝ) : ActualSignedControl.PositiveScale Λ

Velocity scale, given by bandPowerScale chart reference hnear (CoordinateAlgebra.A h).

Equations

• NavierStokes.ActualSignedGeometry.velocityScale chart reference hnear h = NavierStokes.ActualSignedGeometry.bandPowerScale chart reference hnear (NavierStokes.CoordinateAlgebra.A h)

noncomputable def NavierStokes.ActualSignedGeometry.clockScale {Λ : Type} (chart : ℕ → ℕ) (reference : Λ → ℕ → ℕ) (hnear : ∀ (l : Λ) (n : ℕ), chart n ≤ reference l n + 4 ∧ reference l n ≤ chart n + 4) (h : ℝ) : ActualSignedControl.PositiveScale Λ

Clock scale, given by bandPowerScale chart reference hnear (CoordinateAlgebra.A h + 1 / 2).

Equations

• NavierStokes.ActualSignedGeometry.clockScale chart reference hnear h = NavierStokes.ActualSignedGeometry.bandPowerScale chart reference hnear (NavierStokes.CoordinateAlgebra.A h + 1 / 2)

@[simp]

theorem NavierStokes.ActualSignedGeometry.velocityScale_value {Λ : Type} (chart : ℕ → ℕ) (reference : Λ → ℕ → ℕ) (hnear : ∀ (l : Λ) (n : ℕ), chart n ≤ reference l n + 4 ∧ reference l n ≤ chart n + 4) (h : ℝ) (l : Λ) (n : ℕ) : (velocityScale chart reference hnear h).value l n = PhysicalParticularWave.velocityWeight h (ChartScales.Q (chart n)) (ChartScales.Q (reference l n))

@[simp]

theorem NavierStokes.ActualSignedGeometry.clockScale_value {Λ : Type} (chart : ℕ → ℕ) (reference : Λ → ℕ → ℕ) (hnear : ∀ (l : Λ) (n : ℕ), chart n ≤ reference l n + 4 ∧ reference l n ≤ chart n + 4) (h : ℝ) (l : Λ) (n : ℕ) : (clockScale chart reference hnear h).value l n = PhysicalParticularWave.clockWeight h (ChartScales.Q (chart n)) (ChartScales.Q (reference l n))

The selected slot, including the periodic clock's padding

noncomputable def NavierStokes.ActualSignedGeometry.slotGeometry {D h : ℝ} {vr vt : Plane} (sys : PartitionedCovariance.SlotSystem D h vr vt) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (l : SlotColoring.Label) (gap : ℕ) : CommonCoverSolve.Geometry

Slot geometry, constructed using CommonCoverClass.bandGeometry.

Equations

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

noncomputable def NavierStokes.ActualSignedGeometry.clockWindow {D h : ℝ} {vr vt : Plane} (sys : PartitionedCovariance.SlotSystem D h vr vt) (m : ℕ) : PeriodicPhaseAssembly.ClockWindow

Clock window, bundling lower, upper, padding, padding_pos.

Equations

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

theorem NavierStokes.ActualSignedGeometry.slotGeometry_basis {D h : ℝ} {vr vt : Plane} (sys : PartitionedCovariance.SlotSystem D h vr vt) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (l : SlotColoring.Label) (gap : ℕ) (z : Plane) : (slotGeometry sys hdet l gap).basis z = z.1 • vr + (ChartScales.timeCoefficient h l.1 * z.2) • vt

theorem NavierStokes.ActualSignedGeometry.clock_outer_in_slot {D h : ℝ} {vr vt : Plane} (sys : PartitionedCovariance.SlotSystem D h vr vt) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (hh : 0 ≤ h) {l : SlotColoring.Label} (hl : 4 ≤ l.1) (gap : ℕ) : (fun (z : TorusInverse.Plane) => (slotGeometry sys hdet l gap).center + (slotGeometry sys hdet l gap).basis z) '' (clockWindow sys l.1).outer ⊆ PartitionedCovariance.slotSet h sys.radius vr vt l

theorem NavierStokes.ActualSignedGeometry.clockWindow_injective {D h : ℝ} {vr vt : Plane} (sys : PartitionedCovariance.SlotSystem D h vr vt) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (hh : 0 ≤ h) {l : SlotColoring.Label} (hl : 4 ≤ l.1) (gap : ℕ) : Set.InjOn TorusAverages.quotientPoint ((fun (z : TorusInverse.Plane) => (slotGeometry sys hdet l gap).center + (slotGeometry sys hdet l gap).basis z) '' (clockWindow sys l.1).outer)

theorem NavierStokes.ActualSignedGeometry.slotGeometry_separated {D h : ℝ} {vr vt : Plane} (sys : PartitionedCovariance.SlotSystem D h vr vt) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (hh : 0 ≤ h) {l : SlotColoring.Label} (hl : 4 ≤ l.1) (gap : ℕ) : WaveEnvelopeTransport.Separated (slotGeometry sys hdet l gap) sys.radius (ChartScales.slotLength sys.radius h l.1)

theorem NavierStokes.ActualSignedGeometry.slotGeometry_argumentCost {D h : ℝ} {vr vt : Plane} (sys : PartitionedCovariance.SlotSystem D h vr vt) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (hh : 0 ≤ h) {l : SlotColoring.Label} (hl : 4 ≤ l.1) {gap budget : ℕ} (hg : gap ≤ budget) : CommonCoverClass.argumentCost (slotGeometry sys hdet l gap) ≤ CommonCoverClass.bandArgumentCost (TorusAverages.slotChart vr vt hdet) budget * ChartScales.S l.1

theorem NavierStokes.ActualSignedGeometry.slotGeometry_common_cost {D h : ℝ} {vr vt : Plane} (sys : PartitionedCovariance.SlotSystem D h vr vt) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (hh : 0 ≤ h) {index : ℕ → ℕ} {budget : ℕ} (hi : CommonBaseContext.IndexBounds h index budget) {n : ℕ} {l : SlotColoring.Label} (hn : 1 ≤ n) (hl : 4 ≤ l.1) (hnl : n ≤ l.1 + 4) (hln : l.1 ≤ n + 4) : CommonCoverClass.argumentCost (slotGeometry sys hdet l (ChartScales.nativeIndex h l.1 - index n)) ≤ 25 * CommonCoverClass.bandArgumentCost (TorusAverages.slotChart vr vt hdet) (budget + SlotColoring.nativeGap h) * ChartScales.S n

The exact physical change of slow variables and the copy affine map

noncomputable def NavierStokes.ActualSignedGeometry.slowChange (h Q Qr : ℝ) : Slow →L[ℝ] Slow

Slow change as an element of Slow →L[ℝ] Slow.

Equations

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

@[simp]

theorem NavierStokes.ActualSignedGeometry.slowChange_apply (h Q Qr : ℝ) (p : Slow) : (slowChange h Q Qr) p = (PhysicalParticularWave.ratioPower Q Qr (1 / 2) * p.1, PhysicalParticularWave.ratioPower Q Qr (CoordinateAlgebra.D h) * p.2.1, PhysicalParticularWave.ratioPower Q Qr 1 * p.2.2)

theorem NavierStokes.ActualSignedGeometry.slowChange_eq_transition {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (h : ℝ) : ⇑(slowChange h Q Qr) = SimilarityHomogeneity.chartTransition h Q Qr

theorem NavierStokes.ActualSignedGeometry.slowChange_time {h Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) {p : Slow} (ht : 0 < p.2.2) : 0 < ((slowChange h Q Qr) p).2.2

theorem NavierStokes.ActualSignedGeometry.slowChange_radius {h Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) {p : Slow} (hr : 0 < p.1) : 0 < ((slowChange h Q Qr) p).1

theorem NavierStokes.ActualSignedGeometry.normalized_inner_slowChange {F : OutgoingProfile.Profile} {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) {p : Slow} (ht : 0 < p.2.2) : (BaseChartJets.normalizedCoordinates F.data.h ((slowChange F.data.h Q Qr) p)).2 = (BaseChartJets.normalizedCoordinates F.data.h p).2

theorem NavierStokes.ActualSignedGeometry.profileRadius_slowChange {F : OutgoingProfile.Profile} {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) {p : Slow} (ht : 0 < p.2.2) (hr : 0 < p.1) : PrimaryTargetBounds.profileRadius F.data.h ((slowChange F.data.h Q Qr) p) = PrimaryTargetBounds.profileRadius F.data.h p

theorem NavierStokes.ActualSignedGeometry.movingWeight_slowChange {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) {p : Slow} (ht : 0 < p.2.2) (hr : 0 < p.1) : PrimaryTargetBounds.movingWeight W ((slowChange F.data.h Q Qr) p) = PrimaryTargetBounds.movingWeight W p

noncomputable def NavierStokes.ActualSignedGeometry.slowChangeCost (h : ℝ) : ℝ

Slow change cost, given by 1 + powerBound (1 / 2) + powerBound (CoordinateAlgebra.D h) + powerBound 1.

Equations

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

theorem NavierStokes.ActualSignedGeometry.slowChangeCost_one (h : ℝ) : 1 ≤ slowChangeCost h

theorem NavierStokes.ActualSignedGeometry.norm_slowChange_le (h : ℝ) {n m : ℕ} (hnm : n ≤ m + 4) (hmn : m ≤ n + 4) : ‖slowChange h (ChartScales.Q n) (ChartScales.Q m)‖ ≤ slowChangeCost h

noncomputable def NavierStokes.ActualSignedGeometry.meanEquiv : Native ≃ₗᵢ[ℝ] LocalSignedRequest.Point

Mean equiv, given by (ParticularWaveBounds.liftAssoc Plane).symm.trans PhysicalResidualTZ.swapSlow.

Equations

• NavierStokes.ActualSignedGeometry.meanEquiv = (NavierStokes.ParticularWaveBounds.liftAssoc NavierStokes.ActualSignedGeometry.Plane).symm.trans NavierStokes.PhysicalResidualTZ.swapSlow

@[simp]

theorem NavierStokes.ActualSignedGeometry.meanEquiv_apply (x : Native) : meanEquiv x = (x.1.1, (x.1.2.2, x.1.2.1), x.2)

noncomputable def NavierStokes.ActualSignedGeometry.viewStrip {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) (chart : ℕ → ℕ) : WeightedClasses.StripData Native

View strip, constructed using ParticularWaveBounds.reindexStrip.

Equations

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

theorem NavierStokes.ActualSignedGeometry.viewStrip_slow {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) (chart : ℕ → ℕ) (n : ℕ) : (viewStrip W U chart).slow n = max 1 (ChartScales.S (chart n))

theorem NavierStokes.ActualSignedGeometry.viewStrip_mem {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) (chart : ℕ → ℕ) (x : Native) : x ∈ (viewStrip W U chart).domain ↔ x.1 ∈ BaseContextAssembly.slowCarrier W U

theorem NavierStokes.ActualSignedGeometry.viewStrip_zeta {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) (chart : ℕ → ℕ) (x : Native) : (viewStrip W U chart).zeta x = PrimaryTargetBounds.movingWeight W x.1

theorem NavierStokes.ActualSignedGeometry.viewStrip_delta {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) (chart : ℕ → ℕ) (x : Native) : (viewStrip W U chart).delta x = WeightedRadialPrimitive.delta (WeightedRadialPrimitive.logLength (PrimaryTargetBounds.leftRadius W) (PrimaryTargetBounds.rightRadius W)) (WeightedRadialPrimitive.logPosition (PrimaryTargetBounds.leftRadius W) (PrimaryTargetBounds.profileRadius F.data.h x.1))

noncomputable def NavierStokes.ActualSignedGeometry.copyPoint {D h : ℝ} {vr vt : Plane} (sys : PartitionedCovariance.SlotSystem D h vr vt) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (l : SlotColoring.Label) (chart common : ℕ) (k : TorusInverse.Frequency) (x : Native) : Native

Copy point as an element of Native.

Equations

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

noncomputable def NavierStokes.ActualSignedGeometry.copyLinear {D h : ℝ} {vr vt : Plane} (sys : PartitionedCovariance.SlotSystem D h vr vt) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (l : SlotColoring.Label) (chart common : ℕ) : Native →L[ℝ] Native

Copy linear as an element of Native →L[ℝ] Native.

Equations

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

theorem NavierStokes.ActualSignedGeometry.copyPoint_affine {D h : ℝ} {vr vt : Plane} (sys : PartitionedCovariance.SlotSystem D h vr vt) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (l : SlotColoring.Label) (chart common : ℕ) (k : TorusInverse.Frequency) (x : Native) : copyPoint sys hdet l chart common k x = (copyLinear sys hdet l chart common) x + copyPoint sys hdet l chart common k 0

theorem NavierStokes.ActualSignedGeometry.norm_copyLinear_le {D h : ℝ} {vr vt : Plane} (sys : PartitionedCovariance.SlotSystem D h vr vt) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (hh : 0 ≤ h) {index : ℕ → ℕ} {budget : ℕ} (hi : CommonBaseContext.IndexBounds h index budget) {n : ℕ} {l : SlotColoring.Label} (hn : 1 ≤ n) (hl : 4 ≤ l.1) (hnl : n ≤ l.1 + 4) (hln : l.1 ≤ n + 4) : ‖copyLinear sys hdet l n (index n)‖ ≤ (slowChangeCost h + 25 * CommonCoverClass.bandArgumentCost (TorusAverages.slotChart vr vt hdet) (budget + SlotColoring.nativeGap h)) * BaseContextAssembly.slowScale n

The exact coefficient and phase-normal scale factors

theorem NavierStokes.ActualSignedGeometry.sqrt_epsilon (h : ℝ) (n : ℕ) : √(ChartScales.epsilon h n) = ChartScales.Q n ^ (h / 2)

theorem NavierStokes.ActualSignedGeometry.sqrt_epsilon_ratio (h : ℝ) (n m : ℕ) : √(ChartScales.epsilon h m) / √(ChartScales.epsilon h n) = PhysicalParticularWave.ratioPower (ChartScales.Q n) (ChartScales.Q m) (-(h / 2))

noncomputable def NavierStokes.ActualSignedGeometry.roundedCarrier (h : ℝ) (n : ℕ) : ℝ

Rounded carrier, given by (ChartScales.carrier h n : ℝ) * Real.sqrt (ChartScales.epsilon h n).

Equations

• NavierStokes.ActualSignedGeometry.roundedCarrier h n = ↑(NavierStokes.ChartScales.carrier h n) * √(NavierStokes.ChartScales.epsilon h n)

theorem NavierStokes.ActualSignedGeometry.roundedCarrier_bounds {h : ℝ} (hh : 0 ≤ h) (n : ℕ) : 1 ≤ roundedCarrier h n ∧ roundedCarrier h n ≤ 2

noncomputable def NavierStokes.ActualSignedGeometry.coefficientScale {Λ : Type} (chart : ℕ → ℕ) (reference : Λ → ℕ → ℕ) (hnear : ∀ (l : Λ) (n : ℕ), chart n ≤ reference l n + 4 ∧ reference l n ≤ chart n + 4) (h : ℝ) : ActualSignedControl.PositiveScale Λ

Coefficient scale, given by (velocityScale chart reference hnear h).mul (bandPowerScale chart reference hnear (-(h / 2))).

Equations

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

theorem NavierStokes.ActualSignedGeometry.coefficientScale_value {Λ : Type} (chart : ℕ → ℕ) (reference : Λ → ℕ → ℕ) (hnear : ∀ (l : Λ) (n : ℕ), chart n ≤ reference l n + 4 ∧ reference l n ≤ chart n + 4) (h : ℝ) (l : Λ) (n : ℕ) : (coefficientScale chart reference hnear h).value l n = PhysicalSignedWave.coefficientScale (ChartScales.epsilon h (chart n)) (ChartScales.epsilon h (reference l n)) (PhysicalParticularWave.velocityWeight h (ChartScales.Q (chart n)) (ChartScales.Q (reference l n)))

noncomputable def NavierStokes.ActualSignedGeometry.carrierRatioScale {Λ : Type} (chart : ℕ → ℕ) (reference : Λ → ℕ → ℕ) {h : ℝ} (hh : 0 ≤ h) : ActualSignedControl.PositiveScale Λ

Carrier ratio scale, bundling value, lower, upper, lower_pos and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.ActualSignedGeometry.normalScale {Λ : Type} (chart : ℕ → ℕ) (reference : Λ → ℕ → ℕ) (hnear : ∀ (l : Λ) (n : ℕ), chart n ≤ reference l n + 4 ∧ reference l n ≤ chart n + 4) {h : ℝ} (hh : 0 ≤ h) : ActualSignedControl.PositiveScale Λ

Normal scale, given by (carrierRatioScale chart reference hh).mul (bandPowerScale chart reference hnear (h / 2 + 1 / 2)).

Equations

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

theorem NavierStokes.ActualSignedGeometry.normalScale_value {Λ : Type} (chart : ℕ → ℕ) (reference : Λ → ℕ → ℕ) (hnear : ∀ (l : Λ) (n : ℕ), chart n ≤ reference l n + 4 ∧ reference l n ≤ chart n + 4) {h : ℝ} (hh : 0 ≤ h) (l : Λ) (n : ℕ) : (normalScale chart reference hnear hh).value l n = PhysicalParticularWave.normalWeight (ChartScales.Q (chart n)) (ChartScales.Q (reference l n)) ↑(ChartScales.carrier h (chart n)) ↑(ChartScales.carrier h (reference l n))

The concrete prepared-copy chart

noncomputable def NavierStokes.ActualSignedGeometry.copyLabel {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) {Λ : Type} (reference : Λ → ℕ → Label H v a) (sign : Λ → ℕ → Fin 2) (l : Λ) (n : ℕ) : SlotColoring.Label

Copy label, given by PartitionedCovariance.signedLabel (PrimaryGeometryAssembly.label W (reference l n)) (sign l n).

Equations

• NavierStokes.ActualSignedGeometry.copyLabel H v a reference sign l n = NavierStokes.PartitionedCovariance.signedLabel (NavierStokes.PrimaryGeometryAssembly.label W (reference l n)) (sign l n)

noncomputable def NavierStokes.ActualSignedGeometry.phaseCell {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) {vr vt : Plane} (sys : PartitionedCovariance.SlotSystem (CoordinateAlgebra.D F.data.h) F.data.h vr vt) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) {Λ : Type} (reference : Λ → ℕ → Label H v a) (chart index : ℕ → ℕ) (sign : Λ → ℕ → Fin 2) (l : Λ) (n : ℕ) (k : TorusInverse.Frequency) : Set Native

Phase cell, constructed using copyPoint.

Equations

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

theorem NavierStokes.ActualSignedGeometry.phaseCell_open {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) {vr vt : Plane} (sys : PartitionedCovariance.SlotSystem (CoordinateAlgebra.D F.data.h) F.data.h vr vt) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) {Λ : Type} (reference : Λ → ℕ → Label H v a) (chart index : ℕ → ℕ) (sign : Λ → ℕ → Fin 2) (l : Λ) (n : ℕ) (k : TorusInverse.Frequency) : IsOpen (phaseCell H v a sys hdet reference chart index sign l n k)

theorem NavierStokes.ActualSignedGeometry.copy_weight_eq {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) {vr vt : Plane} (sys : PartitionedCovariance.SlotSystem (CoordinateAlgebra.D F.data.h) F.data.h vr vt) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) {Λ : Type} (reference : Λ → ℕ → Label H v a) (chart index : ℕ → ℕ) (sign : Λ → ℕ → Fin 2) (hr0 : 0 < r0) (l : Λ) (n : ℕ) (k : TorusInverse.Frequency) {x : Native} (hx : x ∈ (viewStrip W U chart).domain) : (preparedChart H v a hr0).weight (reference l n) (copyPoint sys hdet (copyLabel H v a reference sign l n) (chart n) (index (chart n)) k x) = (viewStrip W U chart).zeta x

theorem NavierStokes.ActualSignedGeometry.copy_growth_le {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) {vr vt : Plane} (sys : PartitionedCovariance.SlotSystem (CoordinateAlgebra.D F.data.h) F.data.h vr vt) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) {Λ : Type} (reference : Λ → ℕ → Label H v a) (chart index : ℕ → ℕ) (sign : Λ → ℕ → Fin 2) (hchart : ∀ (n : ℕ), 1 ≤ chart n) (hnear : ∀ (l : Λ) (n : ℕ), chart n ≤ BaseChartJets.cellBand (reference l n) + 4 ∧ BaseChartJets.cellBand (reference l n) ≤ chart n + 4) (l : Λ) (n : ℕ) (k : TorusInverse.Frequency) {x : Native} (hx : x ∈ (viewStrip W U chart).domain) : (nativeDomain H v a).growth (reference l n) (copyPoint sys hdet (copyLabel H v a reference sign l n) (chart n) (index (chart n)) k x) ≤ 25 * (viewStrip W U chart).growth n x

noncomputable def NavierStokes.ActualSignedGeometry.copyChart {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) {vr vt : Plane} (sys : PartitionedCovariance.SlotSystem (CoordinateAlgebra.D F.data.h) F.data.h vr vt) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) {Λ : Type} (reference : Λ → ℕ → Label H v a) (chart index : ℕ → ℕ) (sign : Λ → ℕ → Fin 2) (hr0 : 0 < r0) (hchart : ∀ (n : ℕ), 1 ≤ chart n) (hnear : ∀ (l : Λ) (n : ℕ), chart n ≤ BaseChartJets.cellBand (reference l n) + 4 ∧ BaseChartJets.cellBand (reference l n) ≤ chart n + 4) {budget : ℕ} (hi : CommonBaseContext.IndexBounds F.data.h index budget) : ActualSignedControl.CopyChart (viewStrip W U chart) (nativeDomain H v a) (preparedChart H v a hr0).weight (phaseCell H v a sys hdet reference chart index sign)

The copy chart is assembled from the actual dyadic and slot maps. The only indexing restrictions are the active four-level window and the chosen common-cover budget; all analytic comparisons are derived.

Equations

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

theorem NavierStokes.ActualSignedGeometry.copyChart_pull {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) {vr vt : Plane} (sys : PartitionedCovariance.SlotSystem (CoordinateAlgebra.D F.data.h) F.data.h vr vt) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) {Λ : Type} (reference : Λ → ℕ → Label H v a) (chart index : ℕ → ℕ) (sign : Λ → ℕ → Fin 2) (hr0 : 0 < r0) (hchart : ∀ (n : ℕ), 1 ≤ chart n) (hnear : ∀ (l : Λ) (n : ℕ), chart n ≤ BaseChartJets.cellBand (reference l n) + 4 ∧ BaseChartJets.cellBand (reference l n) ≤ chart n + 4) {budget : ℕ} (hi : CommonBaseContext.IndexBounds F.data.h index budget) {E : Type} (f : Label H v a → Native → E) (l : Λ) (n : ℕ) (k : TorusInverse.Frequency) (x : Native) : (copyChart H v a sys hdet U reference chart index sign hr0 hchart hnear hi).pull f l n k x = f (reference l n) (copyPoint sys hdet (copyLabel H v a reference sign l n) (chart n) (index (chart n)) k x)

Actual periodic phase normals on the native cores

@[reducible, inline]

abbrev NavierStokes.ActualSignedGeometry.Cylinder : Type

Cylinder: an abbreviation for PhysicalResidualBridge.Cylinder.

Equations

• NavierStokes.ActualSignedGeometry.Cylinder = NavierStokes.PhysicalResidualBridge.Cylinder

noncomputable def NavierStokes.ActualSignedGeometry.radialVector : Plane

Radial vector, given by TorusInverse.vector .radial.

Equations

• NavierStokes.ActualSignedGeometry.radialVector = NavierStokes.TorusInverse.vector NavierStokes.TorusInverse.Direction.radial

noncomputable def NavierStokes.ActualSignedGeometry.temporalVector : Plane

Temporal vector, given by TorusInverse.vector .temporal.

Equations

• NavierStokes.ActualSignedGeometry.temporalVector = NavierStokes.TorusInverse.vector NavierStokes.TorusInverse.Direction.temporal

theorem NavierStokes.ActualSignedGeometry.vectors_det : radialVector.1 * temporalVector.2 - radialVector.2 * temporalVector.1 ≠ 0

noncomputable def NavierStokes.ActualSignedGeometry.slotLinear (g : CommonCoverSolve.Geometry) : Cylinder →L[ℝ] PhaseCalculus.Slot

Slot linear, bundling toFun, map_add, map_smul, cont.

Equations

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

noncomputable def NavierStokes.ActualSignedGeometry.slotCoordinates (g : CommonCoverSolve.Geometry) (k : TorusInverse.Frequency) (x : Cylinder) : PhaseCalculus.Slot

Slot coordinates, given by ((x.1.1, x.1.2.1), (x.2, (g.coordinates k x.1.2.2).2)).

Equations

• NavierStokes.ActualSignedGeometry.slotCoordinates g k x = ((x.1.1, x.1.2.1), x.2, (g.coordinates k x.1.2.2).2)

theorem NavierStokes.ActualSignedGeometry.slotCoordinates_affine (g : CommonCoverSolve.Geometry) (k : TorusInverse.Frequency) : slotCoordinates g k = fun (x : Cylinder) => (slotLinear g) x + ((0, 0), 0, (g.coordinates k 0).2)

theorem NavierStokes.ActualSignedGeometry.slotCoordinates_hasFDerivAt (g : CommonCoverSolve.Geometry) (k : TorusInverse.Frequency) (x : Cylinder) : HasFDerivAt (slotCoordinates g k) (slotLinear g) x

theorem NavierStokes.ActualSignedGeometry.slot_coordinate_radial {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h radialVector temporalVector) (l : SlotColoring.Label) (gap : ℕ) : (slotGeometry sys vectors_det l gap).coordinateLinear radialVector = (ChartScales.Lambda ^ gap, 0)

theorem NavierStokes.ActualSignedGeometry.slot_coordinates_radial {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h radialVector temporalVector) (l : SlotColoring.Label) (gap i : ℕ) (Q : ℝ) (x : Cylinder) : (slotLinear (slotGeometry sys vectors_det l gap)) ((PhysicalResidualBridge.commonGraph Q h i).radial x) = PhaseCalculus.eR

theorem NavierStokes.ActualSignedGeometry.slot_coordinates_angular (g : CommonCoverSolve.Geometry) (x : Cylinder) : (slotLinear g) (PhysicalResidualBridge.ScaledGraph.angular x) = PhaseCalculus.eTheta

theorem NavierStokes.ActualSignedGeometry.slot_coordinates_axial (g : CommonCoverSolve.Geometry) (Q h : ℝ) (i : ℕ) (x : Cylinder) : (slotLinear g) ((PhysicalResidualBridge.commonGraph Q h i).axial x) = Q ^ h • PhaseCalculus.eZ

noncomputable def NavierStokes.ActualSignedGeometry.periodicPhase {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h radialVector temporalVector) (l : SlotColoring.Label) (gap : ℕ) (epsilon p pz x0 : ℝ) (F G : Slow → ℝ) (x : Cylinder) : ℝ

Periodic phase, constructed using PhaseCalculus.phase.

Equations

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

theorem NavierStokes.ActualSignedGeometry.periodicPhase_germ {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h radialVector temporalVector) (hh : 0 ≤ h) {l : SlotColoring.Label} (hl : 4 ≤ l.1) (gap : ℕ) (epsilon p pz x0 : ℝ) (F G : Slow → ℝ) (k : TorusInverse.Frequency) {x : Cylinder} (hx : (slotGeometry sys vectors_det l gap).coordinates k x.1.2.2 ∈ (clockWindow sys l.1).core) : periodicPhase sys l gap epsilon p pz x0 F G =ᶠ[nhds x] PhaseCalculus.phase epsilon p pz x0 F G ∘ slotCoordinates (slotGeometry sys vectors_det l gap) k

theorem NavierStokes.ActualSignedGeometry.nativePhase_normal {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h radialVector temporalVector) (l : SlotColoring.Label) (gap i : ℕ) {Q : ℝ} (hQ : 0 < Q) (p pz x0 : ℝ) (F G : Slow → ℝ) (k : TorusInverse.Frequency) (theta : ℝ) {x : Cylinder} (hF : DifferentiableAt ℝ F (x.1.1, x.1.2.1)) (hG : DifferentiableAt ℝ G (x.1.1, x.1.2.1)) : HarmonicCalculus.phaseNormal PhysicalResidualBridge.ScaledGraph.radius (PhysicalResidualBridge.commonGraph Q h i).radial PhysicalResidualBridge.ScaledGraph.angular (PhysicalResidualBridge.commonGraph Q h i).axial (PhaseCalculus.phase (Q ^ h) p pz x0 F G ∘ slotCoordinates (slotGeometry sys vectors_det l gap) k) x = PhaseCalculus.phaseNormal (Q ^ h) p pz x0 F G ((x.1.1, x.1.2.1), theta, ((slotGeometry sys vectors_det l gap).coordinates k x.1.2.2).2)

theorem NavierStokes.ActualSignedGeometry.periodicPhase_differentiableAt {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h radialVector temporalVector) (l : SlotColoring.Label) (gap : ℕ) (epsilon p pz x0 : ℝ) (F G : Slow → ℝ) {x : Cylinder} (hF : DifferentiableAt ℝ F (x.1.1, x.1.2.1)) (hG : DifferentiableAt ℝ G (x.1.1, x.1.2.1)) : DifferentiableAt ℝ (periodicPhase sys l gap epsilon p pz x0 F G) x

theorem NavierStokes.ActualSignedGeometry.periodicPhase_normal_germ {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h radialVector temporalVector) (hh : 0 ≤ h) {l : SlotColoring.Label} (hl : 4 ≤ l.1) (gap i : ℕ) {Q : ℝ} (hQ : 0 < Q) (p pz x0 : ℝ) (F G : Slow → ℝ) {S : Set Slow} (hS : IsOpen S) (hF : ContDiffOn ℝ (↑⊤) F S) (hG : ContDiffOn ℝ (↑⊤) G S) (k : TorusInverse.Frequency) (theta : ℝ) {x : Cylinder} (hx : (x.1.1, x.1.2.1) ∈ S) (hc : (slotGeometry sys vectors_det l gap).coordinates k x.1.2.2 ∈ (clockWindow sys l.1).core) : (fun (y : Cylinder) => HarmonicCalculus.phaseNormal PhysicalResidualBridge.ScaledGraph.radius (PhysicalResidualBridge.commonGraph Q h i).radial PhysicalResidualBridge.ScaledGraph.angular (PhysicalResidualBridge.commonGraph Q h i).axial (periodicPhase sys l gap (Q ^ h) p pz x0 F G) y) =ᶠ[nhds x] fun (y : Cylinder) => PhaseCalculus.phaseNormal (Q ^ h) p pz x0 F G ((y.1.1, y.1.2.1), theta, ((slotGeometry sys vectors_det l gap).coordinates k y.1.2.2).2)

theorem NavierStokes.ActualSignedGeometry.phase_normal_view_germ {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h radialVector temporalVector) (hh : 0 ≤ h) {l : SlotColoring.Label} (hl : 4 ≤ l.1) (i gap : ℕ) {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (K Kr p pz x0 : ℝ) (F G : Slow → ℝ) {S : Set Slow} (hS : IsOpen S) (hF : ContDiffOn ℝ (↑⊤) F S) (hG : ContDiffOn ℝ (↑⊤) G S) (k : TorusInverse.Frequency) (theta : ℝ) {x : Cylinder} (hxR : 0 < x.1.1) (hxS : (slowChange h Q Qr) (x.1.1, x.1.2.1) ∈ S) (hc : (slotGeometry sys vectors_det l 0).coordinates k ((CommonCoverSolve.coverPower gap) x.1.2.2) ∈ (clockWindow sys l.1).core) : (fun (y : Cylinder) => HarmonicCalculus.phaseNormal PhysicalResidualBridge.ScaledGraph.radius (PhysicalResidualBridge.commonGraph Q h i).radial PhysicalResidualBridge.ScaledGraph.angular (PhysicalResidualBridge.commonGraph Q h i).axial (fun (z : PhysicalResidualBridge.Cylinder) => Kr / K * periodicPhase sys l 0 (Qr ^ h) p pz x0 F G ((PhysicalParticularWave.cylinderChange h Q Qr gap) z)) y) =ᶠ[nhds x] fun (y : Cylinder) => PhysicalParticularWave.normalWeight Q Qr K Kr • PhaseCalculus.phaseNormal (Qr ^ h) p pz x0 F G ((slowChange h Q Qr) (y.1.1, y.1.2.1), theta, ((slotGeometry sys vectors_det l 0).coordinates k ((CommonCoverSolve.coverPower gap) y.1.2.2)).2)

theorem NavierStokes.ActualSignedGeometry.slotGeometry_refine {D h : ℝ} {vr vt : Plane} (sys : PartitionedCovariance.SlotSystem D h vr vt) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (l : SlotColoring.Label) (gap : ℕ) : CopySolveCompatibility.refineGeometry (slotGeometry sys hdet l 0) gap = slotGeometry sys hdet l gap

theorem NavierStokes.ActualSignedGeometry.slot_coordinates_from_zero {D h : ℝ} {vr vt : Plane} (sys : PartitionedCovariance.SlotSystem D h vr vt) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (l : SlotColoring.Label) (gap : ℕ) (k : TorusInverse.Frequency) (Y : Plane) : (slotGeometry sys hdet l 0).coordinates k ((CommonCoverSolve.coverPower gap) Y) = (slotGeometry sys hdet l gap).coordinates k Y

noncomputable def NavierStokes.ActualSignedGeometry.cylinderNative (x : Cylinder) : Native

Cylinder native, given by ((x.1.1, x.1.2.1), x.1.2.2).

Equations

• NavierStokes.ActualSignedGeometry.cylinderNative x = ((x.1.1, x.1.2.1), x.1.2.2)

theorem NavierStokes.ActualSignedGeometry.copyPoint_eq_reference_view {D h : ℝ} {vr vt : Plane} (sys : PartitionedCovariance.SlotSystem D h vr vt) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (l : SlotColoring.Label) (n common : ℕ) (k : TorusInverse.Frequency) (x : Cylinder) : copyPoint sys hdet l n common k (cylinderNative x) = ParticularWaveBounds.nativePoint (slotGeometry sys hdet l 0) k (cylinderNative ((PhysicalParticularWave.cylinderChange h (ChartScales.Q n) (ChartScales.Q l.1) (ChartScales.nativeIndex h l.1 - common)) x))

theorem NavierStokes.ActualSignedGeometry.reference_view_graph {h : ℝ} (l : SlotColoring.Label) (n common : ℕ) (hi : common ≤ ChartScales.nativeIndex h l.1) {z : ProblemStatement.SpaceTime} (hz : 0 < z.2.ofLp 0) : (PhysicalParticularWave.cylinderChange h (ChartScales.Q n) (ChartScales.Q l.1) (ChartScales.nativeIndex h l.1 - common)) ((PhysicalResidualBridge.commonGraph (ChartScales.Q n) h common).map z) = (PhysicalResidualBridge.commonGraph (ChartScales.Q l.1) h (ChartScales.nativeIndex h l.1)).map z

noncomputable def NavierStokes.ActualSignedGeometry.preparedPhase {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B N0 : ℕ} (sys : PartitionedCovariance.SlotSystem (CoordinateAlgebra.D F.data.h) F.data.h radialVector temporalVector) (a : PrimaryGeometryAssembly.Prepared H v upper B sys.radius N0) (j : Fin 2) (L : Label H v a) : Cylinder → ℝ

Prepared phase as an element of Cylinder → ℝ.

Equations

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

noncomputable def NavierStokes.ActualSignedGeometry.preparedViewPhase {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B N0 : ℕ} (sys : PartitionedCovariance.SlotSystem (CoordinateAlgebra.D F.data.h) F.data.h radialVector temporalVector) (a : PrimaryGeometryAssembly.Prepared H v upper B sys.radius N0) (j : Fin 2) (L : Label H v a) (n common : ℕ) : Cylinder → ℝ

Prepared view phase as an element of Cylinder → ℝ.

Equations

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

theorem NavierStokes.ActualSignedGeometry.phaseNormal_pulseCoordinates {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B N0 : ℕ} (sys : PartitionedCovariance.SlotSystem (CoordinateAlgebra.D F.data.h) F.data.h radialVector temporalVector) (a : PrimaryGeometryAssembly.Prepared H v upper B sys.radius N0) (j : Fin 2) (L : Label H v a) (x : Native) : ActualSignedControl.phaseNormal (PrimaryGeometryAssembly.construction H v a ⋯ j) (pulseCoordinates H v a) L x = (PrimaryGeometryAssembly.construction H v a ⋯ j).phase.normal L (x.1, x.2.2)

theorem NavierStokes.ActualSignedGeometry.preparedView_normal_germ {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B N0 : ℕ} (sys : PartitionedCovariance.SlotSystem (CoordinateAlgebra.D F.data.h) F.data.h radialVector temporalVector) (a : PrimaryGeometryAssembly.Prepared H v upper B sys.radius N0) (j : Fin 2) (L : Label H v a) (n common : ℕ) (k : TorusInverse.Frequency) {x : Cylinder} (hcell : copyPoint sys vectors_det (PartitionedCovariance.signedLabel (PrimaryGeometryAssembly.label W L) j) n common k (cylinderNative x) ∈ (nativeDomain H v a).carrier L) : (fun (y : Cylinder) => HarmonicCalculus.phaseNormal PhysicalResidualBridge.ScaledGraph.radius (PhysicalResidualBridge.commonGraph (ChartScales.Q n) F.data.h common).radial PhysicalResidualBridge.ScaledGraph.angular (PhysicalResidualBridge.commonGraph (ChartScales.Q n) F.data.h common).axial (preparedViewPhase H v sys a j L n common) y) =ᶠ[nhds x] fun (y : Cylinder) => PhysicalParticularWave.normalWeight (ChartScales.Q n) (ChartScales.Q (BaseChartJets.cellBand L)) ↑(ChartScales.carrier F.data.h n) ↑(ChartScales.carrier F.data.h (BaseChartJets.cellBand L)) • ActualSignedControl.phaseNormal (PrimaryGeometryAssembly.construction H v a ⋯ j) (pulseCoordinates H v a) L (copyPoint sys vectors_det (PartitionedCovariance.signedLabel (PrimaryGeometryAssembly.label W L) j) n common k (cylinderNative y))

The normal germ required by the signed-copy control theorem is an output for the actual shared prepared phase and physical chart.

Active-pair indexing retains the true fields on inactive labels

theorem NavierStokes.ActualSignedGeometry.uniformLocalJets_of_selected_pairs {Λ I E X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup E] [NormedSpace ℝ E] (s : WeightedClasses.StripData X) (P : Λ → ℕ → Prop) (e : ℕ → { q : Λ × ℕ // P q.1 q.2 }) (he : Function.Surjective e) {w : Λ → ℕ → X → ℝ} {f : Λ → ℕ → I → X → E} {K : Λ → ℕ → I → Set X} {alpha : ℝ} (hactive : ∀ (l : Λ) (n : ℕ) (i : I), ∀ x ∈ s.domain, x ∈ K l n i → P l n) (hj : PeriodizedWaveBounds.UniformLocalJets (UniformPrimaryWeights.reindexedStrip s fun (q : ℕ) => ((↑(e q)).2, ())) (fun (x : Unit) (q : ℕ) (x_1 : X) => w (↑(e q)).1 (↑(e q)).2 x_1) alpha (fun (x : Unit) (q : ℕ) (i : I) => K (↑(e q)).1 (↑(e q)).2 i) fun (x : Unit) (q : ℕ) (i : I) => f (↑(e q)).1 (↑(e q)).2 i) : PeriodizedWaveBounds.UniformLocalJets s w alpha K f

Restricting the index set does not change a field or any of its jets. This transfers a single uniform estimate back to the original labels on their actual active cells. No values or scales are substituted there.

noncomputable def NavierStokes.ActualSignedGeometry.ActivePairCondition {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) {Λ : Type} (reference : Λ → ℕ → Label H v a) (chart : ℕ → ℕ) (l : Λ) (n : ℕ) : Prop

Active pair condition, given by 1 ≤ chart n ∧ chart n ≤ BaseChartJets.cellBand (reference l n) + 4 ∧ BaseChartJets.cellBand (reference l n) ≤ chart n + 4.

Equations

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

@[reducible, inline]

abbrev NavierStokes.ActualSignedGeometry.ActivePair {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) {Λ : Type} (reference : Λ → ℕ → Label H v a) (chart : ℕ → ℕ) : Type

Active pair: an abbreviation for {q : Λ × ℕ // ActivePairCondition H v a reference chart q.1 q.2}.

Equations

• NavierStokes.ActualSignedGeometry.ActivePair H v a reference chart = { q : Λ × ℕ // NavierStokes.ActualSignedGeometry.ActivePairCondition H v a reference chart q.1 q.2 }

noncomputable def NavierStokes.ActualSignedGeometry.activePhaseCell {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) {vr vt : Plane} (sys : PartitionedCovariance.SlotSystem (CoordinateAlgebra.D F.data.h) F.data.h vr vt) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) {Λ : Type} (reference : Λ → ℕ → Label H v a) (chart index : ℕ → ℕ) (sign : Λ → ℕ → Fin 2) (l : Λ) (n : ℕ) (k : TorusInverse.Frequency) : Set Native

Active phase cell, given by {x | ActivePairCondition H v a reference chart l n ∧ x ∈ phaseCell H v a sys hdet reference chart index sign l n k}.

Equations

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

noncomputable def NavierStokes.ActualSignedGeometry.activeEnumeration {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) {Λ : Type} (reference : Λ → ℕ → Label H v a) (chart : ℕ → ℕ) [Countable Λ] [Nonempty (ActivePair H v a reference chart)] : ℕ → ActivePair H v a reference chart

Active enumeration, given by Classical.choose (exists_surjective_nat (ActivePair H v a reference chart)).

Equations

• NavierStokes.ActualSignedGeometry.activeEnumeration H v a reference chart = Classical.choose ⋯

theorem NavierStokes.ActualSignedGeometry.activeEnumeration_surjective {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) {Λ : Type} (reference : Λ → ℕ → Label H v a) (chart : ℕ → ℕ) [Countable Λ] [Nonempty (ActivePair H v a reference chart)] : Function.Surjective (activeEnumeration H v a reference chart)

noncomputable def NavierStokes.ActualSignedGeometry.activeReference {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) {Λ : Type} (reference : Λ → ℕ → Label H v a) (chart : ℕ → ℕ) [Countable Λ] [Nonempty (ActivePair H v a reference chart)] : Unit → (q : ℕ) → Label H v a

Active reference, given by reference (activeEnumeration H v a reference chart q).val.1 (activeEnumeration H v a reference chart q).val.2.

Equations

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

noncomputable def NavierStokes.ActualSignedGeometry.activeChart {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) {Λ : Type} (reference : Λ → ℕ → Label H v a) (chart : ℕ → ℕ) [Countable Λ] [Nonempty (ActivePair H v a reference chart)] (q : ℕ) : ℕ

Active chart, given by chart (activeEnumeration H v a reference chart q).val.2.

Equations

• NavierStokes.ActualSignedGeometry.activeChart H v a reference chart q = chart (↑(NavierStokes.ActualSignedGeometry.activeEnumeration H v a reference chart q)).2

noncomputable def NavierStokes.ActualSignedGeometry.activeSign {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) {Λ : Type} (reference : Λ → ℕ → Label H v a) (chart : ℕ → ℕ) (sign : Λ → ℕ → Fin 2) [Countable Λ] [Nonempty (ActivePair H v a reference chart)] : Unit → (q : ℕ) → Fin 2

Active sign, given by sign (activeEnumeration H v a reference chart q).val.1 (activeEnumeration H v a reference chart q).val.2.

Equations

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

theorem NavierStokes.ActualSignedGeometry.active_near {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) {Λ : Type} (reference : Λ → ℕ → Label H v a) (chart : ℕ → ℕ) [Countable Λ] [Nonempty (ActivePair H v a reference chart)] (q : ℕ) : activeChart H v a reference chart q ≤ BaseChartJets.cellBand (activeReference H v a reference chart () q) + 4 ∧ BaseChartJets.cellBand (activeReference H v a reference chart () q) ≤ activeChart H v a reference chart q + 4

noncomputable def NavierStokes.ActualSignedGeometry.activeCopyChart {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) {vr vt : Plane} (sys : PartitionedCovariance.SlotSystem (CoordinateAlgebra.D F.data.h) F.data.h vr vt) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) {Λ : Type} (reference : Λ → ℕ → Label H v a) (chart index : ℕ → ℕ) (sign : Λ → ℕ → Fin 2) [Countable Λ] [Nonempty (ActivePair H v a reference chart)] (hr0 : 0 < r0) {budget : ℕ} (hi : CommonBaseContext.IndexBounds F.data.h index budget) : ActualSignedControl.CopyChart (viewStrip W U (activeChart H v a reference chart)) (nativeDomain H v a) (preparedChart H v a hr0).weight (phaseCell H v a sys hdet (activeReference H v a reference chart) (activeChart H v a reference chart) index (activeSign H v a reference chart sign))

Every input of this chart is the original active pair. Its uniform bounds are valid without any comparison for inactive label-band pairs.

Equations

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

theorem NavierStokes.ActualSignedGeometry.active_reindexed_strip {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) {Λ : Type} (reference : Λ → ℕ → Label H v a) (chart : ℕ → ℕ) [Countable Λ] [Nonempty (ActivePair H v a reference chart)] : viewStrip W U (activeChart H v a reference chart) = UniformPrimaryWeights.reindexedStrip (viewStrip W U chart) fun (q : ℕ) => ((↑(activeEnumeration H v a reference chart q)).2, ())

The angle coordinate is retained when making harmonic blocks

noncomputable def NavierStokes.ActualSignedGeometry.cylinderNativeLinear : Cylinder →L[ℝ] Native

Cylinder native linear as an element of Cylinder →L[ℝ] Native.

Equations

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

@[simp]

theorem NavierStokes.ActualSignedGeometry.cylinderNativeLinear_apply (x : Cylinder) : cylinderNativeLinear x = cylinderNative x

theorem NavierStokes.ActualSignedGeometry.norm_cylinderNativeLinear : ‖cylinderNativeLinear‖ ≤ 1

noncomputable def NavierStokes.ActualSignedGeometry.cylinderStrip (s : WeightedClasses.StripData Native) : WeightedClasses.StripData Cylinder

Cylinder strip, constructed using ParticularWaveBounds.reindexStrip.

Equations

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

noncomputable def NavierStokes.ActualSignedGeometry.cylinderCopyChart {Λ I i : Type} {s : WeightedClasses.StripData Native} {V : PrimaryCopyBounds.JetDomain i Native} {weight : i → Native → ℝ} {K : Λ → ℕ → I → Set Native} (c : ActualSignedControl.CopyChart s V weight K) : ActualSignedControl.CopyChart (cylinderStrip s) V weight fun (l : Λ) (n : ℕ) (k : I) => cylinderNative ⁻¹' K l n k

Cylinder copy chart, bundling index, linear, shift, maps and the required compatibility proofs.

Equations

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

theorem NavierStokes.ActualSignedGeometry.cylinderCopyChart_pull {Λ I i E : Type} {s : WeightedClasses.StripData Native} {V : PrimaryCopyBounds.JetDomain i Native} {weight : i → Native → ℝ} {K : Λ → ℕ → I → Set Native} (c : ActualSignedControl.CopyChart s V weight K) (f : i → Native → E) (l : Λ) (n : ℕ) (k : I) (x : Cylinder) : (cylinderCopyChart c).pull f l n k x = c.pull f l n k (cylinderNative x)

The actual cutoffs locate every nonzero native contribution

noncomputable def NavierStokes.ActualSignedGeometry.nativeCutoff {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (L : Label H v a) (x : Native) : ℝ

Native cutoff, constructed using SquaredPartition.dyadicProfile.

Equations

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

theorem NavierStokes.ActualSignedGeometry.nativeCutoff_nonzero_mem {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (hr0 : 0 < r0) (L : Label H v a) {x : Native} (ht : 0 < x.1.2.2) (hactive : PrimaryTargetBounds.profileRadius F.data.h x.1 ∈ Set.Ioo (PrimaryTargetBounds.leftRadius W) (PrimaryTargetBounds.rightRadius W)) (hx : nativeCutoff H v a L x ≠ 0) : x ∈ (nativeDomain H v a).carrier L

theorem NavierStokes.ActualSignedGeometry.nativeCutoff_zero_germ_outside_q {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (L : Label H v a) {x : Native} (ht : 0 < x.1.2.2) (hq : SimilarityHomogeneity.chartQ F.data.h x.1 ∉ Set.Icc (1 / 2) 2) : nativeCutoff H v a L =ᶠ[nhds x] fun (x : Native) => 0

theorem NavierStokes.ActualSignedGeometry.nativeCutoff_zero_germ_outside_cell {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (L : Label H v a) {x : Native} (ht : 0 < x.1.2.2) (hx : x.1 ∉ (PrimaryGeometryAssembly.domain W a.N).carrier L) : nativeCutoff H v a L =ᶠ[nhds x] fun (x : Native) => 0

theorem NavierStokes.ActualSignedGeometry.copy_cutoff_mem_phaseCell {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (hr0 : 0 < r0) {vr vt : Plane} (sys : PartitionedCovariance.SlotSystem (CoordinateAlgebra.D F.data.h) F.data.h vr vt) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) {Λ : Type} (reference : Λ → ℕ → Label H v a) (chart index : ℕ → ℕ) (sign : Λ → ℕ → Fin 2) (l : Λ) (n : ℕ) (k : TorusInverse.Frequency) {x : Native} (hx : x ∈ (viewStrip W U chart).domain) (hn : nativeCutoff H v a (reference l n) (copyPoint sys hdet (copyLabel H v a reference sign l n) (chart n) (index (chart n)) k x) ≠ 0) : x ∈ phaseCell H v a sys hdet reference chart index sign l n k

The solver's (R,(T,Z)) parameter ordering

noncomputable def NavierStokes.ActualSignedGeometry.swapParameter : Slow ≃ₗᵢ[ℝ] Slow

Swap parameter, bundling toFun, invFun, left_inv, right_inv and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.ActualSignedGeometry.parameterLinear (h Q Qr : ℝ) : Slow →L[ℝ] Slow

Parameter linear, constructed using swapParameter.toContinuousLinearEquiv.toContinuousLinearMap.comp.

Equations

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

@[simp]

theorem NavierStokes.ActualSignedGeometry.parameterLinear_apply (h Q Qr : ℝ) (x : Slow) : (parameterLinear h Q Qr) x = PhysicalParticularWave.parameterChange h Q Qr x

theorem NavierStokes.ActualSignedGeometry.norm_parameterLinear_le (h : ℝ) {n m : ℕ} (hnm : n ≤ m + 4) (hmn : m ≤ n + 4) : ‖parameterLinear h (ChartScales.Q n) (ChartScales.Q m)‖ ≤ slowChangeCost h