Identification of the first globally constructed jet with the spatial Fréchet derivative of the original flow.

theorem AVenhance.Infra.Flow.spatialJetFlow_one_identity_eq_firstJetFlow {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (t : ℝ) (x : Homogenization.Vec 2) (s : ℝ) : spatialJetFlow hb X hX 1 t (spatialJetIdentitySeed 1 x) s = firstJetFlow X t (spatialJetIdentitySeed 1 x) s

The first recursively constructed jet flow, started from the identity jet, is exactly the established position/Jacobian augmented flow.

theorem AVenhance.Infra.Flow.spatialJetFlow_one_identity_components {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (t : ℝ) (x : Homogenization.Vec 2) (s : ℝ) : spatialJetFlow hb X hX 1 t (spatialJetIdentitySeed 1 x) s = (X t x s, fun (i : Fin 2) => (fderiv ℝ (fun (y : Homogenization.Vec 2) => X t y s) x) (Pi.single i 1))

In coordinates, the first identity-seeded jet consists of the original flow and its spatial derivative applied to the coordinate directions.