Spatial derivatives of the classical solutions in Section 4 inherit the periodicity needed by the torus energy argument.

theorem AVenhance.Infra.Section4.iteratedFDeriv_z2Periodic {f : Homogenization.Vec 2 → ℝ} (hper : IsZ2Periodic f) (n : ℕ) (k : Fin 2 → ℤ) (x : Homogenization.Vec 2) : iteratedFDeriv ℝ n f (x + latticeShift k) = iteratedFDeriv ℝ n f x

Every iterated spatial derivative of a periodic function is periodic. This is the derivative-level periodicity used when integrating the differentiated equation by parts on the unit cell.