Axis preservation for the mixed physical diagonal

The wave terms below are the actual sums of full, copy-dependent carriers. Only native support geometry and support cells are used. Mean stream potentials and direct angular velocities remain separate inputs and sums.

The support hypotheses may hold on a proper open physical subdomain, such as t < 1 and physicalQ h < qbig. No global smoothness of an uncut stage, common annular radius for all stages, or blow-up of the resulting diagonal is postulated.

Actual copy sums vanish near the axis

theorem NavierStokes.MixedAxisPreservation.copy_sum_zero_germ {H : ℕ} {K : Type u_1} {f : PhysicalCopyBounds.CopyFamily H K} {a b h r0 Z : ℝ} {gap : ℕ} (hf : LocalPhysicalCopyBounds.SupportData f a b h r0 Z gap) (ha : 0 < a) (hh : 0 < h) (hh1 : h < 1 / 2) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (haxis : PhysicalGraphBounds.radialProjection w = 0) : f.sum a h r0 =ᶠ[nhds w] fun (x : ProblemStatement.SpaceTime) => 0

theorem NavierStokes.MixedAxisPreservation.copy_vector_zero_germ {H : ℕ} {K : Type u_1} {f : Fin 3 → PhysicalCopyBounds.CopyFamily H K} {a b h r0 Z : ℝ} {gap : ℕ} (hf : ∀ (i : Fin 3), LocalPhysicalCopyBounds.SupportData (f i) a b h r0 Z gap) (ha : 0 < a) (hh : 0 < h) (hh1 : h < 1 / 2) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (haxis : PhysicalGraphBounds.radialProjection w = 0) : PhysicalCopyBounds.vectorSum f a h r0 =ᶠ[nhds w] fun (x : ProblemStatement.SpaceTime) => 0

structure NavierStokes.MixedAxisPreservation.CopyPotential (h : ℝ) : Type (u + 1)

Primitive data for one actual vector-valued copy sum. Support cells retain the genuine locally finite meaning of the copy periodization.

• Copy : Type u

  Copy of CopyPotential, of type Type u.

• harmonics : ℕ

  Harmonics of CopyPotential, of type ℕ.

• family : Fin 3 → PhysicalCopyBounds.CopyFamily self.harmonics self.Copy

  Family of CopyPotential, of type Fin 3 → PhysicalCopyBounds.CopyFamily harmonics Copy.

• inner : ℝ

  Inner of CopyPotential, of type ℝ.

• outer : ℝ

  Outer of CopyPotential, of type ℝ.

• width : ℝ

  Width of CopyPotential, of type ℝ.

• axialRadius : ℝ

  Axial radius of CopyPotential, of type ℝ.

• gap : ℕ

  Gap of CopyPotential, of type ℕ.

• inner_pos : 0 < self.inner
• support (i : Fin 3) : LocalPhysicalCopyBounds.SupportData (self.family i) self.inner self.outer h self.width self.axialRadius self.gap
• cells (i : Fin 3) : PhysicalCopyBounds.SupportCells (self.family i)

  Cells of CopyPotential, of type ∀ i, PhysicalCopyBounds.SupportCells (family i).

noncomputable def NavierStokes.MixedAxisPreservation.CopyPotential.field {h : ℝ} (p : CopyPotential h) : ProblemStatement.VelocityField

Field, given by PhysicalCopyBounds.vectorSum p.family p.inner h p.width.

Equations

• p.field = NavierStokes.PhysicalCopyBounds.vectorSum p.family p.inner h p.width

theorem NavierStokes.MixedAxisPreservation.CopyPotential.zero_germ {h : ℝ} (p : CopyPotential h) (hh : 0 < h) (hh1 : h < 1 / 2) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (haxis : PhysicalGraphBounds.radialProjection w = 0) : p.field =ᶠ[nhds w] fun (x : ProblemStatement.SpaceTime) => 0

Local primitive support of the mean terms

structure NavierStokes.MixedAxisPreservation.AngularSupport (Ω : Set ProblemStatement.SpaceTime) : Type

Support of a literal angular scalar on the actual physical domain. Smoothness is deliberately absent: the domain can be the raw stage's small-q domain, and axis preservation uses only these support facts.

• scalar : DirectAngularDiagonal.Coefficient

  Scalar of AngularSupport, of type DirectAngularDiagonal.Coefficient.

• inner : DirectAngularDiagonal.Slow → ℝ

  Inner of AngularSupport, of type DirectAngularDiagonal.Slow → ℝ.

• inner_continuous : ContinuousOn (fun (w : ProblemStatement.SpaceTime) => self.inner (DirectAngularDiagonal.slowPoint w)) Ω
• inner_pos (w : ProblemStatement.SpaceTime) : w ∈ Ω → 0 < self.inner (DirectAngularDiagonal.slowPoint w)
• vanishes (w : ProblemStatement.SpaceTime) : w ∈ Ω → DirectAngularDiagonal.radius w < self.inner (DirectAngularDiagonal.slowPoint w) → self.scalar (DirectAngularDiagonal.cylPoint w) = 0

noncomputable def NavierStokes.MixedAxisPreservation.AngularSupport.field {Ω : Set ProblemStatement.SpaceTime} (D : AngularSupport Ω) : ProblemStatement.VelocityField

Field, given by DirectAngularDiagonal.angularField D.scalar.

Equations

• D.field = NavierStokes.DirectAngularDiagonal.angularField D.scalar

noncomputable def NavierStokes.MixedAxisPreservation.AngularSupport.zero (Ω : Set ProblemStatement.SpaceTime) : AngularSupport Ω

Zero, bundling scalar, inner, inner_continuous, inner_pos and the required compatibility proofs.

Equations

• NavierStokes.MixedAxisPreservation.AngularSupport.zero Ω = { scalar := 0, inner := fun (x : NavierStokes.DirectAngularDiagonal.Slow) => 1, inner_continuous := ⋯, inner_pos := ⋯, vanishes := ⋯ }

noncomputable def NavierStokes.MixedAxisPreservation.AngularSupport.add {Ω : Set ProblemStatement.SpaceTime} (D E : AngularSupport Ω) : AngularSupport Ω

Finite direct angular pieces can be combined without taking a radial or axial primitive. The inner support radius is their positive minimum.

Equations

• D.add E = { scalar := D.scalar + E.scalar, inner := fun (s : NavierStokes.DirectAngularDiagonal.Slow) => min (D.inner s) (E.inner s), inner_continuous := ⋯, inner_pos := ⋯, vanishes := ⋯ }

theorem NavierStokes.MixedAxisPreservation.AngularSupport.field_add {Ω : Set ProblemStatement.SpaceTime} (D E : AngularSupport Ω) : (D.add E).field = fun (w : ProblemStatement.SpaceTime) => D.field w + E.field w

noncomputable def NavierStokes.MixedAxisPreservation.AngularSupport.ofAngularData {U : Set DirectAngularDiagonal.Slow} (D : DirectAngularDiagonal.AngularData U) {Ω : Set ProblemStatement.SpaceTime} (hΩ : Ω ⊆ DirectAngularDiagonal.physicalDomain U) : AngularSupport Ω

Existing mean-field AngularData restricts to the required physical domain. Its actual scalar, normalization, and graph are unchanged.

Equations

• NavierStokes.MixedAxisPreservation.AngularSupport.ofAngularData D hΩ = { scalar := D.scalar, inner := D.inner, inner_continuous := ⋯, inner_pos := ⋯, vanishes := ⋯ }

theorem NavierStokes.MixedAxisPreservation.AngularSupport.zero_germ {Ω : Set ProblemStatement.SpaceTime} (D : AngularSupport Ω) (hΩ : IsOpen Ω) {w : ProblemStatement.SpaceTime} (hw : w ∈ Ω) (haxis : DirectAngularDiagonal.radius w = 0) : D.field =ᶠ[nhds w] fun (x : ProblemStatement.SpaceTime) => 0

theorem NavierStokes.MixedAxisPreservation.radius_zero_of_axis {w : ProblemStatement.SpaceTime} (haxis : PhysicalGraphBounds.radialProjection w = 0) : DirectAngularDiagonal.radius w = 0

structure NavierStokes.MixedAxisPreservation.PotentialStage (h : ℝ) (Ω : Set ProblemStatement.SpaceTime) : Type (u + 1)

One potential increment: finitely many actual copy-vector sums and finitely many literal azimuthal mean stream potentials. Direct angular velocities are not included in this potential.

• waveCount : ℕ

  Wave count of PotentialStage, of type ℕ.

• waves : Fin self.waveCount → CopyPotential h

  Waves of PotentialStage, of type Fin waveCount → CopyPotential.{u} h.

• streamCount : ℕ

  Stream count of PotentialStage, of type ℕ.

• streams : Fin self.streamCount → AngularSupport Ω

  Streams of PotentialStage, of type Fin streamCount → AngularSupport Ω.

noncomputable def NavierStokes.MixedAxisPreservation.PotentialStage.field {h : ℝ} {Ω : Set ProblemStatement.SpaceTime} (p : PotentialStage h Ω) : ProblemStatement.VelocityField

Field, defined pointwise by (∑ i : Fin p.waveCount, (p.waves i).field w) + ∑ i : Fin p.streamCount, (p.streams i).field w.

Equations

• p.field w = ∑ i : Fin p.waveCount, (p.waves i).field w + ∑ i : Fin p.streamCount, (p.streams i).field w

theorem NavierStokes.MixedAxisPreservation.PotentialStage.zero_germ {h : ℝ} {Ω : Set ProblemStatement.SpaceTime} (p : PotentialStage h Ω) (hh : 0 < h) (hh1 : h < 1 / 2) (hΩ : IsOpen Ω) {w : ProblemStatement.SpaceTime} (hw : w ∈ Ω) (ht : w ∈ PhysicalWaveSum.preterminal) (haxis : PhysicalGraphBounds.radialProjection w = 0) : p.field =ᶠ[nhds w] fun (x : ProblemStatement.SpaceTime) => 0

noncomputable def NavierStokes.MixedAxisPreservation.potentialSeries {h : ℝ} {Ω : Set ProblemStatement.SpaceTime} (base : ProblemStatement.VelocityField) (p : ℕ → PotentialStage h Ω) : ℕ → ProblemStatement.VelocityField

The zeroth potential is the anchored base; all positive stages are the constructed copy/mean increments.

Equations

• NavierStokes.MixedAxisPreservation.potentialSeries base p 0 = base
• NavierStokes.MixedAxisPreservation.potentialSeries base p j.succ = (p j).field

theorem NavierStokes.MixedAxisPreservation.potentialSeries_zero_germ {h : ℝ} {Ω : Set ProblemStatement.SpaceTime} (base : ProblemStatement.VelocityField) (p : ℕ → PotentialStage h Ω) (hh : 0 < h) (hh1 : h < 1 / 2) (hΩ : IsOpen Ω) {w : ProblemStatement.SpaceTime} (hw : w ∈ Ω) (ht : w ∈ PhysicalWaveSum.preterminal) (haxis : PhysicalGraphBounds.radialProjection w = 0) (j : ℕ) : j ≠ 0 → potentialSeries base p j =ᶠ[nhds w] fun (x : ProblemStatement.SpaceTime) => 0

The actual two diagonal sums

noncomputable def NavierStokes.MixedAxisPreservation.potentialDiagonal {h : ℝ} {Ω : Set ProblemStatement.SpaceTime} (base : ProblemStatement.VelocityField) (p : ℕ → PotentialStage h Ω) (scales : ℕ → ℝ) : ProblemStatement.VelocityField

Potential diagonal, given by SolenoidalDiagonal.potentialSum scales (PhysicalWaveSum.physicalQ h) (potentialSeries base p).

Equations

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

noncomputable def NavierStokes.MixedAxisPreservation.directDiagonal (h : ℝ) {Ω : Set ProblemStatement.SpaceTime} (D : ℕ → AngularSupport Ω) (scales : ℕ → ℝ) : ProblemStatement.VelocityField

Direct diagonal, given by DirectAngularDiagonal.angularSum scales (PhysicalWaveSum.physicalQ h) (fun j => (D j).scalar).

Equations

• NavierStokes.MixedAxisPreservation.directDiagonal h D scales = NavierStokes.DirectAngularDiagonal.angularSum scales (NavierStokes.PhysicalWaveSum.physicalQ h) fun (j : ℕ) => (D j).scalar

noncomputable def NavierStokes.MixedAxisPreservation.mixedDiagonal {h : ℝ} {Ω : Set ProblemStatement.SpaceTime} (base : ProblemStatement.VelocityField) (p : ℕ → PotentialStage h Ω) (D : ℕ → AngularSupport Ω) (scales : ℕ → ℝ) : ProblemStatement.VelocityField

Mixed diagonal, given by DirectAngularDiagonal.mixedVelocity scales (PhysicalWaveSum.physicalQ h) (potentialSeries base p) (fun j => (D j).scalar).

Equations

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

theorem NavierStokes.MixedAxisPreservation.mixedDiagonal_eq {h : ℝ} {Ω : Set ProblemStatement.SpaceTime} (base : ProblemStatement.VelocityField) (p : ℕ → PotentialStage h Ω) (D : ℕ → AngularSupport Ω) (scales : ℕ → ℝ) : mixedDiagonal base p D scales = fun (w : ProblemStatement.SpaceTime) => SpatialCurl.spatialCurl (potentialDiagonal base p scales) w + directDiagonal h D scales w

theorem NavierStokes.MixedAxisPreservation.directDiagonal_zero_germ {h : ℝ} {Ω : Set ProblemStatement.SpaceTime} (D : ℕ → AngularSupport Ω) (hh : 0 < h) (hh1 : h < 1 / 2) {scales : ℕ → ℝ} (hs : Filter.Tendsto scales Filter.atTop Filter.atTop) (hΩ : IsOpen Ω) {w : ProblemStatement.SpaceTime} (hw : w ∈ Ω) (ht : w ∈ PhysicalWaveSum.preterminal) (haxis : PhysicalGraphBounds.radialProjection w = 0) : directDiagonal h D scales =ᶠ[nhds w] fun (x : ProblemStatement.SpaceTime) => 0

theorem NavierStokes.MixedAxisPreservation.potentialDiagonal_eq_cutBase_germ {h : ℝ} {Ω : Set ProblemStatement.SpaceTime} (base : ProblemStatement.VelocityField) (p : ℕ → PotentialStage h Ω) (hh : 0 < h) (hh1 : h < 1 / 2) {scales : ℕ → ℝ} (hs : Filter.Tendsto scales Filter.atTop Filter.atTop) (hΩ : IsOpen Ω) {w : ProblemStatement.SpaceTime} (hw : w ∈ Ω) (ht : w ∈ PhysicalWaveSum.preterminal) (haxis : PhysicalGraphBounds.radialProjection w = 0) : potentialDiagonal base p scales =ᶠ[nhds w] fun (y : ProblemStatement.SpaceTime) => SmoothCutoffs.scaledCutoff (scales 0) (PhysicalWaveSum.physicalQ h y) • base y

theorem NavierStokes.MixedAxisPreservation.mixedDiagonal_eq_cutBase_germ {h : ℝ} {Ω : Set ProblemStatement.SpaceTime} (base : ProblemStatement.VelocityField) (p : ℕ → PotentialStage h Ω) (D : ℕ → AngularSupport Ω) (hh : 0 < h) (hh1 : h < 1 / 2) {scales : ℕ → ℝ} (hs : Filter.Tendsto scales Filter.atTop Filter.atTop) (hΩ : IsOpen Ω) {w : ProblemStatement.SpaceTime} (hw : w ∈ Ω) (ht : w ∈ PhysicalWaveSum.preterminal) (haxis : PhysicalGraphBounds.radialProjection w = 0) : mixedDiagonal base p D scales =ᶠ[nhds w] SpatialCurl.spatialCurl fun (y : ProblemStatement.SpaceTime) => SmoothCutoffs.scaledCutoff (scales 0) (PhysicalWaveSum.physicalQ h y) • base y

Every preterminal axis germ in the support domain is the curl of the cut base, even before its zeroth cutoff has reached the plateau.

theorem NavierStokes.MixedAxisPreservation.mixedDiagonal_eq_base_germ {h : ℝ} {Ω : Set ProblemStatement.SpaceTime} (base : ProblemStatement.VelocityField) (p : ℕ → PotentialStage h Ω) (D : ℕ → AngularSupport Ω) (hh : 0 < h) (hh1 : h < 1 / 2) {scales : ℕ → ℝ} (hs : Filter.Tendsto scales Filter.atTop Filter.atTop) (hΩ : IsOpen Ω) {w : ProblemStatement.SpaceTime} (hw : w ∈ Ω) (ht : w ∈ PhysicalWaveSum.preterminal) (haxis : PhysicalGraphBounds.radialProjection w = 0) (hsmall : |scales 0 * PhysicalWaveSum.physicalQ h w| < 1 / 2) : mixedDiagonal base p D scales =ᶠ[nhds w] SpatialCurl.spatialCurl base

On the zeroth cutoff plateau all potential and direct corrections preserve the base curl on a neighborhood, not just at a point.

theorem NavierStokes.MixedAxisPreservation.mixedDiagonal_axis_jets {h : ℝ} {Ω : Set ProblemStatement.SpaceTime} (base : ProblemStatement.VelocityField) (p : ℕ → PotentialStage h Ω) (D : ℕ → AngularSupport Ω) (hh : 0 < h) (hh1 : h < 1 / 2) {scales : ℕ → ℝ} (hs : Filter.Tendsto scales Filter.atTop Filter.atTop) (hΩ : IsOpen Ω) {w : ProblemStatement.SpaceTime} (hw : w ∈ Ω) (ht : w ∈ PhysicalWaveSum.preterminal) (haxis : PhysicalGraphBounds.radialProjection w = 0) (hsmall : |scales 0 * PhysicalWaveSum.physicalQ h w| < 1 / 2) (k : ℕ) : iteratedFDeriv ℝ k (mixedDiagonal base p D scales) w = iteratedFDeriv ℝ k (SpatialCurl.spatialCurl base) w

theorem NavierStokes.MixedAxisPreservation.radialProjection_origin (t : ℝ) : PhysicalGraphBounds.radialProjection (t, 0) = 0

theorem NavierStokes.MixedAxisPreservation.origin_eventually_base_germ {h : ℝ} {Ω : Set ProblemStatement.SpaceTime} (base : ProblemStatement.VelocityField) (p : ℕ → PotentialStage h Ω) (D : ℕ → AngularSupport Ω) (hh : 0 < h) (hh1 : h < 1 / 2) {scales : ℕ → ℝ} (hs : Filter.Tendsto scales Filter.atTop Filter.atTop) (hΩ : IsOpen Ω) (hΩaxis : ∀ᶠ (t : ℝ) in nhdsWithin 1 (Set.Iio 1), (t, 0) ∈ Ω) : ∀ᶠ (t : ℝ) in nhdsWithin 1 (Set.Iio 1), mixedDiagonal base p D scales =ᶠ[nhds (t, 0)] SpatialCurl.spatialCurl base

Only eventual support near the terminal origin is needed; the raw increments can have a smaller domain than the whole preterminal region.

theorem NavierStokes.MixedAxisPreservation.origin_eventually_eq_base {h : ℝ} {Ω : Set ProblemStatement.SpaceTime} (base : ProblemStatement.VelocityField) (p : ℕ → PotentialStage h Ω) (D : ℕ → AngularSupport Ω) (hh : 0 < h) (hh1 : h < 1 / 2) {scales : ℕ → ℝ} (hs : Filter.Tendsto scales Filter.atTop Filter.atTop) (hΩ : IsOpen Ω) (hΩaxis : ∀ᶠ (t : ℝ) in nhdsWithin 1 (Set.Iio 1), (t, 0) ∈ Ω) : (fun (t : ℝ) => mixedDiagonal base p D scales (t, 0)) =ᶠ[nhdsWithin 1 (Set.Iio 1)] fun (t : ℝ) => SpatialCurl.spatialCurl base (t, 0)

theorem NavierStokes.MixedAxisPreservation.origin_blowup {h : ℝ} {Ω : Set ProblemStatement.SpaceTime} (base : ProblemStatement.VelocityField) (p : ℕ → PotentialStage h Ω) (D : ℕ → AngularSupport Ω) (hh : 0 < h) (hh1 : h < 1 / 2) {scales : ℕ → ℝ} (hs : Filter.Tendsto scales Filter.atTop Filter.atTop) (hΩ : IsOpen Ω) (hΩaxis : ∀ᶠ (t : ℝ) in nhdsWithin 1 (Set.Iio 1), (t, 0) ∈ Ω) (hbase : Filter.Tendsto (fun (t : ℝ) => ‖SpatialCurl.spatialCurl base (t, 0)‖) (nhdsWithin 1 (Set.Iio 1)) Filter.atTop) : Filter.Tendsto (fun (t : ℝ) => ‖mixedDiagonal base p D scales (t, 0)‖) (nhdsWithin 1 (Set.Iio 1)) Filter.atTop

Finite initialization stays in stage zero

noncomputable def NavierStokes.MixedAxisPreservation.initializedBase {h : ℝ} {Ω : Set ProblemStatement.SpaceTime} (base : ProblemStatement.VelocityField) (initial : PotentialStage h Ω) : ProblemStatement.VelocityField

Initialized base, defined pointwise by base w + initial.field w.

Equations

• NavierStokes.MixedAxisPreservation.initializedBase base initial w = base w + initial.field w

noncomputable def NavierStokes.MixedAxisPreservation.initializedSeries {h : ℝ} {Ω : Set ProblemStatement.SpaceTime} (base : ProblemStatement.VelocityField) (initial : PotentialStage h Ω) (p : ℕ → PotentialStage h Ω) : ℕ → ProblemStatement.VelocityField

This is the manuscript's stage numbering: the finite initialization and base share cutoff zero; each subsequent stage has its own cutoff.

Equations

• NavierStokes.MixedAxisPreservation.initializedSeries base initial p = NavierStokes.MixedAxisPreservation.potentialSeries (NavierStokes.MixedAxisPreservation.initializedBase base initial) p

noncomputable def NavierStokes.MixedAxisPreservation.initializedDiagonal {h : ℝ} {Ω : Set ProblemStatement.SpaceTime} (base : ProblemStatement.VelocityField) (initial : PotentialStage h Ω) (p : ℕ → PotentialStage h Ω) (D : ℕ → AngularSupport Ω) (scales : ℕ → ℝ) : ProblemStatement.VelocityField

Initialized diagonal, given by mixedDiagonal (initializedBase base initial) p D scales.

Equations

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

theorem NavierStokes.MixedAxisPreservation.initializedSeries_zero {h : ℝ} {Ω : Set ProblemStatement.SpaceTime} (base : ProblemStatement.VelocityField) (initial : PotentialStage h Ω) (p : ℕ → PotentialStage h Ω) (w : ProblemStatement.SpaceTime) : initializedSeries base initial p 0 w = base w + initial.field w

theorem NavierStokes.MixedAxisPreservation.initializedSeries_succ {h : ℝ} {Ω : Set ProblemStatement.SpaceTime} (base : ProblemStatement.VelocityField) (initial : PotentialStage h Ω) (p : ℕ → PotentialStage h Ω) (j : ℕ) : initializedSeries base initial p (j + 1) = (p j).field

theorem NavierStokes.MixedAxisPreservation.initializedDiagonal_eq {h : ℝ} {Ω : Set ProblemStatement.SpaceTime} (base : ProblemStatement.VelocityField) (initial : PotentialStage h Ω) (p : ℕ → PotentialStage h Ω) (D : ℕ → AngularSupport Ω) (scales : ℕ → ℝ) : initializedDiagonal base initial p D scales = DirectAngularDiagonal.mixedVelocity scales (PhysicalWaveSum.physicalQ h) (initializedSeries base initial p) fun (j : ℕ) => (D j).scalar

theorem NavierStokes.MixedAxisPreservation.initializedBase_germ {h : ℝ} {Ω : Set ProblemStatement.SpaceTime} (base : ProblemStatement.VelocityField) (initial : PotentialStage h Ω) (hh : 0 < h) (hh1 : h < 1 / 2) (hΩ : IsOpen Ω) {w : ProblemStatement.SpaceTime} (hw : w ∈ Ω) (ht : w ∈ PhysicalWaveSum.preterminal) (haxis : PhysicalGraphBounds.radialProjection w = 0) : initializedBase base initial =ᶠ[nhds w] base

theorem NavierStokes.MixedAxisPreservation.initialized_eq_base_germ {h : ℝ} {Ω : Set ProblemStatement.SpaceTime} (base : ProblemStatement.VelocityField) (initial : PotentialStage h Ω) (p : ℕ → PotentialStage h Ω) (D : ℕ → AngularSupport Ω) (hh : 0 < h) (hh1 : h < 1 / 2) {scales : ℕ → ℝ} (hs : Filter.Tendsto scales Filter.atTop Filter.atTop) (hΩ : IsOpen Ω) {w : ProblemStatement.SpaceTime} (hw : w ∈ Ω) (ht : w ∈ PhysicalWaveSum.preterminal) (haxis : PhysicalGraphBounds.radialProjection w = 0) (hsmall : |scales 0 * PhysicalWaveSum.physicalQ h w| < 1 / 2) : initializedDiagonal base initial p D scales =ᶠ[nhds w] SpatialCurl.spatialCurl base

theorem NavierStokes.MixedAxisPreservation.initialized_axis_jets {h : ℝ} {Ω : Set ProblemStatement.SpaceTime} (base : ProblemStatement.VelocityField) (initial : PotentialStage h Ω) (p : ℕ → PotentialStage h Ω) (D : ℕ → AngularSupport Ω) (hh : 0 < h) (hh1 : h < 1 / 2) {scales : ℕ → ℝ} (hs : Filter.Tendsto scales Filter.atTop Filter.atTop) (hΩ : IsOpen Ω) {w : ProblemStatement.SpaceTime} (hw : w ∈ Ω) (ht : w ∈ PhysicalWaveSum.preterminal) (haxis : PhysicalGraphBounds.radialProjection w = 0) (hsmall : |scales 0 * PhysicalWaveSum.physicalQ h w| < 1 / 2) (k : ℕ) : iteratedFDeriv ℝ k (initializedDiagonal base initial p D scales) w = iteratedFDeriv ℝ k (SpatialCurl.spatialCurl base) w

theorem NavierStokes.MixedAxisPreservation.initialized_origin_eventually {h : ℝ} {Ω : Set ProblemStatement.SpaceTime} (base : ProblemStatement.VelocityField) (initial : PotentialStage h Ω) (p : ℕ → PotentialStage h Ω) (D : ℕ → AngularSupport Ω) (hh : 0 < h) (hh1 : h < 1 / 2) {scales : ℕ → ℝ} (hs : Filter.Tendsto scales Filter.atTop Filter.atTop) (hΩ : IsOpen Ω) (hΩaxis : ∀ᶠ (t : ℝ) in nhdsWithin 1 (Set.Iio 1), (t, 0) ∈ Ω) : ∀ᶠ (t : ℝ) in nhdsWithin 1 (Set.Iio 1), initializedDiagonal base initial p D scales =ᶠ[nhds (t, 0)] SpatialCurl.spatialCurl base

theorem NavierStokes.MixedAxisPreservation.initialized_origin_blowup {h : ℝ} {Ω : Set ProblemStatement.SpaceTime} (base : ProblemStatement.VelocityField) (initial : PotentialStage h Ω) (p : ℕ → PotentialStage h Ω) (D : ℕ → AngularSupport Ω) (hh : 0 < h) (hh1 : h < 1 / 2) {scales : ℕ → ℝ} (hs : Filter.Tendsto scales Filter.atTop Filter.atTop) (hΩ : IsOpen Ω) (hΩaxis : ∀ᶠ (t : ℝ) in nhdsWithin 1 (Set.Iio 1), (t, 0) ∈ Ω) (hbase : Filter.Tendsto (fun (t : ℝ) => ‖SpatialCurl.spatialCurl base (t, 0)‖) (nhdsWithin 1 (Set.Iio 1)) Filter.atTop) : Filter.Tendsto (fun (t : ℝ) => ‖initializedDiagonal base initial p D scales (t, 0)‖) (nhdsWithin 1 (Set.Iio 1)) Filter.atTop

The actual small-similarity-parameter domain

noncomputable def NavierStokes.MixedAxisPreservation.localDomain (h qbig : ℝ) : Set ProblemStatement.SpaceTime

Local domain, given by {w | w.1 < 1 ∧ PhysicalWaveSum.physicalQ h w < qbig}.

Equations

• NavierStokes.MixedAxisPreservation.localDomain h qbig = {w : NavierStokes.ProblemStatement.SpaceTime | w.1 < 1 ∧ NavierStokes.PhysicalWaveSum.physicalQ h w < qbig}

theorem NavierStokes.MixedAxisPreservation.localDomain_open {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (qbig : ℝ) : IsOpen (localDomain h qbig)

theorem NavierStokes.MixedAxisPreservation.origin_eventually_localDomain {h qbig : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hqbig : 0 < qbig) : ∀ᶠ (t : ℝ) in nhdsWithin 1 (Set.Iio 1), (t, 0) ∈ localDomain h qbig

Compatibility with the global axis-preservation endpoint

theorem NavierStokes.MixedAxisPreservation.origin_blowup_global {h : ℝ} (base : ProblemStatement.VelocityField) (p : ℕ → PotentialStage h PhysicalWaveSum.preterminal) (D : ℕ → AngularSupport PhysicalWaveSum.preterminal) (hh : 0 < h) (hh1 : h < 1 / 2) {scales : ℕ → ℝ} (hs : Filter.Tendsto scales Filter.atTop Filter.atTop) (hbase : Filter.Tendsto (fun (t : ℝ) => ‖SpatialCurl.spatialCurl base (t, 0)‖) (nhdsWithin 1 (Set.Iio 1)) Filter.atTop) : Filter.Tendsto (fun (t : ℝ) => ‖mixedDiagonal base p D scales (t, 0)‖) (nhdsWithin 1 (Set.Iio 1)) Filter.atTop

When support is known on the full preterminal region, the existing AxisPreservation.origin_blowup theorem applies to the actual copy series. The local-domain theorem above does not require this stronger hypothesis.

The anchored base supplies the actual blow-up

theorem NavierStokes.MixedAxisPreservation.anchored_base_axis_tendsto {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) : Filter.Tendsto (fun (t : ℝ) => ‖SpatialCurl.spatialCurl (TailGaugePotential.finalPotential H v upper B) (t, 0)‖) (nhdsWithin 1 (Set.Iio 1)) Filter.atTop

theorem NavierStokes.MixedAxisPreservation.final_origin_eventually {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) {Ω : Set ProblemStatement.SpaceTime} (p : ℕ → PotentialStage F.data.h Ω) (D : ℕ → AngularSupport Ω) {scales : ℕ → ℝ} (hs : Filter.Tendsto scales Filter.atTop Filter.atTop) (hΩ : IsOpen Ω) (hΩaxis : ∀ᶠ (t : ℝ) in nhdsWithin 1 (Set.Iio 1), (t, 0) ∈ Ω) : (fun (t : ℝ) => mixedDiagonal (TailGaugePotential.finalPotential H v upper B) p D scales (t, 0)) =ᶠ[nhdsWithin 1 (Set.Iio 1)] fun (t : ℝ) => ((1 - t) ^ (-CoordinateAlgebra.A F.data.h) * W.axis.j) • ProblemStatement.coordinateVector 2

theorem NavierStokes.MixedAxisPreservation.final_origin_blowup {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) {Ω : Set ProblemStatement.SpaceTime} (p : ℕ → PotentialStage F.data.h Ω) (D : ℕ → AngularSupport Ω) {scales : ℕ → ℝ} (hs : Filter.Tendsto scales Filter.atTop Filter.atTop) (hΩ : IsOpen Ω) (hΩaxis : ∀ᶠ (t : ℝ) in nhdsWithin 1 (Set.Iio 1), (t, 0) ∈ Ω) : Filter.Tendsto (fun (t : ℝ) => ‖mixedDiagonal (TailGaugePotential.finalPotential H v upper B) p D scales (t, 0)‖) (nhdsWithin 1 (Set.Iio 1)) Filter.atTop

theorem NavierStokes.MixedAxisPreservation.final_speedUnbounded {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) {Ω : Set ProblemStatement.SpaceTime} (p : ℕ → PotentialStage F.data.h Ω) (D : ℕ → AngularSupport Ω) {scales : ℕ → ℝ} (hs : Filter.Tendsto scales Filter.atTop Filter.atTop) (hΩ : IsOpen Ω) (hΩaxis : ∀ᶠ (t : ℝ) in nhdsWithin 1 (Set.Iio 1), (t, 0) ∈ Ω) : ProblemStatement.SpeedUnboundedAtOne (mixedDiagonal (TailGaugePotential.finalPotential H v upper B) p D scales)

theorem NavierStokes.MixedAxisPreservation.local_final_origin_blowup {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) {qbig : ℝ} (hqbig : 0 < qbig) (p : ℕ → PotentialStage F.data.h (localDomain F.data.h qbig)) (D : ℕ → AngularSupport (localDomain F.data.h qbig)) {scales : ℕ → ℝ} (hs : Filter.Tendsto scales Filter.atTop Filter.atTop) : Filter.Tendsto (fun (t : ℝ) => ‖mixedDiagonal (TailGaugePotential.finalPotential H v upper B) p D scales (t, 0)‖) (nhdsWithin 1 (Set.Iio 1)) Filter.atTop

Raw stage support is needed only where q < qbig. The concrete base, the actual cutoff scale, and the literal mixed sums are kept throughout.

theorem NavierStokes.MixedAxisPreservation.local_final_speedUnbounded {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) {qbig : ℝ} (hqbig : 0 < qbig) (p : ℕ → PotentialStage F.data.h (localDomain F.data.h qbig)) (D : ℕ → AngularSupport (localDomain F.data.h qbig)) {scales : ℕ → ℝ} (hs : Filter.Tendsto scales Filter.atTop Filter.atTop) : ProblemStatement.SpeedUnboundedAtOne (mixedDiagonal (TailGaugePotential.finalPotential H v upper B) p D scales)

theorem NavierStokes.MixedAxisPreservation.local_initialized_final_origin_blowup {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) {qbig : ℝ} (hqbig : 0 < qbig) (initial : PotentialStage F.data.h (localDomain F.data.h qbig)) (p : ℕ → PotentialStage F.data.h (localDomain F.data.h qbig)) (D : ℕ → AngularSupport (localDomain F.data.h qbig)) {scales : ℕ → ℝ} (hs : Filter.Tendsto scales Filter.atTop Filter.atTop) : Filter.Tendsto (fun (t : ℝ) => ‖initializedDiagonal (TailGaugePotential.finalPotential H v upper B) initial p D scales (t, 0)‖) (nhdsWithin 1 (Set.Iio 1)) Filter.atTop

theorem NavierStokes.MixedAxisPreservation.local_initialized_final_speedUnbounded {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) {qbig : ℝ} (hqbig : 0 < qbig) (initial : PotentialStage F.data.h (localDomain F.data.h qbig)) (p : ℕ → PotentialStage F.data.h (localDomain F.data.h qbig)) (D : ℕ → AngularSupport (localDomain F.data.h qbig)) {scales : ℕ → ℝ} (hs : Filter.Tendsto scales Filter.atTop Filter.atTop) : ProblemStatement.SpeedUnboundedAtOne (initializedDiagonal (TailGaugePotential.finalPotential H v upper B) initial p D scales)

noncomputable def NavierStokes.MixedAxisPreservation.constructedExponent : ℝ

The exponent belongs to the already selected, constructed profile.

Equations

• NavierStokes.MixedAxisPreservation.constructedExponent = NavierStokes.FinalSlowBase.actualProfile.outgoing.data.h

theorem NavierStokes.MixedAxisPreservation.constructed_origin_blowup (upper : ℝ) (B : ℕ) {qbig : ℝ} (hqbig : 0 < qbig) (p : ℕ → PotentialStage constructedExponent (localDomain constructedExponent qbig)) (D : ℕ → AngularSupport (localDomain constructedExponent qbig)) {scales : ℕ → ℝ} (hs : Filter.Tendsto scales Filter.atTop Filter.atTop) : Filter.Tendsto (fun (t : ℝ) => ‖mixedDiagonal (TailGaugePotential.constructedPotential upper B) p D scales (t, 0)‖) (nhdsWithin 1 (Set.Iio 1)) Filter.atTop

theorem NavierStokes.MixedAxisPreservation.constructed_speedUnbounded (upper : ℝ) (B : ℕ) {qbig : ℝ} (hqbig : 0 < qbig) (p : ℕ → PotentialStage constructedExponent (localDomain constructedExponent qbig)) (D : ℕ → AngularSupport (localDomain constructedExponent qbig)) {scales : ℕ → ℝ} (hs : Filter.Tendsto scales Filter.atTop Filter.atTop) : ProblemStatement.SpeedUnboundedAtOne (mixedDiagonal (TailGaugePotential.constructedPotential upper B) p D scales)

theorem NavierStokes.MixedAxisPreservation.initialized_constructed_origin_blowup (upper : ℝ) (B : ℕ) {qbig : ℝ} (hqbig : 0 < qbig) (initial : PotentialStage constructedExponent (localDomain constructedExponent qbig)) (p : ℕ → PotentialStage constructedExponent (localDomain constructedExponent qbig)) (D : ℕ → AngularSupport (localDomain constructedExponent qbig)) {scales : ℕ → ℝ} (hs : Filter.Tendsto scales Filter.atTop Filter.atTop) : Filter.Tendsto (fun (t : ℝ) => ‖initializedDiagonal (TailGaugePotential.constructedPotential upper B) initial p D scales (t, 0)‖) (nhdsWithin 1 (Set.Iio 1)) Filter.atTop

theorem NavierStokes.MixedAxisPreservation.initialized_constructed_speedUnbounded (upper : ℝ) (B : ℕ) {qbig : ℝ} (hqbig : 0 < qbig) (initial : PotentialStage constructedExponent (localDomain constructedExponent qbig)) (p : ℕ → PotentialStage constructedExponent (localDomain constructedExponent qbig)) (D : ℕ → AngularSupport (localDomain constructedExponent qbig)) {scales : ℕ → ℝ} (hs : Filter.Tendsto scales Filter.atTop Filter.atTop) : ProblemStatement.SpeedUnboundedAtOne (initializedDiagonal (TailGaugePotential.constructedPotential upper B) initial p D scales)