Local Sobolev realization from mollified Leray data

The mollified initial field enters the complete H²ᵏ local mild construction at every even order.

theorem CKN.Leray.regUniformMollifiedInitial_local_bessel_representation (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (k : ℕ) : let b₀ := realVectorL2OfCoordinateFunction (regUniformMollifiedInitial ρ ε hε a) ⋯; ∃ (b : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2), (regularisedBesselSobolevToL2CLM ↑(2 * k) ⋯) b = complexifyVectorL2 b₀ ∧ ∃ (u : C(↑(RegularizedMildTimeInterval (regularisedBesselLocalLifespan ρ ε hε k b)), BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2)), regularisedBesselLocalMap ρ ε hε k b (regularisedBesselLocalLifespan ρ ε hε k b) ⋯ u = u ∧ ‖u‖ ≤ regularisedBesselLocalRadius k b ∧ ∀ (t : ↑(RegularizedMildTimeInterval (regularisedBesselLocalLifespan ρ ε hε k b))), (regularisedBesselSobolevToL2CLM ↑(2 * k) ⋯) (u t) = complexifyVectorL2 (regularizedGlobalMildCurve ρ ε hε b₀ ⋯ ↑t)

Every mollified Leray datum starts a complete H²ᵏ mild path that represents the same global spatial L² trajectory on its lifespan.