Actual differentiated flux pairings on the periodic cell.

theorem AVenhance.Infra.Section4.iterateWordFlux_smooth {A : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} {v : Homogenization.Vec 2 → ℝ} (hA : ContDiff ℝ (↑⊤) A) (hv : ContDiff ℝ (↑⊤) v) (w : List (Fin 2)) : ContDiff ℝ (↑⊤) (iterateWordFlux A v w)

Smoothness of each expanded flux follows from the exact word identity.

theorem AVenhance.Infra.Section4.iterateWordFlux_periodic {A : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} {v : Homogenization.Vec 2 → ℝ} (hA : ContDiff ℝ (↑⊤) A) (hv : ContDiff ℝ (↑⊤) v) (hAp : IsZ2Periodic A) (hvp : IsZ2Periodic v) (w : List (Fin 2)) : IsZ2Periodic (iterateWordFlux A v w)

Periodicity of every expanded flux is inherited from the actual factors.

theorem AVenhance.Infra.Section4.iterate_stream_principal_pairing_zero (ψ u : Homogenization.Vec 2 → ℝ) (x : Homogenization.Vec 2) : Homogenization.vecDot (spaceGrad u x) ((ψ x • sigmaMat).mulVec (spaceGrad u x)) = 0

The principal stream flux cancels pointwise with its own gradient.