Initial-data bounds in the ordered-word convention used by the energy recursion.

theorem AVenhance.Infra.Section4.theta_initial_word_l2_le_of_analytic {R : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} (hθ₀ : IsThetaAnalytic R θ₀) {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {F θ : ℝ → Homogenization.Vec 2 → ℝ} (hsol : IsClassicalSol b κ F θ₀ θ) (w : List (Fin 2)) : √(∫ (x : Homogenization.Vec 2) in unitCube, classicalWordDerivative w θ₀ x ^ 2) ≤ √(l2NormSq θ₀) * (↑w.length.factorial / R ^ w.length)

The paper's analytic initial-data hypothesis gives the same factorial bound for every ordered coordinate word.