Assembly of the actual primary tangent field

The native vector pulse, its integer periodization and covering, and its complex harmonic use the same PairData as the covariance calculation. The exact curl correction remains a separate field.

@[reducible, inline]

abbrev NavierStokes.PrimaryFieldAssembly.Vector : Type

Vector: an abbreviation for Fin 3 → ℝ.

Equations

• NavierStokes.PrimaryFieldAssembly.Vector = (Fin 3 → ℝ)

@[reducible, inline]

abbrev NavierStokes.PrimaryFieldAssembly.SignedIndex : Type

Signed index: an abbreviation for UnsignedLabel × Fin 2.

Equations

• NavierStokes.PrimaryFieldAssembly.SignedIndex = (NavierStokes.PartitionedCovariance.UnsignedLabel × Fin 2)

noncomputable def NavierStokes.PrimaryFieldAssembly.pulseVector (P : PartitionedCovariance.Pulse) (r : ℝ) (z : PartitionedCovariance.Plane) : Vector

The three components of one literal native pulse.

Equations

• NavierStokes.PrimaryFieldAssembly.pulseVector P r z i = Fin.cases (P.radialProfile r z) (fun (i : Fin 2) => P.tangentProfile r i z) i

@[simp]

theorem NavierStokes.PrimaryFieldAssembly.pulseVector_zero (P : PartitionedCovariance.Pulse) (r : ℝ) (z : PartitionedCovariance.Plane) : pulseVector P r z 0 = P.radialProfile r z

@[simp]

theorem NavierStokes.PrimaryFieldAssembly.pulseVector_succ (P : PartitionedCovariance.Pulse) (r : ℝ) (z : PartitionedCovariance.Plane) (i : Fin 2) : pulseVector P r z i.succ = P.tangentProfile r i z

noncomputable def NavierStokes.PrimaryFieldAssembly.nativeVector {D h : ℝ} {vr vt : PartitionedCovariance.Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {U : PartitionedCovariance.UnsignedLabel} (P : PartitionedCovariance.PairData sys U) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (j : Fin 2) : PartitionedCovariance.Plane → Vector

The vector is placed at the actual signed slot center, with exactly the native chart and transverse stretch used in PairData.rawRadial.

Equations

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

@[simp]

theorem NavierStokes.PrimaryFieldAssembly.nativeVector_zero {D h : ℝ} {vr vt : PartitionedCovariance.Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {U : PartitionedCovariance.UnsignedLabel} (P : PartitionedCovariance.PairData sys U) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (j : Fin 2) (Y : PartitionedCovariance.Plane) : nativeVector P hdet j Y 0 = P.rawRadial hdet j Y

@[simp]

theorem NavierStokes.PrimaryFieldAssembly.nativeVector_succ {D h : ℝ} {vr vt : PartitionedCovariance.Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {U : PartitionedCovariance.UnsignedLabel} (P : PartitionedCovariance.PairData sys U) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (j : Fin 2) (Y : PartitionedCovariance.Plane) (i : Fin 2) : nativeVector P hdet j Y i.succ = P.rawTangent hdet j i Y

theorem NavierStokes.PrimaryFieldAssembly.nativeVector_compact {D h : ℝ} {vr vt : PartitionedCovariance.Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {U : PartitionedCovariance.UnsignedLabel} (P : PartitionedCovariance.PairData sys U) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (j : Fin 2) : HasCompactSupport (nativeVector P hdet j)

theorem NavierStokes.PrimaryFieldAssembly.periodize_apply {f : PartitionedCovariance.Plane → Vector} (hf : HasCompactSupport f) (Y : PartitionedCovariance.Plane) (i : Fin 3) : TorusAverages.periodize f Y i = TorusAverages.periodize (fun (z : TorusInverse.Plane) => f z i) Y

Evaluation commutes with the actual lattice sum because its support is finite at the evaluation point.

noncomputable def NavierStokes.PrimaryFieldAssembly.coveredVector {D h : ℝ} {vr vt : PartitionedCovariance.Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {U : PartitionedCovariance.UnsignedLabel} (P : PartitionedCovariance.PairData sys U) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (j : Fin 2) (Y : PartitionedCovariance.Plane) : Vector

The covering is the same integer linear map as the slot construction.

Equations

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

@[simp]

theorem NavierStokes.PrimaryFieldAssembly.coveredVector_zero {D h : ℝ} {vr vt : PartitionedCovariance.Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {U : PartitionedCovariance.UnsignedLabel} (P : PartitionedCovariance.PairData sys U) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (j : Fin 2) (Y : PartitionedCovariance.Plane) : coveredVector P hdet j Y 0 = PartitionedCovariance.covered (SlotColoring.nativeIndex h U.1) (P.rawRadial hdet j) Y

@[simp]

theorem NavierStokes.PrimaryFieldAssembly.coveredVector_succ {D h : ℝ} {vr vt : PartitionedCovariance.Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {U : PartitionedCovariance.UnsignedLabel} (P : PartitionedCovariance.PairData sys U) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (j : Fin 2) (Y : PartitionedCovariance.Plane) (i : Fin 2) : coveredVector P hdet j Y i.succ = PartitionedCovariance.covered (SlotColoring.nativeIndex h U.1) (P.rawTangent hdet j i) Y

noncomputable def NavierStokes.PrimaryFieldAssembly.slotAmplitude {D h : ℝ} {vr vt : PartitionedCovariance.Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {U : PartitionedCovariance.UnsignedLabel} (P : PartitionedCovariance.PairData sys U) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (outer ε : ℝ) (T : PartitionedCovariance.Vec2) (q : ℝ) (x : SlotColoring.Position) (j : Fin 2) (Y : PartitionedCovariance.Plane) : HarmonicCalculus.ComplexVector

The square roots, signed-label mask, and physical outer factor are literal; no fresh choice of amplitudes is made when assembling the field.

Equations

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

noncomputable def NavierStokes.PrimaryFieldAssembly.slotPhase {D h : ℝ} {vr vt : PartitionedCovariance.Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {U : PartitionedCovariance.UnsignedLabel} (P : PartitionedCovariance.PairData sys U) (j : Fin 2) (z : PartitionedCovariance.Plane × ℝ) : ℝ

Slot phase, given by (P.modes j : ℝ) * z.2 + P.phases j z.1.

Equations

• NavierStokes.PrimaryFieldAssembly.slotPhase P j z = ↑(P.modes j) * z.2 + P.phases j z.1

noncomputable def NavierStokes.PrimaryFieldAssembly.slotVelocity {D h : ℝ} {vr vt : PartitionedCovariance.Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {U : PartitionedCovariance.UnsignedLabel} (P : PartitionedCovariance.PairData sys U) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (outer ε : ℝ) (T : PartitionedCovariance.Vec2) (q : ℝ) (x : SlotColoring.Position) (j : Fin 2) (Y : PartitionedCovariance.Plane) (θ : ℝ) : Vector

Real part of the actual complex harmonic carrying the periodized vector pulse. Frequency one here records the full phase; mode_identification below also accepts a frequency kept separately from its phase.

Equations

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

theorem NavierStokes.PrimaryFieldAssembly.real_vectorMode {X : Type u_1} (κ : ℝ) (Φ : X → ℝ) (a : X → Vector) (x : X) (i : Fin 3) : (HarmonicCalculus.vectorMode κ Φ (fun (z : X) (j : Fin 3) => ↑(a z j)) x i).re = a x i * Real.cos (κ * Φ x)

theorem NavierStokes.PrimaryFieldAssembly.slotVelocity_formula {D h : ℝ} {vr vt : PartitionedCovariance.Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {U : PartitionedCovariance.UnsignedLabel} (P : PartitionedCovariance.PairData sys U) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (outer ε : ℝ) (T : PartitionedCovariance.Vec2) (q : ℝ) (x : SlotColoring.Position) (j : Fin 2) (Y : PartitionedCovariance.Plane) (θ : ℝ) (i : Fin 3) : slotVelocity P hdet outer ε T q x j Y θ i = outer * PartitionedCovariance.amplitude ε (PartitionedCovariance.mask D U q x) P.matrix T j * coveredVector P hdet j Y i * Real.cos (↑(P.modes j) * θ + P.phases j Y)

@[simp]

theorem NavierStokes.PrimaryFieldAssembly.slotVelocity_zero {D h : ℝ} {vr vt : PartitionedCovariance.Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {U : PartitionedCovariance.UnsignedLabel} (P : PartitionedCovariance.PairData sys U) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (outer ε : ℝ) (T : PartitionedCovariance.Vec2) (q : ℝ) (x : SlotColoring.Position) (j : Fin 2) (Y : PartitionedCovariance.Plane) (θ : ℝ) : slotVelocity P hdet outer ε T q x j Y θ 0 = P.radialWave hdet outer ε T q x j Y θ

@[simp]

theorem NavierStokes.PrimaryFieldAssembly.slotVelocity_succ {D h : ℝ} {vr vt : PartitionedCovariance.Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {U : PartitionedCovariance.UnsignedLabel} (P : PartitionedCovariance.PairData sys U) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (outer ε : ℝ) (T : PartitionedCovariance.Vec2) (q : ℝ) (x : SlotColoring.Position) (j : Fin 2) (Y : PartitionedCovariance.Plane) (θ : ℝ) (i : Fin 2) : slotVelocity P hdet outer ε T q x j Y θ i.succ = P.tangentWave hdet outer ε T q x j i Y θ

theorem NavierStokes.PrimaryFieldAssembly.slotVelocity_mask_zero {D h : ℝ} {vr vt : PartitionedCovariance.Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {U : PartitionedCovariance.UnsignedLabel} (P : PartitionedCovariance.PairData sys U) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (outer ε : ℝ) (T : PartitionedCovariance.Vec2) (q : ℝ) (x : SlotColoring.Position) (hm : PartitionedCovariance.mask D U q x = 0) (j : Fin 2) (Y : PartitionedCovariance.Plane) (θ : ℝ) : slotVelocity P hdet outer ε T q x j Y θ = 0

theorem NavierStokes.PrimaryFieldAssembly.finite_active_slots (D : ℝ) (N : ℕ) {q : ℝ} (hq : 0 < q) (x : SlotColoring.Position) : ∃ (F : Finset SignedIndex), ∀ a ∉ F, PartitionedCovariance.mask D (PartitionedCovariance.tailLabel N a.1) q x = 0

The same finite set of signed labels works for all auxiliary points and all angles at a positive physical point.

noncomputable def NavierStokes.PrimaryFieldAssembly.principalField {D h : ℝ} {vr vt : PartitionedCovariance.Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {N : ℕ} (P : (U : PartitionedCovariance.UnsignedLabel) → PartitionedCovariance.PairData sys (PartitionedCovariance.tailLabel N U)) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (outer ε : PartitionedCovariance.UnsignedLabel → ℝ) (T : PartitionedCovariance.UnsignedLabel → PartitionedCovariance.Vec2) (q : ℝ) (x : SlotColoring.Position) (Y : PartitionedCovariance.Plane) (θ : ℝ) : Vector

Principal field, given by ∑ᶠ a : SignedIndex, slotVelocity (P a.1) hdet (outer a.1) (ε a.1) (T a.1) q x a.2 Y θ.

Equations

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

theorem NavierStokes.PrimaryFieldAssembly.principalField_finite {D h : ℝ} {vr vt : PartitionedCovariance.Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {N : ℕ} (P : (U : PartitionedCovariance.UnsignedLabel) → PartitionedCovariance.PairData sys (PartitionedCovariance.tailLabel N U)) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (outer ε : PartitionedCovariance.UnsignedLabel → ℝ) (T : PartitionedCovariance.UnsignedLabel → PartitionedCovariance.Vec2) {q : ℝ} (hq : 0 < q) (x : SlotColoring.Position) : ∃ (F : Finset SignedIndex), ∀ (Y : PartitionedCovariance.Plane) (θ : ℝ), principalField P hdet outer ε T q x Y θ = ∑ a ∈ F, slotVelocity (P a.1) hdet (outer a.1) (ε a.1) (T a.1) q x a.2 Y θ

theorem NavierStokes.PrimaryFieldAssembly.principalField_apply {D h : ℝ} {vr vt : PartitionedCovariance.Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {N : ℕ} (P : (U : PartitionedCovariance.UnsignedLabel) → PartitionedCovariance.PairData sys (PartitionedCovariance.tailLabel N U)) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (outer ε : PartitionedCovariance.UnsignedLabel → ℝ) (T : PartitionedCovariance.UnsignedLabel → PartitionedCovariance.Vec2) {q : ℝ} (hq : 0 < q) (x : SlotColoring.Position) (Y : PartitionedCovariance.Plane) (θ : ℝ) (i : Fin 3) : principalField P hdet outer ε T q x Y θ i = ∑ᶠ (a : SignedIndex), slotVelocity (P a.1) hdet (outer a.1) (ε a.1) (T a.1) q x a.2 Y θ i

theorem NavierStokes.PrimaryFieldAssembly.principalField_components {D h : ℝ} {vr vt : PartitionedCovariance.Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {N : ℕ} (P : (U : PartitionedCovariance.UnsignedLabel) → PartitionedCovariance.PairData sys (PartitionedCovariance.tailLabel N U)) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (outer ε : PartitionedCovariance.UnsignedLabel → ℝ) (T : PartitionedCovariance.UnsignedLabel → PartitionedCovariance.Vec2) {q : ℝ} (hq : 0 < q) (x : SlotColoring.Position) (Y : PartitionedCovariance.Plane) (θ : ℝ) : principalField P hdet outer ε T q x Y θ 0 = PartitionedCovariance.assembledRadial P hdet outer ε T q x Y θ ∧ ∀ (i : Fin 2), principalField P hdet outer ε T q x Y θ i.succ = PartitionedCovariance.assembledTangent P hdet outer ε T q x i Y θ

theorem NavierStokes.PrimaryFieldAssembly.physical_principal_covariance {D h : ℝ} {vr vt : PartitionedCovariance.Plane} (sys : PartitionedCovariance.SlotSystem D h vr vt) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (N : ℕ) (hN : 1 ≤ N) (P : (U : PartitionedCovariance.UnsignedLabel) → PartitionedCovariance.PairData sys (PartitionedCovariance.tailLabel N U)) {q : ℝ} (hq : 0 < q) (hqN : q ≤ ChartScales.Q N) (x : SlotColoring.Position) (T0 : PartitionedCovariance.Vec2) (hcone : ∀ (U : PartitionedCovariance.UnsignedLabel), PartitionedCovariance.mask D (PartitionedCovariance.tailLabel N U) q x ≠ 0 → SmoothCovariance.StrictCone (P U).matrix (PartitionedCovariance.chartTarget h q N T0 U)) (i : Fin 2) : (PartitionedCovariance.doubleAverage fun (Y : PartitionedCovariance.Plane) (θ : ℝ) => principalField P hdet (PartitionedCovariance.physicalOuter h N) (PartitionedCovariance.physicalViscosity h N) (PartitionedCovariance.chartTarget h q N T0) q x Y θ 0 * principalField P hdet (PartitionedCovariance.physicalOuter h N) (PartitionedCovariance.physicalViscosity h N) (PartitionedCovariance.chartTarget h q N T0) q x Y θ i.succ) = q ^ (-PartitionedCovariance.velocityExponent h - 1 / 2) * T0 i

The angular integral and torus-square integral of this actual vector field give the physical target, with the original inverse square roots.

A single cutoff, before periodization

theorem NavierStokes.PrimaryFieldAssembly.periodize_smul_of_injective_support {S : Set PartitionedCovariance.Plane} (hS : Set.InjOn TorusAverages.quotientPoint S) {ψ : PartitionedCovariance.Plane → ℝ} {a : PartitionedCovariance.Plane → Vector} (hψ : Function.support ψ ⊆ S) (ha : Function.support a ⊆ S) (Y : PartitionedCovariance.Plane) : TorusAverages.periodize ψ Y • TorusAverages.periodize a Y = TorusAverages.periodize (fun (z : TorusInverse.Plane) => ψ z • a z) Y

Multiplication by a locally supported cutoff commutes with actual periodization on an injective slot. No choice of a lattice copy is needed.

theorem NavierStokes.PrimaryFieldAssembly.cutoff_periodized_coefficient {D h : ℝ} {vr vt : PartitionedCovariance.Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {U : PartitionedCovariance.UnsignedLabel} (P : PartitionedCovariance.PairData sys U) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (j : Fin 2) (ψ : PartitionedCovariance.Plane → ℝ) (a : PartitionedCovariance.Plane → Vector) (hψ : Function.support ψ ⊆ PartitionedCovariance.slotSet h sys.radius vr vt (PartitionedCovariance.signedLabel U j)) (ha : Function.support a ⊆ PartitionedCovariance.slotSet h sys.radius vr vt (PartitionedCovariance.signedLabel U j)) (hlocal : ∀ (z : PartitionedCovariance.Plane), ψ z • a z = nativeVector P hdet j z) (outer ε : ℝ) (T : PartitionedCovariance.Vec2) (q : ℝ) (x : SlotColoring.Position) (Y : PartitionedCovariance.Plane) : (TorusAverages.periodize ψ ((SlotGeometry.cover ^ SlotColoring.nativeIndex h U.1) Y) • fun (i : Fin 3) => ↑(outer * PartitionedCovariance.amplitude ε (PartitionedCovariance.mask D U q x) P.matrix T j * TorusAverages.periodize a ((SlotGeometry.cover ^ SlotColoring.nativeIndex h U.1) Y) i)) = slotAmplitude P hdet outer ε T q x j Y

Primitive local factorization suffices to identify the coefficient after applying its single cutoff. This is not an assumed covariance or assembled-field identity.

theorem NavierStokes.PrimaryFieldAssembly.mode_identification {D h : ℝ} {vr vt : PartitionedCovariance.Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {X : Type u_1} (κ : ℝ) (Φ : X → ℝ) (a : X → HarmonicCalculus.ComplexVector) (z : X) {U : PartitionedCovariance.UnsignedLabel} (P : PartitionedCovariance.PairData sys U) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (outer ε : ℝ) (T : PartitionedCovariance.Vec2) (q : ℝ) (x : SlotColoring.Position) (j : Fin 2) (Y : PartitionedCovariance.Plane) (θ : ℝ) (ha : a z = slotAmplitude P hdet outer ε T q x j Y) (hphase : κ * Φ z = slotPhase P j (Y, θ)) : (fun (i : Fin 3) => (HarmonicCalculus.vectorMode κ Φ a z i).re) = slotVelocity P hdet outer ε T q x j Y θ

Identification with any actual frequency/phase presentation of the same harmonic, including the frequency convention of WaveCoefficients.

theorem NavierStokes.PrimaryFieldAssembly.actual_phase_identification (k ε p pz x0 : ℝ) (F G : PhaseCalculus.Slow → ℝ) (s : PhaseCalculus.Slow) (v : PartitionedCovariance.Plane → ℝ) (m : ℤ) (hm : k * p = ↑m) (Y : PartitionedCovariance.Plane) (θ : ℝ) : k * PhaseCalculus.phase ε p pz x0 F G (s, θ, v Y) = ↑m * θ + k * (pz / ε * s.2.1 + x0 * s.1 - v Y * (p * F s + pz * G s))

The phase in the manuscript gives precisely the recorded integer angular mode and the recorded slow phase remainder.

theorem NavierStokes.PrimaryFieldAssembly.rounded_phase_identification (k ε target pz x0 : ℝ) (hk : k ≠ 0) (F G : PhaseCalculus.Slow → ℝ) (s : PhaseCalculus.Slow) (v : PartitionedCovariance.Plane → ℝ) (Y : PartitionedCovariance.Plane) (θ : ℝ) : k * PhaseCalculus.phase ε (PhaseEstimates.roundedFrequency k target) pz x0 F G (s, θ, v Y) = ↑(PhaseEstimates.nonzeroRound (k * target)) * θ + PartitionedCovariance.roundedPhaseRemainder k ε target pz x0 F G s v Y

The rounded angular frequency is the exact same nonzero integer as in the pair data; this identity does not use an approximate rounding bound.

The exact curl retains its covariance error

noncomputable def NavierStokes.PrimaryFieldAssembly.cutoffVelocity {X : Type u_1} (a : LinearWaveBounds.WaveCoefficients X) (ψ : ℕ → X → ℝ) (n : ℕ) (x : X) : Vector

Cutoff velocity, defined pointwise by (vectorMode (a.frequency n) (a.phase n) ((a.withCutoff ψ).amplitude n) x i).re.

Equations

• NavierStokes.PrimaryFieldAssembly.cutoffVelocity a ψ n x i = (NavierStokes.HarmonicCalculus.vectorMode (a.frequency n) (a.phase n) ((a.withCutoff ψ).amplitude n) x i).re

noncomputable def NavierStokes.PrimaryFieldAssembly.curlVelocity {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (a : LinearWaveBounds.WaveCoefficients X) (s : WeightedClasses.StripData X) (d : LinearWaveBounds.GraphDirections X) (ψ : ℕ → X → ℝ) (n : ℕ) (x : X) : Vector

Curl velocity, defined pointwise by (vectorMode (a.frequency n) (a.phase n) ((a.withCutoff ψ).curlCorrection s d n) x i).re.

Equations

• NavierStokes.PrimaryFieldAssembly.curlVelocity a s d ψ n x i = (NavierStokes.HarmonicCalculus.vectorMode (a.frequency n) (a.phase n) ((a.withCutoff ψ).curlCorrection s d n) x i).re

noncomputable def NavierStokes.PrimaryFieldAssembly.correctedVelocity {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (a : LinearWaveBounds.WaveCoefficients X) (s : WeightedClasses.StripData X) (d : LinearWaveBounds.GraphDirections X) (ψ : ℕ → X → ℝ) (n : ℕ) (x : X) : Vector

Corrected velocity, defined pointwise by (vectorMode (a.frequency n) (a.phase n) ((a.corrected s d ψ).amplitude n) x i).re.

Equations

• NavierStokes.PrimaryFieldAssembly.correctedVelocity a s d ψ n x i = (NavierStokes.HarmonicCalculus.vectorMode (a.frequency n) (a.phase n) ((a.corrected s d ψ).amplitude n) x i).re

theorem NavierStokes.PrimaryFieldAssembly.correctedVelocity_split {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (a : LinearWaveBounds.WaveCoefficients X) (s : WeightedClasses.StripData X) (d : LinearWaveBounds.GraphDirections X) (ψ : ℕ → X → ℝ) (n : ℕ) (x : X) : correctedVelocity a s d ψ n x = cutoffVelocity a ψ n x + curlVelocity a s d ψ n x

theorem NavierStokes.PrimaryFieldAssembly.cutoffVelocity_identification {D h : ℝ} {vr vt : PartitionedCovariance.Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {X : Type u_1} (a : LinearWaveBounds.WaveCoefficients X) (ψ : ℕ → X → ℝ) (n : ℕ) (z : X) {U : PartitionedCovariance.UnsignedLabel} (P : PartitionedCovariance.PairData sys U) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (outer ε : ℝ) (T : PartitionedCovariance.Vec2) (q : ℝ) (x : SlotColoring.Position) (j : Fin 2) (Y : PartitionedCovariance.Plane) (θ : ℝ) (ha : (a.withCutoff ψ).amplitude n z = slotAmplitude P hdet outer ε T q x j Y) (hphase : a.frequency n * a.phase n z = slotPhase P j (Y, θ)) : cutoffVelocity a ψ n z = slotVelocity P hdet outer ε T q x j Y θ

noncomputable def NavierStokes.PrimaryFieldAssembly.covarianceError (V R : PartitionedCovariance.Plane → ℝ → Vector) (i : Fin 2) (Y : PartitionedCovariance.Plane) (θ : ℝ) : ℝ

Covariance error, given by V Y θ 0 * R Y θ i.succ + R Y θ 0 * V Y θ i.succ + R Y θ 0 * R Y θ i.succ.

Equations

• NavierStokes.PrimaryFieldAssembly.covarianceError V R i Y θ = V Y θ 0 * R Y θ i.succ + R Y θ 0 * V Y θ i.succ + R Y θ 0 * R Y θ i.succ

theorem NavierStokes.PrimaryFieldAssembly.covariance_expansion (V R : PartitionedCovariance.Plane → ℝ → Vector) (i : Fin 2) (Y : PartitionedCovariance.Plane) (θ : ℝ) : (V Y θ + R Y θ) 0 * (V Y θ + R Y θ) i.succ = V Y θ 0 * V Y θ i.succ + covarianceError V R i Y θ

theorem NavierStokes.PrimaryFieldAssembly.doubleAverage_add {f g : PartitionedCovariance.Plane → ℝ → ℝ} (hf : Continuous (Function.uncurry f)) (hg : Continuous (Function.uncurry g)) : (PartitionedCovariance.doubleAverage fun (Y : PartitionedCovariance.Plane) (θ : ℝ) => f Y θ + g Y θ) = PartitionedCovariance.doubleAverage f + PartitionedCovariance.doubleAverage g

theorem NavierStokes.PrimaryFieldAssembly.averaged_covariance_expansion (V R : PartitionedCovariance.Plane → ℝ → Vector) (hV : Continuous (Function.uncurry V)) (hR : Continuous (Function.uncurry R)) (i : Fin 2) : (PartitionedCovariance.doubleAverage fun (Y : PartitionedCovariance.Plane) (θ : ℝ) => (V Y θ + R Y θ) 0 * (V Y θ + R Y θ) i.succ) = (PartitionedCovariance.doubleAverage fun (Y : PartitionedCovariance.Plane) (θ : ℝ) => V Y θ 0 * V Y θ i.succ) + PartitionedCovariance.doubleAverage (covarianceError V R i)

The covariance of the exact curl has three explicitly retained error products, rather than being identified with the principal covariance.

Canonical source data: actual ODE pulses and the same matrix

structure NavierStokes.PrimaryFieldAssembly.SourcePair (Q : Type) [NormedAddCommGroup Q] {D h : ℝ} {vr vt : PartitionedCovariance.Plane} (sys : PartitionedCovariance.SlotSystem D h vr vt) (U : PartitionedCovariance.UnsignedLabel) : Type

Primitive data for a signed pair of actual ODE pulses. No local field, matrix, or covariance identity is a field of this structure.

• domain : Set Q

  Domain of SourcePair, of type Set Q.

• point : Q

  Point of SourcePair, of type Q.

• point_mem : self.point ∈ self.domain
• frame : Fin 2 → PrimaryODE.FrameData Q

  Frame of SourcePair, of type Fin 2 → PrimaryODE.FrameData Q.

• lam : Fin 2 → ℝ

  Lam of SourcePair, of type Fin 2 → ℝ.

• rate : Fin 2 → ℝ

  Rate of SourcePair, of type Fin 2 → ℝ.

• length : Fin 2 → ℝ

  Length of SourcePair, of type Fin 2 → ℝ.

• length_pos (j : Fin 2) : 0 < self.length j
• coefficient_continuous (j : Fin 2) : ContinuousOn ((self.frame j).coefficient 1) (self.domain ×ˢ Set.Icc 0 (self.length j))
• kinematics (j : Fin 2) : (self.frame j).Kinematics self.point (Set.Icc 0 (self.length j))
• stretch : PartitionedCovariance.Vec2

  Stretch of SourcePair, of type Vec2.

• stretch_pos (j : Fin 2) : 0 < self.stretch j
• fits (j : Fin 2) : self.length j ≤ 2 * sys.radius / self.stretch j
• mode : Fin 2 → ℤ

  Mode of SourcePair, of type Fin 2 → ℤ.

• mode_ne (j : Fin 2) : self.mode j ≠ 0
• phase : Fin 2 → PartitionedCovariance.Plane → ℝ

  Phase of SourcePair, of type Fin 2 → Plane → ℝ.

noncomputable def NavierStokes.PrimaryFieldAssembly.SourcePair.pairData {D h : ℝ} {vr vt : PartitionedCovariance.Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {Q : Type} [NormedAddCommGroup Q] {U : PartitionedCovariance.UnsignedLabel} (A : SourcePair Q sys U) : PartitionedCovariance.PairData sys U

Pair data, bundling pulses, ci, ci_pos, fits and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.PrimaryFieldAssembly.SourcePair.sourceMatrix {D h : ℝ} {vr vt : PartitionedCovariance.Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {Q : Type} [NormedAddCommGroup Q] {U : PartitionedCovariance.UnsignedLabel} (A : SourcePair Q sys U) : PartitionedCovariance.Mat2

The matrix is computed directly from the normalized ODE fundamentals, with the exact determinant, transverse scale, and slot-length prefactor.

Equations

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

theorem NavierStokes.PrimaryFieldAssembly.SourcePair.sourceMatrix_eq {D h : ℝ} {vr vt : PartitionedCovariance.Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {Q : Type} [NormedAddCommGroup Q] {U : PartitionedCovariance.UnsignedLabel} (A : SourcePair Q sys U) : A.sourceMatrix = A.pairData.matrix

theorem NavierStokes.PrimaryFieldAssembly.SourcePair.pulseVector_eq {D h : ℝ} {vr vt : PartitionedCovariance.Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {Q : Type} [NormedAddCommGroup Q] {U : PartitionedCovariance.UnsignedLabel} (A : SourcePair Q sys U) (j : Fin 2) (z : PartitionedCovariance.Plane) : pulseVector (A.pairData.pulses j) sys.radius z = fun (i : Fin 3) => (PrimaryPulseBounds.localPrimaryProfile (A.frame j) (A.lam j) (A.rate j) (A.length j) sys.radius A.point z).ofLp i

noncomputable def NavierStokes.PrimaryFieldAssembly.SourcePair.nativeSource {D h : ℝ} {vr vt : PartitionedCovariance.Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {Q : Type} [NormedAddCommGroup Q] {U : PartitionedCovariance.UnsignedLabel} (A : SourcePair Q sys U) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (j : Fin 2) : PartitionedCovariance.Plane → Vector

The source vector is evaluated from cutoffPulse, rather than from arbitrarily supplied radial and tangent component functions.

Equations

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

theorem NavierStokes.PrimaryFieldAssembly.SourcePair.nativeSource_eq {D h : ℝ} {vr vt : PartitionedCovariance.Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {Q : Type} [NormedAddCommGroup Q] {U : PartitionedCovariance.UnsignedLabel} (A : SourcePair Q sys U) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (j : Fin 2) : A.nativeSource hdet j = nativeVector A.pairData hdet j

noncomputable def NavierStokes.PrimaryFieldAssembly.SourcePair.nativeCoefficient {D h : ℝ} {vr vt : PartitionedCovariance.Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {Q : Type} [NormedAddCommGroup Q] {U : PartitionedCovariance.UnsignedLabel} (A : SourcePair Q sys U) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (outer ε : ℝ) (T : PartitionedCovariance.Vec2) (q : ℝ) (x : SlotColoring.Position) (j : Fin 2) (Y : PartitionedCovariance.Plane) : HarmonicCalculus.ComplexVector

The native complex coefficient has the literal inverse-square-root amplitude and a single local Gaussian cutoff.

Equations

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

noncomputable def NavierStokes.PrimaryFieldAssembly.SourcePair.actualAmplitude {D h : ℝ} {vr vt : PartitionedCovariance.Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {Q : Type} [NormedAddCommGroup Q] {U : PartitionedCovariance.UnsignedLabel} (A : SourcePair Q sys U) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (outer ε : ℝ) (T : PartitionedCovariance.Vec2) (q : ℝ) (x : SlotColoring.Position) (j : Fin 2) (Y : PartitionedCovariance.Plane) : HarmonicCalculus.ComplexVector

Actual amplitude, given by TorusAverages.periodize (A.nativeCoefficient hdet outer ε T q x j) ((SlotGeometry.cover ^ SlotColoring.nativeIndex h U.1) Y).

Equations

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

theorem NavierStokes.PrimaryFieldAssembly.SourcePair.actualAmplitude_eq {D h : ℝ} {vr vt : PartitionedCovariance.Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {Q : Type} [NormedAddCommGroup Q] {U : PartitionedCovariance.UnsignedLabel} (A : SourcePair Q sys U) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (outer ε : ℝ) (T : PartitionedCovariance.Vec2) (q : ℝ) (x : SlotColoring.Position) (j : Fin 2) (Y : PartitionedCovariance.Plane) : A.actualAmplitude hdet outer ε T q x j Y = slotAmplitude A.pairData hdet outer ε T q x j Y

The actual periodized complex coefficient equals the coefficient used in the radial/tangent covariance assembly.

noncomputable def NavierStokes.PrimaryFieldAssembly.SourcePair.actualVelocity {D h : ℝ} {vr vt : PartitionedCovariance.Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {Q : Type} [NormedAddCommGroup Q] {U : PartitionedCovariance.UnsignedLabel} (A : SourcePair Q sys U) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (outer ε : ℝ) (T : PartitionedCovariance.Vec2) (q : ℝ) (x : SlotColoring.Position) (j : Fin 2) (Y : PartitionedCovariance.Plane) (θ : ℝ) : Vector

Actual velocity, defined pointwise by (vectorMode 1 (slotPhase A.pairData j) (fun z => A.actualAmplitude hdet outer ε T q x j z.1) (Y, θ) i).re.

Equations

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

theorem NavierStokes.PrimaryFieldAssembly.SourcePair.actualVelocity_eq {D h : ℝ} {vr vt : PartitionedCovariance.Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {Q : Type} [NormedAddCommGroup Q] {U : PartitionedCovariance.UnsignedLabel} (A : SourcePair Q sys U) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (outer ε : ℝ) (T : PartitionedCovariance.Vec2) (q : ℝ) (x : SlotColoring.Position) (j : Fin 2) (Y : PartitionedCovariance.Plane) (θ : ℝ) : A.actualVelocity hdet outer ε T q x j Y θ = slotVelocity A.pairData hdet outer ε T q x j Y θ

noncomputable def NavierStokes.PrimaryFieldAssembly.sourceField {D h : ℝ} {vr vt : PartitionedCovariance.Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {Q : Type} [NormedAddCommGroup Q] {N : ℕ} (A : (U : PartitionedCovariance.UnsignedLabel) → SourcePair Q sys (PartitionedCovariance.tailLabel N U)) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (outer ε : PartitionedCovariance.UnsignedLabel → ℝ) (T : PartitionedCovariance.UnsignedLabel → PartitionedCovariance.Vec2) (q : ℝ) (x : SlotColoring.Position) (Y : PartitionedCovariance.Plane) (θ : ℝ) : Vector

Source field, given by ∑ᶠ a : SignedIndex, (A a.1).actualVelocity hdet (outer a.1) (ε a.1) (T a.1) q x a.2 Y θ.

Equations

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

theorem NavierStokes.PrimaryFieldAssembly.sourceField_eq {D h : ℝ} {vr vt : PartitionedCovariance.Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {Q : Type} [NormedAddCommGroup Q] {N : ℕ} (A : (U : PartitionedCovariance.UnsignedLabel) → SourcePair Q sys (PartitionedCovariance.tailLabel N U)) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (outer ε : PartitionedCovariance.UnsignedLabel → ℝ) (T : PartitionedCovariance.UnsignedLabel → PartitionedCovariance.Vec2) (q : ℝ) (x : SlotColoring.Position) (Y : PartitionedCovariance.Plane) (θ : ℝ) : sourceField A hdet outer ε T q x Y θ = principalField (fun (U : PartitionedCovariance.UnsignedLabel) => (A U).pairData) hdet outer ε T q x Y θ

theorem NavierStokes.PrimaryFieldAssembly.physical_source_covariance {D h : ℝ} {vr vt : PartitionedCovariance.Plane} {Q : Type} [NormedAddCommGroup Q] (sys : PartitionedCovariance.SlotSystem D h vr vt) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (N : ℕ) (hN : 1 ≤ N) (A : (U : PartitionedCovariance.UnsignedLabel) → SourcePair Q sys (PartitionedCovariance.tailLabel N U)) {q : ℝ} (hq : 0 < q) (hqN : q ≤ ChartScales.Q N) (x : SlotColoring.Position) (T0 : PartitionedCovariance.Vec2) (hcone : ∀ (U : PartitionedCovariance.UnsignedLabel), PartitionedCovariance.mask D (PartitionedCovariance.tailLabel N U) q x ≠ 0 → SmoothCovariance.StrictCone (A U).sourceMatrix (PartitionedCovariance.chartTarget h q N T0 U)) (i : Fin 2) : (PartitionedCovariance.doubleAverage fun (Y : PartitionedCovariance.Plane) (θ : ℝ) => sourceField A hdet (PartitionedCovariance.physicalOuter h N) (PartitionedCovariance.physicalViscosity h N) (PartitionedCovariance.chartTarget h q N T0) q x Y θ 0 * sourceField A hdet (PartitionedCovariance.physicalOuter h N) (PartitionedCovariance.physicalViscosity h N) (PartitionedCovariance.chartTarget h q N T0) q x Y θ i.succ) = q ^ (-PartitionedCovariance.velocityExponent h - 1 / 2) * T0 i

End-to-end principal covariance for the actual ODE/source coefficient. The assumed cone concerns its actual normalized ODE integral matrix.

Adapter to the actual WaveCoefficients.withCutoff field

noncomputable def NavierStokes.PrimaryFieldAssembly.cutoffModeField {X : Type u_1} (a : SignedIndex → LinearWaveBounds.WaveCoefficients X) (ψ : SignedIndex → ℕ → X → ℝ) (band : SignedIndex → ℕ) (point : SignedIndex → PartitionedCovariance.Plane → ℝ → X) (Y : PartitionedCovariance.Plane) (θ : ℝ) : Vector

Cutoff mode field, given by ∑ᶠ b : SignedIndex, cutoffVelocity (a b) (ψ b) (band b) (point b Y θ).

Equations

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

theorem NavierStokes.PrimaryFieldAssembly.cutoffModeField_eq_source {D h : ℝ} {vr vt : PartitionedCovariance.Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {X : Type u_1} {Q : Type} [NormedAddCommGroup Q] {N : ℕ} (A : (U : PartitionedCovariance.UnsignedLabel) → SourcePair Q sys (PartitionedCovariance.tailLabel N U)) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (outer ε : PartitionedCovariance.UnsignedLabel → ℝ) (T : PartitionedCovariance.UnsignedLabel → PartitionedCovariance.Vec2) (q : ℝ) (x : SlotColoring.Position) (a : SignedIndex → LinearWaveBounds.WaveCoefficients X) (ψ : SignedIndex → ℕ → X → ℝ) (band : SignedIndex → ℕ) (point : SignedIndex → PartitionedCovariance.Plane → ℝ → X) (hcoeff : ∀ (b : SignedIndex) (Y : PartitionedCovariance.Plane) (θ : ℝ), ((a b).withCutoff (ψ b)).amplitude (band b) (point b Y θ) = (A b.1).actualAmplitude hdet (outer b.1) (ε b.1) (T b.1) q x b.2 Y) (hphase : ∀ (b : SignedIndex) (Y : PartitionedCovariance.Plane) (θ : ℝ), (a b).frequency (band b) * (a b).phase (band b) (point b Y θ) = slotPhase (A b.1).pairData b.2 (Y, θ)) (Y : PartitionedCovariance.Plane) (θ : ℝ) : cutoffModeField a ψ band point Y θ = sourceField A hdet outer ε T q x Y θ

The only bindings are the constructed coefficient and phase. The field and its assembled covariance are conclusions of this adapter.

theorem NavierStokes.PrimaryFieldAssembly.cutoffModeField_physical_covariance {D h : ℝ} {vr vt : PartitionedCovariance.Plane} {X : Type u_1} {Q : Type} [NormedAddCommGroup Q] (sys : PartitionedCovariance.SlotSystem D h vr vt) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (N : ℕ) (hN : 1 ≤ N) (A : (U : PartitionedCovariance.UnsignedLabel) → SourcePair Q sys (PartitionedCovariance.tailLabel N U)) {q : ℝ} (hq : 0 < q) (hqN : q ≤ ChartScales.Q N) (x : SlotColoring.Position) (T0 : PartitionedCovariance.Vec2) (hcone : ∀ (U : PartitionedCovariance.UnsignedLabel), PartitionedCovariance.mask D (PartitionedCovariance.tailLabel N U) q x ≠ 0 → SmoothCovariance.StrictCone (A U).sourceMatrix (PartitionedCovariance.chartTarget h q N T0 U)) (a : SignedIndex → LinearWaveBounds.WaveCoefficients X) (ψ : SignedIndex → ℕ → X → ℝ) (band : SignedIndex → ℕ) (point : SignedIndex → PartitionedCovariance.Plane → ℝ → X) (hcoeff : ∀ (b : SignedIndex) (Y : PartitionedCovariance.Plane) (θ : ℝ), ((a b).withCutoff (ψ b)).amplitude (band b) (point b Y θ) = (A b.1).actualAmplitude hdet (PartitionedCovariance.physicalOuter h N b.1) (PartitionedCovariance.physicalViscosity h N b.1) (PartitionedCovariance.chartTarget h q N T0 b.1) q x b.2 Y) (hphase : ∀ (b : SignedIndex) (Y : PartitionedCovariance.Plane) (θ : ℝ), (a b).frequency (band b) * (a b).phase (band b) (point b Y θ) = slotPhase (A b.1).pairData b.2 (Y, θ)) (i : Fin 2) : (PartitionedCovariance.doubleAverage fun (Y : PartitionedCovariance.Plane) (θ : ℝ) => cutoffModeField a ψ band point Y θ 0 * cutoffModeField a ψ band point Y θ i.succ) = q ^ (-PartitionedCovariance.velocityExponent h - 1 / 2) * T0 i

theorem NavierStokes.PrimaryFieldAssembly.finite_corrected_field_split {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {ι : Type u_2} (F : Finset ι) (a : ι → LinearWaveBounds.WaveCoefficients X) (s : ι → WeightedClasses.StripData X) (d : ι → LinearWaveBounds.GraphDirections X) (ψ : ι → ℕ → X → ℝ) (band : ι → ℕ) (point : ι → X) : ∑ b ∈ F, correctedVelocity (a b) (s b) (d b) (ψ b) (band b) (point b) = ∑ b ∈ F, cutoffVelocity (a b) (ψ b) (band b) (point b) + ∑ b ∈ F, curlVelocity (a b) (s b) (d b) (ψ b) (band b) (point b)

A finite exact-curl assembly retains the sum of its actual curl corrections. This applies before any covariance estimate is made.

The angular covariance is a genuine function on the auxiliary torus

theorem NavierStokes.PrimaryFieldAssembly.covered_periodic (n : ℕ) (f : PartitionedCovariance.Plane → ℝ) (Y : PartitionedCovariance.Plane) (k : TorusInverse.Frequency) : PartitionedCovariance.covered n f (Y + TorusAverages.latticePoint k) = PartitionedCovariance.covered n f Y

theorem NavierStokes.PrimaryFieldAssembly.slot_cross_zero {D h : ℝ} {vr vt : PartitionedCovariance.Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {N : ℕ} (hN : 1 ≤ N) (P : (U : PartitionedCovariance.UnsignedLabel) → PartitionedCovariance.PairData sys (PartitionedCovariance.tailLabel N U)) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (outer ε : PartitionedCovariance.UnsignedLabel → ℝ) (T : PartitionedCovariance.UnsignedLabel → PartitionedCovariance.Vec2) {q : ℝ} (hq : 0 < q) (x : SlotColoring.Position) {a b : SignedIndex} (hab : a ≠ b) (Y : PartitionedCovariance.Plane) (θ : ℝ) (i : Fin 2) : slotVelocity (P a.1) hdet (outer a.1) (ε a.1) (T a.1) q x a.2 Y θ 0 * slotVelocity (P b.1) hdet (outer b.1) (ε b.1) (T b.1) q x b.2 Y θ i.succ = 0

noncomputable def NavierStokes.PrimaryFieldAssembly.diagonalCovariance {D h : ℝ} {vr vt : PartitionedCovariance.Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {N : ℕ} (P : (U : PartitionedCovariance.UnsignedLabel) → PartitionedCovariance.PairData sys (PartitionedCovariance.tailLabel N U)) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (outer ε : PartitionedCovariance.UnsignedLabel → ℝ) (T : PartitionedCovariance.UnsignedLabel → PartitionedCovariance.Vec2) (q : ℝ) (x : SlotColoring.Position) (a : SignedIndex) (i : Fin 2) (Y : PartitionedCovariance.Plane) : ℝ

Diagonal covariance as an element of ℝ.

Equations

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

theorem NavierStokes.PrimaryFieldAssembly.angular_principal_finite {D h : ℝ} {vr vt : PartitionedCovariance.Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {N : ℕ} (hN : 1 ≤ N) (P : (U : PartitionedCovariance.UnsignedLabel) → PartitionedCovariance.PairData sys (PartitionedCovariance.tailLabel N U)) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (outer ε : PartitionedCovariance.UnsignedLabel → ℝ) (T : PartitionedCovariance.UnsignedLabel → PartitionedCovariance.Vec2) {q : ℝ} (hq : 0 < q) (x : SlotColoring.Position) (i : Fin 2) : ∃ (F : Finset SignedIndex), ∀ (Y : PartitionedCovariance.Plane), (SmoothLoop.angularMean fun (θ : ℝ) => principalField P hdet outer ε T q x Y θ 0 * principalField P hdet outer ε T q x Y θ i.succ) = ∑ a ∈ F, diagonalCovariance P hdet outer ε T q x a i Y

Both off-diagonal elimination and angular integration are performed on the actual finite active family, before descending to the torus.

theorem NavierStokes.PrimaryFieldAssembly.angular_principal_regular {D h : ℝ} {vr vt : PartitionedCovariance.Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {N : ℕ} (hN : 1 ≤ N) (P : (U : PartitionedCovariance.UnsignedLabel) → PartitionedCovariance.PairData sys (PartitionedCovariance.tailLabel N U)) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (outer ε : PartitionedCovariance.UnsignedLabel → ℝ) (T : PartitionedCovariance.UnsignedLabel → PartitionedCovariance.Vec2) {q : ℝ} (hq : 0 < q) (x : SlotColoring.Position) (i : Fin 2) : have f := fun (Y : PartitionedCovariance.Plane) => SmoothLoop.angularMean fun (θ : ℝ) => principalField P hdet outer ε T q x Y θ 0 * principalField P hdet outer ε T q x Y θ i.succ; Continuous f ∧ ∀ (Y : PartitionedCovariance.Plane) (k : TorusInverse.Frequency), f (Y + TorusAverages.latticePoint k) = f Y

theorem NavierStokes.PrimaryFieldAssembly.principal_torus_average {D h : ℝ} {vr vt : PartitionedCovariance.Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {N : ℕ} (hN : 1 ≤ N) (P : (U : PartitionedCovariance.UnsignedLabel) → PartitionedCovariance.PairData sys (PartitionedCovariance.tailLabel N U)) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (outer ε : PartitionedCovariance.UnsignedLabel → ℝ) (T : PartitionedCovariance.UnsignedLabel → PartitionedCovariance.Vec2) {q : ℝ} (hq : 0 < q) (x : SlotColoring.Position) (i : Fin 2) : ∃ (g : C(TorusInverse.Torus, ℂ)), (∀ (Y : TorusInverse.Plane), g (TorusAverages.quotientPoint Y) = ↑(SmoothLoop.angularMean fun (θ : ℝ) => principalField P hdet outer ε T q x Y θ 0 * principalField P hdet outer ε T q x Y θ i.succ)) ∧ ∫ (z : TorusInverse.Torus), g z ∂TorusInverse.torusMeasure = ↑(PartitionedCovariance.doubleAverage fun (Y : PartitionedCovariance.Plane) (θ : ℝ) => principalField P hdet outer ε T q x Y θ 0 * principalField P hdet outer ε T q x Y θ i.succ)

The square average is exactly the Haar integral of the angular covariance's continuous descent to the auxiliary torus.

theorem NavierStokes.PrimaryFieldAssembly.physical_source_torus_covariance {D h : ℝ} {vr vt : PartitionedCovariance.Plane} {Q : Type} [NormedAddCommGroup Q] (sys : PartitionedCovariance.SlotSystem D h vr vt) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (N : ℕ) (hN : 1 ≤ N) (A : (U : PartitionedCovariance.UnsignedLabel) → SourcePair Q sys (PartitionedCovariance.tailLabel N U)) {q : ℝ} (hq : 0 < q) (hqN : q ≤ ChartScales.Q N) (x : SlotColoring.Position) (T0 : PartitionedCovariance.Vec2) (hcone : ∀ (U : PartitionedCovariance.UnsignedLabel), PartitionedCovariance.mask D (PartitionedCovariance.tailLabel N U) q x ≠ 0 → SmoothCovariance.StrictCone (A U).sourceMatrix (PartitionedCovariance.chartTarget h q N T0 U)) (i : Fin 2) : ∃ (g : C(TorusInverse.Torus, ℂ)), (∀ (Y : TorusInverse.Plane), g (TorusAverages.quotientPoint Y) = ↑(SmoothLoop.angularMean fun (θ : ℝ) => sourceField A hdet (PartitionedCovariance.physicalOuter h N) (PartitionedCovariance.physicalViscosity h N) (PartitionedCovariance.chartTarget h q N T0) q x Y θ 0 * sourceField A hdet (PartitionedCovariance.physicalOuter h N) (PartitionedCovariance.physicalViscosity h N) (PartitionedCovariance.chartTarget h q N T0) q x Y θ i.succ)) ∧ ∫ (z : TorusInverse.Torus), g z ∂TorusInverse.torusMeasure = ↑(q ^ (-PartitionedCovariance.velocityExponent h - 1 / 2) * T0 i)

theorem NavierStokes.PrimaryFieldAssembly.nativeVector_continuous {D h : ℝ} {vr vt : PartitionedCovariance.Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {U : PartitionedCovariance.UnsignedLabel} (P : PartitionedCovariance.PairData sys U) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (j : Fin 2) : Continuous (nativeVector P hdet j)

theorem NavierStokes.PrimaryFieldAssembly.slotVelocity_continuous {D h : ℝ} {vr vt : PartitionedCovariance.Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {U : PartitionedCovariance.UnsignedLabel} (P : PartitionedCovariance.PairData sys U) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (outer ε : ℝ) (T : PartitionedCovariance.Vec2) (q : ℝ) (x : SlotColoring.Position) (j : Fin 2) (hphase : Continuous (P.phases j)) : Continuous fun (z : PartitionedCovariance.Plane × ℝ) => slotVelocity P hdet outer ε T q x j z.1 z.2

theorem NavierStokes.PrimaryFieldAssembly.principalField_continuous {D h : ℝ} {vr vt : PartitionedCovariance.Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {N : ℕ} (P : (U : PartitionedCovariance.UnsignedLabel) → PartitionedCovariance.PairData sys (PartitionedCovariance.tailLabel N U)) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (outer ε : PartitionedCovariance.UnsignedLabel → ℝ) (T : PartitionedCovariance.UnsignedLabel → PartitionedCovariance.Vec2) {q : ℝ} (hq : 0 < q) (x : SlotColoring.Position) (hphase : ∀ (U : PartitionedCovariance.UnsignedLabel) (j : Fin 2), Continuous ((P U).phases j)) : Continuous fun (z : PartitionedCovariance.Plane × ℝ) => principalField P hdet outer ε T q x z.1 z.2

theorem NavierStokes.PrimaryFieldAssembly.physical_source_plus_remainder {D h : ℝ} {vr vt : PartitionedCovariance.Plane} {Q : Type} [NormedAddCommGroup Q] (sys : PartitionedCovariance.SlotSystem D h vr vt) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (N : ℕ) (hN : 1 ≤ N) (A : (U : PartitionedCovariance.UnsignedLabel) → SourcePair Q sys (PartitionedCovariance.tailLabel N U)) {q : ℝ} (hq : 0 < q) (hqN : q ≤ ChartScales.Q N) (x : SlotColoring.Position) (T0 : PartitionedCovariance.Vec2) (hcone : ∀ (U : PartitionedCovariance.UnsignedLabel), PartitionedCovariance.mask D (PartitionedCovariance.tailLabel N U) q x ≠ 0 → SmoothCovariance.StrictCone (A U).sourceMatrix (PartitionedCovariance.chartTarget h q N T0 U)) (hphase : ∀ (U : PartitionedCovariance.UnsignedLabel) (j : Fin 2), Continuous ((A U).phase j)) (R : PartitionedCovariance.Plane → ℝ → Vector) (hR : Continuous (Function.uncurry R)) (i : Fin 2) : have V := sourceField A hdet (PartitionedCovariance.physicalOuter h N) (PartitionedCovariance.physicalViscosity h N) (PartitionedCovariance.chartTarget h q N T0) q x; (PartitionedCovariance.doubleAverage fun (Y : PartitionedCovariance.Plane) (θ : ℝ) => (V Y θ + R Y θ) 0 * (V Y θ + R Y θ) i.succ) = q ^ (-PartitionedCovariance.velocityExponent h - 1 / 2) * T0 i + PartitionedCovariance.doubleAverage (covarianceError V R i)

The physical covariance target belongs to the principal field. Adding the actual curl remainder preserves all three covariance error terms.

theorem NavierStokes.PrimaryFieldAssembly.slotVelocity_angular_periodic {D h : ℝ} {vr vt : PartitionedCovariance.Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {U : PartitionedCovariance.UnsignedLabel} (P : PartitionedCovariance.PairData sys U) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (outer ε : ℝ) (T : PartitionedCovariance.Vec2) (q : ℝ) (x : SlotColoring.Position) (j : Fin 2) (Y : PartitionedCovariance.Plane) (θ : ℝ) : slotVelocity P hdet outer ε T q x j Y (θ + 2 * Real.pi) = slotVelocity P hdet outer ε T q x j Y θ

Integer angular modes give actual full-turn periodicity.

theorem NavierStokes.PrimaryFieldAssembly.principalField_angular_periodic {D h : ℝ} {vr vt : PartitionedCovariance.Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {N : ℕ} (P : (U : PartitionedCovariance.UnsignedLabel) → PartitionedCovariance.PairData sys (PartitionedCovariance.tailLabel N U)) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (outer ε : PartitionedCovariance.UnsignedLabel → ℝ) (T : PartitionedCovariance.UnsignedLabel → PartitionedCovariance.Vec2) (q : ℝ) (x : SlotColoring.Position) (Y : PartitionedCovariance.Plane) (θ : ℝ) : principalField P hdet outer ε T q x Y (θ + 2 * Real.pi) = principalField P hdet outer ε T q x Y θ

theorem NavierStokes.PrimaryFieldAssembly.principalField_auxiliary_periodic {D h : ℝ} {vr vt : PartitionedCovariance.Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {N : ℕ} (P : (U : PartitionedCovariance.UnsignedLabel) → PartitionedCovariance.PairData sys (PartitionedCovariance.tailLabel N U)) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (outer ε : PartitionedCovariance.UnsignedLabel → ℝ) (T : PartitionedCovariance.UnsignedLabel → PartitionedCovariance.Vec2) (q : ℝ) (x : SlotColoring.Position) (hphase : ∀ (U : PartitionedCovariance.UnsignedLabel) (j : Fin 2) (Y : PartitionedCovariance.Plane) (k : TorusInverse.Frequency), (P U).phases j (Y + TorusAverages.latticePoint k) = (P U).phases j Y) (Y : PartitionedCovariance.Plane) (θ : ℝ) (k : TorusInverse.Frequency) : principalField P hdet outer ε T q x (Y + TorusAverages.latticePoint k) θ = principalField P hdet outer ε T q x Y θ

Full-field auxiliary periodicity uses the source phase convention. The angular covariance's periodicity above needed no such hypothesis.

Explicit conversion from chart velocity to physical velocity

theorem NavierStokes.PrimaryFieldAssembly.slotVelocity_outer_scale {D h : ℝ} {vr vt : PartitionedCovariance.Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {U : PartitionedCovariance.UnsignedLabel} (P : PartitionedCovariance.PairData sys U) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (outer ε : ℝ) (T : PartitionedCovariance.Vec2) (q : ℝ) (x : SlotColoring.Position) (j : Fin 2) (Y : PartitionedCovariance.Plane) (θ : ℝ) : slotVelocity P hdet outer ε T q x j Y θ = outer • slotVelocity P hdet 1 ε T q x j Y θ

theorem NavierStokes.PrimaryFieldAssembly.SourcePair.actualVelocity_outer_scale {D h : ℝ} {vr vt : PartitionedCovariance.Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {Q : Type} [NormedAddCommGroup Q] {U : PartitionedCovariance.UnsignedLabel} (A : SourcePair Q sys U) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (outer ε : ℝ) (T : PartitionedCovariance.Vec2) (q : ℝ) (x : SlotColoring.Position) (j : Fin 2) (Y : PartitionedCovariance.Plane) (θ : ℝ) : A.actualVelocity hdet outer ε T q x j Y θ = outer • A.actualVelocity hdet 1 ε T q x j Y θ

noncomputable def NavierStokes.PrimaryFieldAssembly.scaledCutoffModeField {X : Type u_1} (outer : PartitionedCovariance.UnsignedLabel → ℝ) (a : SignedIndex → LinearWaveBounds.WaveCoefficients X) (ψ : SignedIndex → ℕ → X → ℝ) (band : SignedIndex → ℕ) (point : SignedIndex → PartitionedCovariance.Plane → ℝ → X) (Y : PartitionedCovariance.Plane) (θ : ℝ) : Vector

Chart velocity is converted to physical velocity outside the chart coefficient. The weighted class of the original coefficient is unchanged.

Equations

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

theorem NavierStokes.PrimaryFieldAssembly.scaledCutoffModeField_eq_source {D h : ℝ} {vr vt : PartitionedCovariance.Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {X : Type u_1} {Q : Type} [NormedAddCommGroup Q] {N : ℕ} (A : (U : PartitionedCovariance.UnsignedLabel) → SourcePair Q sys (PartitionedCovariance.tailLabel N U)) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (outer ε : PartitionedCovariance.UnsignedLabel → ℝ) (T : PartitionedCovariance.UnsignedLabel → PartitionedCovariance.Vec2) (q : ℝ) (x : SlotColoring.Position) (a : SignedIndex → LinearWaveBounds.WaveCoefficients X) (ψ : SignedIndex → ℕ → X → ℝ) (band : SignedIndex → ℕ) (point : SignedIndex → PartitionedCovariance.Plane → ℝ → X) (hcoeff : ∀ (b : SignedIndex) (Y : PartitionedCovariance.Plane) (θ : ℝ), ((a b).withCutoff (ψ b)).amplitude (band b) (point b Y θ) = (A b.1).actualAmplitude hdet 1 (ε b.1) (T b.1) q x b.2 Y) (hphase : ∀ (b : SignedIndex) (Y : PartitionedCovariance.Plane) (θ : ℝ), (a b).frequency (band b) * (a b).phase (band b) (point b Y θ) = slotPhase (A b.1).pairData b.2 (Y, θ)) (Y : PartitionedCovariance.Plane) (θ : ℝ) : scaledCutoffModeField outer a ψ band point Y θ = sourceField A hdet outer ε T q x Y θ

theorem NavierStokes.PrimaryFieldAssembly.scaledCutoffModeField_physical_covariance {D h : ℝ} {vr vt : PartitionedCovariance.Plane} {X : Type u_1} {Q : Type} [NormedAddCommGroup Q] (sys : PartitionedCovariance.SlotSystem D h vr vt) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (N : ℕ) (hN : 1 ≤ N) (A : (U : PartitionedCovariance.UnsignedLabel) → SourcePair Q sys (PartitionedCovariance.tailLabel N U)) {q : ℝ} (hq : 0 < q) (hqN : q ≤ ChartScales.Q N) (x : SlotColoring.Position) (T0 : PartitionedCovariance.Vec2) (hcone : ∀ (U : PartitionedCovariance.UnsignedLabel), PartitionedCovariance.mask D (PartitionedCovariance.tailLabel N U) q x ≠ 0 → SmoothCovariance.StrictCone (A U).sourceMatrix (PartitionedCovariance.chartTarget h q N T0 U)) (a : SignedIndex → LinearWaveBounds.WaveCoefficients X) (ψ : SignedIndex → ℕ → X → ℝ) (band : SignedIndex → ℕ) (point : SignedIndex → PartitionedCovariance.Plane → ℝ → X) (hcoeff : ∀ (b : SignedIndex) (Y : PartitionedCovariance.Plane) (θ : ℝ), ((a b).withCutoff (ψ b)).amplitude (band b) (point b Y θ) = (A b.1).actualAmplitude hdet 1 (PartitionedCovariance.physicalViscosity h N b.1) (PartitionedCovariance.chartTarget h q N T0 b.1) q x b.2 Y) (hphase : ∀ (b : SignedIndex) (Y : PartitionedCovariance.Plane) (θ : ℝ), (a b).frequency (band b) * (a b).phase (band b) (point b Y θ) = slotPhase (A b.1).pairData b.2 (Y, θ)) (i : Fin 2) : (PartitionedCovariance.doubleAverage fun (Y : PartitionedCovariance.Plane) (θ : ℝ) => scaledCutoffModeField (PartitionedCovariance.physicalOuter h N) a ψ band point Y θ 0 * scaledCutoffModeField (PartitionedCovariance.physicalOuter h N) a ψ band point Y θ i.succ) = q ^ (-PartitionedCovariance.velocityExponent h - 1 / 2) * T0 i

The physical factor is exactly Q^(-A) applied to each chart field. It is not inserted into the coefficient before the chart wave estimates.

theorem NavierStokes.PrimaryFieldAssembly.finite_scaled_corrected_field_split {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {ι : Type u_2} (F : Finset ι) (outer : ι → ℝ) (a : ι → LinearWaveBounds.WaveCoefficients X) (s : ι → WeightedClasses.StripData X) (d : ι → LinearWaveBounds.GraphDirections X) (ψ : ι → ℕ → X → ℝ) (band : ι → ℕ) (point : ι → X) : ∑ b ∈ F, outer b • correctedVelocity (a b) (s b) (d b) (ψ b) (band b) (point b) = ∑ b ∈ F, outer b • cutoffVelocity (a b) (ψ b) (band b) (point b) + ∑ b ∈ F, outer b • curlVelocity (a b) (s b) (d b) (ψ b) (band b) (point b)