API: Integrate Glimm-Jaffe AQFT Framework into PhysLean

[or4nge19]

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