Mixed candidate assembly from primitive axis zero germs

Potential increments may be arbitrary physical fields. Their local axis zero germs replace the copy-potential representation used by the original consumer. All raw estimates, finite residual estimates, shrinking support and finite endpoint-extension obligations remain unchanged. The diagonal schedule, axis blow-up, infinite residual limits and candidate consequences are derived.

Consequences of the actual candidate fields

No candidate existence is asserted here. The first results use precisely CandidateProperties. Force derivatives at initial time are taken within the physical future half-space. For the actual globally smooth constructed force these are proved equal to its ordinary full derivatives.

A concrete periodic H³ supremum bound

Coordinate fundamental-theorem-of-calculus estimates are iterated over the unit cube. All derivatives below are the ordinary Frechet coordinate derivatives on ProblemStatement.Space.

noncomputable def NavierStokes.PeriodicSobolev.replaceCoord (i : Fin 3) (x : ProblemStatement.Space) (s : ℝ) : ProblemStatement.Space

Replace coord, given by x + (s - x i) • coordinateVector i.

Equations

• NavierStokes.PeriodicSobolev.replaceCoord i x s = x + (s - x.ofLp i) • NavierStokes.ProblemStatement.coordinateVector i

@[simp]

theorem NavierStokes.PeriodicSobolev.replaceCoord_apply (i j : Fin 3) (x : ProblemStatement.Space) (s : ℝ) : (replaceCoord i x s).ofLp j = if j = i then s else x.ofLp j

@[simp]

theorem NavierStokes.PeriodicSobolev.replaceCoord_self (i : Fin 3) (x : ProblemStatement.Space) : replaceCoord i x (x.ofLp i) = x

theorem NavierStokes.PeriodicSobolev.continuous_replaceCoord (i : Fin 3) : Continuous fun (z : ProblemStatement.Space × ℝ) => replaceCoord i z.1 z.2

theorem NavierStokes.PeriodicSobolev.hasDerivAt_replaceCoord (i : Fin 3) (x : ProblemStatement.Space) (s : ℝ) : HasDerivAt (replaceCoord i x) (ProblemStatement.coordinateVector i) s

noncomputable def NavierStokes.PeriodicSobolev.average (i : Fin 3) (h : ProblemStatement.Space → ℝ) (x : ProblemStatement.Space) : ℝ

Unit interval averaging after replacing one coordinate.

Equations

• NavierStokes.PeriodicSobolev.average i h x = ∫ (s : ℝ) in Set.Icc 0 1, h (NavierStokes.PeriodicSobolev.replaceCoord i x s)

theorem NavierStokes.PeriodicSobolev.average_eq_interval (i : Fin 3) (h : ProblemStatement.Space → ℝ) (x : ProblemStatement.Space) : average i h x = ∫ (s : ℝ) in 0..1, h (replaceCoord i x s)

theorem NavierStokes.PeriodicSobolev.continuous_average {h : ProblemStatement.Space → ℝ} (hh : Continuous h) (i : Fin 3) : Continuous (average i h)

theorem NavierStokes.PeriodicSobolev.average_nonneg {h : ProblemStatement.Space → ℝ} (hh : ∀ (x : ProblemStatement.Space), 0 ≤ h x) (i : Fin 3) (x : ProblemStatement.Space) : 0 ≤ average i h x

theorem NavierStokes.PeriodicSobolev.average_mono_on_curve {h k : ProblemStatement.Space → ℝ} (hh : Continuous h) (hk : Continuous k) (i : Fin 3) (x : ProblemStatement.Space) (hle : ∀ s ∈ Set.Icc 0 1, h (replaceCoord i x s) ≤ k (replaceCoord i x s)) : average i h x ≤ average i k x

theorem NavierStokes.PeriodicSobolev.average_add {h k : ProblemStatement.Space → ℝ} (hh : Continuous h) (hk : Continuous k) (i : Fin 3) (x : ProblemStatement.Space) : average i (fun (y : ProblemStatement.Space) => h y + k y) x = average i h x + average i k x

theorem NavierStokes.PeriodicSobolev.average_const_mul (a : ℝ) (h : ProblemStatement.Space → ℝ) (i : Fin 3) (x : ProblemStatement.Space) : average i (fun (y : ProblemStatement.Space) => a * h y) x = a * average i h x

noncomputable def NavierStokes.PeriodicSobolev.sqField (f : ProblemStatement.Space → ProblemStatement.Space) (x : ProblemStatement.Space) : ℝ

Sq field, given by ‖f x‖ ^ 2.

Equations

• NavierStokes.PeriodicSobolev.sqField f x = ‖f x‖ ^ 2

theorem NavierStokes.PeriodicSobolev.continuous_sqField {f : ProblemStatement.Space → ProblemStatement.Space} (hf : Continuous f) : Continuous (sqField f)

theorem NavierStokes.PeriodicSobolev.line_energy_bound {f : ProblemStatement.Space → ProblemStatement.Space} (hf : ContDiff ℝ (↑⊤) f) (i : Fin 3) (x : ProblemStatement.Space) (hx : x.ofLp i ∈ Set.Icc 0 1) : sqField f x ≤ 2 * (average i (sqField f) x + average i (sqField (PeriodicIntegration.spatialPartial i f)) x)

theorem NavierStokes.PeriodicSobolev.averaged_line_energy_bound {f : ProblemStatement.Space → ProblemStatement.Space} (hf : ContDiff ℝ (↑⊤) f) (i j : Fin 3) (hji : j ≠ i) (x : ProblemStatement.Space) (hx : x.ofLp j ∈ Set.Icc 0 1) : average i (sqField f) x ≤ 2 * (average i (average j (sqField f)) x + average i (average j (sqField (PeriodicIntegration.spatialPartial j f))) x)

theorem NavierStokes.PeriodicSobolev.twice_averaged_line_energy_bound {f : ProblemStatement.Space → ProblemStatement.Space} (hf : ContDiff ℝ (↑⊤) f) (i j k : Fin 3) (hki : k ≠ i) (hkj : k ≠ j) (x : ProblemStatement.Space) (hx : x.ofLp k ∈ Set.Icc 0 1) : average i (average j (sqField f)) x ≤ 2 * (average i (average j (average k (sqField f))) x + average i (average j (average k (sqField (PeriodicIntegration.spatialPartial k f)))) x)

noncomputable def NavierStokes.PeriodicSobolev.cubePoint (a b c : ℝ) : ProblemStatement.Space

Cube point, given by toSpace ![a, b, c].

Equations

• NavierStokes.PeriodicSobolev.cubePoint a b c = NavierStokes.PeriodicIntegration.toSpace ![a, b, c]

noncomputable def NavierStokes.PeriodicSobolev.boxIntegral (h : ProblemStatement.Space → ℝ) : ℝ

An explicit iterated product Lebesgue integral on the unit cube.

Equations

• NavierStokes.PeriodicSobolev.boxIntegral h = ∫ (a : ℝ) (b : ℝ) (c : ℝ) in Set.Icc 0 1, h (NavierStokes.PeriodicSobolev.cubePoint a b c)

theorem NavierStokes.PeriodicSobolev.averages_eq_boxIntegral (h : ProblemStatement.Space → ℝ) (x : ProblemStatement.Space) : average 0 (average 1 (average 2 h)) x = boxIntegral h

theorem NavierStokes.PeriodicSobolev.boxIntegral_nonneg {h : ProblemStatement.Space → ℝ} (hh : ∀ (x : ProblemStatement.Space), 0 ≤ h x) : 0 ≤ boxIntegral h

noncomputable def NavierStokes.PeriodicSobolev.mixedEnergy (f : ProblemStatement.Space → ProblemStatement.Space) : ℝ

The eight mixed derivatives with each coordinate used at most once. Every derivative here has total order at most three.

Equations

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

theorem NavierStokes.PeriodicSobolev.mixedEnergy_nonneg (f : ProblemStatement.Space → ProblemStatement.Space) : 0 ≤ mixedEnergy f

theorem NavierStokes.PeriodicSobolev.norm_sq_le_eight_mixedEnergy_on_cube {f : ProblemStatement.Space → ProblemStatement.Space} (hf : ContDiff ℝ (↑⊤) f) (x : ProblemStatement.Space) (hx : ∀ (i : Fin 3), x.ofLp i ∈ Set.Icc 0 1) : ‖f x‖ ^ 2 ≤ 8 * mixedEnergy f

Three successive coordinate FTC estimates. No periodicity is needed for the estimate at a point already in the closed unit cube.

theorem NavierStokes.PeriodicSobolev.norm_sq_le_eight_mixedEnergy {f : ProblemStatement.Space → ProblemStatement.Space} (hf : ContDiff ℝ (↑⊤) f) (hp : PeriodicIntegration.UnitPeriods f) (x : ProblemStatement.Space) : ‖f x‖ ^ 2 ≤ 8 * mixedEnergy f

The pointwise estimate on all of space follows by an explicitly proved integer-lattice reduction to the cube.

noncomputable def NavierStokes.PeriodicSobolev.derivativeH3Energy (f : ProblemStatement.Space → ProblemStatement.Space) : ℝ

A derivative definition of the H³ energy. Every ordered coordinate derivative of order two and three is included, as are the zeroth and all first derivatives. The selected mixed derivatives have an extra copy; these fixed positive multiplicities only change the choice of H³ norm.

Equations

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

noncomputable def NavierStokes.PeriodicSobolev.derivativeH3Norm (f : ProblemStatement.Space → ProblemStatement.Space) : ℝ

Derivative H3 norm, given by Real.sqrt (derivativeH3Energy f).

Equations

• NavierStokes.PeriodicSobolev.derivativeH3Norm f = √(NavierStokes.PeriodicSobolev.derivativeH3Energy f)

theorem NavierStokes.PeriodicSobolev.mixedEnergy_le_derivativeH3Energy (f : ProblemStatement.Space → ProblemStatement.Space) : mixedEnergy f ≤ derivativeH3Energy f

theorem NavierStokes.PeriodicSobolev.derivativeH3Energy_nonneg (f : ProblemStatement.Space → ProblemStatement.Space) : 0 ≤ derivativeH3Energy f

theorem NavierStokes.PeriodicSobolev.derivativeH3Norm_nonneg (f : ProblemStatement.Space → ProblemStatement.Space) : 0 ≤ derivativeH3Norm f

theorem NavierStokes.PeriodicSobolev.norm_le_three_derivativeH3Norm {f : ProblemStatement.Space → ProblemStatement.Space} (hf : ContDiff ℝ (↑⊤) f) (hp : PeriodicIntegration.UnitPeriods f) (x : ProblemStatement.Space) : ‖f x‖ ≤ 3 * derivativeH3Norm f

A concrete H³-to-supremum estimate with the harmless numerical constant 3.

def NavierStokes.PeriodicSobolev.DerivativeH3UnboundedAtOne (u : ProblemStatement.VelocityField) : Prop

Derivative H3 unbounded at one, given by ∀ M : ℝ, 0 < M → ∀ δ : ℝ, 0 < δ → ∃ t : ℝ, t ∈ Ioo (1 - δ) 1 ∧ M < derivativeH3Norm (fun x => u (t, x)).

Equations

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

theorem NavierStokes.PeriodicSobolev.speed_unbounded_implies_derivativeH3_unbounded {u : ProblemStatement.VelocityField} (hu : ∀ t ∈ Set.Ico 0 1, ContDiff ℝ ↑⊤ fun (x : ProblemStatement.Space) => u (t, x)) (hp : ProblemStatement.UnitSpatialPeriodsOn (Set.Ico 0 1) u) (hb : ProblemStatement.SpeedUnboundedAtOne u) : DerivativeH3UnboundedAtOne u

Pointwise speed blow-up forces unbounded H³ norm arbitrarily close to time one, by the proved embedding rather than an assumed Sobolev theorem.

theorem NavierStokes.PeriodicSobolev.candidate_derivativeH3_unbounded {u : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} {f : ProblemStatement.VelocityField} (h : ProblemStatement.CandidateProperties u p f) : DerivativeH3UnboundedAtOne u

The candidate specification therefore entails the explicitly defined H³ norm blow-up condition, without asserting existence of a candidate.

Conditional maximal classical lifespan of the candidate

An actual CandidateProperties witness has maximal classical lifespan one. The proof uses the proved periodic uniqueness theorem and a compactness bound for a continuous periodic field across time one. It assumes no general Navier--Stokes existence theorem and never identifies pressure gauges.

noncomputable def NavierStokes.MaximalLifespan.lifespanDomain (T : ℝ) : Set ProblemStatement.SpaceTime

Lifespan domain, given by Ico 0 T ×ˢ univ.

Equations

• NavierStokes.MaximalLifespan.lifespanDomain T = Set.Ico 0 T ×ˢ Set.univ

structure NavierStokes.MaximalLifespan.ClassicalSolution (f : ProblemStatement.VelocityField) (initial : ProblemStatement.Space → ProblemStatement.Space) (T : ℝ) (u : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) : Prop

A finite, positive classical lifespan for the exact viscosity-one PDE. The initial datum is an actual spatial velocity field. Pressures are retained as witnesses but are never required to agree with a different gauge.

• lifespan_pos : 0 < T
• velocity_smooth : ContDiffOn ℝ (↑⊤) u (lifespanDomain T)
• pressure_smooth : ContDiffOn ℝ (↑⊤) p (lifespanDomain T)
• velocity_periodic : ProblemStatement.UnitSpatialPeriodsOn (Set.Ico 0 T) u
• pressure_periodic : ProblemStatement.UnitSpatialPeriodsOn (Set.Ico 0 T) p
• initial_velocity (x : ProblemStatement.Space) : u (0, x) = initial x
• divergence_free (t : ℝ) : t ∈ Set.Ico 0 T → ∀ (x : ProblemStatement.Space), ProblemStatement.spatialDivergence u t x = 0
• navier_stokes (t : ℝ) : t ∈ Set.Ioo 0 T → ∀ (x : ProblemStatement.Space), ProblemStatement.navierStokesResidual u p t x = f (t, x)

theorem NavierStokes.MaximalLifespan.ClassicalSolution.toSolutionOn {f : ProblemStatement.VelocityField} {initial : ProblemStatement.Space → ProblemStatement.Space} {T : ℝ} {u : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} (solution : ClassicalSolution f initial T u p) : SolutionOn 1 0 initial (Set.Ico 0 T) f u p

The local equation and arbitrary initial datum, independently of periodicity.

noncomputable def NavierStokes.MaximalLifespan.VelocityAgreesOn (T : ℝ) (u v : ProblemStatement.VelocityField) : Prop

Velocity agrees on, given by ∀ t ∈ Ico (0 : ℝ) T, ∀ x : Space, u (t, x) = v (t, x).

Equations

• NavierStokes.MaximalLifespan.VelocityAgreesOn T u v = ∀ t ∈ Set.Ico 0 T, ∀ (x : NavierStokes.ProblemStatement.Space), u (t, x) = v (t, x)

noncomputable def NavierStokes.MaximalLifespan.HasClassicalExtension (f : ProblemStatement.VelocityField) (initial : ProblemStatement.Space → ProblemStatement.Space) (T : ℝ) (u : ProblemStatement.VelocityField) : Prop

An extension has a strictly larger time interval and preserves the velocity on the entire original interval. Its pressure may have a different time-dependent spatially constant normalization.

Equations

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

noncomputable def NavierStokes.MaximalLifespan.IsMaximalClassicalSolution (f : ProblemStatement.VelocityField) (initial : ProblemStatement.Space → ProblemStatement.Space) (T : ℝ) (u : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) : Prop

Is maximal classical solution, given by ClassicalSolution f initial T u p ∧ ¬HasClassicalExtension f initial T u.

Equations

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

noncomputable def NavierStokes.MaximalLifespan.admissibleLifespans (f : ProblemStatement.VelocityField) (initial : ProblemStatement.Space → ProblemStatement.Space) : Set ℝ

The actual set of finite positive times supported by classical solutions for the fixed force and initial datum. No existence is built into the definition.

Equations

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

theorem NavierStokes.MaximalLifespan.ClassicalSolution.restrict {f : ProblemStatement.VelocityField} {initial : ProblemStatement.Space → ProblemStatement.Space} {S T : ℝ} {u : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} (h : ClassicalSolution f initial T u p) (hS : 0 < S) (hST : S ≤ T) : ClassicalSolution f initial S u p

theorem NavierStokes.MaximalLifespan.ClassicalSolution.agree_on_overlap {f : ProblemStatement.VelocityField} {initial : ProblemStatement.Space → ProblemStatement.Space} {T S : ℝ} {u v : ProblemStatement.VelocityField} {p q : ProblemStatement.PressureField} (hu : ClassicalSolution f initial T u p) (hv : ClassicalSolution f initial S v q) : VelocityAgreesOn (min T S) u v

Any two actual classical solutions agree on their common interval. This is derived by restriction to each compact subinterval and the proved energy uniqueness theorem. Only velocity equality is asserted.

theorem NavierStokes.MaximalLifespan.candidate_is_classical_solution {u : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} {f : ProblemStatement.VelocityField} (h : ProblemStatement.CandidateProperties u p f) : ClassicalSolution f (fun (x : ProblemStatement.Space) => 0) 1 u p

theorem NavierStokes.MaximalLifespan.candidate_agree_on_overlap {u v : ProblemStatement.VelocityField} {p q : ProblemStatement.PressureField} {f : ProblemStatement.VelocityField} {T : ℝ} (h : ProblemStatement.CandidateProperties u p f) (hv : ClassicalSolution f (fun (x : ProblemStatement.Space) => 0) T v q) : VelocityAgreesOn (min T 1) v u

theorem NavierStokes.MaximalLifespan.periodic_bound_on_slab {V : Type u_1} [NormedAddCommGroup V] {g : ProblemStatement.SpaceTime → V} {a b : ℝ} (hg : ContinuousOn g (Set.Icc a b ×ˢ Set.univ)) (hperiod : ProblemStatement.UnitSpatialPeriodsOn (Set.Icc a b) g) : ∃ (B : ℝ), 0 < B ∧ ∀ t ∈ Set.Icc a b, ∀ (x : ProblemStatement.Space), ‖g (t, x)‖ ≤ B

Compactness bounds a relatively continuous periodic field on an entire closed time slab, uniformly over all spatial points.

theorem NavierStokes.MaximalLifespan.unbounded_excludes_continuous_extension {u v : ProblemStatement.VelocityField} (h : ProblemStatement.SpeedUnboundedAtOne u) (hv : ContinuousOn v (Set.Icc 0 1 ×ˢ Set.univ)) (hpv : ProblemStatement.UnitSpatialPeriodsOn (Set.Icc 0 1) v) (hagrees : VelocityAgreesOn 1 u v) : False

Unbounded speed rules out even a continuous periodic extension through time one, once agreement with the original field is known.

theorem NavierStokes.MaximalLifespan.candidate_no_solution_after_one {u v : ProblemStatement.VelocityField} {p q : ProblemStatement.PressureField} {f : ProblemStatement.VelocityField} {T : ℝ} (h : ProblemStatement.CandidateProperties u p f) (hT : 1 < T) (hv : ClassicalSolution f (fun (x : ProblemStatement.Space) => 0) T v q) : False

No classical solution for the same force and datum can have lifespan larger than one. Uniqueness supplies the required pre-one agreement.

theorem NavierStokes.MaximalLifespan.candidate_all_lifespans_le_one {u v : ProblemStatement.VelocityField} {p q : ProblemStatement.PressureField} {f : ProblemStatement.VelocityField} {T : ℝ} (h : ProblemStatement.CandidateProperties u p f) (hv : ClassicalSolution f (fun (x : ProblemStatement.Space) => 0) T v q) : T ≤ 1

theorem NavierStokes.MaximalLifespan.candidate_is_maximal {u : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} {f : ProblemStatement.VelocityField} (h : ProblemStatement.CandidateProperties u p f) : IsMaximalClassicalSolution f (fun (x : ProblemStatement.Space) => 0) 1 u p

The given lifespan-one solution is maximal under extension of its velocity. No literal equality between pressure representatives is required.

theorem NavierStokes.MaximalLifespan.candidate_extends_shorter_solution {u v : ProblemStatement.VelocityField} {p q : ProblemStatement.PressureField} {f : ProblemStatement.VelocityField} {T : ℝ} (h : ProblemStatement.CandidateProperties u p f) (hv : ClassicalSolution f (fun (x : ProblemStatement.Space) => 0) T v q) (hT : T < 1) : HasClassicalExtension f (fun (x : ProblemStatement.Space) => 0) T v

Any shorter classical solution extends by the actual candidate field.

theorem NavierStokes.MaximalLifespan.maximal_lifespan_eq_one {u v : ProblemStatement.VelocityField} {p q : ProblemStatement.PressureField} {f : ProblemStatement.VelocityField} {T : ℝ} (h : ProblemStatement.CandidateProperties u p f) (hv : IsMaximalClassicalSolution f (fun (x : ProblemStatement.Space) => 0) T v q) : T = 1

Every maximal classical solution for these data has exactly lifespan one.

theorem NavierStokes.MaximalLifespan.candidate_greatest_lifespan {u : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} {f : ProblemStatement.VelocityField} (h : ProblemStatement.CandidateProperties u p f) : IsGreatest (admissibleLifespans f fun (x : ProblemStatement.Space) => 0) 1

There is a greatest admissible finite classical lifespan, and it is one. Existence at that time comes solely from the supplied candidate witness.

theorem NavierStokes.MaximalLifespan.candidate_admissible_lifespans {u : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} {f : ProblemStatement.VelocityField} (h : ProblemStatement.CandidateProperties u p f) : (admissibleLifespans f fun (x : ProblemStatement.Space) => 0) = Set.Ioc 0 1

The entire set of finite admissible classical lifespans is (0,1].

theorem NavierStokes.MaximalLifespan.candidate_excludes_global_solution {u v : ProblemStatement.VelocityField} {p q : ProblemStatement.PressureField} {f : ProblemStatement.VelocityField} (h : ProblemStatement.CandidateProperties u p f) (hv : ContDiffOn ℝ (↑⊤) v ProblemStatement.futureDomain) (hq : ContDiffOn ℝ (↑⊤) q ProblemStatement.futureDomain) (hpv : ProblemStatement.UnitSpatialPeriodsOn (Set.Ici 0) v) (hpq : ProblemStatement.UnitSpatialPeriodsOn (Set.Ici 0) q) (hvzero : ∀ (x : ProblemStatement.Space), v (0, x) = 0) (hdv : ∀ (t : ℝ), 0 ≤ t → ∀ (x : ProblemStatement.Space), ProblemStatement.spatialDivergence v t x = 0) (hNSv : ∀ (t : ℝ), 0 < t → ∀ (x : ProblemStatement.Space), ProblemStatement.navierStokesResidual v q t x = f (t, x)) : False

A global classical solution would restrict to a forbidden lifespan greater than one. This makes the exclusion of infinite-time continuation explicit without assuming any existence theorem.

theorem NavierStokes.MaximalLifespan.zero_classical_solution_of_zero_force {f : ProblemStatement.VelocityField} {T : ℝ} (hT : 0 < T) (hf : ∀ t ∈ Set.Ioo 0 T, ∀ (x : ProblemStatement.Space), f (t, x) = 0) : ClassicalSolution f (fun (x : ProblemStatement.Space) => 0) T (fun (x : ProblemStatement.SpaceTime) => 0) fun (x : ProblemStatement.SpaceTime) => 0

theorem NavierStokes.MaximalLifespan.candidate_force_nonzero_before_one {u : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} {f : ProblemStatement.VelocityField} (h : ProblemStatement.CandidateProperties u p f) : ∃ t ∈ Set.Ioo 0 1, ∃ (x : ProblemStatement.Space), f (t, x) ≠ 0

The specified force must be nonzero somewhere before the breakdown time. Otherwise uniqueness identifies the candidate with the zero solution.

theorem NavierStokes.CandidateConsequences.future_uniqueDiff : UniqueDiffOn ℝ ProblemStatement.futureDomain

noncomputable def NavierStokes.CandidateConsequences.futureJet (f : ProblemStatement.VelocityField) (m : ℕ) : ProblemStatement.SpaceTime → ProblemStatement.SpaceTime [×m]→L[ℝ] ProblemStatement.Space

The physical full spacetime jet, including its one-sided value at time zero.

Equations

• NavierStokes.CandidateConsequences.futureJet f m = iteratedFDerivWithin ℝ m f NavierStokes.ProblemStatement.futureDomain

theorem NavierStokes.CandidateConsequences.futureJet_continuous {f : ProblemStatement.VelocityField} (hf : ContDiffOn ℝ (↑⊤) f ProblemStatement.futureDomain) (m : ℕ) : ContinuousOn (futureJet f m) ProblemStatement.futureDomain

theorem NavierStokes.CandidateConsequences.futureJet_periodic {f : ProblemStatement.VelocityField} (hp : ProblemStatement.UnitSpatialPeriodsOn (Set.Ici 0) f) (m : ℕ) : ProblemStatement.UnitSpatialPeriodsOn (Set.Ici 0) (futureJet f m)

theorem NavierStokes.CandidateConsequences.futureJet_eq_full {f : ProblemStatement.VelocityField} {t : ℝ} (ht : 0 ≤ t) (x : ProblemStatement.Space) (m : ℕ) (hf : ContDiffAt ℝ (↑⊤) f (t, x)) : futureJet f m (t, x) = iteratedFDeriv ℝ m f (t, x)

theorem NavierStokes.CandidateConsequences.futureJet_eq_full_of_pos {f : ProblemStatement.VelocityField} (hf : ContDiffOn ℝ (↑⊤) f ProblemStatement.futureDomain) {t : ℝ} (ht : 0 < t) (x : ProblemStatement.Space) (m : ℕ) : futureJet f m (t, x) = iteratedFDeriv ℝ m f (t, x)

theorem NavierStokes.CandidateConsequences.futureJet_decay {f : ProblemStatement.VelocityField} (hf : ContDiffOn ℝ (↑⊤) f ProblemStatement.futureDomain) (hp : ProblemStatement.UnitSpatialPeriodsOn (Set.Ici 0) f) (hs : ProblemStatement.CompactFutureTimeSupport f) (m : ℕ) (K : ℝ) (hK : 0 ≤ K) : ∃ (C : ℝ), 0 < C ∧ ∀ (t : ℝ), 0 ≤ t → ∀ (x : ProblemStatement.Space), ‖futureJet f m (t, x)‖ ≤ C * (1 + t) ^ (-K)

Compact future time support gives arbitrary polynomial decay of the physical one-sided jets, using only future smoothness and future periodicity.

theorem NavierStokes.CandidateConsequences.full_forceJet_decay {u : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} {f : ProblemStatement.VelocityField} (h : ProblemStatement.CandidateProperties u p f) (hf : ContDiff ℝ (↑⊤) f) (m : ℕ) (K : ℝ) (hK : 0 ≤ K) : ∃ (C : ℝ), 0 < C ∧ ∀ (t : ℝ), 0 ≤ t → ∀ (x : ProblemStatement.Space), ‖iteratedFDeriv ℝ m f (t, x)‖ ≤ C * (1 + t) ^ (-K)

The ordinary tensor bound for the same force. Global smoothness is provided by the actual force constructor; negative-time periodicity is not needed.

theorem NavierStokes.CandidateConsequences.full_forceMixed_decay {u : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} {f : ProblemStatement.VelocityField} (h : ProblemStatement.CandidateProperties u p f) (hf : ContDiff ℝ (↑⊤) f) (m : ℕ) (K : ℝ) (hK : 0 ≤ K) : ∃ (C : ℝ), 0 < C ∧ ∀ (t : ℝ), 0 ≤ t → ∀ (x : ProblemStatement.Space) (directions : Fin m → Fin 4) (j : Fin 3), |((iteratedFDeriv ℝ m f (t, x)) fun (i : Fin m) => CompactForceDecay.spacetimeCoordinate (directions i)).ofLp j| ≤ C * (1 + t) ^ (-K)

structure NavierStokes.CandidateConsequences.Consequences (u : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) (f : ProblemStatement.VelocityField) : Prop

All conclusions here follow from the exact candidate properties alone.

• maximal : MaximalLifespan.IsMaximalClassicalSolution f (fun (x : ProblemStatement.Space) => 0) 1 u p
• lifespans : (MaximalLifespan.admissibleLifespans f fun (x : ProblemStatement.Space) => 0) = Set.Ioc 0 1
• h3_unbounded : PeriodicSobolev.DerivativeH3UnboundedAtOne u
• force_nonzero : ∃ t ∈ Set.Ioo 0 1, ∃ (x : ProblemStatement.Space), f (t, x) ≠ 0
• force_jet_decay (m : ℕ) (K : ℝ) : 0 ≤ K → ∃ (C : ℝ), 0 < C ∧ ∀ (t : ℝ), 0 ≤ t → ∀ (x : ProblemStatement.Space), ‖futureJet f m (t, x)‖ ≤ C * (1 + t) ^ (-K)

theorem NavierStokes.CandidateConsequences.consequences_of_candidate {u : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} {f : ProblemStatement.VelocityField} (h : ProblemStatement.CandidateProperties u p f) : Consequences u p f

theorem NavierStokes.CandidateConsequences.h3_tendsto_of_speed_tendsto {u : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} {f : ProblemStatement.VelocityField} (h : ProblemStatement.CandidateProperties u p f) (x : ℝ → ProblemStatement.Space) (hx : Filter.Tendsto (fun (t : ℝ) => ‖u (t, x t)‖) (nhdsWithin 1 (Set.Iio 1)) Filter.atTop) : Filter.Tendsto (fun (t : ℝ) => PeriodicSobolev.derivativeH3Norm fun (y : ProblemStatement.Space) => u (t, y)) (nhdsWithin 1 (Set.Iio 1)) Filter.atTop

Retaining one growing physical trajectory strengthens unboundedness to a genuine limit. No monotonicity of the velocity or its norm is assumed.

theorem NavierStokes.CandidateConsequences.mixed_activated_speed_tendsto {A v : ProblemStatement.VelocityField} (haxis : Filter.Tendsto (fun (t : ℝ) => ‖MixedPeriodicAssembly.velocity A v (t, 0)‖) (nhdsWithin 1 (Set.Iio 1)) Filter.atTop) : Filter.Tendsto (fun (t : ℝ) => ‖TimeLocalization.activatedVelocity (MixedPeriodicAssembly.periodicVelocity A v) (t, 0)‖) (nhdsWithin 1 (Set.Iio 1)) Filter.atTop

theorem NavierStokes.CandidateConsequences.mixed_exists_force_with_consequences {A v : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} (hA : ContDiffOn ℝ (↑⊤) A (SpacetimeEndpoint.openPast 1)) (hv : ContDiffOn ℝ (↑⊤) v (SpacetimeEndpoint.openPast 1)) (hp : ContDiffOn ℝ (↑⊤) p (SpacetimeEndpoint.openPast 1)) (hd : ∀ t < 1, ∀ (x : ProblemStatement.Space), ProblemStatement.spatialDivergence (SpatialLocalization.cutPotential v) t x = 0) (hz : JointResidualLimits.VanishingJointJets (MixedPeriodicAssembly.originalResidual A v p)) (eA : JointResidualLimits.AwayExtensions A) (ev : JointResidualLimits.AwayExtensions v) (ep : JointResidualLimits.AwayExtensions p) (haxis : Filter.Tendsto (fun (t : ℝ) => ‖MixedPeriodicAssembly.velocity A v (t, 0)‖) (nhdsWithin 1 (Set.Iio 1)) Filter.atTop) : ∃ (F : ProblemStatement.VelocityField), ProblemStatement.CandidateProperties (TimeLocalization.activatedVelocity (MixedPeriodicAssembly.periodicVelocity A v)) (TimeLocalization.activatedPressure (SpatialLocalization.periodicPressure p)) F ∧ ContDiff ℝ (↑⊤) F ∧ Consequences (TimeLocalization.activatedVelocity (MixedPeriodicAssembly.periodicVelocity A v)) (TimeLocalization.activatedPressure (SpatialLocalization.periodicPressure p)) F ∧ Filter.Tendsto (fun (t : ℝ) => PeriodicSobolev.derivativeH3Norm fun (x : ProblemStatement.Space) => TimeLocalization.activatedVelocity (MixedPeriodicAssembly.periodicVelocity A v) (t, x)) (nhdsWithin 1 (Set.Iio 1)) Filter.atTop ∧ (∀ (m : ℕ) (K : ℝ), 0 ≤ K → ∃ (C : ℝ), 0 < C ∧ ∀ (t : ℝ), 0 ≤ t → ∀ (x : ProblemStatement.Space) (directions : Fin m → Fin 4) (j : Fin 3), |((iteratedFDeriv ℝ m F (t, x)) fun (i : Fin m) => CompactForceDecay.spacetimeCoordinate (directions i)).ofLp j| ≤ C * (1 + t) ^ (-K)) ∧ ∀ (n : ℕ) (x : ProblemStatement.Space), iteratedFDeriv ℝ n F (1, x) = MixedPeriodicAssembly.boundaryLimits A v p eA ev ep x n

The exact mixed assembly inputs produce one force carrying all the lifespan, Sobolev, and full force-jet conclusions. Nothing is assumed about the output force, the infinite-time PDE, or the Sobolev embedding.

Retaining the actual mixed candidate and its consequences

The finite-stage inputs are exactly those of MixedCandidateAssembly.candidate_of_finite_stages. The same selected schedule supplies the actual velocity and pressure sums, their endpoint extensions, and the force with all proved consequences.

noncomputable def NavierStokes.MixedCandidateWitness.SelectedSchedule (h qbig : ℝ) (A B : ℕ → ProblemStatement.VelocityField) (P : ℕ → ProblemStatement.PressureField) (a : ℕ → ℕ) : Prop

All properties of the single scale sequence selected from the finite stage estimates, including smooth sums and vanishing residual jets.

Equations

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

theorem NavierStokes.MixedCandidateWitness.exists_candidate_witness_of_finite_stages {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (bandFloor : ℕ) {qbig C : ℝ} (hqbig : 0 < qbig) (initial : MixedAxisPreservation.PotentialStage F.data.h (MixedAxisPreservation.localDomain F.data.h qbig)) (stages : ℕ → MixedAxisPreservation.PotentialStage F.data.h (MixedAxisPreservation.localDomain F.data.h qbig)) (D : ℕ → DirectAngularDiagonal.AngularData (LocalAngularDiagonal.localSlowDomain F.data.h qbig)) (pInitial : ProblemStatement.PressureField) (pStages : ℕ → ProblemStatement.PressureField) (E : MixedCandidateAssembly.StageEstimates F.data.h qbig (MixedCandidateAssembly.potentialStages H v upper bandFloor initial stages) (LocalAngularDiagonal.rawSeries D) (MixedCandidateAssembly.pressureStages H v upper bandFloor pInitial pStages)) (hInitial : MixedDiagonalExtensions.SublevelShrinkingSupport F.data.h C qbig initial.field) (hStages : ∀ (j : ℕ), MixedDiagonalExtensions.SublevelShrinkingSupport F.data.h C qbig (stages j).field) (hDirect : ∀ (j : ℕ), MixedDiagonalExtensions.SublevelShrinkingSupport F.data.h C qbig (LocalAngularDiagonal.rawSeries D j)) (hpInitial : MixedDiagonalExtensions.SublevelShrinkingSupport F.data.h C qbig pInitial) (hpStages : ∀ (j : ℕ), MixedDiagonalExtensions.SublevelShrinkingSupport F.data.h C qbig (pStages j)) (eA : ∀ (x : ProblemStatement.Space), x.ofLp 2 ≠ 0 → EndpointCoordinates.endpointRoot (2 * F.data.h) (x.ofLp 2) < qbig → ∀ (j : ℕ), Nonempty (JointResidualLimits.OneSidedExtension (MixedCandidateAssembly.potentialStages H v upper bandFloor initial stages j) x)) (eB : ∀ (x : ProblemStatement.Space), x.ofLp 2 ≠ 0 → EndpointCoordinates.endpointRoot (2 * F.data.h) (x.ofLp 2) < qbig → ∀ (j : ℕ), Nonempty (JointResidualLimits.OneSidedExtension (LocalAngularDiagonal.rawSeries D j) x)) (eP : ∀ (x : ProblemStatement.Space), x.ofLp 2 ≠ 0 → EndpointCoordinates.endpointRoot (2 * F.data.h) (x.ofLp 2) < qbig → ∀ (j : ℕ), Nonempty (JointResidualLimits.OneSidedExtension (MixedCandidateAssembly.pressureStages H v upper bandFloor pInitial pStages j) x)) : have A := MixedCandidateAssembly.potentialStages H v upper bandFloor initial stages; have B := LocalAngularDiagonal.rawSeries D; have P := MixedCandidateAssembly.pressureStages H v upper bandFloor pInitial pStages; ∃ (a : ℕ → ℕ), SelectedSchedule F.data.h qbig A B P a ∧ have ASum := SolenoidalDiagonal.potentialSum (fun (j : ℕ) => ↑(a j)) (PhysicalWaveSum.physicalQ F.data.h) A; have BSum := SolenoidalDiagonal.potentialSum (fun (j : ℕ) => ↑(a j)) (PhysicalWaveSum.physicalQ F.data.h) B; have PSum := SolenoidalDiagonal.potentialSum (fun (j : ℕ) => ↑(a j)) (PhysicalWaveSum.physicalQ F.data.h) P; ∃ (ea : JointResidualLimits.AwayExtensions ASum) (eb : JointResidualLimits.AwayExtensions BSum) (ep : JointResidualLimits.AwayExtensions PSum) (forcing : ProblemStatement.VelocityField), ProblemStatement.CandidateProperties (TimeLocalization.activatedVelocity (MixedPeriodicAssembly.periodicVelocity ASum BSum)) (TimeLocalization.activatedPressure (SpatialLocalization.periodicPressure PSum)) forcing ∧ ContDiff ℝ (↑⊤) forcing ∧ CandidateConsequences.Consequences (TimeLocalization.activatedVelocity (MixedPeriodicAssembly.periodicVelocity ASum BSum)) (TimeLocalization.activatedPressure (SpatialLocalization.periodicPressure PSum)) forcing ∧ Filter.Tendsto (fun (t : ℝ) => PeriodicSobolev.derivativeH3Norm fun (x : ProblemStatement.Space) => TimeLocalization.activatedVelocity (MixedPeriodicAssembly.periodicVelocity ASum BSum) (t, x)) (nhdsWithin 1 (Set.Iio 1)) Filter.atTop ∧ (∀ (m : ℕ) (K : ℝ), 0 ≤ K → ∃ (C : ℝ), 0 < C ∧ ∀ (t : ℝ), 0 ≤ t → ∀ (x : ProblemStatement.Space) (directions : Fin m → Fin 4) (j : Fin 3), |((iteratedFDeriv ℝ m forcing (t, x)) fun (i : Fin m) => CompactForceDecay.spacetimeCoordinate (directions i)).ofLp j| ≤ C * (1 + t) ^ (-K)) ∧ ∀ (n : ℕ) (x : ProblemStatement.Space), iteratedFDeriv ℝ n forcing (1, x) = MixedPeriodicAssembly.boundaryLimits ASum BSum PSum ea eb ep x n

The original finite-stage inputs produce one schedule and its actual activated fields, together with the full mixed-force conclusion.

def NavierStokes.GermCandidateAssembly.AxisZeroOn (Ω : Set ProblemStatement.SpaceTime) (f : ProblemStatement.VelocityField) : Prop

A property of the actual primitive field on a local physical domain. The zero neighborhood may depend on the point and on the stage.

Equations

• NavierStokes.GermCandidateAssembly.AxisZeroOn Ω f = ∀ w ∈ Ω, NavierStokes.PhysicalGraphBounds.radialProjection w = 0 → f =ᶠ[nhds w] fun (x : NavierStokes.ProblemStatement.SpaceTime) => 0

theorem NavierStokes.GermCandidateAssembly.AxisZeroOn.add {Ω : Set ProblemStatement.SpaceTime} {f g : ProblemStatement.VelocityField} (hf : AxisZeroOn Ω f) (hg : AxisZeroOn Ω g) : AxisZeroOn Ω fun (w : ProblemStatement.SpaceTime) => f w + g w

theorem NavierStokes.GermCandidateAssembly.potentialStage_axisZeroOn {h qbig : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (p : MixedAxisPreservation.PotentialStage h (MixedAxisPreservation.localDomain h qbig)) : AxisZeroOn (MixedAxisPreservation.localDomain h qbig) p.field

The original concrete potential-stage data supplies the new hypothesis directly. No regularity assertion about its copy representation is added.

theorem NavierStokes.GermCandidateAssembly.angularSupport_axisZeroOn {h qbig : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (p : MixedAxisPreservation.AngularSupport (MixedAxisPreservation.localDomain h qbig)) : AxisZeroOn (MixedAxisPreservation.localDomain h qbig) p.field

Literal supported mean-stream potentials satisfy the same local property.

noncomputable def NavierStokes.GermCandidateAssembly.initializedSeries (base initial : ProblemStatement.VelocityField) (stages : ℕ → ProblemStatement.VelocityField) : ℕ → ProblemStatement.VelocityField

The base and finite initialization retain the same zeroth cutoff.

Equations

• NavierStokes.GermCandidateAssembly.initializedSeries base initial stages 0 = fun (w : NavierStokes.ProblemStatement.SpaceTime) => base w + initial w
• NavierStokes.GermCandidateAssembly.initializedSeries base initial stages j.succ = stages j

theorem NavierStokes.GermCandidateAssembly.initializedSeries_zero (base initial : ProblemStatement.VelocityField) (stages : ℕ → ProblemStatement.VelocityField) (w : ProblemStatement.SpaceTime) : initializedSeries base initial stages 0 w = base w + initial w

theorem NavierStokes.GermCandidateAssembly.initializedSeries_succ (base initial : ProblemStatement.VelocityField) (stages : ℕ → ProblemStatement.VelocityField) (j : ℕ) : initializedSeries base initial stages (j + 1) = stages j

theorem NavierStokes.GermCandidateAssembly.initializedSeries_of_potentialStage {h : ℝ} {Ω : Set ProblemStatement.SpaceTime} (base : ProblemStatement.VelocityField) (initial : MixedAxisPreservation.PotentialStage h Ω) (stages : ℕ → MixedAxisPreservation.PotentialStage h Ω) : (initializedSeries base initial.field fun (j : ℕ) => (stages j).field) = MixedAxisPreservation.initializedSeries base initial stages

Substituting the original stage fields gives exactly the original series.

theorem NavierStokes.GermCandidateAssembly.potentialSum_eq_base_germ {scales : ℕ → ℝ} (hs : Filter.Tendsto scales Filter.atTop Filter.atTop) {q : ProblemStatement.SpaceTime → ℝ} {base initial : ProblemStatement.VelocityField} {stages : ℕ → ProblemStatement.VelocityField} {w : ProblemStatement.SpaceTime} (hq : ContinuousAt q w) (hpos : 0 < q w) (hInitial : initial =ᶠ[nhds w] fun (x : ProblemStatement.SpaceTime) => 0) (hStages : ∀ (j : ℕ), stages j =ᶠ[nhds w] fun (x : ProblemStatement.SpaceTime) => 0) (hsmall : |scales 0 * q w| < 1 / 2) : SolenoidalDiagonal.potentialSum scales q (initializedSeries base initial stages) =ᶠ[nhds w] base

Local finiteness intersects only finitely many stage-dependent zero neighborhoods. On the zeroth cutoff plateau the actual potential sum has the base germ, including the finite initialization.

noncomputable def NavierStokes.GermCandidateAssembly.potentialStages {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (bandFloor : ℕ) (initial : ProblemStatement.VelocityField) (stages : ℕ → ProblemStatement.VelocityField) : ℕ → ProblemStatement.VelocityField

Potential stages, given by initializedSeries (TailGaugePotential.finalPotential H v upper bandFloor) initial stages.

Equations

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

theorem NavierStokes.GermCandidateAssembly.origin_eventually_base {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (bandFloor : ℕ) {qbig : ℝ} (hqbig : 0 < qbig) (initial : ProblemStatement.VelocityField) (stages : ℕ → ProblemStatement.VelocityField) (D : ℕ → DirectAngularDiagonal.AngularData (LocalAngularDiagonal.localSlowDomain F.data.h qbig)) (hInitial : AxisZeroOn (MixedAxisPreservation.localDomain F.data.h qbig) initial) (hStages : ∀ (j : ℕ), AxisZeroOn (MixedAxisPreservation.localDomain F.data.h qbig) (stages j)) {scales : ℕ → ℝ} (hs : Filter.Tendsto scales Filter.atTop Filter.atTop) : (fun (t : ℝ) => MixedPeriodicAssembly.velocity (SolenoidalDiagonal.potentialSum scales (PhysicalWaveSum.physicalQ F.data.h) (potentialStages H v upper bandFloor initial stages)) (SolenoidalDiagonal.potentialSum scales (PhysicalWaveSum.physicalQ F.data.h) (LocalAngularDiagonal.rawSeries D)) (t, 0)) =ᶠ[nhdsWithin 1 (Set.Iio 1)] fun (t : ℝ) => FinalSlowBase.velocity H v upper bandFloor (t, 0)

The actual mixed diagonal agrees at the origin with the constructed slow base for all sufficiently late times. Its blow-up is not an input.

theorem NavierStokes.GermCandidateAssembly.origin_blowup {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (bandFloor : ℕ) {qbig : ℝ} (hqbig : 0 < qbig) (initial : ProblemStatement.VelocityField) (stages : ℕ → ProblemStatement.VelocityField) (D : ℕ → DirectAngularDiagonal.AngularData (LocalAngularDiagonal.localSlowDomain F.data.h qbig)) (hInitial : AxisZeroOn (MixedAxisPreservation.localDomain F.data.h qbig) initial) (hStages : ∀ (j : ℕ), AxisZeroOn (MixedAxisPreservation.localDomain F.data.h qbig) (stages j)) {scales : ℕ → ℝ} (hs : Filter.Tendsto scales Filter.atTop Filter.atTop) : Filter.Tendsto (fun (t : ℝ) => ‖MixedPeriodicAssembly.velocity (SolenoidalDiagonal.potentialSum scales (PhysicalWaveSum.physicalQ F.data.h) (potentialStages H v upper bandFloor initial stages)) (SolenoidalDiagonal.potentialSum scales (PhysicalWaveSum.physicalQ F.data.h) (LocalAngularDiagonal.rawSeries D)) (t, 0)‖) (nhdsWithin 1 (Set.Iio 1)) Filter.atTop

theorem NavierStokes.GermCandidateAssembly.exists_candidate_witness_of_finite_stages {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (bandFloor : ℕ) {qbig C : ℝ} (hqbig : 0 < qbig) (initial : ProblemStatement.VelocityField) (stages : ℕ → ProblemStatement.VelocityField) (D : ℕ → DirectAngularDiagonal.AngularData (LocalAngularDiagonal.localSlowDomain F.data.h qbig)) (pInitial : ProblemStatement.PressureField) (pStages : ℕ → ProblemStatement.PressureField) (E : MixedCandidateAssembly.StageEstimates F.data.h qbig (potentialStages H v upper bandFloor initial stages) (LocalAngularDiagonal.rawSeries D) (MixedCandidateAssembly.pressureStages H v upper bandFloor pInitial pStages)) (hInitial : MixedDiagonalExtensions.SublevelShrinkingSupport F.data.h C qbig initial) (hStages : ∀ (j : ℕ), MixedDiagonalExtensions.SublevelShrinkingSupport F.data.h C qbig (stages j)) (hDirect : ∀ (j : ℕ), MixedDiagonalExtensions.SublevelShrinkingSupport F.data.h C qbig (LocalAngularDiagonal.rawSeries D j)) (hpInitial : MixedDiagonalExtensions.SublevelShrinkingSupport F.data.h C qbig pInitial) (hpStages : ∀ (j : ℕ), MixedDiagonalExtensions.SublevelShrinkingSupport F.data.h C qbig (pStages j)) (eA : ∀ (x : ProblemStatement.Space), x.ofLp 2 ≠ 0 → EndpointCoordinates.endpointRoot (2 * F.data.h) (x.ofLp 2) < qbig → ∀ (j : ℕ), Nonempty (JointResidualLimits.OneSidedExtension (potentialStages H v upper bandFloor initial stages j) x)) (eB : ∀ (x : ProblemStatement.Space), x.ofLp 2 ≠ 0 → EndpointCoordinates.endpointRoot (2 * F.data.h) (x.ofLp 2) < qbig → ∀ (j : ℕ), Nonempty (JointResidualLimits.OneSidedExtension (LocalAngularDiagonal.rawSeries D j) x)) (eP : ∀ (x : ProblemStatement.Space), x.ofLp 2 ≠ 0 → EndpointCoordinates.endpointRoot (2 * F.data.h) (x.ofLp 2) < qbig → ∀ (j : ℕ), Nonempty (JointResidualLimits.OneSidedExtension (MixedCandidateAssembly.pressureStages H v upper bandFloor pInitial pStages j) x)) (hInitialAxis : AxisZeroOn (MixedAxisPreservation.localDomain F.data.h qbig) initial) (hStagesAxis : ∀ (j : ℕ), AxisZeroOn (MixedAxisPreservation.localDomain F.data.h qbig) (stages j)) : have A := potentialStages H v upper bandFloor initial stages; have B := LocalAngularDiagonal.rawSeries D; have P := MixedCandidateAssembly.pressureStages H v upper bandFloor pInitial pStages; ∃ (a : ℕ → ℕ), MixedCandidateWitness.SelectedSchedule F.data.h qbig A B P a ∧ have ASum := SolenoidalDiagonal.potentialSum (fun (j : ℕ) => ↑(a j)) (PhysicalWaveSum.physicalQ F.data.h) A; have BSum := SolenoidalDiagonal.potentialSum (fun (j : ℕ) => ↑(a j)) (PhysicalWaveSum.physicalQ F.data.h) B; have PSum := SolenoidalDiagonal.potentialSum (fun (j : ℕ) => ↑(a j)) (PhysicalWaveSum.physicalQ F.data.h) P; ∃ (ea : JointResidualLimits.AwayExtensions ASum) (eb : JointResidualLimits.AwayExtensions BSum) (ep : JointResidualLimits.AwayExtensions PSum) (forcing : ProblemStatement.VelocityField), ProblemStatement.CandidateProperties (TimeLocalization.activatedVelocity (MixedPeriodicAssembly.periodicVelocity ASum BSum)) (TimeLocalization.activatedPressure (SpatialLocalization.periodicPressure PSum)) forcing ∧ ContDiff ℝ (↑⊤) forcing ∧ CandidateConsequences.Consequences (TimeLocalization.activatedVelocity (MixedPeriodicAssembly.periodicVelocity ASum BSum)) (TimeLocalization.activatedPressure (SpatialLocalization.periodicPressure PSum)) forcing ∧ Filter.Tendsto (fun (t : ℝ) => PeriodicSobolev.derivativeH3Norm fun (x : ProblemStatement.Space) => TimeLocalization.activatedVelocity (MixedPeriodicAssembly.periodicVelocity ASum BSum) (t, x)) (nhdsWithin 1 (Set.Iio 1)) Filter.atTop ∧ (∀ (m : ℕ) (K : ℝ), 0 ≤ K → ∃ (C : ℝ), 0 < C ∧ ∀ (t : ℝ), 0 ≤ t → ∀ (x : ProblemStatement.Space) (directions : Fin m → Fin 4) (j : Fin 3), |((iteratedFDeriv ℝ m forcing (t, x)) fun (i : Fin m) => CompactForceDecay.spacetimeCoordinate (directions i)).ofLp j| ≤ C * (1 + t) ^ (-K)) ∧ ∀ (n : ℕ) (x : ProblemStatement.Space), iteratedFDeriv ℝ n forcing (1, x) = MixedPeriodicAssembly.boundaryLimits ASum BSum PSum ea eb ep x n

This has the original finite-stage obligations, with arbitrary physical potential increments and their primitive local axis zero germs. It returns the same selected schedule, exact mixed fields and full force consequences.

theorem NavierStokes.GermCandidateAssembly.candidate_of_finite_stages {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (bandFloor : ℕ) {qbig C : ℝ} (hqbig : 0 < qbig) (initial : ProblemStatement.VelocityField) (stages : ℕ → ProblemStatement.VelocityField) (D : ℕ → DirectAngularDiagonal.AngularData (LocalAngularDiagonal.localSlowDomain F.data.h qbig)) (pInitial : ProblemStatement.PressureField) (pStages : ℕ → ProblemStatement.PressureField) (E : MixedCandidateAssembly.StageEstimates F.data.h qbig (potentialStages H v upper bandFloor initial stages) (LocalAngularDiagonal.rawSeries D) (MixedCandidateAssembly.pressureStages H v upper bandFloor pInitial pStages)) (hInitial : MixedDiagonalExtensions.SublevelShrinkingSupport F.data.h C qbig initial) (hStages : ∀ (j : ℕ), MixedDiagonalExtensions.SublevelShrinkingSupport F.data.h C qbig (stages j)) (hDirect : ∀ (j : ℕ), MixedDiagonalExtensions.SublevelShrinkingSupport F.data.h C qbig (LocalAngularDiagonal.rawSeries D j)) (hpInitial : MixedDiagonalExtensions.SublevelShrinkingSupport F.data.h C qbig pInitial) (hpStages : ∀ (j : ℕ), MixedDiagonalExtensions.SublevelShrinkingSupport F.data.h C qbig (pStages j)) (eA : ∀ (x : ProblemStatement.Space), x.ofLp 2 ≠ 0 → EndpointCoordinates.endpointRoot (2 * F.data.h) (x.ofLp 2) < qbig → ∀ (j : ℕ), Nonempty (JointResidualLimits.OneSidedExtension (potentialStages H v upper bandFloor initial stages j) x)) (eB : ∀ (x : ProblemStatement.Space), x.ofLp 2 ≠ 0 → EndpointCoordinates.endpointRoot (2 * F.data.h) (x.ofLp 2) < qbig → ∀ (j : ℕ), Nonempty (JointResidualLimits.OneSidedExtension (LocalAngularDiagonal.rawSeries D j) x)) (eP : ∀ (x : ProblemStatement.Space), x.ofLp 2 ≠ 0 → EndpointCoordinates.endpointRoot (2 * F.data.h) (x.ofLp 2) < qbig → ∀ (j : ℕ), Nonempty (JointResidualLimits.OneSidedExtension (MixedCandidateAssembly.pressureStages H v upper bandFloor pInitial pStages j) x)) (hInitialAxis : AxisZeroOn (MixedAxisPreservation.localDomain F.data.h qbig) initial) (hStagesAxis : ∀ (j : ℕ), AxisZeroOn (MixedAxisPreservation.localDomain F.data.h qbig) (stages j)) : ProblemStatement.candidateStatement

The manuscript's exact candidate target follows from the same primitive finite-stage data; no separate candidate witness is assumed.