Complete Sobolev paths on uniform continuation grids

The physical L² energy bound fixes one positive continuation step. Successive Sobolev restarts then concatenate into a path through any finite number of steps.

theorem CKN.Leray.regularisedBesselGlobalGridPath (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (k : ℕ) (b₀ : ↥RealVectorL2) (hbJ : RegularizedMildJData b₀) (b : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2) (hb : (regularisedBesselSobolevToL2CLM ↑(2 * k) ⋯) b = complexifyVectorL2 b₀) (n : ℕ) : have δ := regularisedBesselUniformEnergyStep ρ ε hε k ‖b₀‖; ∃ (v : C(↑(RegularizedMildTimeInterval (↑n * δ)), BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2)), ∀ (t : ↑(RegularizedMildTimeInterval (↑n * δ))), (regularisedBesselSobolevToL2CLM ↑(2 * k) ⋯) (v t) = complexifyVectorL2 (regularizedGlobalMildCurve ρ ε hε b₀ hbJ ↑t)

A complete Sobolev realization at time zero extends continuously through any finite number of uniform continuation steps.