The identification of this repository's three independent spatial-derivative formalisms — the multi-index multiPartial/spatialPartial pair used to state the pointwise vorticity-equation bounds of Serrin's route, the gradVec/classicalGradient pair used by the cutoff library, and the gradPair/partialLaplacian pair used by the Green's-identity machinery of the local Caccioppoli inequality — so that a bound proved in one idiom is available in the others for the proof of lem:aniso:annulus's interior estimates.

theorem CIV.spatialPartial_eq_gradPair (g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (i : Fin 3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : CKN.spatialPartial g i z = gradPair 3 g z (CKN.basisVec i)

theorem CIV.gradVec_eq_gradPair_comp_fst (χ : CKN.Foundation.Parabolic.Vec3 → ℝ) (x : CKN.Foundation.Parabolic.Vec3) (τ : ℝ) (i : Fin 3) : gradVec χ x i = gradPair 3 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => χ z.1) (x, τ) (CKN.basisVec i)

theorem CIV.partialLaplacian_three_eq_sum_spatialSecondPartial (g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (z : CKN.Foundation.Parabolic.ParabolicPoint) : partialLaplacian 3 3 g z = ∑ i : Fin 3, CKN.spatialSecondPartial g i i z

theorem CIV.multiPartial_single_eq_spatialPartial (g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (i : Fin 3) : multiPartial g (Pi.single i 1) = CKN.spatialPartial g i