theorem flow_param_derivatives {n : ℕ} (Psi : CM18.FlowMap n) (phi : CM18.ScalarField n) (m : CM18.Metric n) (mInv : CM18.InverseMetric n) (hphi : ContDiff ℝ ⊤ phi) (xt : CM18.Spacetime n) (hm : ∀ (alpha beta : Fin (n + 1)), ContDiff ℝ ⊤ fun (y : CM18.Spacetime n) => m y alpha beta) (hmInv : ∀ (alpha beta : Fin (n + 1)), ContDiff ℝ ⊤ fun (y : CM18.Spacetime n) => mInv y alpha beta) : deriv (fun (eps : ℝ) => CM18.transformedField Psi phi eps xt) 0 = -∑ alpha : Fin (n + 1), Psi.Y xt alpha * CM18.spacetimeGradient phi xt alpha ∧ (∀ (mu : Fin (n + 1)), deriv (fun (eps : ℝ) => CM18.transformedGradient Psi phi eps xt mu) 0 = -(fderiv ℝ (fun (y : CM18.Spacetime n) => ∑ alpha : Fin (n + 1), Psi.Y y alpha * CM18.spacetimeGradient phi y alpha) xt) (Pi.single mu 1)) ∧ (∀ (mu nu : Fin (n + 1)), deriv (fun (eps : ℝ) => CM18.transformedMetric Psi m eps xt mu nu) 0 = -(∑ alpha : Fin (n + 1), m xt alpha nu * (fderiv ℝ (fun (y : CM18.Spacetime n) => Psi.Y y alpha) xt) (Pi.single mu 1) + ∑ alpha : Fin (n + 1), m xt mu alpha * (fderiv ℝ (fun (y : CM18.Spacetime n) => Psi.Y y alpha) xt) (Pi.single nu 1) + ∑ alpha : Fin (n + 1), Psi.Y xt alpha * (fderiv ℝ (fun (y : CM18.Spacetime n) => m y mu nu) xt) (Pi.single alpha 1))) ∧ (∀ (mu nu : Fin (n + 1)), deriv (fun (eps : ℝ) => CM18.transformedInverseMetric Psi mInv eps xt mu nu) 0 = ∑ alpha : Fin (n + 1), mInv xt alpha nu * (fderiv ℝ (fun (y : CM18.Spacetime n) => Psi.Y y mu) xt) (Pi.single alpha 1) + ∑ alpha : Fin (n + 1), mInv xt mu alpha * (fderiv ℝ (fun (y : CM18.Spacetime n) => Psi.Y y nu) xt) (Pi.single alpha 1) - ∑ alpha : Fin (n + 1), Psi.Y xt alpha * (fderiv ℝ (fun (y : CM18.Spacetime n) => mInv y mu nu) xt) (Pi.single alpha 1)) ∧ deriv (fun (eps : ℝ) => (Matrix.of fun (mu nu : Fin (n + 1)) => Psi.invJacobian eps xt mu nu).det) 0 = -∑ alpha : Fin (n + 1), (fderiv ℝ (fun (y : CM18.Spacetime n) => Psi.Y y alpha) xt) (Pi.single alpha 1)

Proposition 2.0.2 (packaged): derivatives with respect to the flow parameter $\epsilon$ at $\epsilon = 0$ of the transformed scalar field $\widetilde{\varphi}$, its gradient $\widetilde{\nabla}_\mu \widetilde{\varphi}$, the metric $\widetilde{m}_{\mu\nu}$, the inverse metric $(\widetilde{m}^{-1})^{\mu\nu}$, and $\det M^{-1}$, expressed in terms of the generating vector field $Y$.