The first round of prop:bootstrap with its source data supplied

The one-round velocity improvement of prop:bootstrap takes three inputs: the pressure-gradient producer, the gradient-slot heat representation, and the localized source data of eq:local-equation at the first-round exponents (6/5, 25/11) and (3, 25/6). The last of these is first_round_source_package_of_sws, so the round below carries only the two remaining inputs.

theorem CKN.Core.Step4.routeA_final_source_package_of_sws : routeAFinalSourcePackage

The localized first-round source data of eq:local-equation in the exact shape consumed by the one-round velocity improvement.

theorem CKN.Core.Step4.routeA_one_round_velocity_improvement_of_gradient_inputs (hG : routeAGradientProducer) (hL : routeAGradientSlotRepresentation) (q : ℝ) : 5 / 2 < q → ∀ {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}, IsSuitableWeakSolutionIntegrable Ω I q u Du p f → ∀ (z₀ : Foundation.Parabolic.ParabolicPoint) (R : ℝ), 0 < R → Metric.ball z₀ (2 * R) ⊆ spaceTimeSet Ω I → morreyVecMem 3 (25 / 3) (Metric.ball z₀ R) u → (∀ (i : Fin 3), morreyVecMem 2 (25 / 8) (Metric.ball z₀ R) fun (z : Foundation.Parabolic.ParabolicPoint) => Du z i) → morreyVecMem 3 25 (Metric.ball z₀ (R / 4)) u

One round of prop:bootstrap on an arbitrary parabolic ball: from u ∈ M^{3,25/3} and ∇u ∈ M^{2,25/8} on 𝔅_R(z₀) the velocity improves to u ∈ M^{3,25} on 𝔅_{R/4}(z₀), given the pressure-gradient producer and the gradient-slot heat representation.