One quantitative adjacent material/spatial commutator step.
theorem
AVenhance.Infra.Section4.amnr_normal_order_adjacent_abs_le_of_finite_lower_bounds
{b : AmnrSpace → Homogenization.Vec 2}
{f : AmnrSpace → ℝ}
{N cut q : ℕ}
(hb : ContDiff ℝ (↑⊤) b)
(hf : ContDiff ℝ (↑N) f)
{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))
:
An adjacent swap is controlled by its ordered term and strictly smaller weighted budgets. This calculus helper retains both finite induction indices.