Upstreaming results from OSforGFF

Stream: PhysLean

[Joseph Tooby-Smith]

Following on from #Natural sciences > Formalization of quantum field theory , I think it would be nice to think about what results from the repo OSforGFF, we can upstream to PhysLean. I think this would be a nice little task for someone.

In particular, the first step would be working out how the results from there fit in to PhysLean (perhaps with reference to https://physlean.com/APITracker.html) and what requirements they fulfil.

It seems natural to start with SpaceTime results related thereto. Though it seems that SpaceTime in OSforGFF is Euclidean SpaceTime not Minkowski as it is in PhysLean, so they may be better fitted into:

https://github.com/lean-phys-community/PhysLean/tree/master/PhysLean/SpaceAndTime/TimeAndSpace

If anyone wants to volunteer to help with this upstreaming, that would be great.

[Matteo Cipollina]

I'd be happy to volunteer, if no one else has particular motivation, as I'm already doing/experimenting with some generalizations on NuclearSpace, providing core API and making an attempt to discharge the minlos_theorem axiom here, leveraging the API in https://github.com/RemyDegenne/kolmogorov_extension4

[Joseph Tooby-Smith]

That would be great @Matteo Cipollina. Maybe we should create a GitHub issue and break it down into small task. What do you think?

[Matteo Cipollina]

Joseph Tooby-Smith ha scritto:

That would be great Matteo Cipollina. Maybe we should create a GitHub issue and break it down into small task. What do you think?

Sure, I'll start with SpaceTime as you suggested.
Here is a draft issue : issue 938

[Joseph Tooby-Smith]

Thanks Matteo! I also made a more specific one just for the SpaceTime stuff here PhysLean#939.

[Joseph Tooby-Smith]

Also made one for the Euclidean group here PhysLean#940