Feynman diagrams

Stream: Natural sciences

[Joseph Tooby-Smith]

I am interested in starting a project, as part of HepLean (https://github.com/HEPLean/HepLean), towards the formalisation of Feynman diagrams.

Feynman diagrams are a graph(ical) representation, used in high energy physics, of certain algebraic expressions. There are a set of rules called `Feynman rules', which allow you to go from a Feynman diagram to its corresponding algebraic expression. The Feynman rules depend on the specific physical theory under study (e.g. the Standard Model of particle physics).

There are a number of mathematical ways to represent Feynman diagrams, e.g.:
https://arxiv.org/pdf/math/0106001 or (defn. 12) in https://arxiv.org/pdf/math/0212121.

Sorry this is all a bit vague, but if this sounds interesting to anyone (so much so that they want to get involved) please let me know.

[Mr Proof]

I'm just thinking about what kinds of things you could use the proof assistant for.

Perhaps you could prove things like "The three loop term in the perturbation series is between A and B" where A and B are two rational numbers. If you could have a formal proof of that rather than a numerical calculation which might not be trusted then that would actually be a useful result. Or you could prove upper and lower bounds on physical quantities.

[Joseph Tooby-Smith]

There are examples of the sorts of things which can be formalised here. (Although note this is not the final version of things).

A suitable target is to reproduce features of FeynCalc.

[Dean Young]

The paper seems to relate these to string diagrams, in the way of monoidal categories. Is it possible that this would then use monoidal categories (along with Yumo Mizuno's widget)?

Categories-for-Quantum-Theory.pdf

[Joseph Tooby-Smith]

I would like to see the string diagram approach formalised (along with its relationship to other approaches). It is, however, not the approach I have been taking. The primary reason I am not taking this approach is that I can't see how one can extract 'symmetry factors' from it.

The approach I am taking is a categorical approach in which the objects are Feynman diagrams, and the morphisms are such that the cardinality of the automorphism group of a Feynman diagram is the symmetry factor.