Preservation of the actual closed carrier of a harmonic label

The support argument uses the whole native Volterra path. A pointwise zero of the source is not used as a zero of its particular solution. The Gaussian clock cutoff supplies the temporal boundary of the carrier; the source supplies its slow and transverse boundaries.

theorem NavierStokes.LabelSupportPreservation.corrected_zero_of_raw {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : PeriodizedWaveBounds.CopyData D I) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) {n : ℕ} {i : I} {x : D} (ha : a.amplitude n i =ᶠ[nhds x] fun (x : D) => 0) : (a.corrected s d i).amplitude n =ᶠ[nhds x] fun (x : D) => 0

A zero raw amplitude gives a zero corrected amplitude as a germ, including every derivative in the literal curl correction.

theorem NavierStokes.LabelSupportPreservation.localized_pressure_zero_of_raw {D I : Type} [NormedAddCommGroup D] (a : PeriodizedWaveBounds.CopyData D I) {n : ℕ} {i : I} {x : D} (hp : a.pressure n i =ᶠ[nhds x] fun (x : D) => 0) : (a.localized i).pressure n =ᶠ[nhds x] fun (x : D) => 0

theorem NavierStokes.LabelSupportPreservation.common_zero_germs_of_native {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : PeriodizedWaveBounds.CopyData D I) (K : PeriodizedWaveBounds.Cells D I) (hs : ∀ (n : ℕ) (i : I), Function.support (a.cutoff n i) ⊆ K.carrier n i) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) {n : ℕ} {x : D} (hf : a.source n =ᶠ[nhds x] fun (x : D) => 0) (hnative : ∀ (i : I), x ∈ K.carrier n i → (a.cutoff n i =ᶠ[nhds x] fun (x : D) => 0) ∨ (a.amplitude n i =ᶠ[nhds x] fun (x : D) => 0) ∧ a.pressure n i =ᶠ[nhds x] fun (x : D) => 0) : ((a.commonCorrected s d).amplitude n =ᶠ[nhds x] fun (x : D) => 0) ∧ (a.common.pressure n =ᶠ[nhds x] fun (x : D) => 0) ∧ a.globalGaussian d n =ᶠ[nhds x] fun (x : D) => 0

The uncovered source is retained. Either a zero cutoff or two zero raw fields in every covering copy suffices for the three assembled fields.

theorem NavierStokes.LabelSupportPreservation.nativeCutoff_source_time_zero_germ {r L c : ℝ} (hr : 0 < r) (hL : 0 < L) (hc : 0 < c) {z : TorusInverse.Plane} (hz : z.2 ∉ Set.Icc (L / c / 6) (5 * (L / c) / 6)) : ActualGaussianCoverage.nativeCutoff r L hr hL c =ᶠ[nhds z] fun (x : TorusInverse.Plane) => 0

Outside the closed Gaussian source window, the actual cutoff is identically zero on a neighborhood, even inside the padded clock cell.

theorem NavierStokes.LabelSupportPreservation.complexCopyPressure_zero_germ {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (t : CommonCoverSolve.TangentData P ProblemStatement.Space) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (k : TorusInverse.Frequency) (frequency : ℝ) {f : P × TorusInverse.Plane → HarmonicCalculus.ComplexVector} {x : P × TorusInverse.Plane} (heta : (g.coordinates k x.2).2 ∈ Set.Ioo a b) (hf : ∀ v ∈ Set.Icc a b, f =ᶠ[nhds (x.1, g.path k x.2 v)] fun (x : P × TorusInverse.Plane) => 0) : ParticularWaveBounds.complexCopyPressure t f g hab k frequency =ᶠ[nhds x] fun (x : P × TorusInverse.Plane) => 0

The actual projected particular pressure also vanishes near a path of zero source. The time coordinate is in the open integration interval.

theorem NavierStokes.LabelSupportPreservation.data_pressure_zero_germ {Label P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : PhaseJetBounds.Domain (Label × ℕ) PhaseCalculus.Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (clock : ActualSignedControl.PositiveScale Label) (reference : Label → ℕ → CommonCoverSolve.Geometry) (gap : Label → ℕ → ℕ) (r : Label → ℕ → ℝ) (hr : ∀ (l : Label) (n : ℕ), 0 < r l n) (base : Label → LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)) (tangent : Label → ℕ → CommonCoverSolve.TangentData (P × ℝ) ProblemStatement.Space) (ctx : CorrectionState.Context (P × TorusInverse.Plane)) (u : CorrectionState.State (P × TorusInverse.Plane)) (b : Label → CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (G A : Label → HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)) (j : ℤ) (s : WeightedClasses.StripData P) (S : Label → ℕ → Set P) (hS : ∀ (l : Label) (n : ℕ), IsClosed (S l n)) (hsupport : ∀ (l : Label), HarmonicSourceSupport.InputSupportOn (s.domain ×ˢ Set.univ) (ActualGaussianCoverage.sourceRegions F clock reference gap r S l) (b l) (G l) (A l)) (l : Label) (n : ℕ) (k : TorusInverse.Frequency) {x : (P × ℝ) × TorusInverse.Plane} (hx : x.1.1 ∈ s.domain) (htime : ((ScaledActualParticularControl.geometry reference gap clock l n).coordinates k x.2).2 ∈ Set.Ioo 0 (ScaledActualParticularControl.length F clock l n)) (hpath : ∀ v ∈ Set.Icc 0 (ScaledActualParticularControl.length F clock l n), (x.1.1, (ScaledActualParticularControl.geometry reference gap clock l n).path k x.2 v) ∉ ActualGaussianCoverage.sourceRegions F clock reference gap r S l n) : (ActualGaussianCoverage.data F clock reference gap r hr base tangent ctx u b G A j l).pressure n k =ᶠ[nhds x] fun (x : (P × ℝ) × TorusInverse.Plane) => 0

theorem NavierStokes.LabelSupportPreservation.data_native_zero_alternative {Label P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : PhaseJetBounds.Domain (Label × ℕ) PhaseCalculus.Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (clock : ActualSignedControl.PositiveScale Label) (reference : Label → ℕ → CommonCoverSolve.Geometry) (gap : Label → ℕ → ℕ) (r : Label → ℕ → ℝ) (hr : ∀ (l : Label) (n : ℕ), 0 < r l n) (base : Label → LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)) (tangent : Label → ℕ → CommonCoverSolve.TangentData (P × ℝ) ProblemStatement.Space) (ctx : CorrectionState.Context (P × TorusInverse.Plane)) (u : CorrectionState.State (P × TorusInverse.Plane)) (b : Label → CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (G A : Label → HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)) (j : ℤ) (s : WeightedClasses.StripData P) (S : Label → ℕ → Set P) (hS : ∀ (l : Label) (n : ℕ), IsClosed (S l n)) (hsupport : ∀ (l : Label), HarmonicSourceSupport.InputSupportOn (s.domain ×ˢ Set.univ) (ActualGaussianCoverage.sourceRegions F clock reference gap r S l) (b l) (G l) (A l)) (hinj : ∀ (l : Label) (n : ℕ), Set.InjOn TorusAverages.quotientPoint ((fun (z : TorusInverse.Plane) => (reference l n).center + (reference l n).basis z) '' (ActualGaussianCoverage.referenceWindow (r l n) (F.L (l, n)) ⋯ ⋯).outer)) (l : Label) (n : ℕ) (k : TorusInverse.Frequency) {x : (P × ℝ) × TorusInverse.Plane} (hx : x.1.1 ∈ s.domain) (hk : x ∈ PeriodizedWaveBounds.nativeCell (ScaledActualParticularControl.geometry reference gap clock l n) (ActualGaussianCoverage.outerFamily F clock r l n) k) (hn : (x.1.1, x.2) ∉ ActualGaussianCoverage.sourceRegions F clock reference gap r S l n) : ((ActualGaussianCoverage.data F clock reference gap r hr base tangent ctx u b G A j l).cutoff n k =ᶠ[nhds x] fun (x : (P × ℝ) × TorusInverse.Plane) => 0) ∨ ((ActualGaussianCoverage.data F clock reference gap r hr base tangent ctx u b G A j l).amplitude n k =ᶠ[nhds x] fun (x : (P × ℝ) × TorusInverse.Plane) => 0) ∧ (ActualGaussianCoverage.data F clock reference gap r hr base tangent ctx u b G A j l).pressure n k =ᶠ[nhds x] fun (x : (P × ℝ) × TorusInverse.Plane) => 0

The exact particular solve retains the smaller source cell, even though its raw cutoff is supported on a larger padded cell.

theorem NavierStokes.LabelSupportPreservation.particular_zero_germs {Label P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : PhaseJetBounds.Domain (Label × ℕ) PhaseCalculus.Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (clock : ActualSignedControl.PositiveScale Label) (reference : Label → ℕ → CommonCoverSolve.Geometry) (gap : Label → ℕ → ℕ) (r : Label → ℕ → ℝ) (hr : ∀ (l : Label) (n : ℕ), 0 < r l n) (base : Label → LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)) (tangent : Label → ℕ → CommonCoverSolve.TangentData (P × ℝ) ProblemStatement.Space) (ctx : CorrectionState.Context (P × TorusInverse.Plane)) (u : CorrectionState.State (P × TorusInverse.Plane)) (b : Label → CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (G A : Label → HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)) (j : ℤ) (s : WeightedClasses.StripData P) (S : Label → ℕ → Set P) (hS : ∀ (l : Label) (n : ℕ), IsClosed (S l n)) (hsupport : ∀ (l : Label), HarmonicSourceSupport.InputSupportOn (s.domain ×ˢ Set.univ) (ActualGaussianCoverage.sourceRegions F clock reference gap r S l) (b l) (G l) (A l)) (hinj : ∀ (l : Label) (n : ℕ), Set.InjOn TorusAverages.quotientPoint ((fun (z : TorusInverse.Plane) => (reference l n).center + (reference l n).basis z) '' (ActualGaussianCoverage.referenceWindow (r l n) (F.L (l, n)) ⋯ ⋯).outer)) (outStrip : WeightedClasses.StripData ((P × ℝ) × TorusInverse.Plane)) (d : LinearWaveBounds.GraphDirections ((P × ℝ) × TorusInverse.Plane)) (l : Label) (n : ℕ) {x : (P × ℝ) × TorusInverse.Plane} (hx : x.1.1 ∈ s.domain) (hn : (x.1.1, x.2) ∉ ActualGaussianCoverage.sourceRegions F clock reference gap r S l n) : (((ActualGaussianCoverage.data F clock reference gap r hr base tangent ctx u b G A j l).commonCorrected outStrip d).amplitude n =ᶠ[nhds x] fun (x : (P × ℝ) × TorusInverse.Plane) => 0) ∧ ((ActualGaussianCoverage.data F clock reference gap r hr base tangent ctx u b G A j l).common.pressure n =ᶠ[nhds x] fun (x : (P × ℝ) × TorusInverse.Plane) => 0) ∧ (ActualGaussianCoverage.data F clock reference gap r hr base tangent ctx u b G A j l).globalGaussian d n =ᶠ[nhds x] fun (x : (P × ℝ) × TorusInverse.Plane) => 0

All three literal particular output fields have zero germs off the incoming label carrier. This is independent of every numerical jet bound.

noncomputable def NavierStokes.LabelSupportPreservation.signedCopyData {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (base : LinearWaveBounds.WaveCoefficients D) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) (matrix : I → ℕ → D → SignedWaveUpdate.Mat2) (target : I → ℕ → D → SignedWaveUpdate.Vec2) (request : ℕ → D → SignedWaveUpdate.Vec2) (mask : I → ℕ → D → ℝ) (fundamental normalMotion : I → ℕ → D → ProblemStatement.Space) (action : I → ℕ → D → ProblemStatement.Space →L[ℝ] ProblemStatement.Space) (cutoff : I → ℕ → D → ℝ) (column : Fin 2) : PeriodizedWaveBounds.CopyData D I

The same copy data as the signed update: the inverse-quotient amplitude, its projected homogeneous pressure, and zero inhomogeneous source.

Equations

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

theorem NavierStokes.LabelSupportPreservation.signed_raw_zero_of_mask {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (base : LinearWaveBounds.WaveCoefficients D) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) (matrix : I → ℕ → D → SignedWaveUpdate.Mat2) (target : I → ℕ → D → SignedWaveUpdate.Vec2) (request : ℕ → D → SignedWaveUpdate.Vec2) (mask : I → ℕ → D → ℝ) (fundamental normalMotion : I → ℕ → D → ProblemStatement.Space) (action : I → ℕ → D → ProblemStatement.Space →L[ℝ] ProblemStatement.Space) (cutoff : I → ℕ → D → ℝ) (column : Fin 2) (n : ℕ) (i : I) (x : D) (hm : mask i n x = 0) : (signedCopyData base s d matrix target request mask fundamental normalMotion action cutoff column).amplitude n i x = 0 ∧ (signedCopyData base s d matrix target request mask fundamental normalMotion action cutoff column).pressure n i x = 0

theorem NavierStokes.LabelSupportPreservation.signed_zero_germs_of_mask_germs {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (base : LinearWaveBounds.WaveCoefficients D) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) (matrix : I → ℕ → D → SignedWaveUpdate.Mat2) (target : I → ℕ → D → SignedWaveUpdate.Vec2) (request : ℕ → D → SignedWaveUpdate.Vec2) (mask : I → ℕ → D → ℝ) (fundamental normalMotion : I → ℕ → D → ProblemStatement.Space) (action : I → ℕ → D → ProblemStatement.Space →L[ℝ] ProblemStatement.Space) (cutoff : I → ℕ → D → ℝ) (column : Fin 2) (K : PeriodizedWaveBounds.Cells D I) (hcutoff : ∀ (n : ℕ) (i : I), Function.support (cutoff i n) ⊆ K.carrier n i) {n : ℕ} {x : D} (hm : ∀ (i : I), mask i n =ᶠ[nhds x] fun (x : D) => 0) : (((signedCopyData base s d matrix target request mask fundamental normalMotion action cutoff column).commonCorrected s d).amplitude n =ᶠ[nhds x] fun (x : D) => 0) ∧ ((signedCopyData base s d matrix target request mask fundamental normalMotion action cutoff column).common.pressure n =ᶠ[nhds x] fun (x : D) => 0) ∧ (signedCopyData base s d matrix target request mask fundamental normalMotion action cutoff column).globalGaussian d n =ᶠ[nhds x] fun (x : D) => 0

theorem NavierStokes.LabelSupportPreservation.zero_germ_of_local_support {D E : Type} [NormedAddCommGroup D] [Zero E] {U K : Set D} (hU : IsOpen U) (hK : IsClosed K) {f : D → E} (hs : U ∩ Function.support f ⊆ K) {x : D} (hx : x ∈ U) (hn : x ∉ K) : f =ᶠ[nhds x] fun (x : D) => 0

Relative support on an open physical domain gives ambient zero germs outside a closed carrier. No off-domain totalization is constrained.

theorem NavierStokes.LabelSupportPreservation.pair_input_support {D : Type} {U K : Set D} (j : ℤ) {f : D → ℂ} (hf : ∀ x ∈ U, x ∉ K → f x = 0) : HarmonicSourceSupport.NonzeroSupportedOn U K (HarmonicResidual.realCoefficients (ErrorHarmonics.conjugatePair j f))

theorem NavierStokes.LabelSupportPreservation.modeBlock_inputSupport {D : Type} {U : Set D} {K : ℕ → Set D} (j : ℤ) (frequency : ℕ → ℝ) (phase : ℕ → D → ℝ) (angularFrequency : ℕ → ℤ) {v g : ℕ → D → HarmonicCalculus.ComplexVector} {p : ℕ → D → ℂ} (hv : ∀ (n : ℕ), ∀ x ∈ U, x ∉ K n → v n x = 0) (hp : ∀ (n : ℕ), ∀ x ∈ U, x ∉ K n → p n x = 0) (hg : ∀ (n : ℕ), ∀ x ∈ U, x ∉ K n → g n x = 0) : HarmonicSourceSupport.InputSupportOn U K (ParticularWaveAssembly.modeBlock j frequency phase angularFrequency v p) (ParticularWaveAssembly.modeBlock j frequency phase angularFrequency g fun (x : ℕ) (x_1 : D) => 0).velocity 0

A coefficient assembly needs only the literal amplitude values at the zero-angle section. It needs no global angular independence premise.

theorem NavierStokes.LabelSupportPreservation.inputSupport_addBlock {D : Type} {U : Set D} {K : ℕ → Set D} {a b : CorrectionState.HarmonicBlock D} {G H A : HarmonicResidual.BlockCoefficients D} (ha : HarmonicSourceSupport.InputSupportOn U K a G A) (hb : HarmonicSourceSupport.InputSupportOn U K b H 0) : HarmonicSourceSupport.InputSupportOn U K (HarmonicWaveInteraction.addBlock a b) (G + H) A

The actual carrier-retaining update preserves the very same support set; in particular, axisymmetric aliases are not added to a label.

theorem NavierStokes.LabelSupportPreservation.inputSupport_two_updates {D : Type} {U : Set D} {K : ℕ → Set D} {a b c : CorrectionState.HarmonicBlock D} {G H J A : HarmonicResidual.BlockCoefficients D} (ha : HarmonicSourceSupport.InputSupportOn U K a G A) (hb : HarmonicSourceSupport.InputSupportOn U K b H 0) (hc : HarmonicSourceSupport.InputSupportOn U K c J 0) : HarmonicSourceSupport.InputSupportOn U K (HarmonicWaveInteraction.addBlock (HarmonicWaveInteraction.addBlock a b) c) (G + H + J) A

theorem NavierStokes.LabelSupportPreservation.real_supported_sum {D ι : Type} {U K : Set D} (L : Finset ι) (f : ι → HarmonicFields.Coefficients D) (hf : ∀ l ∈ L, HarmonicSourceSupport.NonzeroSupportedOn U K (HarmonicResidual.realCoefficients (f l))) : HarmonicSourceSupport.NonzeroSupportedOn U K (HarmonicResidual.realCoefficients (∑ l ∈ L, f l))

theorem NavierStokes.LabelSupportPreservation.inputSupport_sumBlock {D ι : Type} {U : Set D} {K : ℕ → Set D} (L : Finset ι) (frequency : ℕ → ℝ) (phase : ℕ → D → ℝ) (angularFrequency : ℕ → ℤ) (blocks : ι → CorrectionState.HarmonicBlock D) (gaussians : ι → HarmonicResidual.BlockCoefficients D) (hs : ∀ l ∈ L, HarmonicSourceSupport.InputSupportOn U K (blocks l) (gaussians l) 0) : HarmonicSourceSupport.InputSupportOn U K (ErrorHarmonics.sumBlock L frequency phase angularFrequency blocks) (fun (n : ℕ) (i : Fin 3) => ∑ l ∈ L, gaussians l n i) 0

theorem NavierStokes.LabelSupportPreservation.assembledBlock_inputSupport {D : Type} {U : Set D} {K : ℕ → Set D} (N : ℕ) (frequency : ℕ → ℝ) (phase : ℕ → D → ℝ) (angularFrequency : ℕ → ℤ) {v g : ℤ → ℕ → D → HarmonicCalculus.ComplexVector} {p : ℤ → ℕ → D → ℂ} (hv : ∀ j ∈ ParticularWaveAssembly.modes N, ∀ (n : ℕ), ∀ x ∈ U, x ∉ K n → v j n x = 0) (hp : ∀ j ∈ ParticularWaveAssembly.modes N, ∀ (n : ℕ), ∀ x ∈ U, x ∉ K n → p j n x = 0) (hg : ∀ j ∈ ParticularWaveAssembly.modes N, ∀ (n : ℕ), ∀ x ∈ U, x ∉ K n → g j n x = 0) : HarmonicSourceSupport.InputSupportOn U K (ParticularWaveAssembly.assembledBlock N frequency phase angularFrequency v p) (ParticularWaveAssembly.assembledBlock N frequency phase angularFrequency g fun (x : ℤ) (x_1 : ℕ) (x_2 : D) => 0).velocity 0

theorem NavierStokes.LabelSupportPreservation.blockOfCoefficients_inputSupport {D : Type} {U : Set D} {K : ℕ → Set D} (a : LinearWaveBounds.WaveCoefficients (D × ℝ)) (angularFrequency : ℕ → ℤ) {g : ℕ → D × ℝ → HarmonicCalculus.ComplexVector} (hv : ∀ (n : ℕ), ∀ x ∈ U, x ∉ K n → a.amplitude n (x, 0) = 0) (hp : ∀ (n : ℕ), ∀ x ∈ U, x ∉ K n → a.pressure n (x, 0) = 0) (hg : ∀ (n : ℕ), ∀ x ∈ U, x ∉ K n → g n (x, 0) = 0) : HarmonicSourceSupport.InputSupportOn U K (SignedWaveUpdate.blockOfCoefficients a angularFrequency) (SignedWaveUpdate.coefficientBlock a.frequency (fun (n : ℕ) (x : D) => a.phase n (x, 0)) angularFrequency (fun (n : ℕ) (x : D) => g n (x, 0)) fun (x : ℕ) (x_1 : D) => 0).velocity 0

theorem NavierStokes.LabelSupportPreservation.particular_mode_inputSupport {Label P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : PhaseJetBounds.Domain (Label × ℕ) PhaseCalculus.Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (clock : ActualSignedControl.PositiveScale Label) (reference : Label → ℕ → CommonCoverSolve.Geometry) (gap : Label → ℕ → ℕ) (r : Label → ℕ → ℝ) (hr : ∀ (l : Label) (n : ℕ), 0 < r l n) (base : Label → LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)) (tangent : Label → ℕ → CommonCoverSolve.TangentData (P × ℝ) ProblemStatement.Space) (ctx : CorrectionState.Context (P × TorusInverse.Plane)) (u : CorrectionState.State (P × TorusInverse.Plane)) (b : Label → CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (G A : Label → HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)) (s : WeightedClasses.StripData P) (S : Label → ℕ → Set P) (hS : ∀ (l : Label) (n : ℕ), IsClosed (S l n)) (hsupport : ∀ (l : Label), HarmonicSourceSupport.InputSupportOn (s.domain ×ˢ Set.univ) (ActualGaussianCoverage.sourceRegions F clock reference gap r S l) (b l) (G l) (A l)) (hinj : ∀ (l : Label) (n : ℕ), Set.InjOn TorusAverages.quotientPoint ((fun (z : TorusInverse.Plane) => (reference l n).center + (reference l n).basis z) '' (ActualGaussianCoverage.referenceWindow (r l n) (F.L (l, n)) ⋯ ⋯).outer)) (outStrip : WeightedClasses.StripData ((P × ℝ) × TorusInverse.Plane)) (d : LinearWaveBounds.GraphDirections ((P × ℝ) × TorusInverse.Plane)) (j : ℤ) (l : Label) : HarmonicSourceSupport.InputSupportOn (s.domain ×ˢ Set.univ) (ActualGaussianCoverage.sourceRegions F clock reference gap r S l) (ParticularWaveAssembly.nativeModeBlock j (b l) ((ActualGaussianCoverage.data F clock reference gap r hr base tangent ctx u b G A j l).commonCorrected outStrip d)) (ParticularWaveAssembly.nativeModeBlock j (b l) (have __src := base l; { radius := __src.radius, radialBase := __src.radialBase, frequencyBase := __src.frequencyBase, axialBase := __src.axialBase, phase := __src.phase, amplitude := (ActualGaussianCoverage.data F clock reference gap r hr base tangent ctx u b G A j l).globalGaussian d, pressure := fun (x : ℕ) (x_1 : (P × ℝ) × TorusInverse.Plane) => 0, frequency := __src.frequency })).velocity 0

A single actual particular mode, with its actual Gaussian error, has the same carrier as its incoming label.

theorem NavierStokes.LabelSupportPreservation.particular_assembled_inputSupport {Label P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {D : PhaseJetBounds.Domain (Label × ℕ) PhaseCalculus.Slow} (F : PrimaryPulseBounds.PhaseConstruction D) (clock : ActualSignedControl.PositiveScale Label) (reference : Label → ℕ → CommonCoverSolve.Geometry) (gap : Label → ℕ → ℕ) (r : Label → ℕ → ℝ) (hr : ∀ (l : Label) (n : ℕ), 0 < r l n) (base : Label → LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)) (tangent : Label → ℕ → CommonCoverSolve.TangentData (P × ℝ) ProblemStatement.Space) (ctx : CorrectionState.Context (P × TorusInverse.Plane)) (u : CorrectionState.State (P × TorusInverse.Plane)) (b : Label → CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (G A : Label → HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)) (s : WeightedClasses.StripData P) (S : Label → ℕ → Set P) (hS : ∀ (l : Label) (n : ℕ), IsClosed (S l n)) (hsupport : ∀ (l : Label), HarmonicSourceSupport.InputSupportOn (s.domain ×ˢ Set.univ) (ActualGaussianCoverage.sourceRegions F clock reference gap r S l) (b l) (G l) (A l)) (hinj : ∀ (l : Label) (n : ℕ), Set.InjOn TorusAverages.quotientPoint ((fun (z : TorusInverse.Plane) => (reference l n).center + (reference l n).basis z) '' (ActualGaussianCoverage.referenceWindow (r l n) (F.L (l, n)) ⋯ ⋯).outer)) (outStrip : WeightedClasses.StripData ((P × ℝ) × TorusInverse.Plane)) (d : LinearWaveBounds.GraphDirections ((P × ℝ) × TorusInverse.Plane)) (N : ℕ) (l : Label) : HarmonicSourceSupport.InputSupportOn (s.domain ×ˢ Set.univ) (ActualGaussianCoverage.sourceRegions F clock reference gap r S l) (ErrorHarmonics.sumBlock (ParticularWaveAssembly.modes N) (b l).frequency (b l).phase (b l).angularFrequency fun (j : ℤ) => ParticularWaveAssembly.nativeModeBlock j (b l) ((ActualGaussianCoverage.data F clock reference gap r hr base tangent ctx u b G A j l).commonCorrected outStrip d)) (fun (n : ℕ) (i : Fin 3) => ∑ j ∈ ParticularWaveAssembly.modes N, (ParticularWaveAssembly.nativeModeBlock j (b l) (have __src := base l; { radius := __src.radius, radialBase := __src.radialBase, frequencyBase := __src.frequencyBase, axialBase := __src.axialBase, phase := __src.phase, amplitude := (ActualGaussianCoverage.data F clock reference gap r hr base tangent ctx u b G A j l).globalGaussian d, pressure := fun (x : ℕ) (x_1 : (P × ℝ) × TorusInverse.Plane) => 0, frequency := __src.frequency })).velocity n i) 0

Finite reassembly of all signed particular modes retains the fixed label carrier, with no growth or derivative estimate as an input.

theorem NavierStokes.LabelSupportPreservation.signed_inputSupport {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (base : LinearWaveBounds.WaveCoefficients (D × ℝ)) (s : WeightedClasses.StripData (D × ℝ)) (d : LinearWaveBounds.GraphDirections (D × ℝ)) (matrix : I → ℕ → D × ℝ → SignedWaveUpdate.Mat2) (target : I → ℕ → D × ℝ → SignedWaveUpdate.Vec2) (request : ℕ → D × ℝ → SignedWaveUpdate.Vec2) (mask : I → ℕ → D × ℝ → ℝ) (fundamental normalMotion : I → ℕ → D × ℝ → ProblemStatement.Space) (action : I → ℕ → D × ℝ → ProblemStatement.Space →L[ℝ] ProblemStatement.Space) (cutoff : I → ℕ → D × ℝ → ℝ) (column : Fin 2) (outer : PeriodizedWaveBounds.Cells (D × ℝ) I) (hcutoff : ∀ (n : ℕ) (i : I), Function.support (cutoff i n) ⊆ outer.carrier n i) {U : Set D} {K : ℕ → Set D} (hU : IsOpen U) (hK : ∀ (n : ℕ), IsClosed (K n)) (hmask : ∀ (n : ℕ) (i : I), U ×ˢ Set.univ ∩ Function.support (mask i n) ⊆ Prod.fst ⁻¹' K n) (angularFrequency : ℕ → ℤ) : HarmonicSourceSupport.InputSupportOn U K (SignedWaveUpdate.blockOfCoefficients ((signedCopyData base s d matrix target request mask fundamental normalMotion action cutoff column).commonCorrected s d) angularFrequency) (SignedWaveUpdate.coefficientBlock base.frequency (fun (n : ℕ) (x : D) => base.phase n (x, 0)) angularFrequency (fun (n : ℕ) (x : D) => (signedCopyData base s d matrix target request mask fundamental normalMotion action cutoff column).globalGaussian d n (x, 0)) fun (x : ℕ) (x_1 : D) => 0).velocity 0

Local support of the actual signed masks supplies the new block's support. Mask support is the only hypothesis on the inverse quotient, fundamental, and projected pressure; their numerical size is immaterial.

theorem NavierStokes.LabelSupportPreservation.transported_mask_support {P Q : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup Q] [NormedSpace ℝ Q] (χ : P →L[ℝ] Q) (g : CommonCoverSolve.Geometry) (k : TorusInverse.Frequency) {S : Set Q} {r L c : ℝ} (hc : 0 < c) {mask : Q × TorusInverse.Plane → ℝ} (hm : Function.support mask ⊆ S ×ˢ ActualGaussianCoverage.sourceCell r L 1) : (Function.support fun (x : P × TorusInverse.Plane) => mask (χ x.1, CopySolveCompatibility.nativeTimeMap 0 c (g.coordinates k x.2))) ⊆ ActualGaussianCoverage.sourceRegion (⇑χ ⁻¹' S) g r L c

Clock transport of a native mask keeps the actual source window. The primitive mask may contain all radial and dyadic slow cutoffs.

theorem NavierStokes.LabelSupportPreservation.transported_carrier_closed {P Q : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup Q] [NormedSpace ℝ Q] (χ : P →L[ℝ] Q) (g : CommonCoverSolve.Geometry) {S : Set Q} (hS : IsClosed S) (r L c : ℝ) : IsClosed (ActualGaussianCoverage.sourceRegion (⇑χ ⁻¹' S) g r L c)

The slow pullback and the locally finite native union form one closed carrier. This is the closure used by the next residual-source calculation.

theorem NavierStokes.LabelSupportPreservation.transported_mask_tsupport {P Q : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup Q] [NormedSpace ℝ Q] (χ : P →L[ℝ] Q) (g : CommonCoverSolve.Geometry) (k : TorusInverse.Frequency) {S : Set Q} (hS : IsClosed S) {r L c : ℝ} (hc : 0 < c) {mask : Q × TorusInverse.Plane → ℝ} (hm : Function.support mask ⊆ S ×ˢ ActualGaussianCoverage.sourceCell r L 1) : (tsupport fun (x : P × TorusInverse.Plane) => mask (χ x.1, CopySolveCompatibility.nativeTimeMap 0 c (g.coordinates k x.2))) ⊆ ActualGaussianCoverage.sourceRegion (⇑χ ⁻¹' S) g r L c

theorem NavierStokes.LabelSupportPreservation.transported_mask_zero_germ {P Q : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup Q] [NormedSpace ℝ Q] (χ : P →L[ℝ] Q) (g : CommonCoverSolve.Geometry) (k : TorusInverse.Frequency) {S : Set Q} (hS : IsClosed S) {r L c : ℝ} (hc : 0 < c) {mask : Q × TorusInverse.Plane → ℝ} (hm : Function.support mask ⊆ S ×ˢ ActualGaussianCoverage.sourceCell r L 1) {x : P × TorusInverse.Plane} (hx : x ∉ ActualGaussianCoverage.sourceRegion (⇑χ ⁻¹' S) g r L c) : (fun (y : P × TorusInverse.Plane) => mask (χ y.1, CopySolveCompatibility.nativeTimeMap 0 c (g.coordinates k y.2))) =ᶠ[nhds x] fun (x : P × TorusInverse.Plane) => 0