Finite constants for quantitative ordering of material/spatial words.

def AVenhance.Infra.Section4.amnrNormalOrderConstant (N : ℕ) (Cb : ℝ) : ℕ → ℝ

Constants are indexed by the weighted total budget. Each commutator product involves two strictly smaller budgets.

Equations

• One or more equations did not get rendered due to their size.
• AVenhance.Infra.Section4.amnrNormalOrderConstant N Cb 0 = 1

def AVenhance.Infra.Section4.amnrNormalOrderSwapFactor (N : ℕ) (Cb : ℝ) (q : ℕ) : ℝ

The per-swap factor at a positive weighted budget.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.Section4.amnrNormalOrderConstant_one_le {N : ℕ} {Cb : ℝ} (hCb : 0 ≤ Cb) (q : ℕ) : 1 ≤ amnrNormalOrderConstant N Cb q

theorem AVenhance.Infra.Section4.amnrNormalOrderSwapFactor_one_le {N : ℕ} {Cb : ℝ} (hCb : 0 ≤ Cb) (q : ℕ) : 1 ≤ amnrNormalOrderSwapFactor N Cb q

theorem AVenhance.Infra.Section4.amnrNormalOrderSwapFactor_pow_le {N q : ℕ} {Cb : ℝ} (hCb : 0 ≤ Cb) (w : List (Option (Fin 2))) (hw : w.length ≤ N) : amnrNormalOrderSwapFactor N Cb q ^ amnrWordInversions w ≤ amnrNormalOrderConstant N Cb (q + 1)

The finite inversion count is absorbed at its current weighted level.

theorem AVenhance.Infra.Section4.amnrNormalOrderSwapFactor_absorb {N q : ℕ} {Cb : ℝ} (hCb : 0 ≤ Cb) (r : ℕ) : amnrNormalOrderSwapFactor N Cb q ^ r + 2 ^ (N + 1) * Cb * amnrNormalOrderConstant N Cb q ^ 2 ≤ amnrNormalOrderSwapFactor N Cb q ^ (r + 1)

One swapped word and its commutator correction fit the next inversion power.