Quantitative ordering by weighted budget and finite inversion count.
theorem
AVenhance.Infra.Section4.amnr_normal_order_family_abs_le_of_canonical_bounds
{b : AmnrSpace → Homogenization.Vec 2}
{f : AmnrSpace → ℝ}
(hb : ContDiff ℝ (↑⊤) b)
(hf : ContDiff ℝ (↑⊤) f)
{N cut : ℕ}
{S H F Cb : ℝ}
(hS : 0 ≤ S)
(hH : 0 ≤ H)
(hF : 0 ≤ F)
(hCb : 0 ≤ Cb)
(z : AmnrSpace)
(hprimitive :
∀ (a : Option (Fin 2 × Fin 2)) (α : List (Fin 2)) (n : ℕ),
amnrBudget (amnrMixedWord α n) + amnrNormalFieldCost a ≤ N →
n + amnrNormalFieldReserve a ≤ cut →
|amnrWord b (amnrMixedWord α n) (amnrNormalField b f a) z| ≤ amnrNormalFieldAmplitude F Cb H a * amnrWeight S H (amnrMixedWord α n))
(a : Option (Fin 2 × Fin 2))
(w : List (Option (Fin 2)))
(hbudget : amnrBudget w + amnrNormalFieldCost a ≤ N)
(hcut : amnrMaterialCount w + amnrNormalFieldReserve a ≤ cut)
:
|amnrWord b w (amnrNormalField b f a) z| ≤ amnrNormalOrderConstant N Cb N * amnrNormalFieldAmplitude F Cb H a * amnrWeight S H w
Arbitrary actual words are controlled by canonical primitive jets. Gradient coefficients reserve two weighted units and one material level. This generic conditional lemma proves all commutator bookkeeping explicitly.
theorem
AVenhance.Infra.Section4.amnr_word_abs_le_of_mixed_bounds_and_lower_gradients
{b : AmnrSpace → Homogenization.Vec 2}
{f : AmnrSpace → ℝ}
(hb : ContDiff ℝ (↑⊤) b)
(hf : ContDiff ℝ (↑⊤) f)
{N cut : ℕ}
{S H F Cb : ℝ}
(hS : 0 ≤ S)
(hH : 0 ≤ H)
(hF : 0 ≤ F)
(hCb : 0 ≤ Cb)
(z : AmnrSpace)
(hfb :
∀ (α : List (Fin 2)) (n : ℕ),
α.length + 2 * n ≤ N → n ≤ cut → |amnrWord b (amnrMixedWord α n) f z| ≤ F * amnrWeight S H (amnrMixedWord α n))
(hBb :
∀ (p i : Fin 2) (α : List (Fin 2)),
∀ n < cut,
α.length + 2 * n + 2 ≤ N →
|amnrWord b (amnrMixedWord α n) (amnrVelocityGradient b p i) z| ≤ Cb * H * amnrWeight S H (amnrMixedWord α n))
(w : List (Option (Fin 2)))
(hbudget : amnrBudget w ≤ N)
(hcut : amnrMaterialCount w ≤ cut)
:
Canonical scalar jets and strictly lower velocity-gradient levels give arbitrary scalar words at the identical weighted budget.