Anomaly cancellation conditions

Stream: Natural sciences

[Joseph Tooby-Smith]

As an example of a use of lean in high energy physics, I am planning on putting together an api for the anomaly cancelation conditions. These are (for the standard model of particle physics) a set of 6 diophantine equations in 18 variables, given in equations 1a-1f of https://arxiv.org/pdf/2006.03588.pdf. The solutions of these equations are of physical interest, specifying the allowed charges particles can take under the addition of an extra U(1) gauge group to the standard mode gauge algebra.

There are a number of simple known facts about these equations and variations thereof which are of interest to physicists. Formalising these equations and facts thereof seems like a good first step in the direction of formalizing aspects of high energy physics, not least because the underlying mathematics is fairly simple and very concrete.

If anyone would like to get involved with this, or has other comments please let me know.

[Patrick Massot]

Be careful that being very concrete is a bad thing for formalization. Abstract things are almost always easier to formalize.

[Kevin Buzzard]

If it's any help, subtracting 3 * equation 1c from equation 1a gives you a simpler equation 1a' which could be used instead.

[Joseph Tooby-Smith]

@Patrick Massot What I meant by 'concrete' was that the problem is very well defined, poor choice of words on my part. But I agree that this may lead to issues.

@Kevin Buzzard The equations are written in the way they are in that paper because of their physical origin from certain Feynman diagrams. I care less about actually formalising the solution that happens to be the subject of that paper (which I don't think the average physicist would care about), and care more about formalizing a bunch of simple facts physicists know and do care about them and their solutions. A sort of 'baby steps of lean into high-energy physics' project.

[Tyler Josephson ⚛️]

I like it! This looks like an excellent problem to tackle, since the underlying math looks nice and simple (but also includes a decent amount of tedium, so there's motivation to formalize to ensure no mistakes compared to the handwritten situation). My questions:

Is there motivation for computing different solutions to these equations, depending on different situations? If so, you could think about programming a verified software for doing those calculations in Lean, rather than just writing some proofs about the math.

Would the relevant variables be natural numbers or integers? If they're reals, then computing solutions to this would become tricky, but if not, then writing executable code based on this model would be straightforward, too.

[Joseph Tooby-Smith]

Hi @Tyler Josephson ⚛️ , thanks :). To answer your questions:

1) Yes there is motivation. This has been done (using an unverified program) here : https://inspirehep.net/literature/1708575 (and for a very similar set of equations here: https://inspirehep.net/literature/1886600). I think the only point of writing a verified version would be for demonstration purposes - although maybe this is a good enough reason in itself.

2) They are integers (although one can take them to be rationals if one so chooses since the equations are homogenous).

[Tyler Josephson ⚛️]

Sounds like a great project, then. You refer to “a very similar set of equations” - you could also consider formalizing both of them, and formally defining how they are related to one another (Is one a special case of the other? Are both specific instances of a third, more general thing?)

[Tyler Josephson ⚛️]

Also, what did you have in mine when you say “API”?

[Joseph Tooby-Smith]

@Tyler Josephson ⚛️ There is an injective map from solutions of one into solutions of the other, but not vice versa. And yes they are more specific instances of a more general thing. However to formalize that more general thing requires going out of the theory of diophantine equations, and integers, and into the theory of Lie algebras and their representations. It is probably worth formalizing this at some point, but maybe not the priority.

Maybe my use of "API" is not standard. I meant a collection of all results (or as many as possible) relate to these equations, such that if at some point in the future lean takes off in the physics community, these results could be used in other proofs and definitions etc.

[Joseph Tooby-Smith]

FYI (in case anyone comes across this and is interested), I am working on this in this GitHub repository: https://github.com/jstoobysmith/Anomaly_Cancellation_in_Lean

[Joseph Tooby-Smith]

I've moved the above repository into a more generic one for high energy physics: https://github.com/HEPLean/HepLean. The aim of this repository is to be an open-source library of theorems, proofs, definitions, calculations etc from high energy physics.

[Tyler Josephson ⚛️]

Cool!