Lax Lean Archive

Infiltration automata and infiltration-finite series

Lax619925.Infiltration · concepts/Lax619925/Infiltration.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 infiltration-finite if it belongs to a finitely generated differential infiltration algebra (paper §7): it is an infiltration polynomial in a finite tuple of series that is closed under left derivatives. Equivalently (the coincidence), it is recognised by an infiltration automaton (k,F,Δ)(k, F, Δ): a configuration space Q[X1,…,Xk]ℚ[X_1, …, X_k], a final-weight functional FF, and a transition ΔaΔ_a that extends to an infiltration of the configuration space (the paper's infiltration-algebra structure, §7). By the fundamental relationship an infiltration ΔΔ is S−idS − id for the endomorphism S=id+ΔS = id + Δ, so the extension is computed by substituting Xi↦Xi+ΔaXiX_i ↦ X_i + Δ_a X_i and subtracting the identity. The infiltration-finite series form an effective prevariety, so equality and the commutativity problem are decidable for them; the equality decision reduces to ideal membership in the configuration polynomial ring (the ideal-membership statement), via the same ideal-chain argument as for the Hadamard and shuffle automata.

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

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

    1 InfiltrationAntiDerivativeClosure proven

    2 InfiltrationClosure proven

    3 InfiltrationCoincidence proven

    4 InfiltrationCommutativityDecidable proven

    5 InfiltrationEffectivePrevariety proven

    6 InfiltrationEqualityDecidable proven

    In the paper

    • page 34 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.Finsupp.Basic
    9import Mathlib.Algebra.MvPolynomial.Basic
    10import Mathlib.Algebra.MvPolynomial.Eval
    11
    12/-!
    13---
    14title: Infiltration automata and infiltration-finite series
    15type: theorem
    16---
    17A series is *infiltration-finite* if it belongs to a finitely generated
    18differential infiltration algebra (paper §7): it is an infiltration polynomial in
    19a finite tuple of series that is closed under left derivatives. Equivalently (the
    20coincidence), it is recognised by an *infiltration automaton* `(k, F, Δ)`: a
    21configuration space `ℚ[X_1, …, X_k]`, a final-weight functional `F`, and a
    22transition `Δ_a` that extends to an *infiltration* of the configuration space
    23(the paper's infiltration-algebra structure, §7). By the fundamental relationship
    24an infiltration `Δ` is `S − id` for the endomorphism `S = id + Δ`, so the extension
    25is computed by substituting `X_i ↦ X_i + Δ_a X_i` and subtracting the identity.
    26The infiltration-finite series form an effective prevariety, so equality and the
    27commutativity problem are decidable for them; the equality decision reduces to
    28ideal membership in the configuration polynomial ring (the ideal-membership
    29statement), via the same ideal-chain argument as for the Hadamard and shuffle
    30automata.
    31-/
    32
    33namespace Lax619925.Infiltration
    34
    35open Lax619925.Series Lax619925.Prevariety Lax619925.Commutativity
    36
    37/-- The recursive core of the infiltration product, defined by primitive recursion on
    38 the word: `(f ↑ g) ε = f ε · g ε` and
    39 `(f ↑ g) (a·w) = ((leftDeriv a f) ↑ g) w + (f ↑ (leftDeriv a g)) w
    40 + ((leftDeriv a f) ↑ (leftDeriv a g)) w`. The recursion measure is the word
    41 length (the series arguments change at each step). -/
    42noncomputable def infiltrationRec (α : Type*) (f g : Series α) (w : List α) : ℚ :=
    43 match w with
    44 | [] => f [] * g []
    45 | a :: w' => infiltrationRec α (leftDeriv α a f) g w'
    46 + infiltrationRec α f (leftDeriv α a g) w'
    47 + infiltrationRec α (leftDeriv α a f) (leftDeriv α a g) w'
    48 termination_by w.length
    49
    50/-- The infiltration product of two series, characterised by the base case
    51 `(f ↑ g) ε = f ε · g ε` and the step rule
    52 `leftDeriv a (f ↑ g) = (leftDeriv a f) ↑ g + f ↑ (leftDeriv a g)
    53 + (leftDeriv a f) ↑ (leftDeriv a g)`. It is the synchronising-interleaving
    54 analogue of the shuffle product (the extra last term allows the two series to
    55 consume the letter jointly). -/
    56noncomputable def infiltration (α : Type*) (f g : Series α) : Series α :=
    57 fun w => infiltrationRec α f g w
    58
    59/-- The unit of the infiltration product: the delta series, `1` on the empty word and
    60 `0` elsewhere. Unlike the constant-`1` series (the unit of the pointwise product),
    61 the delta series is the unit of the *infiltration* product. -/
    62def infiltrationUnit (α : Type*) : Series α := fun w => if w = [] then 1 else 0
    63
    64/-- The `n`-fold iterated infiltration power of `f`: `infiltrationPow α f 0 =
    65 infiltrationUnit α` (the infiltration unit) and `infiltrationPow α f (n+1) = f ↑
    66 infiltrationPow α f n`. This is the infiltration analogue of the pointwise power
    67 `f ^ n` used in `hadamardEval`. -/
    68noncomputable def infiltrationPow (α : Type*) (f : Series α) (n : ℕ) : Series α :=
    69 match n with
    70 | 0 => infiltrationUnit α
    71 | n + 1 => infiltration α f (infiltrationPow α f n)
    72
    73/-- The infiltration product of the iterated infiltration powers
    74 `fs 0 ↑^[d 0] ⋯ fs (k-1) ↑^[d (k-1)]`, where `↑` is the infiltration product and
    75 `↑^[n]` is the iterated infiltration power (`infiltrationPow`). This is the
    76 infiltration analogue of the pointwise monomial product `∏ i, (fs i) ^ (d i)` used in
    77 `hadamardEval`; it is the infiltration fold of the commutative-associative infiltration
    78 operation over all indices (the zero-exponent terms contribute the infiltration unit,
    79 which is the identity). It is computed as a right-fold over the index list, so that
    80 the definition does not depend on the `Std.Commutative`/`Std.Associative` instances
    81 (which the axiom-free concept package cannot carry); the proof package shows it equals
    82 the corresponding `Finset.fold` (`infiltrationProd_eq_fold`). -/
    83noncomputable def infiltrationProd (α : Type*) (k : ℕ) (fs : Fin k → Series α) (d : Fin k →₀ ℕ) : Series α :=
    84 (((Finset.univ : Finset (Fin k)).toList).map (fun i => infiltrationPow α (fs i) (d i))).foldr
    85 (fun x acc => infiltration α x acc) (infiltrationUnit α)
    86
    87/-- The evaluation of the polynomial `p` in the *infiltration* algebra, sending `X_i` to
    88 `fs i`: `infiltrationEval α k fs p = ∑ d ∈ p.support, p.coeff d · (fs 0 ↑^[d 0] ⋯
    89 fs (k-1) ↑^[d (k-1)])`, where `↑` is the infiltration product and `↑^[n]` is the
    90 iterated infiltration power. This is the infiltration analogue of `hadamardEval`
    91 (which evaluates in the pointwise ring); because the infiltration ring cannot be a
    92 `CommRing` instance on `Series α` (which already carries the pointwise ring), it is
    93 defined directly as the sum over the polynomial's support of the coefficients times
    94 the infiltration product of the iterated powers. -/
    95noncomputable def infiltrationEval (α : Type*) (k : ℕ) (fs : Fin k → Series α)
    96 (p : MvPolynomial (Fin k) ℚ) : Series α :=
    97 p.support.sum fun m => p.coeff m • infiltrationProd α k fs m
    98
    99/-- An *infiltration automaton* over `α`: a dimension `k ≥ 1` (the number of
    100 nonterminals `X_1, …, X_k`), a final-weight functional `F`, and a transition
    101 `Δ` assigning to each letter `a` and nonterminal `X_i` a polynomial `Δ a i` in
    102 the nonterminals. The configuration space is the polynomial ring
    103 `ℚ[X_1, …, X_k] = MvPolynomial (Fin k) ℚ`. -/
    104structure InfiltrationAutomaton (α : Type*) where
    105 dim : ℕ
    106 hdim : 0 < dim
    107 F : Fin dim → ℚ
    108 Δ : α → Fin dim → MvPolynomial (Fin dim) ℚ
    109
    110/-- The word extension of the transition: `Δ_w` is the map of the configuration
    111 space obtained by composing the letter infiltrations along the word,
    112 right-to-left. Each letter infiltration `Δ_a` is `S_a − id`, where `S_a` is
    113 the endomorphism substituting `X_i ↦ X_i + Δ_a X_i` (the fundamental
    114 relationship). The composition law is unchanged from the Hadamard case:
    115 `Δ_ε` is the identity and `Δ_{a·w} = Δ_w ∘ Δ_a`. -/
    116noncomputable def InfiltrationAutomaton.Mword {α : Type*} (A : InfiltrationAutomaton α)
    117 (w : List α) : MvPolynomial (Fin A.dim) ℚ → MvPolynomial (Fin A.dim) ℚ :=
    118 w.foldr (fun a φ => fun β =>
    119 φ (MvPolynomial.aeval (fun i => MvPolynomial.X i + A.Δ a i) β - β)) id
    120
    121/-- The series recognised by the automaton at a configuration `cfg`:
    122 `⟦A⟧_cfg (w) = F(Δ_w cfg)`, the final-weight functional applied to the
    123 configuration reached after reading `w`. -/
    124noncomputable def InfiltrationAutomaton.sem {α : Type*} (A : InfiltrationAutomaton α)
    125 (cfg : MvPolynomial (Fin A.dim) ℚ) : Series α :=
    126 fun w => MvPolynomial.eval (fun i => A.F i) (A.Mword w cfg)
    127
    128/-- The series recognised by the automaton: the semantics at the initial
    129 configuration `X_0` (the first nonterminal). -/
    130noncomputable def InfiltrationAutomaton.recognised {α : Type*}
    131 (A : InfiltrationAutomaton α) : Series α :=
    132 A.sem (MvPolynomial.X (Fin.mk 0 A.hdim))
    133
    134/-- A series is *infiltration-finite* (working definition, paper §7) if it belongs to a
    135 finitely generated differential infiltration algebra: it is an infiltration polynomial
    136 in a finite tuple of series `fs` that is closed under left derivatives, i.e.
    137 `f = infiltrationEval k fs p` for some polynomial `p`, and `leftDeriv a (fs i)` is
    138 again an infiltration polynomial in `fs` for every letter `a` and index `i`. Here
    139 `infiltrationEval k fs` is the evaluation in the infiltration algebra generated by
    140 `fs`. -/
    141def IsInfiltrationFinite (α : Type*) (f : Series α) : Prop :=
    142 ∃ k : ℕ, ∃ fs : Fin k → Series α, ∃ p : MvPolynomial (Fin k) ℚ,
    143 f = infiltrationEval α k fs p ∧
    144 ∀ a : α, ∀ i : Fin k, ∃ q : MvPolynomial (Fin k) ℚ,
    145 leftDeriv α a (fs i) = infiltrationEval α k fs q
    146
    147/-- A series is *infiltration-recognisable* if it is recognised by some infiltration
    148 automaton. -/
    149def IsInfiltrationRecognisable (α : Type*) (f : Series α) : Prop :=
    150 ∃ A : InfiltrationAutomaton α, A.recognised = f
    151
    152/-- A series is infiltration-finite if and only if it is infiltration-recognisable
    153 (paper §7, the coincidence lemma): the finitely generated differential infiltration
    154 algebras are exactly the languages of infiltration automata. -/
    155axiom InfiltrationCoincidence (α : Type*) (f : Series α) :
    156 IsInfiltrationFinite α f ↔ IsInfiltrationRecognisable α f
    157
    158/-- The class of infiltration-finite series is closed under addition, scalar
    159 multiplication, the infiltration product, and right derivatives (paper §7, the
    160 closure lemma). These four parts hold over any alphabet. -/
    161axiom InfiltrationClosure (α : Type*) :
    162 (∀ (f g : Series α), IsInfiltrationFinite α f → IsInfiltrationFinite α g → IsInfiltrationFinite α (f + g)) ∧
    163 (∀ (c : ℚ) (f : Series α), IsInfiltrationFinite α f → IsInfiltrationFinite α (c • f)) ∧
    164 (∀ (f g : Series α), IsInfiltrationFinite α f → IsInfiltrationFinite α g → IsInfiltrationFinite α (infiltration α f g)) ∧
    165 (∀ (a : α) (f : Series α), IsInfiltrationFinite α f → IsInfiltrationFinite α (rightDeriv α a f))
    166
    167/-- The class of infiltration-finite series over a *finite* alphabet is closed under
    168 left anti-derivatives (paper §7): if `g` is a left anti-derivative of a tuple
    169 `f` of infiltration-finite series, then `g` is infiltration-finite. The
    170 finiteness of the alphabet is essential — the witnessing generator set is
    171 extended by one series per letter, so it is finite only when the alphabet is. -/
    172axiom InfiltrationAntiDerivativeClosure (α : Type*) [Fintype α] :
    173 ∀ (g : Series α) (f : α → Series α), IsLeftAntiDerivative α g f →
    174 (∀ a, IsInfiltrationFinite α (f a)) → IsInfiltrationFinite α g
    175
    176/-- The class of infiltration-finite series is an effective prevariety over a finite
    177 alphabet (paper §7, theorem): there is an effective prevariety whose image is
    178 exactly the infiltration-finite series, with presentations given by infiltration
    179 automata. -/
    180axiom InfiltrationEffectivePrevariety (α : Type*) [Fintype α] :
    181 ∃ P : EffectivePrevariety α, ∀ f, IsInfiltrationFinite α f ↔ ∃ r : P.Rep, P.sem r = f
    182
    183/-- The equality (zeroness) problem is decidable for infiltration automata over a
    184 finite alphabet (paper §7): there is a procedure that, given an infiltration
    185 automaton, decides whether the series it recognises is the zero series. The
    186 decision reduces to ideal membership in the configuration polynomial ring, the
    187 ideal-membership statement. -/
    188axiom InfiltrationEqualityDecidable (α : Type*) [Fintype α] :
    189 ∃ d : InfiltrationAutomaton α → Bool, ∀ A, d A = true ↔ A.recognised = 0
    190
    191/-- In particular, the commutativity problem is decidable for infiltration-finite
    192 series over a finite alphabet (paper §7): there is a procedure that, given an
    193 infiltration automaton, decides whether the series it recognises is commutative.
    194 This is the meta-theorem applied to the effective prevariety of
    195 infiltration-finite series. -/
    196axiom InfiltrationCommutativityDecidable (α : Type*) [Fintype α] :
    197 ∃ d : InfiltrationAutomaton α → Bool, ∀ A, d A = true ↔ IsCommutative α (A.recognised)
    198
    199end Lax619925.Infiltration
    200
    Show 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…