C¹ breakdown for the concrete compactly supported datum. The infinite-limsup statement is expressed directly: after every time below the maximal time, the actual gradient supremum exceeds every real bound. The norms are bounded-continuous-function norms at individual times, not totalized real L∞ seminorms of unverified measurable fields.

The full smooth initial datum retains the common support of its finite initial base and its actual summable packet increments.

theorem EulerPacketInduction.Stage.initialDataLimit_support {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} (P : (n : ℕ) → Stage S n) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) (hbase : tsupport (initialBase P).field ⊆ Metric.closedBall 0 2) : tsupport (initialDataLimit P hq hB).field ⊆ Metric.closedBall 0 2

theorem EulerPacketInduction.Stage.initialDataLimit_compact {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} (P : (n : ℕ) → Stage S n) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) (hbase : tsupport (initialBase P).field ⊆ Metric.closedBall 0 2) : HasCompactSupport (initialDataLimit P hq hB).field

theorem EulerPacketInduction.Stage.initialDataLimit_support_of_physical {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} (P : (n : ℕ) → Stage S n) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) (hbase : (tsupport fun (x : EulerSmoothLimit.Space) => (P 1).state.evolution.velocity (0, x)) ⊆ Metric.closedBall 0 2) : tsupport (initialDataLimit P hq hB).field ⊆ Metric.closedBall 0 2

A compactly supported, smooth, divergence-free initial velocity whose ordinary smooth Euler solutions have a finite maximal horizon. The separate continuation and vorticity criteria are not asserted here.

theorem EulerPacketInduction.initialDatum_support : tsupport initialDatum.field ⊆ Metric.closedBall 0 2

theorem EulerPacketInduction.initialDatum_compact : HasCompactSupport initialDatum.field

theorem EulerPacketInduction.lifespan_le_one : lifespan.duration ≤ 1

def EulerPacketInduction.HasSmoothEulerSolution (u₀ : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (T : ℝ) : Prop

Has smooth euler solution, given by ∃ hT : 0 < T, ∃ U : Evolution T hT.le, (U.velocity ⟨0,le_rfl,hT.le⟩).field=u₀.

Equations

• EulerPacketInduction.HasSmoothEulerSolution u₀ T = ∃ (hT : 0 < T) (U : EulerOrdinarySobolev.Evolution T ⋯), (U.velocity ⟨0, ⋯⟩).field = u₀

theorem EulerPacketInduction.hasSmoothEulerSolution_iff (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (T : ℝ) : HasSmoothEulerSolution A.field T ↔ EulerOrdinarySobolev.HasEulerEvolution A T

theorem EulerPacketInduction.exists_compact_smooth_finite_lifespan : ∃ (u₀ : EulerSmoothLimit.Space → EulerSmoothLimit.Space), ContDiff ℝ (↑⊤) u₀ ∧ HasCompactSupport u₀ ∧ (∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u₀ x = 0) ∧ ∃ (T : ℝ), 0 < T ∧ T ≤ 1 ∧ (∀ (t : ℝ), 0 < t → t < T → HasSmoothEulerSolution u₀ t) ∧ ∀ (t : ℝ), T < t → ¬HasSmoothEulerSolution u₀ t

noncomputable def EulerOrdinarySobolev.FiniteLifespan.maximalVelocityNorm {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (t : L.Time) : ℝ

Maximal velocity norm, given by ‖finiteField (L.maximalField t)‖.

Equations

• L.maximalVelocityNorm t = ‖EulerMeanSobolevBoundedField.finiteField (L.maximalField t)‖

noncomputable def EulerOrdinarySobolev.FiniteLifespan.maximalGradientNorm {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (t : L.Time) : ℝ

Maximal gradient norm, given by ‖finiteField (L.maximalField t).derivative‖.

Equations

• L.maximalGradientNorm t = ‖EulerMeanSobolevBoundedField.finiteField (L.maximalField t).derivative‖

noncomputable def EulerOrdinarySobolev.FiniteLifespan.maximalC1Norm {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (t : L.Time) : ℝ

Maximal C1 norm, given by L.maximalVelocityNorm t+L.maximalGradientNorm t.

Equations

• L.maximalC1Norm t = L.maximalVelocityNorm t + L.maximalGradientNorm t

theorem EulerOrdinarySobolev.FiniteLifespan.maximalVelocityNorm_nonneg {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (t : L.Time) : 0 ≤ L.maximalVelocityNorm t

theorem EulerOrdinarySobolev.FiniteLifespan.maximalGradientNorm_nonneg {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (t : L.Time) : 0 ≤ L.maximalGradientNorm t

theorem EulerOrdinarySobolev.FiniteLifespan.maximalVelocityNorm_le_iff {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (t : L.Time) (K : ℝ) : L.maximalVelocityNorm t ≤ K ↔ ∀ (x : EulerSmoothLimit.Space), ‖L.maximalVelocity t x‖ ≤ K

theorem EulerOrdinarySobolev.FiniteLifespan.maximalGradientNorm_le_iff {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (t : L.Time) (K : ℝ) : L.maximalGradientNorm t ≤ K ↔ ∀ (x : EulerSmoothLimit.Space), ‖fderiv ℝ (L.maximalVelocity t) x‖ ≤ K

theorem EulerOrdinarySobolev.FiniteLifespan.maximalVelocityNorm_continuous {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) : Continuous L.maximalVelocityNorm

theorem EulerOrdinarySobolev.FiniteLifespan.maximalGradientNorm_continuous {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) : Continuous L.maximalGradientNorm

theorem EulerOrdinarySobolev.FiniteLifespan.maximalC1Norm_continuous {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) : Continuous L.maximalC1Norm

theorem EulerOrdinarySobolev.FiniteLifespan.maximalGradientNorm_eq_evolution {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (S : ℝ) (hS : 0 < S) (hSL : S < L.duration) (t : ↑(Set.Icc 0 S)) : L.maximalGradientNorm (L.shorterTime S hSL t) = (L.evolution S hS hSL).gradientNormPath t

theorem EulerOrdinarySobolev.FiniteLifespan.maximalVelocity_gradient_unbounded_near_endpoint {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (τ K : ℝ) (hτ : τ < L.duration) : ∃ (t : L.Time) (x : EulerSmoothLimit.Space), τ < ↑t ∧ K < ‖fderiv ℝ (L.maximalVelocity t) x‖

theorem EulerOrdinarySobolev.FiniteLifespan.maximalGradientNorm_unbounded_near_endpoint {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (τ K : ℝ) (hτ : τ < L.duration) : ∃ (t : L.Time), τ < ↑t ∧ K < L.maximalGradientNorm t

theorem EulerOrdinarySobolev.FiniteLifespan.maximalC1Norm_unbounded_near_endpoint {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (τ K : ℝ) (hτ : τ < L.duration) : ∃ (t : L.Time), τ < ↑t ∧ K < L.maximalC1Norm t

@[reducible, inline]

abbrev EulerPacketInduction.MaximalTime : Type

Maximal time: an abbreviation for lifespan.Time.

Equations

• EulerPacketInduction.MaximalTime = EulerPacketInduction.lifespan.Time

noncomputable def EulerPacketInduction.maximalVelocity (t : MaximalTime) : EulerSmoothLimit.Space → EulerSmoothLimit.Space

Maximal velocity, given by lifespan.maximalVelocity t.

Equations

• EulerPacketInduction.maximalVelocity t = EulerPacketInduction.lifespan.maximalVelocity t

noncomputable def EulerPacketInduction.maximalPressure (t : MaximalTime) : EulerSmoothLimit.Space → ℝ

Maximal pressure, given by lifespan.maximalPressure t.

Equations

• EulerPacketInduction.maximalPressure t = EulerPacketInduction.lifespan.maximalPressure t

noncomputable def EulerPacketInduction.maximalVelocityNorm (t : MaximalTime) : ℝ

Maximal velocity norm, given by lifespan.maximalVelocityNorm t.

Equations

• EulerPacketInduction.maximalVelocityNorm t = EulerPacketInduction.lifespan.maximalVelocityNorm t

noncomputable def EulerPacketInduction.maximalGradientNorm (t : MaximalTime) : ℝ

Maximal gradient norm, given by lifespan.maximalGradientNorm t.

Equations

• EulerPacketInduction.maximalGradientNorm t = EulerPacketInduction.lifespan.maximalGradientNorm t

noncomputable def EulerPacketInduction.maximalC1Norm (t : MaximalTime) : ℝ

Maximal C1 norm, given by lifespan.maximalC1Norm t.

Equations

• EulerPacketInduction.maximalC1Norm t = EulerPacketInduction.lifespan.maximalC1Norm t

theorem EulerPacketInduction.initialDatum_no_endpoint : ¬HasSmoothEulerSolution initialDatum.field lifespan.duration

theorem EulerPacketInduction.maximalVelocity_initial : maximalVelocity lifespan.initialTime = initialDatum.field

theorem EulerPacketInduction.maximalVelocity_smooth (t : MaximalTime) : ContDiff ℝ (↑⊤) (maximalVelocity t)

theorem EulerPacketInduction.maximalVelocity_joint_continuous : Continuous fun (z : MaximalTime × EulerSmoothLimit.Space) => maximalVelocity z.1 z.2

theorem EulerPacketInduction.maximalVelocity_divergence (t : MaximalTime) (x : EulerSmoothLimit.Space) : EulerSmoothLimit.divergence (maximalVelocity t) x = 0

theorem EulerPacketInduction.maximalPressure_spec (t : MaximalTime) : ContDiff ℝ (↑⊤) (maximalPressure t) ∧ maximalPressure t 0 = 0 ∧ ∀ (x : EulerSmoothLimit.Space), gradient (maximalPressure t) x = (lifespan.maximalPressureField t).field x

theorem EulerPacketInduction.maximalGradientNorm_spec (t : MaximalTime) (K : ℝ) : maximalGradientNorm t ≤ K ↔ ∀ (x : EulerSmoothLimit.Space), ‖fderiv ℝ (maximalVelocity t) x‖ ≤ K

theorem EulerPacketInduction.maximalVelocityNorm_spec (t : MaximalTime) (K : ℝ) : maximalVelocityNorm t ≤ K ↔ ∀ (x : EulerSmoothLimit.Space), ‖maximalVelocity t x‖ ≤ K

theorem EulerPacketInduction.maximalGradientNorm_continuous : Continuous maximalGradientNorm

theorem EulerPacketInduction.maximalC1Norm_continuous : Continuous maximalC1Norm

theorem EulerPacketInduction.pointwiseGradient_unbounded_near_maximal_time (τ K : ℝ) (hτ : τ < lifespan.duration) : ∃ (t : MaximalTime) (x : EulerSmoothLimit.Space), τ < ↑t ∧ K < ‖fderiv ℝ (maximalVelocity t) x‖

theorem EulerPacketInduction.gradient_unbounded_near_maximal_time (τ K : ℝ) (hτ : τ < lifespan.duration) : ∃ (t : MaximalTime), τ < ↑t ∧ K < maximalGradientNorm t

The gradient supremum has infinite upper limit at the actual maximal time.

theorem EulerPacketInduction.c1_unbounded_near_maximal_time (τ K : ℝ) (hτ : τ < lifespan.duration) : ∃ (t : MaximalTime), τ < ↑t ∧ K < maximalC1Norm t

The same characterization for the sum of the actual velocity and gradient suprema.

theorem EulerPacketInduction.initialDatum_c1_breakdown : 0 < lifespan.duration ∧ lifespan.duration ≤ 1 ∧ ¬HasSmoothEulerSolution initialDatum.field lifespan.duration ∧ ∀ τ < lifespan.duration, ∀ (K : ℝ), ∃ (t : MaximalTime), τ < ↑t ∧ K < maximalC1Norm t