Lax Lean Archive

The commutativity problem

Lax619925.Commutativity · concepts/Lax619925/Commutativity.lean · lax-619925

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    The commutativity problem asks whether a series is commutative, i.e. constant on words with the same Parikh image. The key observation (paper §3) is that commutativity is characterised by two finite families of equations, swap and rotate, which makes it decidable for effective prevarieties (the meta-theorem). Conversely, the zeroness problem reduces to commutativity: given ff, one builds a series gg over a two-letter-enlarged alphabet, supported on words beginning with the two fresh letters, such that gg is commutative exactly when f=0f = 0.

    Concept map
    3 concepts; 7 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 3 statements. Each proof establishes one of them relative to its assumptions.

    1 AntiDerivativeCommutativeIffZero proven

    2 EffectivePrevarietyCommutativityDecidable proven

    3 FiniteAxiomatisation proven

    In the paper

    • page 9 of this submission's paper

    Lean source view on GitHub

    1import Lax619925.Series
    2import Lax619925.Prevariety
    3import Mathlib.Data.Real.Basic
    4import Mathlib.Data.Fintype.Basic
    5
    6/-!
    7---
    8title: The commutativity problem
    9type: theorem
    10---
    11The commutativity problem asks whether a series is commutative, i.e. constant on
    12words with the same Parikh image. The key observation (paper §3) is that
    13commutativity is characterised by two finite families of equations, *swap* and
    14*rotate*, which makes it decidable for effective prevarieties (the meta-theorem).
    15Conversely, the zeroness problem reduces to commutativity: given `f`, one builds
    16a series `g` over a two-letter-enlarged alphabet, supported on words beginning
    17with the two fresh letters, such that `g` is commutative exactly when `f = 0`.
    18-/
    19
    20namespace Lax619925.Commutativity
    21
    22open Lax619925.Series Lax619925.Prevariety
    23
    24/-- The *swap* equation: for all letters `a, b`,
    25 `leftDeriv a (leftDeriv b f) = leftDeriv b (leftDeriv a f)`.
    26 It expresses that exchanging the first two letters of a word does not change
    27 the coefficient. -/
    28def SatisfiesSwap (α : Type*) (f : Series α) : Prop :=
    29 ∀ a b, leftDeriv α a (leftDeriv α b f) = leftDeriv α b (leftDeriv α a f)
    30
    31/-- The *rotate* equation: for all letters `a`,
    32 `leftDeriv a f = rightDeriv a f`.
    33 It expresses that moving the first letter to the end does not change the
    34 coefficient. -/
    35def SatisfiesRotate (α : Type*) (f : Series α) : Prop :=
    36 ∀ a, leftDeriv α a f = rightDeriv α a f
    37
    38/-- A series `g` is a *left anti-derivative* of the tuple of series `f` if
    39 `leftDeriv a g = f a` for every letter `a`. Once the value `g ε` is fixed,
    40 left anti-derivatives are unique. -/
    41def IsLeftAntiDerivative (α : Type*) (g : Series α) (f : α → Series α) : Prop :=
    42 ∀ a, leftDeriv α a g = f a
    43
    44/-- The alphabet `α` extended by two fresh letters `fresh0` and `fresh1`, modelling
    45 the paper's enlarged alphabet `Γ = Σ ∪ {a, b}`. -/
    46inductive Fresh2 (α : Type*) where
    47 | letter : α → Fresh2 α
    48 | fresh0 : Fresh2 α
    49 | fresh1 : Fresh2 α
    50
    51/-- Lift a word over the extended alphabet back to a word over `α`, returning
    52 `some` of the original word when no fresh letter occurs and `none` otherwise. -/
    53def liftWordOpt (α : Type*) (w : List (Fresh2 α)) : Option (List α) :=
    54 match w with
    55 | [] => some []
    56 | s :: w' =>
    57 match s with
    58 | .letter a => (liftWordOpt α w').map (fun rest => a :: rest)
    59 | .fresh0 | .fresh1 => none
    60
    61/-- The extension of a series over `α` to the extended alphabet `Fresh2 α`, by zero
    62 on words containing one of the two fresh letters. -/
    63def extendSeries (α : Type*) (f : Series α) : Series (Fresh2 α) := fun w =>
    64 match liftWordOpt α w with
    65 | some rest => f rest
    66 | none => 0
    67
    68/-- The series `g` over the extended alphabet associated to `f` in the paper's
    69 equality-reduces-to-commutativity construction: `g` is zero except on words
    70 beginning with the two fresh letters, where `g (fresh0 :: fresh1 :: rest) = f (rest)`
    71 (with `f` extended by zero). Hence `leftDeriv b (leftDeriv a g) = extendSeries f`
    72 for `a = fresh0`, `b = fresh1`, while every other second left derivative vanishes;
    73 in particular `g ε = g x = 0` for every letter `x`. -/
    74def antiDerivativeSeries (α : Type*) (f : Series α) : Series (Fresh2 α) := fun w =>
    75 match w with
    76 | .fresh0 :: .fresh1 :: rest => extendSeries α f rest
    77 | _ => 0
    78
    79/-- A series is commutative if and only if it satisfies the swap and rotate equations
    80 for all letters (paper §3, lemma `commutativity`). Swaps and rotations generate
    81 all commutatively equivalent words, so the two finite families of equations
    82 characterise commutativity. -/
    83axiom FiniteAxiomatisation (α : Type*) (f : Series α) :
    84 IsCommutative α f ↔ SatisfiesSwap α f ∧ SatisfiesRotate α f
    85
    86/-- The commutativity problem is decidable for effective prevarieties of series
    87 (paper §3, theorem `commutativity for effective prevarieties`): over a finite
    88 alphabet, there is a procedure that, given a presentation `r`, decides whether
    89 `sem r` is commutative — it returns `true` exactly when `sem r` is commutative.
    90 By the finite axiomatisation this reduces to finitely many equality tests on
    91 presentations, decided by the prevariety's `decEq`. -/
    92axiom EffectivePrevarietyCommutativityDecidable (α : Type*) [Fintype α]
    93 (P : EffectivePrevariety α) :
    94 ∃ d : P.Rep → Bool, ∀ r, d r = true ↔ IsCommutative α (P.sem r)
    95
    96/-- The series `antiDerivativeSeries f` is commutative if and only if `f = 0`
    97 (paper §3, lemma `equality reduces to commutativity`). If `f ≠ 0` with
    98 `f (w) ≠ 0` for some word `w`, then `g (fresh0 · fresh1 · w) = f (w) ≠ 0` while
    99 `g (fresh1 · fresh0 · w) = 0`, and the two words are commutatively equivalent,
    100 so `g` is not commutative; conversely `f = 0` forces `g = 0`. -/
    101axiom AntiDerivativeCommutativeIffZero (α : Type*) (f : Series α) :
    102 IsCommutative (Fresh2 α) (antiDerivativeSeries α f) ↔ f = 0
    103
    104end Lax619925.Commutativity
    105
    Show ProofShow ProofShow Proof
    Builds on
    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…