The stream velocity is classically divergence-free, so its inverse-flow cofactor Piola identity follows from the source sequence alone.

theorem AVenhance.Infra.Section5.spatialDivergence_eq_vecDiv {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : Flow.SmoothPeriodicField b) (t : ℝ) (x : Homogenization.Vec 2) : Flow.spatialDivergence b t x = vecDiv (b t) x

The flow's trace divergence agrees with the classical divergence.

theorem AVenhance.Infra.Section5.streamVel_spatialDivergence_eq_zero {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (t : ℝ) (x : Homogenization.Vec 2) : Flow.spatialDivergence (streamVel (Φ (m - 1))) t x = 0

Every predecessor stream has zero classical spatial divergence.

theorem AVenhance.Infra.Section5.xFlowInv_cofactorPiola_of_streamSeq {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (t : ℝ) (x : Homogenization.Vec 2) {g : Homogenization.Vec 2 → Homogenization.Vec 2} {Lg : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2} (hg : HasFDerivAt g Lg (I.xFlowInv hΦ m l t x)) : vecDiv (fun (y : Homogenization.Vec 2) => (rowCofactor (gradMatrix (I.xFlowInv hΦ m l t) y)).mulVec (g (I.xFlowInv hΦ m l t y))) x = vecDiv g (I.xFlowInv hΦ m l t x)

Full inverse-flow cofactor transport for the source flow. The cofactor-divergence identity follows from the C² flow slice; determinant one follows from Liouville and the divergence identity derived above.