Lax Lean Archive

The local realization of generating series of finite Lie rank

lax-825748·registered·created ·GitHub @dc84fb0·Lean v4.33.0 epoch · mathlib db584cd6d46c

Loading review…

Community review

Flags

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

No flags have been submitted.

    Community review

    Flag this submission

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

    Abstract

    A real noncommutative generating series admits a finite-dimensional analytic differential representation if and only if its Lie rank is finite and it satisfies the convergence condition on ordered products of Lie polynomials. The Lie rank is the least representation dimension. Two representations of that dimension are equivalent by an analytic change of coordinates fixing the origin.

    The algebraic foundation consists of shuffle multiplication, the Poincaré–Birkhoff–Witt theorem, and formal coordinates on the annihilator of a finite-codimension Lie subalgebra. The analytic argument uses factorial estimates for iterated vector fields, convergence of residual series, and the analytic inverse function theorem. Convergence is expressed by geometric bounds on commutative power-series coefficients. Both the output and all vector-field coefficients are required to converge.

    The submission includes the real-coefficient algebraic foundation and its proofs, so it has no dependencies on other archive submissions. The source paper records the three approved corrections to the analytic statements and estimates.

    The LaTeX sources of the paper were taken from the heuklyd papers collection.

    View annotated paper

    11 pages · 20 marked passages

    Concepts

    Concept map
    32 concepts
    100%
    Proven claimDefinitionThis submissionA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.

    Proofs

    Proof networkview on GitHub

    100%
    assumptions conclusionProven claimStatement 1, 2, … of a claim with several statementsClaim from this submissionProof — open large view for details
    Proof list

    Lean sources for these proofs: proofs/ on GitHub

    Proof code is not displayed; the archive records each proof's checked relationship between claims.

    Related submissions

    No other submission in the archive builds on this one, and this one builds on none.

    Cite this

    This is only the formalizers. The authors of the formalized results may be different (see References).

    @misc{lax-825748,
  title = {The local realization of generating series of finite Lie rank},
  year = {2026},
  howpublished = {Lax Archive, lax-825748},
  url = {https://laxarchive.org/lax-825748/},
}

    References

    1. Christophe Reutenauer. The local realization of generating series of finite Lie rank. In Algebraic and Geometric Methods in Nonlinear Control Theory 33–43, 1986.
    2. Michel Fliess. Réalisation locale des systèmes non linéaires, algèbres de Lie filtrées transitives et séries génératrices non commutatives. Inventiones Mathematicae 71:521–537, 1983.

    Discussion

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

    Loading discussion…