Source envelopes along an entire common-cover slot path

The common-cover envelope is an actual sum over native copies. Injectivity of the padded native rectangle identifies the one copy met by a slot path. The source itself is not assumed periodic on the native torus.

noncomputable def NavierStokes.WaveEnvelopeTransport.rectangle (r L : ℝ) : Set TorusInverse.Plane

The full padded integration rectangle, including both time endpoints.

Equations

• NavierStokes.WaveEnvelopeTransport.rectangle r L = Set.Icc (-r) r ×ˢ Set.Icc 0 L

noncomputable def NavierStokes.WaveEnvelopeTransport.nativeRegion (g : CommonCoverSolve.Geometry) (r L : ℝ) : Set TorusInverse.Plane

Native region, given by (fun z => g.center + g.basis z) '' rectangle r L.

Equations

• NavierStokes.WaveEnvelopeTransport.nativeRegion g r L = (fun (z : NavierStokes.TorusInverse.Plane) => g.center + g.basis z) '' NavierStokes.WaveEnvelopeTransport.rectangle r L

noncomputable def NavierStokes.WaveEnvelopeTransport.Separated (g : CommonCoverSolve.Geometry) (r L : ℝ) : Prop

A geometric injectivity condition, independent of all source fields.

Equations

• NavierStokes.WaveEnvelopeTransport.Separated g r L = Set.InjOn NavierStokes.TorusAverages.quotientPoint (NavierStokes.WaveEnvelopeTransport.nativeRegion g r L)

theorem NavierStokes.WaveEnvelopeTransport.native_coordinate_lattice (g : CommonCoverSolve.Geometry) (k : TorusInverse.Frequency) (Y : TorusInverse.Plane) : g.center + g.basis (g.coordinates k Y) = TorusAverages.latticePoint (-k) + (CommonCoverSolve.coverPower g.gap) Y

theorem NavierStokes.WaveEnvelopeTransport.copy_unique {g : CommonCoverSolve.Geometry} {r L : ℝ} (hsep : Separated g r L) {k l : TorusInverse.Frequency} {Y : TorusInverse.Plane} (hk : g.coordinates k Y ∈ rectangle r L) (hl : g.coordinates l Y ∈ rectangle r L) : k = l

noncomputable def NavierStokes.WaveEnvelopeTransport.copyEnvelope (g : CommonCoverSolve.Geometry) (r L : ℝ) (W : ℝ → ℝ) (Y : TorusInverse.Plane) : ℝ

The envelope of the grouped label on the common cover. The summands are nonzero only on their own native integration rectangles.

Equations

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

theorem NavierStokes.WaveEnvelopeTransport.copyEnvelope_nonneg (g : CommonCoverSolve.Geometry) (r L : ℝ) {W : ℝ → ℝ} (hW : ∀ (s : ℝ), 0 ≤ W s) (Y : TorusInverse.Plane) : 0 ≤ copyEnvelope g r L W Y

theorem NavierStokes.WaveEnvelopeTransport.copyEnvelope_eq_copy {g : CommonCoverSolve.Geometry} {r L : ℝ} (hsep : Separated g r L) (W : ℝ → ℝ) {k : TorusInverse.Frequency} {Y : TorusInverse.Plane} (hk : g.coordinates k Y ∈ rectangle r L) : copyEnvelope g r L W Y = W (g.coordinates k Y).2

theorem NavierStokes.WaveEnvelopeTransport.coordinates_path_in_rectangle (g : CommonCoverSolve.Geometry) (k : TorusInverse.Frequency) (Y : TorusInverse.Plane) {r L s : ℝ} (hξ : (g.coordinates k Y).1 ∈ Set.Icc (-r) r) (hs : s ∈ Set.Icc 0 L) : g.coordinates k (g.path k Y s) ∈ rectangle r L

theorem NavierStokes.WaveEnvelopeTransport.copyEnvelope_path {g : CommonCoverSolve.Geometry} {r L : ℝ} (hsep : Separated g r L) (W : ℝ → ℝ) (k : TorusInverse.Frequency) (Y : TorusInverse.Plane) (hξ : (g.coordinates k Y).1 ∈ Set.Icc (-r) r) {s : ℝ} (hs : s ∈ Set.Icc 0 L) : copyEnvelope g r L W (g.path k Y s) = W s

Exact envelope identification at every integration time, including the entry and exit. No bound at the current point is extrapolated.

theorem NavierStokes.WaveEnvelopeTransport.entire_path_in_rectangle (g : CommonCoverSolve.Geometry) (k : TorusInverse.Frequency) (Y : TorusInverse.Plane) {r L : ℝ} (hξ : (g.coordinates k Y).1 ∈ Set.Icc (-r) r) : Set.MapsTo (g.path k Y) (Set.Icc 0 L) {Z : TorusInverse.Plane | g.coordinates k Z ∈ rectangle r L}

theorem NavierStokes.WaveEnvelopeTransport.path_transverse (g : CommonCoverSolve.Geometry) (k : TorusInverse.Frequency) (Y : TorusInverse.Plane) (s : ℝ) : (g.coordinates k (g.path k Y s)).1 = (g.coordinates k Y).1

theorem NavierStokes.WaveEnvelopeTransport.path_time (g : CommonCoverSolve.Geometry) (k : TorusInverse.Frequency) (Y : TorusInverse.Plane) (s : ℝ) : (g.coordinates k (g.path k Y s)).2 = s

theorem NavierStokes.WaveEnvelopeTransport.source_path_observable {P : Type} {V : Type u_1} (g : CommonCoverSolve.Geometry) (k : TorusInverse.Frequency) (F : P → V) (z : P × TorusInverse.Plane) (s : ℝ) : F (CommonCoverClass.sourceArgument g k (z, s)).1 = F z.1

theorem NavierStokes.WaveEnvelopeTransport.source_path_mem {P : Type} (g : CommonCoverSolve.Geometry) (k : TorusInverse.Frequency) {U : Set P} {z : P × TorusInverse.Plane} (hz : z.1 ∈ U) (s : ℝ) : CommonCoverClass.sourceArgument g k (z, s) ∈ U ×ˢ Set.univ

theorem NavierStokes.WaveEnvelopeTransport.source_path_domain {P : Type} (g : CommonCoverSolve.Geometry) (k : TorusInverse.Frequency) (U : Set P) (r L : ℝ) : Set.MapsTo (CommonCoverClass.sourceArgument g k) ({z : P × TorusInverse.Plane | z.1 ∈ U ∧ (g.coordinates k z.2).1 ∈ Set.Icc (-r) r} ×ˢ Set.Icc 0 L) {z : P × TorusInverse.Plane | z.1 ∈ U ∧ g.coordinates k z.2 ∈ rectangle r L}

theorem NavierStokes.WaveEnvelopeTransport.cutoff_on_path (g : CommonCoverSolve.Geometry) (k : TorusInverse.Frequency) (Y : TorusInverse.Plane) (L s : ℝ) : GaussianTailFlat.slotCutoff L (g.coordinates k (g.path k Y s)).2 = GaussianTailFlat.slotCutoff L s

The actual GaussianTailFlat cutoff is evaluated at the integration time, on the same native copy used to evaluate the source.

theorem NavierStokes.WaveEnvelopeTransport.reference_envelope_on_path {g : CommonCoverSolve.Geometry} {r L : ℝ} (hsep : Separated g r L) (lam u : ℝ) (k : TorusInverse.Frequency) (Y : TorusInverse.Plane) (hξ : (g.coordinates k Y).1 ∈ Set.Icc (-r) r) {s : ℝ} (hs : s ∈ Set.Icc 0 L) : copyEnvelope g r L (GaussianEnvelope.envelope (GaussianEnvelope.referenceRate lam u L) (L / 2)) (g.path k Y s) = GaussianEnvelope.envelope (GaussianEnvelope.referenceRate lam u L) (L / 2) s

theorem NavierStokes.WaveEnvelopeTransport.reference_envelope_path_gaussian {g : CommonCoverSolve.Geometry} {r L lam u : ℝ} (hsep : Separated g r L) (hlam : 0 < lam) (hu : 0 < u) (hL : 0 < L) (k : TorusInverse.Frequency) (Y : TorusInverse.Plane) (hξ : (g.coordinates k Y).1 ∈ Set.Icc (-r) r) {s : ℝ} (hs : s ∈ Set.Icc 0 L) : Real.exp (-(u * GaussianEnvelope.referenceMaxSlope lam u) * (s - L / 2) ^ 2 / (2 * L)) ≤ copyEnvelope g r L (GaussianEnvelope.envelope (GaussianEnvelope.referenceRate lam u L) (L / 2)) (g.path k Y s) ∧ copyEnvelope g r L (GaussianEnvelope.envelope (GaussianEnvelope.referenceRate lam u L) (L / 2)) (g.path k Y s) ≤ Real.exp (-(u * GaussianEnvelope.referenceMinSlope lam u) * (s - L / 2) ^ 2 / (2 * L))

theorem NavierStokes.WaveEnvelopeTransport.separated_bandGeometry (B : TorusInverse.Plane ≃L[ℝ] TorusInverse.Plane) (h : ℝ) (n gap : ℕ) (center : TorusInverse.Plane) {r r0 R : ℝ} (hr : r < R) (hr0 : r0 < R) (hsmall : ‖↑B‖ * R < 1 / 2) : Separated (CommonCoverClass.bandGeometry B h n gap center) r (ChartScales.slotLength r0 h n)

A concrete geometric criterion, uniform in the band and covering gap. After multiplying slot time by ci, the full rectangle has transverse half-width r0, so its injectivity does not deteriorate as L grows.

theorem NavierStokes.WaveEnvelopeTransport.exists_separated_native_rectangle (B : TorusInverse.Plane ≃L[ℝ] TorusInverse.Plane) : ∃ (r : ℝ), 0 < r ∧ ∀ (h : ℝ) (n gap : ℕ) (center : TorusInverse.Plane), Separated (CommonCoverClass.bandGeometry B h n gap center) r (ChartScales.slotLength r h n)

noncomputable def NavierStokes.WaveEnvelopeTransport.copyCell {P : Type} (g : CommonCoverSolve.Geometry) (r L : ℝ) (k : TorusInverse.Frequency) : Set (P × TorusInverse.Plane)

Copy cell, given by {z | g.coordinates k z.2 ∈ rectangle r L}.

Equations

• NavierStokes.WaveEnvelopeTransport.copyCell g r L k = {z : P × NavierStokes.TorusInverse.Plane | g.coordinates k z.2 ∈ NavierStokes.WaveEnvelopeTransport.rectangle r L}

theorem NavierStokes.WaveEnvelopeTransport.copyCell_closed {P : Type} [NormedAddCommGroup P] (g : CommonCoverSolve.Geometry) (r L : ℝ) (k : TorusInverse.Frequency) : IsClosed (copyCell g r L k)

theorem NavierStokes.WaveEnvelopeTransport.copyCell_locallyFinite {P : Type} [NormedAddCommGroup P] (g : CommonCoverSolve.Geometry) (r L : ℝ) : LocallyFinite (copyCell g r L)

noncomputable def NavierStokes.WaveEnvelopeTransport.grouped {P V : Type} [NormedAddCommGroup V] (F : TorusInverse.Frequency → P × TorusInverse.Plane → V) (z : P × TorusInverse.Plane) : V

Coefficients may differ in every native copy. This is an actual sum of common-cover fields, with no substitution of a native-periodic source.

Equations

• NavierStokes.WaveEnvelopeTransport.grouped F z = ∑' (k : NavierStokes.TorusInverse.Frequency), F k z

theorem NavierStokes.WaveEnvelopeTransport.grouped_eventually_eq_copy {P V : Type} [NormedAddCommGroup P] [NormedAddCommGroup V] {g : CommonCoverSolve.Geometry} {r L : ℝ} (hsep : Separated g r L) (F : TorusInverse.Frequency → P × TorusInverse.Plane → V) (hsupport : ∀ (k : TorusInverse.Frequency), Function.support (F k) ⊆ copyCell g r L k) {k : TorusInverse.Frequency} {z : P × TorusInverse.Plane} (hz : z ∈ copyCell g r L k) : grouped F =ᶠ[nhds z] F k

theorem NavierStokes.WaveEnvelopeTransport.grouped_eventually_zero {P V : Type} [NormedAddCommGroup P] [NormedAddCommGroup V] {g : CommonCoverSolve.Geometry} {r L : ℝ} (F : TorusInverse.Frequency → P × TorusInverse.Plane → V) (hsupport : ∀ (k : TorusInverse.Frequency), Function.support (F k) ⊆ copyCell g r L k) {z : P × TorusInverse.Plane} (hz : ∀ (k : TorusInverse.Frequency), z ∉ copyCell g r L k) : grouped F =ᶠ[nhds z] fun (x : P × TorusInverse.Plane) => 0

theorem NavierStokes.WaveEnvelopeTransport.grouped_on_entire_path {P V : Type} [NormedAddCommGroup P] [NormedAddCommGroup V] {g : CommonCoverSolve.Geometry} {r L : ℝ} (hsep : Separated g r L) (F : TorusInverse.Frequency → P × TorusInverse.Plane → V) (hsupport : ∀ (k : TorusInverse.Frequency), Function.support (F k) ⊆ copyCell g r L k) (k : TorusInverse.Frequency) (p : P) (Y : TorusInverse.Plane) (hξ : (g.coordinates k Y).1 ∈ Set.Icc (-r) r) (v : ℝ) : v ∈ Set.Icc 0 L → grouped F (p, g.path k Y v) = F k (p, g.path k Y v)

theorem NavierStokes.WaveEnvelopeTransport.grouped_path_zero_of_transverse_support {P V : Type} [NormedAddCommGroup P] [NormedAddCommGroup V] {g : CommonCoverSolve.Geometry} {r L : ℝ} (hsep : Separated g r L) (F : TorusInverse.Frequency → P × TorusInverse.Plane → V) (hsupport : ∀ (k : TorusInverse.Frequency), Function.support (F k) ⊆ copyCell g r L k) (k : TorusInverse.Frequency) (p : P) (Y : TorusInverse.Plane) (T : Set ℝ) (htransverse : Function.support (F k) ⊆ {z : P × TorusInverse.Plane | (g.coordinates k z.2).1 ∈ T}) (hξ : (g.coordinates k Y).1 ∈ Set.Icc (-r) r) (hξT : (g.coordinates k Y).1 ∉ T) (v : ℝ) : v ∈ Set.Icc 0 L → grouped F (p, g.path k Y v) = 0

A transverse support exclusion for the actual copy coefficient excludes the entire grouped source on the entire integration path.

theorem NavierStokes.WaveEnvelopeTransport.grouped_path_zero_of_slow_support {P V : Type} [NormedAddCommGroup V] (g : CommonCoverSolve.Geometry) (F : TorusInverse.Frequency → P × TorusInverse.Plane → V) (U : Set P) (hsupport : ∀ (k : TorusInverse.Frequency), Function.support (F k) ⊆ {z : P × TorusInverse.Plane | z.1 ∈ U}) (k : TorusInverse.Frequency) {p : P} (hp : p ∉ U) (Y : TorusInverse.Plane) (v : ℝ) : grouped F (p, g.path k Y v) = 0

theorem NavierStokes.WaveEnvelopeTransport.grouped_waveClass {P V : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] (s : WeightedClasses.StripData P) (g : ℕ → CommonCoverSolve.Geometry) (r L : ℕ → ℝ) (hsep : ∀ (n : ℕ), Separated (g n) (r n) (L n)) (W : ℕ → ℝ → ℝ) (hW : ∀ (n : ℕ) (v : ℝ), 0 ≤ W n v) (α : ℝ) (F : ℕ → TorusInverse.Frequency → P × TorusInverse.Plane → V) (hFs : ∀ (n : ℕ) (k : TorusInverse.Frequency), ContDiffOn ℝ (↑⊤) (F n k) (CommonCoverClass.sourceStrip s).domain) (hFsupport : ∀ (n : ℕ) (k : TorusInverse.Frequency), Function.support (F n k) ⊆ copyCell (g n) (r n) (L n) k) (hFjets : ∀ (N : ℕ), ∃ (C : ℝ), 0 ≤ C ∧ ∃ (d : ℕ), ∀ (n : ℕ) (k : TorusInverse.Frequency) (z : P × TorusInverse.Plane), z.1 ∈ s.domain → ∀ j ≤ N, ‖iteratedFDeriv ℝ j (F n k) z‖ ≤ C * s.epsilon n ^ α * s.growth n z.1 ^ d * √(s.zeta z.1) * W n ((g n).coordinates k z.2).2) : WeightedClasses.WaveClass (CommonCoverClass.sourceStrip s) (fun (n : ℕ) (z : P × TorusInverse.Plane) => copyEnvelope (g n) (r n) (L n) (W n) z.2) α fun (n : ℕ) => grouped (F n)

Uniform bounds on the actual supported copy coefficients give the WaveClass of their actual grouped field. Local finiteness and geometric separation justify all derivatives of the sum.

theorem NavierStokes.WaveEnvelopeTransport.waveClass_sourceArgument_bound {P V : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] (s : WeightedClasses.StripData P) (B : TorusInverse.Plane ≃L[ℝ] TorusInverse.Plane) {h : ℝ} (hh : 0 ≤ h) (gapBound : ℕ) (band gap : ℕ → ℕ) (center : ℕ → TorusInverse.Plane) (r L : ℕ → ℝ) (hband : ∀ (n : ℕ), 4 ≤ band n) (hgap : ∀ (n : ℕ), gap n ≤ gapBound) (hslow : ∀ (n : ℕ), s.slow n = ChartScales.S (band n)) (hsep : ∀ (n : ℕ), Separated (CommonCoverClass.bandGeometry B h (band n) (gap n) (center n)) (r n) (L n)) (W : ℕ → ℝ → ℝ) (hW : ∀ (n : ℕ) (v : ℝ), 0 ≤ W n v) {α : ℝ} {f : ℕ → P × TorusInverse.Plane → V} (hf : WeightedClasses.WaveClass (CommonCoverClass.sourceStrip s) (fun (n : ℕ) (z : P × TorusInverse.Plane) => copyEnvelope (CommonCoverClass.bandGeometry B h (band n) (gap n) (center n)) (r n) (L n) (W n) z.2) α f) (N : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∃ (d : ℕ), ∀ (n : ℕ) (k : TorusInverse.Frequency) (z : P × TorusInverse.Plane), z.1 ∈ s.domain → (CommonCoverSolve.Geometry.coordinates (CommonCoverClass.bandGeometry B h (band n) (gap n) (center n)) k z.2).1 ∈ Set.Icc (-r n) (r n) → ∀ v ∈ Set.Icc 0 (L n), ∀ j ≤ N, ‖iteratedFDeriv ℝ j (fun (x : CommonCoverClass.Joint P) => f n (CommonCoverClass.sourceArgument (CommonCoverClass.bandGeometry B h (band n) (gap n) (center n)) k x)) (z, v)‖ ≤ C * s.growth n z.1 ^ d * (s.epsilon n ^ α * √(s.zeta z.1)) * W n v

Full joint derivatives of the actual source along every point of the slot. The inverse-edge factor remains frozen in s.growth n z.1. The source may depend on the common coordinate in any way allowed by its actual WaveClass; native periodicity is not a premise.

theorem NavierStokes.WaveEnvelopeTransport.clm_apply_jet_bound_on {X V H : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup H] [NormedSpace ℝ H] {U : Set X} (hU : IsOpen U) {A : X → V →L[ℝ] H} {f : X → V} (hA : ContDiffOn ℝ (↑⊤) A U) (hf : ContDiffOn ℝ (↑⊤) f U) {x : X} (hx : x ∈ U) (N : ℕ) {C D : ℝ} (hC : 0 ≤ C) (hD : 0 ≤ D) (hAj : ∀ j ≤ N, ‖iteratedFDeriv ℝ j A x‖ ≤ C) (hfj : ∀ j ≤ N, ‖iteratedFDeriv ℝ j f x‖ ≤ D) (j : ℕ) (hj : j ≤ N) : ‖iteratedFDeriv ℝ j (fun (y : X) => (A y) (f y)) x‖ ≤ 2 ^ N * C * D

theorem NavierStokes.WaveEnvelopeTransport.waveClass_forcingAlong_bound {P V H : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup H] [NormedSpace ℝ H] (s : WeightedClasses.StripData P) (B : TorusInverse.Plane ≃L[ℝ] TorusInverse.Plane) {h : ℝ} (hh : 0 ≤ h) (gapBound : ℕ) (band gap : ℕ → ℕ) (center : ℕ → TorusInverse.Plane) (r L : ℕ → ℝ) (hband : ∀ (n : ℕ), 4 ≤ band n) (hgap : ∀ (n : ℕ), gap n ≤ gapBound) (hslow : ∀ (n : ℕ), s.slow n = ChartScales.S (band n)) (hsep : ∀ (n : ℕ), Separated (CommonCoverClass.bandGeometry B h (band n) (gap n) (center n)) (r n) (L n)) (W : ℕ → ℝ → ℝ) (hW : ∀ (n : ℕ) (v : ℝ), 0 ≤ W n v) (I : ℕ → Set ℝ) (hI : ∀ (n : ℕ), IsOpen (I n)) (hLI : ∀ (n : ℕ), Set.Icc 0 (L n) ⊆ I n) (d : ℕ → CommonCoverSolve.LinearData P V H) {α : ℝ} (hf : WeightedClasses.WaveClass (CommonCoverClass.sourceStrip s) (fun (n : ℕ) (z : P × TorusInverse.Plane) => copyEnvelope (CommonCoverClass.bandGeometry B h (band n) (gap n) (center n)) (r n) (L n) (W n) z.2) α fun (n : ℕ) => (d n).source) (hB : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (d n).forcingMap (s.domain ×ˢ Set.univ ×ˢ I n)) (hBj : ∀ (N : ℕ), ∃ (C : ℝ), 0 ≤ C ∧ ∃ (p : ℕ), ∀ (n : ℕ), ∀ x ∈ s.domain, ∀ ξ ∈ Set.Icc (-r n) (r n), ∀ v ∈ Set.Icc 0 (L n), ∀ j ≤ N, ‖iteratedFDeriv ℝ j (d n).forcingMap (x, ξ, v)‖ ≤ C * s.growth n x ^ p) (N : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∃ (p : ℕ), ∀ (n : ℕ) (k : TorusInverse.Frequency) (z : P × TorusInverse.Plane), z.1 ∈ s.domain → (CommonCoverSolve.Geometry.coordinates (CommonCoverClass.bandGeometry B h (band n) (gap n) (center n)) k z.2).1 ∈ Set.Icc (-r n) (r n) → ∀ v ∈ Set.Icc 0 (L n), ∀ j ≤ N, ‖iteratedFDeriv ℝ j ((d n).forcingAlong (CommonCoverClass.bandGeometry B h (band n) (gap n) (center n)) k) (z, v)‖ ≤ C * s.growth n z.1 ^ p * (s.epsilon n ^ α * √(s.zeta z.1)) * W n v

The actual projected source operator along the whole integration path. Only native forcing-map jets and the original common-cover source class are inputs. Both affine pullbacks and their Leibniz product are differentiated.

theorem NavierStokes.WaveEnvelopeTransport.native_source_path {P : Type} (h : ℝ) (n gap : ℕ) (center : TorusInverse.Plane) (k : TorusInverse.Frequency) (z : P × TorusInverse.Plane) (v : ℝ) : CommonCoverClass.sourceArgument (CommonCoverClass.bandGeometry CommonCoverClass.nativeBasis h n gap center) k (z, v) = (z.1, z.2 + (CommonCoverSolve.coverPower gap).symm ((ChartScales.timeCoefficient h n * (v - (CommonCoverSolve.Geometry.coordinates (CommonCoverClass.bandGeometry CommonCoverClass.nativeBasis h n gap center) k z.2).2)) • PhysicalGraphBounds.timeDirection))

The path used by the source estimate is the manuscript's literal path, with its actual time coefficient and inverse integer covering.

theorem NavierStokes.WaveEnvelopeTransport.anchoredSolve_zero_of_grouped_transverse_support {P V H : Type} [NormedAddCommGroup P] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup H] [NormedSpace ℝ H] [CompleteSpace H] (d : CommonCoverSolve.LinearData P V H) {g : CommonCoverSolve.Geometry} {r L : ℝ} (hL : 0 ≤ L) (hsep : Separated g r L) (F : TorusInverse.Frequency → P × TorusInverse.Plane → V) (hsource : d.source = grouped F) (hsupport : ∀ (k : TorusInverse.Frequency), Function.support (F k) ⊆ copyCell g r L k) (k : TorusInverse.Frequency) (p : P) (Y : TorusInverse.Plane) (T : Set ℝ) (htransverse : Function.support (F k) ⊆ {z : P × TorusInverse.Plane | (g.coordinates k z.2).1 ∈ T}) (hξ : (g.coordinates k Y).1 ∈ Set.Icc (-r) r) (hξT : (g.coordinates k Y).1 ∉ T) (v : ℝ) : d.anchoredSolve g hL k (p, Y) v = 0

The constructed zero-entry solve vanishes where the grouped source has no transverse support, using its values along every integration time.