Formal calculus for vertex algebras, sorry-free library with

Stream: maths

[Justin McClung]

Hi. I've formalized Chapter 1 (Formal Calculus) of Nozaradan's Introduction to Vertex Algebras in Lean 4. It's complete and sorry-free.

https://github.com/JustinMcClung/formal-distribution

About 3,850 lines across 11 files. Covers formal distributions, expansion operators, formal delta (all properties from Prop 1.3.5), decomposition theorem, locality with j-th products, and Fourier transform / lambda-brackets.

Design choices worth noting:

• Two structure types (FormalDistribution / GeneralizedFormalDistribution) for finite vs bounded-finite support so delta lives in the right type without axioms.
• Locality, delta, decomposition, j-th products all parameterized over arbitrary variable pairs (i, j) in n-variable distributions. Standard 2-variable API recovered via abbrev aliases.
• HahnSeries bridge gives a CommRing instance for 1D distributions via Function.Injective.commRing, connecting to Mathlib.Algebra.Vertex.VertexOperator.

I'm continuing to formalize the next chapters and have two questions:

1. Are there pieces worth upstreaming into Mathlib? Happy to prepare PRs starting small.
2. Anything in the design that would create friction with the existing vertex algebra development? I'd rather fix it now than after another 4,000 lines.

Thanks.

[Weiyi Wang]

I have little knowledge in this area aside from the name, but I noticed there is #25822 floating around. Maybe Scott Carnahan can chime in? (I was notified he did provide input. Sorry for the unnecessary ping!)

[Kevin Buzzard]

Out of interest -- were LLMs used at all in this work? The current conventions of this community are that when they are, this should be clearly highlighted.