One quantitative adjacent material/spatial commutator step.

theorem AVenhance.Infra.Section4.amnr_normal_order_adjacent_abs_le_of_lower_bounds {b : AmnrSpace → Homogenization.Vec 2} {f : AmnrSpace → ℝ} (hb : ContDiff ℝ (↑⊤) b) (hf : ContDiff ℝ (↑⊤) f) {N cut q : ℕ} {S H F Cb : ℝ} (hS : 0 ≤ S) (hH : 0 ≤ H) (hF : 0 ≤ F) (hCb : 0 ≤ Cb) (z : AmnrSpace) (a : Option (Fin 2 × Fin 2)) (u v : List (Option (Fin 2))) (i : Fin 2) (hbudget : amnrBudget (u ++ none :: some i :: v) + amnrNormalFieldCost a ≤ q + 1) (hq : q + 1 ≤ N) (hcut : amnrMaterialCount (u ++ none :: some i :: v) + amnrNormalFieldReserve a ≤ cut) (hlower : ∀ (a : Option (Fin 2 × Fin 2)) (w : List (Option (Fin 2))), amnrBudget w + amnrNormalFieldCost a ≤ q → amnrMaterialCount w + amnrNormalFieldReserve a ≤ cut → |amnrWord b w (amnrNormalField b f a) z| ≤ amnrNormalOrderConstant N Cb q * amnrNormalFieldAmplitude F Cb H a * amnrWeight S H w) (hswap : |amnrWord b (u ++ some i :: none :: v) (amnrNormalField b f a) z| ≤ amnrNormalFieldAmplitude F Cb H a * amnrWeight S H (u ++ none :: some i :: v) * amnrNormalOrderSwapFactor N Cb q ^ amnrWordInversions (u ++ some i :: none :: v)) : |amnrWord b (u ++ none :: some i :: v) (amnrNormalField b f a) z| ≤ amnrNormalFieldAmplitude F Cb H a * amnrWeight S H (u ++ none :: some i :: v) * amnrNormalOrderSwapFactor N Cb q ^ amnrWordInversions (u ++ none :: some i :: v)

An adjacent swap is controlled by its ordered term and strictly smaller weighted budgets. This calculus helper retains both finite induction indices.