The recursively constructed jet flows obey the composition and inverse identities of a genuine global flow.
theorem
AVenhance.Infra.Flow.FiniteJetFlowGroupLaw.spatialJetSolutions_unique_on_window
{b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
(hb : SmoothPeriodicField b)
(n : ℕ)
{f g : ℝ → SpatialJetState n}
(a d r : ℝ)
(hr : r ∈ Set.Ioo a d)
(hf : ContinuousOn f (Set.Icc a d))
(hf' : ∀ (q : ℝ), HasDerivAt f (spatialJetField b n q (f q)) q)
(hg : ContinuousOn g (Set.Icc a d))
(hg' : ∀ (q : ℝ), HasDerivAt g (spatialJetField b n q (g q)) q)
(hinit : f r = g r)
(t : ℝ)
: