Strict lower-level budgets for every actual correction factor.

theorem AVenhance.Infra.Section4.amnrFactorCount_le_sum (A : List AmnrAdvectionFactor) (a : AmnrAdvectionFactor) (ha : a ∈ A) (F : List (Option (Fin 2)) → ℕ) : F a.2 ≤ (List.map (fun (b : AmnrAdvectionFactor) => F b.2) A).sum

theorem AVenhance.Infra.Section4.amnrCorrectionBudgets (α : List (Fin 2)) (n : ℕ) (t : AmnrAdvectionTerm) (ht : t ∈ amnrSpatialAdvectionTerms α (amnrMaterialErrorTerms n)) : t.scalarWord ≠ [] ∧ amnrMaterialCount t.scalarWord < n ∧ amnrBudget t.scalarWord + 1 ≤ α.length + 2 * n ∧ ∀ a ∈ t.factors, amnrMaterialCount a.2 < n ∧ amnrBudget a.2 + 2 ≤ α.length + 2 * n

The scalar word is nonempty and every scalar and velocity word uses strictly fewer material derivatives than the current induction level.