Local recovery and ordinary uniqueness identify the canonical maximal velocity with every global Comparator solution.

theorem Euler.ComparatorBridge.maximalVelocity_eq_of_local_evolution {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : EulerOrdinarySobolev.FiniteLifespan A) {v : EulerSmoothLimit.Space → ℝ → EulerSmoothLimit.Space} {p : EulerSmoothLimit.Space → ℝ → ℝ} (h : EulerExistenceAndSmoothnessR3 A.field v p) (hcompact : ∀ (t : L.Time), HasCompactSupport (EulerMeanCutoffCurl.vectorCurl (L.maximalVelocity t))) (hlocal : HasLocalEvolutionAtCompactCurl v) (t : L.Time) : L.maximalVelocity t = fun (x : EulerSmoothLimit.Space) => v x ↑t

theorem Euler.ComparatorBridge.maximalVelocity_eq_of_compactCurlLocalUpgrade {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : EulerOrdinarySobolev.FiniteLifespan A) {v : EulerSmoothLimit.Space → ℝ → EulerSmoothLimit.Space} {p : EulerSmoothLimit.Space → ℝ → ℝ} (h : EulerExistenceAndSmoothnessR3 A.field v p) (hcompact : ∀ (t : L.Time), HasCompactSupport (EulerMeanCutoffCurl.vectorCurl (L.maximalVelocity t))) (hupgrade : CompactCurlLocalUpgrade) (t : L.Time) : L.maximalVelocity t = fun (x : EulerSmoothLimit.Space) => v x ↑t

The local analytic bridge suffices to identify the Comparator with the canonical maximal solution, without additional time or space assumptions.