Lax Lean Archive

Linearly-finite and recognisable series

Lax619925.Recognisable · concepts/Lax619925/Recognisable.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

    A series is linearly finite if it lies in a finitely generated Qℚ-space of series closed under left derivatives; it is recognisable if it is recognised by a linear representation (k,x,y,M)(k, x, y, M), i.e. f(w)=x⋅M(w)⋅yf (w) = x · M(w) · y. The two notions coincide (a classical result). The class of recognisable series is an effective prevariety — equality is decidable by linear algebra — and hence the commutativity problem is decidable for it (paper §4). This is the only chain in the proof network that does not depend on the ideal-membership statement.

    Concept map
    4 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

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

    1 LinearlyFiniteAntiDerivativeClosure proven

    2 LinearlyFiniteClosure proven

    3 RecognisableCommutativityDecidable proven

    4 RecognisableEffectivePrevariety proven

    5 RecognisableEqualityDecidable proven

    6 RecognisableLinearlyFinite proven

    7 RecognisableReversal proven

    8 RecognisableRightDeriv proven

    In the paper

    • page 11 of this submission's paper

    Lean source view on GitHub

    1import Lax619925.Series
    2import Lax619925.Prevariety
    3import Lax619925.Commutativity
    4import Mathlib.Data.Real.Basic
    5import Mathlib.Data.Fin.Basic
    6import Mathlib.Data.Fintype.Basic
    7import Mathlib.Data.Finset.Basic
    8import Mathlib.Data.Matrix.Basic
    9import Mathlib.LinearAlgebra.Span.Basic
    10
    11/-!
    12---
    13title: Linearly-finite and recognisable series
    14type: theorem
    15---
    16A series is *linearly finite* if it lies in a finitely generated `ℚ`-space of
    17series closed under left derivatives; it is *recognisable* if it is recognised by
    18a linear representation `(k, x, y, M)`, i.e. `f (w) = x · M(w) · y`. The two
    19notions coincide (a classical result). The class of recognisable series is an
    20effective prevariety — equality is decidable by linear algebra — and hence the
    21commutativity problem is decidable for it (paper §4). This is the only chain in
    22the proof network that does not depend on the ideal-membership statement.
    23-/
    24
    25namespace Lax619925.Recognisable
    26
    27open Lax619925.Series Lax619925.Prevariety Lax619925.Commutativity
    28
    29/-- A linear representation over `α`: a dimension `k`, a row vector `init` of
    30 initial weights, a column vector `final` of final weights, and a transition
    31 function `M` assigning to each letter a `k × k` matrix. The transition function
    32 extends homomorphically to words by `M(ε) = 1` and `M(a·w) = M(a) · M(w)` (the
    33 definition `Mword`), and the series recognised is `f (w) = x · M(w) · y` (the
    34 definition `sem`). Both are computed from the four core fields. -/
    35structure LinearRepresentation (α : Type*) where
    36 dim : ℕ
    37 init : Fin dim → ℚ
    38 final : Fin dim → ℚ
    39 M : α → Matrix (Fin dim) (Fin dim) ℚ
    40
    41/-- The word product `M(w)`: `M(ε) = 1` and `M(a·w) = M(a) · M(w)`, the transition
    42 matrices composed right-to-left along the word. -/
    43def LinearRepresentation.Mword {α : Type*} (r : LinearRepresentation α) (w : List α) :
    44 Matrix (Fin r.dim) (Fin r.dim) ℚ :=
    45 w.foldr (fun a A => r.M a * A) 1
    46
    47/-- The series recognised by the representation: `f (w) = x · M(w) · y`, the dot
    48 product of the initial vector with the word product applied to the final vector. -/
    49def LinearRepresentation.sem {α : Type*} (r : LinearRepresentation α) (w : List α) : ℚ :=
    50 dotProduct r.init (Matrix.mulVec (r.Mword w) r.final)
    51
    52/-- A series is *recognisable* if it is recognised by some linear representation. -/
    53def IsRecognisable (α : Type*) (f : Series α) : Prop :=
    54 ∃ r : LinearRepresentation α, r.sem = f
    55
    56/-- A series is *linearly finite* if it belongs to a finitely generated `ℚ`-space of
    57 series (the span of a finite set of generators `G`) that is closed under left
    58 derivatives: `f ∈ span G` and `leftDeriv a g ∈ span G` for all `a` and `g ∈ G`. -/
    59def IsLinearlyFinite (α : Type*) (f : Series α) : Prop :=
    60 ∃ G : Finset (Series α), f ∈ Submodule.span ℚ G ∧ ∀ a, ∀ g ∈ G, leftDeriv α a g ∈ Submodule.span ℚ G
    61
    62/-- A series is recognisable if and only if it is linearly finite
    63 (paper §4, the classical coincidence lemma). -/
    64axiom RecognisableLinearlyFinite (α : Type*) (f : Series α) :
    65 IsRecognisable α f ↔ IsLinearlyFinite α f
    66
    67/-- The class of linearly finite series is closed under scalar product, addition,
    68 and left derivatives (paper §4, lemma `recognisable closure properties`). The
    69 closure is effective: each operation is witnessed by an explicit finite set of
    70 generators. These three parts hold over any alphabet. -/
    71axiom LinearlyFiniteClosure (α : Type*) :
    72 (∀ (f g : Series α), IsLinearlyFinite α f → IsLinearlyFinite α g → IsLinearlyFinite α (f + g)) ∧
    73 (∀ (c : ℚ) (f : Series α), IsLinearlyFinite α f → IsLinearlyFinite α (c • f)) ∧
    74 (∀ (a : α) (f : Series α), IsLinearlyFinite α f → IsLinearlyFinite α (leftDeriv α a f))
    75
    76/-- The class of linearly finite series over a *finite* alphabet is closed under left
    77 anti-derivatives (paper §4, lemma `recognisable closure properties`): if `g` is a
    78 left anti-derivative of a tuple `f` of linearly finite series, then `g` is linearly
    79 finite. The finiteness of the alphabet is essential — the witnessing generator set
    80 is `{g} ∪ ⋃ₐ Gₐ`, one finite set `Gₐ` per letter, so it is finite only when the
    81 alphabet is. -/
    82axiom LinearlyFiniteAntiDerivativeClosure (α : Type*) [Fintype α] :
    83 ∀ (g : Series α) (f : α → Series α), IsLeftAntiDerivative α g f →
    84 (∀ a, IsLinearlyFinite α (f a)) → IsLinearlyFinite α g
    85
    86/-- If `f` is recognisable, then its reversal is recognisable (paper §4): the
    87 transposed representation `(k, yᵀ, xᵀ, Mᵀ)` recognises `reversal f`. -/
    88axiom RecognisableReversal (α : Type*) (f : Series α) (hf : IsRecognisable α f) :
    89 IsRecognisable α (reversal α f)
    90
    91/-- If `f` is recognisable, then its right derivative is recognisable
    92 (paper §4, corollary `recognisable derive right`), by double reversal:
    93 `rightDeriv a f = reversal (leftDeriv a (reversal f))`. -/
    94axiom RecognisableRightDeriv (α : Type*) (a : α) (f : Series α) (hf : IsRecognisable α f) :
    95 IsRecognisable α (rightDeriv α a f)
    96
    97/-- The equality (zeroness) problem is decidable for recognisable series over a finite
    98 alphabet (paper §4): there is a procedure that, given a linear representation,
    99 decides whether the series it recognises is the zero series. It checks, by linear
    100 algebra, that the initial vector annihilates the subspace reachable from the final
    101 vector. This is condition (3) in the definition of effective prevariety. -/
    102axiom RecognisableEqualityDecidable (α : Type*) [Fintype α] :
    103 ∃ d : LinearRepresentation α → Bool, ∀ r, d r = true ↔ r.sem = 0
    104
    105/-- The class of recognisable (= linearly finite) series is an effective prevariety
    106 (paper §4, theorem): there is an effective prevariety whose image is exactly the
    107 recognisable series, with presentations given by linear representations. -/
    108axiom RecognisableEffectivePrevariety (α : Type*) [Fintype α] :
    109 ∃ P : EffectivePrevariety α, ∀ f, IsRecognisable α f ↔ ∃ r : P.Rep, P.sem r = f
    110
    111/-- In particular, the commutativity problem is decidable for recognisable series over
    112 a finite alphabet (paper §4): there is a procedure that, given a linear
    113 representation, decides whether the series it recognises is commutative. This is
    114 the meta-theorem applied to the effective prevariety of recognisable series. -/
    115axiom RecognisableCommutativityDecidable (α : Type*) [Fintype α] :
    116 ∃ d : LinearRepresentation α → Bool, ∀ r, d r = true ↔ IsCommutative α (r.sem)
    117
    118end Lax619925.Recognisable
    119
    Show ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow Proof
    Builds on
    Used by

    none

    From Mathlib

    Discussion

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

    Loading discussion…