Documentation

LeanPool.AnomalousDiffusion.AVenhance.Infra.Section4.Amnr.WordOrdering

Finite ordering measures for material/spatial commutator induction.

source
def AVenhance.Infra.Section4.amnrSpatialCount :
List (Option (Fin 2)) → ℕ

Number of spatial letters in an actual derivative word.

Equations
Instances For
    source
    def AVenhance.Infra.Section4.amnrMaterialCount :
    List (Option (Fin 2)) → ℕ

    Number of material letters, tracked separately from the weighted budget.

    Equations
    Instances For
      source
      def AVenhance.Infra.Section4.amnrWordInversions :
      List (Option (Fin 2)) → ℕ

      Number of material letters lying outside a spatial derivative.

      Equations
      Instances For
        source
        theorem AVenhance.Infra.Section4.amnrSpatialCount_append (w v : List (Option (Fin 2))) :
        amnrSpatialCount (w ++ v) = amnrSpatialCount w + amnrSpatialCount v
        source
        theorem AVenhance.Infra.Section4.amnrMaterialCount_append (w v : List (Option (Fin 2))) :
        amnrMaterialCount (w ++ v) = amnrMaterialCount w + amnrMaterialCount v
        source
        theorem AVenhance.Infra.Section4.amnrMaterialCount_eq_count_none (w : List (Option (Fin 2))) :
        amnrMaterialCount w = List.count none w
        source
        theorem AVenhance.Infra.Section4.amnrCounts_length (w : List (Option (Fin 2))) :
        amnrSpatialCount w + amnrMaterialCount w = w.length
        source
        theorem AVenhance.Infra.Section4.amnrCounts_budget (w : List (Option (Fin 2))) :
        amnrSpatialCount w + 2 * amnrMaterialCount w = amnrBudget w
        source
        theorem AVenhance.Infra.Section4.amnrWordInversions_append (w v : List (Option (Fin 2))) :
        amnrWordInversions (w ++ v) = amnrWordInversions w + amnrWordInversions v + amnrMaterialCount w * amnrSpatialCount v

        Concatenation counts precisely the new cross inversions.

        source
        theorem AVenhance.Infra.Section4.amnrWordInversions_swap (u v : List (Option (Fin 2))) (i : Fin 2) :
        amnrWordInversions (u ++ none :: some i :: v) = amnrWordInversions (u ++ some i :: none :: v) + 1

        Swapping an adjacent material/spatial pair removes exactly one inversion.

        source
        theorem AVenhance.Infra.Section4.amnrWordInversions_le_length_sq (w : List (Option (Fin 2))) :
        amnrWordInversions w ≤ w.length ^ 2

        Every inversion measure stays within the square of the weighted budget.

        source
        theorem AVenhance.Infra.Section4.amnrWord_mixed_or_adjacent (w : List (Option (Fin 2))) :
        IsAmnrMixedWord w ∨ ∃ (u : List (Option (Fin 2))) (i : Fin 2) (v : List (Option (Fin 2))), w = u ++ none :: some i :: v

        A word is canonical or admits one adjacent commutator swap.