API: Integrate Glimm-Jaffe AQFT Framework into PhysLean

Details

Key data structure

The API is built around the FieldConfiguration type representing tempered distributions as field configurations, combined with Euclidean spacetime and test function spaces:

• FieldConfiguration := SpaceTime →d[ℝ] ℝ - tempered distributions on Euclidean spacetime 1
• SpaceTime := EuclideanSpace ℝ (Fin STDimension) - 4D Euclidean spacetime (must remain Euclidean for OS reconstruction)
• TestFunction := SchwartzMap SpaceTime ℝ - Schwartz test functions
• GJGeneratingFunctional - generating functional Z[J] = ∫ exp(i⟨ω, J⟩) dμ(ω)

The axioms have been discharged here in the spacetime Hermite model.

Need

This API is needed to provide a mathematically rigorous foundation for constructive quantum field theory in PhysLean using the Osterwalder-Schrader approach. After completion, it will:

• Enable formalization of Glimm-Jaffe constructive QFT framework
• Support Schwinger functions and correlation functions via functional derivatives
• Provide basis for implementing Osterwalder-Schrader axioms
• Allow rigorous treatment of Euclidean field measures and generating functionals
• Bridge distribution theory with QFT

Requirements

Core Framework

• Preserve Euclidean SpaceTime definition (essential for OS reconstruction)
• Keep STDimension := 4 and related constants
• Maintain getTimeComponent and spatialPart functions for Euclidean space
• Retain Lebesgue measure μ := volume

Distribution Integration

• Replace FieldConfiguration with SpaceTime →d[ℝ] ℝ notation
• Update distributionPairing to use distribution evaluation
• Integrate Distribution.fderivD for derivatives 2
• Ensure measurable space instance works with new type

Test Function Infrastructure

• Keep schwartzMul operation for complex test functions
• Preserve schwartz_comp_clm helper function
• Maintain complex_testfunction_decompose and associated lemmas
• Keep distributionPairingℂ_real for complex test function pairing

Generating Functionals

• Preserve GJGeneratingFunctional definition Z[J] = ∫ exp(i⟨ω, J⟩) dμ(ω)
• Keep GJGeneratingFunctionalℂ for complex analyticity
• Maintain GJMean for mean field calculations

Documentation and Integration

• Add module docstring following PhysLean standards
• Document integration decisions (Euclidean vs Lorentzian)
• Add references to Osterwalder-Schrader literature
• Ensure compatibility with existing PhysLean distribution infrastructure

Corresponding file system

The API should be integrated into PhysLean's QFT module hierarchy:

PhysLean/QFT/
├── ConstructiveQFT/
│   ├── EuclideanFramework.lean  # Core framework (minimal changes from user's file)
│   ├── GlimmJaffe.lean         # GJ framework specifics
│   └── OsterwalderSchrader.lean # OS axioms implementation

Related existing PhysLean infrastructure:

• PhysLean/Mathematics/Distribution/Basic.lean - Distribution types and derivatives
• PhysLean/SpaceAndTime/Space/Basic.lean - Spatial coordinates (for spatial slices)
• Note: PhysLean/SpaceAndTime/SpaceTime/Basic.lean uses Lorentzian spacetime and should NOT be used for this Euclidean framework 3

Wiki pages you might want to explore:

• Overview (HEPLean/PhysLean)

Citations