Residual estimates for the mixed diagonal sum

The direct angular increments are summed as velocity fields, while the potential increments are differentiated after cutoff. Both use the same scale sequence. The actual mixed tail is estimated from these two different operations; it is not identified with the curl of an unspecified potential.

The finite uncut background and residual estimates are explicit inputs from the correction construction. The infinite-tail estimates and the resulting residual decay are proved here.

One physical diagonal schedule for potentials, direct fields, and pressure

The three input sequences are fixed actual fields. Separate raw losses and logarithmic factors are combined before applying the proved cutoff estimates. The initial stage is retained explicitly in every resulting full sum.

@[reducible, inline]

abbrev NavierStokes.MixedDiagonalSchedule.Component : Type

Component: an abbreviation for Fin 3.

Equations

• NavierStokes.MixedDiagonalSchedule.Component = Fin 3

noncomputable def NavierStokes.MixedDiagonalSchedule.Component.potential : Component

Potential, given by 0.

Equations

• NavierStokes.MixedDiagonalSchedule.Component.potential = 0

noncomputable def NavierStokes.MixedDiagonalSchedule.Component.direct : Component

Direct, given by 1.

Equations

• NavierStokes.MixedDiagonalSchedule.Component.direct = 1

noncomputable def NavierStokes.MixedDiagonalSchedule.Component.pressure : Component

Pressure, given by 2.

Equations

• NavierStokes.MixedDiagonalSchedule.Component.pressure = 2

@[reducible]

noncomputable def NavierStokes.MixedDiagonalSchedule.ComponentSpace (c : Component) : Type

Component space, with branches according to c = 2.

Equations

• NavierStokes.MixedDiagonalSchedule.ComponentSpace c = if c = 2 then ℝ else NavierStokes.ProblemStatement.Space

@[instance_reducible]

noncomputable instance NavierStokes.MixedDiagonalSchedule.instNormedAddCommGroupComponentSpace (c : Component) : NormedAddCommGroup (ComponentSpace c)

Equations

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

@[instance_reducible]

noncomputable instance NavierStokes.MixedDiagonalSchedule.instNormedSpaceRealComponentSpace (c : Component) : NormedSpace ℝ (ComponentSpace c)

Equations

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

noncomputable def NavierStokes.MixedDiagonalSchedule.family (A B : ℕ → ProblemStatement.VelocityField) (P : ℕ → ProblemStatement.PressureField) (c : Component) : ℕ → ProblemStatement.SpaceTime → ComponentSpace c

Literal component selection; no new physical fields are chosen.

Equations

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

noncomputable def NavierStokes.MixedDiagonalSchedule.scalarFamily (A B P : ℕ → ℕ → ℝ) : Component → ℕ → ℕ → ℝ

Scalar family, given by Fin.cases A (Fin.cases B (Fin.cases P (fun i => Fin.elim0 i))).

Equations

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

noncomputable def NavierStokes.MixedDiagonalSchedule.commonRawLoss (LA LB LP : ℕ → ℝ) (m : ℕ) : ℝ

Common raw loss, given by max (LA m) (max (LB m) (LP m)).

Equations

• NavierStokes.MixedDiagonalSchedule.commonRawLoss LA LB LP m = max (LA m) (max (LB m) (LP m))

noncomputable def NavierStokes.MixedDiagonalSchedule.commonLoss (LA LB LP : ℕ → ℝ) : ℕ → ℝ

Common loss, given by CutStageEstimates.cutLoss (commonRawLoss LA LB LP).

Equations

• NavierStokes.MixedDiagonalSchedule.commonLoss LA LB LP = NavierStokes.CutStageEstimates.cutLoss (NavierStokes.MixedDiagonalSchedule.commonRawLoss LA LB LP)

theorem NavierStokes.MixedDiagonalSchedule.potential_loss_le (LA LB LP : ℕ → ℝ) (m : ℕ) : LA m ≤ commonRawLoss LA LB LP m

theorem NavierStokes.MixedDiagonalSchedule.direct_loss_le (LA LB LP : ℕ → ℝ) (m : ℕ) : LB m ≤ commonRawLoss LA LB LP m

theorem NavierStokes.MixedDiagonalSchedule.pressure_loss_le (LA LB LP : ℕ → ℝ) (m : ℕ) : LP m ≤ commonRawLoss LA LB LP m

structure NavierStokes.MixedDiagonalSchedule.ThreeCutBounds (a : ℕ → ℕ) (h : ℝ) (A B : ℕ → ProblemStatement.VelocityField) (P : ℕ → ProblemStatement.PressureField) (g L : ℕ → ℝ) (S : Set ProblemStatement.SpaceTime) : Prop

The simultaneous estimates required by the mixed residual consumer. All three refer to the supplied full sequences, including their initial terms.

• potential : DiagonalJetBounds.CutStageBounds (fun (j : ℕ) => ↑(a j)) (PhysicalWaveSum.physicalQ h) A g L S
• direct : DiagonalJetBounds.CutStageBounds (fun (j : ℕ) => ↑(a j)) (PhysicalWaveSum.physicalQ h) B g L S
• pressure : DiagonalJetBounds.CutStageBounds (fun (j : ℕ) => ↑(a j)) (PhysicalWaveSum.physicalQ h) P g L S

structure NavierStokes.MixedDiagonalSchedule.ThreeSmoothSums (a : ℕ → ℕ) (h : ℝ) (A B : ℕ → ProblemStatement.VelocityField) (P : ℕ → ProblemStatement.PressureField) : Prop

Three smooth sums data, collecting potential, direct, pressure.

• potential : ContDiffOn ℝ (↑⊤) (SolenoidalDiagonal.potentialSum (fun (j : ℕ) => ↑(a j)) (PhysicalWaveSum.physicalQ h) A) PhysicalWaveSum.preterminal
• direct : ContDiffOn ℝ (↑⊤) (SolenoidalDiagonal.potentialSum (fun (j : ℕ) => ↑(a j)) (PhysicalWaveSum.physicalQ h) B) PhysicalWaveSum.preterminal
• pressure : ContDiffOn ℝ (↑⊤) (SolenoidalDiagonal.potentialSum (fun (j : ℕ) => ↑(a j)) (PhysicalWaveSum.physicalQ h) P) PhysicalWaveSum.preterminal

theorem NavierStokes.MixedDiagonalSchedule.raw_bounds_mono_loss {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {q : E → ℝ} {A : ℕ → E → V} {g L L' : ℕ → ℝ} {C p : ℕ → ℕ → ℝ} {S : Set E} (hpos : ∀ x ∈ S, 0 < q x) (hL : ∀ (m : ℕ), L m ≤ L' m) (hb : CutStageEstimates.RawStageBounds q A g L C p S) : CutStageEstimates.RawStageBounds q A g L' (fun (j m : ℕ) => |C j m|) p S

Enlarge only the fixed derivative loss. Absolute values remove any unnecessary sign assumption on the originally supplied raw constants.

theorem NavierStokes.MixedDiagonalSchedule.cut_bounds_of_positiveStages {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {a : ℕ → ℝ} {q : E → ℝ} {A : ℕ → E → V} {g L : ℕ → ℝ} {S : Set E} (hb : DiagonalJetBounds.CutStageBounds a q (CutStageEstimates.positiveStages A) g L S) : DiagonalJetBounds.CutStageBounds a q A g L S

Suppressing stage zero does not change any positive-stage estimate.

theorem NavierStokes.MixedDiagonalSchedule.exists_three_component_schedule {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {S : Set ProblemStatement.SpaceTime} (hS : S ⊆ PhysicalWaveSum.preterminal) {A B : ℕ → ProblemStatement.VelocityField} {P : ℕ → ProblemStatement.PressureField} (hA : ∀ (j : ℕ), 1 ≤ j → ContDiffOn ℝ (↑⊤) (A j) PhysicalWaveSum.preterminal) (hB : ∀ (j : ℕ), 1 ≤ j → ContDiffOn ℝ (↑⊤) (B j) PhysicalWaveSum.preterminal) (hP : ∀ (j : ℕ), 1 ≤ j → ContDiffOn ℝ (↑⊤) (P j) PhysicalWaveSum.preterminal) (g LA LB LP : ℕ → ℝ) (CA CB CP pA pB pP : ℕ → ℕ → ℝ) (rawA : CutStageEstimates.RawStageBounds (PhysicalWaveSum.physicalQ h) A g LA CA pA S) (rawB : CutStageEstimates.RawStageBounds (PhysicalWaveSum.physicalQ h) B g LB CB pB S) (rawP : CutStageEstimates.RawStageBounds (PhysicalWaveSum.physicalQ h) P g LP CP pP S) (hg : ∀ (j : ℕ), 1 ≤ j → 0 < g j) (lower : ℕ) : ∃ (a : ℕ → ℕ), lower ≤ a 0 ∧ (∀ (j : ℕ), 0 < a j) ∧ (∀ (j : ℕ), 2 * a j ≤ a (j + 1)) ∧ StrictMono a ∧ Filter.Tendsto (fun (j : ℕ) => ↑(a j)) Filter.atTop Filter.atTop ∧ ThreeCutBounds a h A B P (fun (j : ℕ) => g j / 2) (commonLoss LA LB LP) S

Simultaneous bounds for the fixed three input families and one actual integer schedule. No cut-stage estimate is a hypothesis.

theorem NavierStokes.MixedDiagonalSchedule.full_sum_eq_initial_add_positive {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup V] [NormedSpace ℝ V] {a : ℕ → ℝ} (ha : Filter.Tendsto a Filter.atTop Filter.atTop) {q : E → ℝ} {x : E} (hq : ContinuousAt q x) (hpos : 0 < q x) (A : ℕ → E → V) : SolenoidalDiagonal.potentialSum a q A x = SolenoidalDiagonal.cutStage a q A 0 x + SolenoidalDiagonal.potentialSum a q (CutStageEstimates.positiveStages A) x

Exact initial-stage bookkeeping for the actual sum. The full sequence is never replaced by its positive part without retaining this first term.

theorem NavierStokes.MixedDiagonalSchedule.physical_initial_split {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {a : ℕ → ℕ} (ha : StrictMono a) {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : ℕ → ProblemStatement.SpaceTime → V) : Set.EqOn (SolenoidalDiagonal.potentialSum (fun (j : ℕ) => ↑(a j)) (PhysicalWaveSum.physicalQ h) A) (fun (w : ProblemStatement.SpaceTime) => SolenoidalDiagonal.cutStage (fun (j : ℕ) => ↑(a j)) (PhysicalWaveSum.physicalQ h) A 0 w + SolenoidalDiagonal.potentialSum (fun (j : ℕ) => ↑(a j)) (PhysicalWaveSum.physicalQ h) (CutStageEstimates.positiveStages A) w) PhysicalWaveSum.preterminal

theorem NavierStokes.MixedDiagonalSchedule.physical_initial_split_germ {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {a : ℕ → ℕ} (ha : StrictMono a) {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : ℕ → ProblemStatement.SpaceTime → V) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) : SolenoidalDiagonal.potentialSum (fun (j : ℕ) => ↑(a j)) (PhysicalWaveSum.physicalQ h) A =ᶠ[nhds w] fun (z : ProblemStatement.SpaceTime) => SolenoidalDiagonal.cutStage (fun (j : ℕ) => ↑(a j)) (PhysicalWaveSum.physicalQ h) A 0 z + SolenoidalDiagonal.potentialSum (fun (j : ℕ) => ↑(a j)) (PhysicalWaveSum.physicalQ h) (CutStageEstimates.positiveStages A) z

theorem NavierStokes.MixedDiagonalSchedule.physical_initial_split_jets {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {a : ℕ → ℕ} (ha : StrictMono a) {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : ℕ → ProblemStatement.SpaceTime → V) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (m : ℕ) : iteratedFDeriv ℝ m (SolenoidalDiagonal.potentialSum (fun (j : ℕ) => ↑(a j)) (PhysicalWaveSum.physicalQ h) A) w = iteratedFDeriv ℝ m (fun (z : ProblemStatement.SpaceTime) => SolenoidalDiagonal.cutStage (fun (j : ℕ) => ↑(a j)) (PhysicalWaveSum.physicalQ h) A 0 z + SolenoidalDiagonal.potentialSum (fun (j : ℕ) => ↑(a j)) (PhysicalWaveSum.physicalQ h) (CutStageEstimates.positiveStages A) z) w

theorem NavierStokes.MixedDiagonalSchedule.exists_three_component_schedule_smooth {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {S : Set ProblemStatement.SpaceTime} (hS : S ⊆ PhysicalWaveSum.preterminal) {A B : ℕ → ProblemStatement.VelocityField} {P : ℕ → ProblemStatement.PressureField} (hA : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (A j) PhysicalWaveSum.preterminal) (hB : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (B j) PhysicalWaveSum.preterminal) (hP : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (P j) PhysicalWaveSum.preterminal) (g LA LB LP : ℕ → ℝ) (CA CB CP pA pB pP : ℕ → ℕ → ℝ) (rawA : CutStageEstimates.RawStageBounds (PhysicalWaveSum.physicalQ h) A g LA CA pA S) (rawB : CutStageEstimates.RawStageBounds (PhysicalWaveSum.physicalQ h) B g LB CB pB S) (rawP : CutStageEstimates.RawStageBounds (PhysicalWaveSum.physicalQ h) P g LP CP pP S) (hg : ∀ (j : ℕ), 1 ≤ j → 0 < g j) (lower : ℕ) : ∃ (a : ℕ → ℕ), lower ≤ a 0 ∧ (∀ (j : ℕ), 0 < a j) ∧ (∀ (j : ℕ), 2 * a j ≤ a (j + 1)) ∧ StrictMono a ∧ Filter.Tendsto (fun (j : ℕ) => ↑(a j)) Filter.atTop Filter.atTop ∧ ThreeCutBounds a h A B P (fun (j : ℕ) => g j / 2) (commonLoss LA LB LP) S ∧ ThreeSmoothSums a h A B P

The same schedule also yields smooth full sums when stage zero is smooth. The quantitative input still concerns only positive stages.

theorem NavierStokes.MixedDiagonalSchedule.full_sum_smooth_of_initial {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {h qbig : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {a : ℕ → ℕ} (ha : StrictMono a) (ha0 : 0 < a 0) (hrecip : 1 / ↑(a 0) < qbig) {A : ℕ → ProblemStatement.SpaceTime → V} (hA0 : ContDiffOn ℝ (↑⊤) (A 0) (CutStageEstimates.physicalSublevel h qbig)) (hp : ContDiffOn ℝ (↑⊤) (SolenoidalDiagonal.potentialSum (fun (j : ℕ) => ↑(a j)) (PhysicalWaveSum.physicalQ h) (CutStageEstimates.positiveStages A)) PhysicalWaveSum.preterminal) : ContDiffOn ℝ (↑⊤) (SolenoidalDiagonal.potentialSum (fun (j : ℕ) => ↑(a j)) (PhysicalWaveSum.physicalQ h) A) PhysicalWaveSum.preterminal

Reattach the actual initial cutoff term to a smooth positive sum. The initial field only needs smoothness on its original valid q-domain.

theorem NavierStokes.MixedDiagonalSchedule.full_sum_zero_of_sublevel_le {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {h qbig : ℝ} {a : ℕ → ℕ} (ha : ∀ (j : ℕ), 0 < a j) (hrecip : ∀ (j : ℕ), 1 / ↑(a j) < qbig) (A : ℕ → ProblemStatement.SpaceTime → V) {w : ProblemStatement.SpaceTime} (hw : qbig ≤ PhysicalWaveSum.physicalQ h w) : SolenoidalDiagonal.potentialSum (fun (j : ℕ) => ↑(a j)) (PhysicalWaveSum.physicalQ h) A w = 0

Every full sum, including stage zero, is genuinely zero beyond the original validity range. No value of the uncut totalization is used there.

theorem NavierStokes.MixedDiagonalSchedule.exists_three_component_local_schedule {h qbig : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hqbig : 0 < qbig) {S : Set ProblemStatement.SpaceTime} (hS : S ⊆ PhysicalWaveSum.preterminal) {A B : ℕ → ProblemStatement.VelocityField} {P : ℕ → ProblemStatement.PressureField} (hA : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (A j) (CutStageEstimates.physicalSublevel h qbig)) (hB : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (B j) (CutStageEstimates.physicalSublevel h qbig)) (hP : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (P j) (CutStageEstimates.physicalSublevel h qbig)) (g LA LB LP : ℕ → ℝ) (CA CB CP pA pB pP : ℕ → ℕ → ℝ) (rawA : CutStageEstimates.RawStageBounds (PhysicalWaveSum.physicalQ h) A g LA CA pA (S ∩ CutStageEstimates.physicalSublevel h qbig)) (rawB : CutStageEstimates.RawStageBounds (PhysicalWaveSum.physicalQ h) B g LB CB pB (S ∩ CutStageEstimates.physicalSublevel h qbig)) (rawP : CutStageEstimates.RawStageBounds (PhysicalWaveSum.physicalQ h) P g LP CP pP (S ∩ CutStageEstimates.physicalSublevel h qbig)) (hg : ∀ (j : ℕ), 1 ≤ j → 0 < g j) (lower : ℕ) : ∃ (a : ℕ → ℕ), lower ≤ a 0 ∧ (∀ (j : ℕ), 0 < a j) ∧ (∀ (j : ℕ), 2 * a j ≤ a (j + 1)) ∧ StrictMono a ∧ Filter.Tendsto (fun (j : ℕ) => ↑(a j)) Filter.atTop Filter.atTop ∧ (∀ (j : ℕ), 1 / ↑(a j) < qbig) ∧ ThreeCutBounds a h A B P (fun (j : ℕ) => g j / 2) (commonLoss LA LB LP) S ∧ ThreeSmoothSums a h A B P

Local-q version for all three literal families. The initial scale places every support inside the validity region; the full sums, with stage zero retained, are smooth on all preterminal spacetime.

noncomputable def NavierStokes.MixedDiagonalResidual.velocity (a : ℕ → ℝ) (q : ProblemStatement.SpaceTime → ℝ) (A B : ℕ → ProblemStatement.VelocityField) : ProblemStatement.VelocityField

Velocity, defined pointwise by SolenoidalDiagonal.velocitySum a q A z + SolenoidalDiagonal.potentialSum a q B z.

Equations

• NavierStokes.MixedDiagonalResidual.velocity a q A B z = NavierStokes.SolenoidalDiagonal.velocitySum a q A z + NavierStokes.SolenoidalDiagonal.potentialSum a q B z

noncomputable def NavierStokes.MixedDiagonalResidual.uncutVelocity (A B : ℕ → ProblemStatement.VelocityField) (J : ℕ) : ProblemStatement.VelocityField

Stage zero remains in every nonempty uncut prefix.

Equations

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

noncomputable def NavierStokes.MixedDiagonalResidual.pressure (a : ℕ → ℝ) (q : ProblemStatement.SpaceTime → ℝ) (P : ℕ → ProblemStatement.PressureField) : ProblemStatement.PressureField

Pressure, given by SolenoidalDiagonal.potentialSum a q P.

Equations

• NavierStokes.MixedDiagonalResidual.pressure a q P = NavierStokes.SolenoidalDiagonal.potentialSum a q P

noncomputable def NavierStokes.MixedDiagonalResidual.residual (a : ℕ → ℝ) (q : ProblemStatement.SpaceTime → ℝ) (A B : ℕ → ProblemStatement.VelocityField) (P : ℕ → ProblemStatement.PressureField) : ProblemStatement.VelocityField

Residual, defined pointwise by navierStokesResidual (velocity a q A B) (pressure a q P) z.1 z.2.

Equations

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

theorem NavierStokes.MixedDiagonalResidual.residual_eq_originalResidual (a : ℕ → ℝ) (q : ProblemStatement.SpaceTime → ℝ) (A B : ℕ → ProblemStatement.VelocityField) (P : ℕ → ProblemStatement.PressureField) : residual a q A B P = MixedPeriodicAssembly.originalResidual (SolenoidalDiagonal.potentialSum a q A) (SolenoidalDiagonal.potentialSum a q B) (SolenoidalDiagonal.potentialSum a q P)

The residual is exactly the nonlinear residual used by the mixed localization and force construction, including both cross interactions.

theorem NavierStokes.MixedDiagonalResidual.velocity_smooth {a : ℕ → ℝ} (ha : Filter.Tendsto a Filter.atTop Filter.atTop) {q : ProblemStatement.SpaceTime → ℝ} {A B : ℕ → ProblemStatement.VelocityField} {U : Set ProblemStatement.SpaceTime} (hU : IsOpen U) (hqpos : ∀ z ∈ U, 0 < q z) (hq : ContDiffOn ℝ (↑⊤) q U) (hA : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (A j) U) (hB : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (B j) U) : ContDiffOn ℝ (↑⊤) (velocity a q A B) U

theorem NavierStokes.MixedDiagonalResidual.velocity_smooth_of_sums {a : ℕ → ℕ} {h : ℝ} {A B : ℕ → ProblemStatement.VelocityField} {P : ℕ → ProblemStatement.PressureField} (hs : MixedDiagonalSchedule.ThreeSmoothSums a h A B P) : ContDiffOn ℝ (↑⊤) (velocity (fun (j : ℕ) => ↑(a j)) (PhysicalWaveSum.physicalQ h) A B) PhysicalWaveSum.preterminal

Smoothness of the full cut sums suffices. The raw stages need not be smooth outside the positive-scale domain where they are constructed.

theorem NavierStokes.MixedDiagonalResidual.uncutVelocity_smooth {A B : ℕ → ProblemStatement.VelocityField} {U : Set ProblemStatement.SpaceTime} (hU : IsOpen U) (hA : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (A j) U) (hB : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (B j) U) (J : ℕ) : ContDiffOn ℝ (↑⊤) (uncutVelocity A B J) U

noncomputable def NavierStokes.MixedDiagonalResidual.velocityLoss (LA LB : ℕ → ℝ) (m : ℕ) : ℝ

One derivative is paid for the potential component only. The loss depends on the derivative order, never on the stage number.

Equations

• NavierStokes.MixedDiagonalResidual.velocityLoss LA LB m = max (LA (m + 1)) (LB m)

theorem NavierStokes.MixedDiagonalResidual.velocity_tail_jetRate {a : ℕ → ℝ} (ha : Filter.Tendsto a Filter.atTop Filter.atTop) {q : ProblemStatement.SpaceTime → ℝ} {A B : ℕ → ProblemStatement.VelocityField} {g LA LB : ℕ → ℝ} {U : Set ProblemStatement.SpaceTime} {l : Filter ProblemStatement.SpaceTime} (hU : IsOpen U) (hqpos : ∀ z ∈ U, 0 < q z) (hq : ContDiffOn ℝ (↑⊤) q U) (hA : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (A j) U) (hB : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (B j) U) (hg : Monotone g) (hbA : DiagonalJetBounds.CutStageBounds a q A g LA U) (hbB : DiagonalJetBounds.CutStageBounds a q B g LB U) (hlU : ∀ᶠ (z : ProblemStatement.SpaceTime) in l, z ∈ U) (hlq : ∀ᶠ (z : ProblemStatement.SpaceTime) in l, 0 < q z ∧ q z ≤ 1) (hqzero : Filter.Tendsto q l (nhds 0)) (J m : ℕ) (hm : m + 1 ≤ J + 3) : DiagonalResidual.JetRate l q (fun (z : ProblemStatement.SpaceTime) => velocity a q A B z - uncutVelocity A B J z) m (g (J + 1) - velocityLoss LA LB m)

theorem NavierStokes.MixedDiagonalResidual.residual_jetRate {a : ℕ → ℝ} (ha : Filter.Tendsto a Filter.atTop Filter.atTop) {q : ProblemStatement.SpaceTime → ℝ} {A B : ℕ → ProblemStatement.VelocityField} {P : ℕ → ProblemStatement.PressureField} {g LA LB LP Lbg Lres : ℕ → ℝ} {U : Set ProblemStatement.SpaceTime} {l : Filter ProblemStatement.SpaceTime} (hU : IsOpen U) (hqpos : ∀ z ∈ U, 0 < q z) (hq : ContDiffOn ℝ (↑⊤) q U) (hA : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (A j) U) (hB : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (B j) U) (hP : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (P j) U) (hgmono : Monotone g) (hgtop : Filter.Tendsto g Filter.atTop Filter.atTop) (hbA : DiagonalJetBounds.CutStageBounds a q A g LA U) (hbB : DiagonalJetBounds.CutStageBounds a q B g LB U) (hbP : DiagonalJetBounds.CutStageBounds a q P g LP U) (hlU : ∀ᶠ (z : ProblemStatement.SpaceTime) in l, z ∈ U) (hqzero : Filter.Tendsto q l (nhds 0)) (hbg : ∀ (J m : ℕ), DiagonalResidual.JetRate l q (uncutVelocity A B J) m (-Lbg m)) (hres : ∀ (J m : ℕ), DiagonalResidual.JetRate l q (fun (z : ProblemStatement.SpaceTime) => ProblemStatement.navierStokesResidual (uncutVelocity A B J) (DiagonalJetBounds.uncutPrefix P (J + 1)) z.1 z.2) m (g J - Lres m)) (m : ℕ) (r : ℝ) (hr : 0 ≤ r) : DiagonalResidual.JetRate l q (residual a q A B P) m r

Every positive power follows by selecting an adequately advanced finite uncut stage. No one fixed tail is assumed to have all powers.

theorem NavierStokes.MixedDiagonalResidual.physical_vanishingJointJets {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {a : ℕ → ℝ} (ha : Filter.Tendsto a Filter.atTop Filter.atTop) {A B : ℕ → ProblemStatement.VelocityField} {P : ℕ → ProblemStatement.PressureField} {g LA LB LP Lbg Lres : ℕ → ℝ} {U : Set ProblemStatement.SpaceTime} (hU : IsOpen U) (hUp : U ⊆ PhysicalWaveSum.preterminal) (hlU : ∀ᶠ (z : ProblemStatement.SpaceTime) in nhdsWithin (1, 0) (SpacetimeEndpoint.openPast 1), z ∈ U) (hA : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (A j) U) (hB : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (B j) U) (hP : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (P j) U) (hgmono : Monotone g) (hgtop : Filter.Tendsto g Filter.atTop Filter.atTop) (hbA : DiagonalJetBounds.CutStageBounds a (PhysicalWaveSum.physicalQ h) A g LA U) (hbB : DiagonalJetBounds.CutStageBounds a (PhysicalWaveSum.physicalQ h) B g LB U) (hbP : DiagonalJetBounds.CutStageBounds a (PhysicalWaveSum.physicalQ h) P g LP U) (hbg : ∀ (J m : ℕ), DiagonalResidual.JetRate (nhdsWithin (1, 0) (SpacetimeEndpoint.openPast 1)) (PhysicalWaveSum.physicalQ h) (uncutVelocity A B J) m (-Lbg m)) (hres : ∀ (J m : ℕ), DiagonalResidual.JetRate (nhdsWithin (1, 0) (SpacetimeEndpoint.openPast 1)) (PhysicalWaveSum.physicalQ h) (fun (z : ℝ × ProblemStatement.Space) => ProblemStatement.navierStokesResidual (uncutVelocity A B J) (DiagonalJetBounds.uncutPrefix P (J + 1)) z.1 z.2) m (g J - Lres m)) : JointResidualLimits.VanishingJointJets (residual a (PhysicalWaveSum.physicalQ h) A B P)

The actual physical scale has its joint zero limit at the origin. Thus the finite-stage construction inputs give the tensor limits needed by MixedPeriodicAssembly, rather than postulating those limits.

theorem NavierStokes.MixedDiagonalResidual.exists_physical_schedule_residual_zero {h qbig : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hqbig : 0 < qbig) {S : Set ProblemStatement.SpaceTime} (hSopen : IsOpen S) (hS : S ⊆ PhysicalWaveSum.preterminal) (hlS : ∀ᶠ (z : ProblemStatement.SpaceTime) in nhdsWithin (1, 0) (SpacetimeEndpoint.openPast 1), z ∈ S) {A B : ℕ → ProblemStatement.VelocityField} {P : ℕ → ProblemStatement.PressureField} (hA : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (A j) (CutStageEstimates.physicalSublevel h qbig)) (hB : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (B j) (CutStageEstimates.physicalSublevel h qbig)) (hP : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (P j) (CutStageEstimates.physicalSublevel h qbig)) (g LA LB LP Lbg Lres : ℕ → ℝ) (CA CB CP pA pB pP : ℕ → ℕ → ℝ) (rawA : CutStageEstimates.RawStageBounds (PhysicalWaveSum.physicalQ h) A g LA CA pA (S ∩ CutStageEstimates.physicalSublevel h qbig)) (rawB : CutStageEstimates.RawStageBounds (PhysicalWaveSum.physicalQ h) B g LB CB pB (S ∩ CutStageEstimates.physicalSublevel h qbig)) (rawP : CutStageEstimates.RawStageBounds (PhysicalWaveSum.physicalQ h) P g LP CP pP (S ∩ CutStageEstimates.physicalSublevel h qbig)) (hg0 : 0 ≤ g 0) (hg : ∀ (j : ℕ), 1 ≤ j → 0 < g j) (hgmono : Monotone g) (hgtop : Filter.Tendsto g Filter.atTop Filter.atTop) (hbg : ∀ (J m : ℕ), DiagonalResidual.JetRate (nhdsWithin (1, 0) (SpacetimeEndpoint.openPast 1)) (PhysicalWaveSum.physicalQ h) (uncutVelocity A B J) m (-Lbg m)) (hres : ∀ (J m : ℕ), DiagonalResidual.JetRate (nhdsWithin (1, 0) (SpacetimeEndpoint.openPast 1)) (PhysicalWaveSum.physicalQ h) (fun (z : ℝ × ProblemStatement.Space) => ProblemStatement.navierStokesResidual (uncutVelocity A B J) (DiagonalJetBounds.uncutPrefix P (J + 1)) z.1 z.2) m (g J - Lres m)) (lower : ℕ) : ∃ (a : ℕ → ℕ), lower ≤ a 0 ∧ (∀ (j : ℕ), 0 < a j) ∧ (∀ (j : ℕ), 2 * a j ≤ a (j + 1)) ∧ StrictMono a ∧ Filter.Tendsto (fun (j : ℕ) => ↑(a j)) Filter.atTop Filter.atTop ∧ (∀ (j : ℕ), 1 / ↑(a j) < qbig) ∧ MixedDiagonalSchedule.ThreeCutBounds a h A B P (fun (j : ℕ) => g j / 2) (MixedDiagonalSchedule.commonLoss LA LB LP) S ∧ MixedDiagonalSchedule.ThreeSmoothSums a h A B P ∧ JointResidualLimits.VanishingJointJets (residual (fun (j : ℕ) => ↑(a j)) (PhysicalWaveSum.physicalQ h) A B P)

A single schedule is selected from the three genuine raw estimates. The resulting mixed residual has joint zero jets. All raw fields are used only on their stated positive-scale domain, and stage zero is retained.