Lax Lean Archive

Multivariate polynomial recursive sequences

Lax619925.Polyrec · concepts/Lax619925/Polyrec.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 multivariate polynomial recursive sequence (polyrec sequence) in dd variables is a kk-tuple of sequences f:Nd→Qf : ℕ^d → ℚ satisfying polynomial equations shiftjfi=pi(j)(f1,…,fk)shift_j f_i = p^{(j)}_i(f_1, …, f_k) (paper §5.4), where shiftjshift_j is the shift in the jj-th coordinate and pi(j)p^{(j)}_i are polynomials evaluated pointwise in the sequences. The consistency problem asks whether, given the equations and an initial condition fi(0)=cif_i(0) = c_i, a solution exists. This is decidable (paper §5.4, theorem polyrecconsistencypolyrec consistency): the polyrec system is isomorphic to a Hadamard system over the dd-letter alphabet, so a solution exists exactly when the companion Hadamard series are commutative, which is decidable.

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

    Each proof establishes this claim relative to its assumptions.

    In the paper

    • page 18 of this submission's paper

    Lean source view on GitHub

    1import Lax619925.Series
    2import Lax619925.Hadamard
    3import Mathlib.Data.Real.Basic
    4import Mathlib.Data.Fin.Basic
    5import Mathlib.Data.Fintype.Basic
    6import Mathlib.Data.Finset.Basic
    7import Mathlib.Algebra.MvPolynomial.Basic
    8
    9/-!
    10---
    11title: Multivariate polynomial recursive sequences
    12type: theorem
    13---
    14A *multivariate polynomial recursive sequence* (polyrec sequence) in `d` variables
    15is a `k`-tuple of sequences `f : ℕ^d → ℚ` satisfying polynomial equations
    16`shift_j f_i = p^{(j)}_i(f_1, …, f_k)` (paper §5.4), where `shift_j` is the shift
    17in the `j`-th coordinate and `p^{(j)}_i` are polynomials evaluated pointwise in the
    18sequences. The *consistency problem* asks whether, given the equations and an
    19initial condition `f_i(0) = c_i`, a solution exists. This is decidable (paper
    20§5.4, theorem `polyrec consistency`): the polyrec system is isomorphic to a
    21Hadamard system over the `d`-letter alphabet, so a solution exists exactly when
    22the companion Hadamard series are commutative, which is decidable.
    23-/
    24
    25namespace Lax619925.Polyrec
    26
    27open Lax619925.Series Lax619925.Hadamard
    28
    29/-- A multivariate sequence in `d` variables: a function `ℕ^d → ℚ`, represented
    30 as a function on the multi-index type `Fin d → ℕ`. -/
    31abbrev Seq (d : ℕ) := (Fin d → ℕ) → ℚ
    32
    33/-- The shift of a multivariate sequence in the `j`-th coordinate:
    34 `(shift d j f) n = f (n + e_j)`, where `e_j` is the `j`-th unit vector.
    35 The shifts in different coordinates commute. -/
    36def shift (d : ℕ) (j : Fin d) (f : Seq d) : Seq d :=
    37 fun n => f (fun i => n i + if i = j then 1 else 0)
    38
    39/-- The pointwise (Hadamard-algebra) evaluation of the polynomial `p` at the tuple
    40 of sequences `fs`: `evalSeq d k fs p n = Σ_m p.coeff m · ∏_i (fs i n)^{m i}`,
    41 the interpretation of `p` in the pointwise ring of sequences, where the
    42 variable `X_i` is mapped to `fs i` and the multiplication is pointwise. -/
    43def evalSeq (d k : ℕ) (fs : Fin k → Seq d) (p : MvPolynomial (Fin k) ℚ) : Seq d :=
    44 fun n => p.support.sum fun m => p.coeff m * ∏ i : Fin k, (fs i) n ^ (m i)
    45
    46/-- A `k`-tuple of multivariate sequences `f` *solves* the polyrec system
    47 `(p, c)` if it satisfies the initial condition `f_i(0) = c_i` and the
    48 polynomial equations `shift_j f_i = p^{(j)}_i(f_1, …, f_k)` for all `i, j`,
    49 where `p^{(j)}_i` is evaluated pointwise in the sequences (the Hadamard
    50 algebra). Here `0` is the zero multi-index, the origin of `ℕ^d`. -/
    51def SolvesPolyrec (d k : ℕ) (f : Fin k → Seq d)
    52 (p : Fin k → Fin d → MvPolynomial (Fin k) ℚ) (c : Fin k → ℚ) : Prop :=
    53 (∀ i, f i 0 = c i) ∧ ∀ i j, shift d j (f i) = evalSeq d k f (p i j)
    54
    55/-- The polyrec consistency problem is decidable (paper §5.4, theorem
    56 `polyrec consistency`): there is a procedure that, given the polynomial
    57 equations `p` and the initial condition `c`, decides whether a solution
    58 exists. The decision reduces to the commutativity of the companion Hadamard
    59 series, which is decidable. -/
    60axiom PolyrecConsistency (d k : ℕ) (hd : 0 < d) (hk : 0 < k) :
    61 ∃ dec : (Fin k → Fin d → MvPolynomial (Fin k) ℚ) → (Fin k → ℚ) → Bool,
    62 ∀ p c, dec p c = true ↔ ∃ f : Fin k → Seq d, SolvesPolyrec d k f p c
    63
    64end Lax619925.Polyrec
    65
    Show 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…