ModularPhysics

A formalization of stochastic analysis and SPDEs. The Itô calculus stack is self-contained relative to Mathlib and includes a fully proven Itô formula (0 sorrys on the critical path), Itô isometry, Brownian motion quadratic variation, and a Kolmogorov–Chentsov theorem for Hölder continuous modifications. The core Itô formula proof chain (33 files, ~24k lines, 0 sorrys, 0 axioms) has been extracted into a standalone repository: stochasticpde-itocalculus. Additional tracks cover Hairer's regularity structures, BPHZ renormalization, and singular SPDE fixed-point formulations.

Formalization of constructive two-dimensional φ⁴ Euclidean quantum field theory, following Glimm–Jaffe (20 Lean modules). The end-to-end pipeline runs from a free Gaussian field through finite-volume measure construction, correlation inequalities, reflection positivity, infinite-volume limits, OS axiom verification, and reconstruction to Wightman theory. Depends on gaussian-field, heat kernel infrastructure, and OSReconstruction. Open frontier obligations are represented explicitly as 26 structured ...Model interface assumptions, collected in a bundled entrypoint.

The mathematical bridge between Euclidean and relativistic quantum field theory. Formalizes the Osterwalder–Schrader reconstruction theorem: Schwinger functions satisfying the OS axioms can be analytically continued to Wightman functions defining a relativistic QFT. Includes substantial supporting infrastructure in several complex variables and von Neumann algebras. Depends on gaussian-field for Hermite–Schwartz expansions, nuclear space definitions, and Gaussian measure construction.

Umbrella integration repo for the geometric foundations of string theory, composed from three active sub-repositories. The architecture enforces strict independence between proof engines — no cross-smuggling of theorems between analytic and algebraic tracks.

Algebraic structures appearing in string theory, split into focused domain repositories. The umbrella repo provides split planning, extraction scripts, and coordination.

Encodes the logical architecture of theoretical physics in Lean 4: which hypotheses are required, what each framework claims, and how frameworks relate or conflict. The goal is explicitness rather than full mathematical rigor — proof-heavy formalization is delegated to the other repositories. All non-derived physical premises are tracked through a PhysicsAssumption system with stable IDs and a master registry. The project is split into a strict Core target (architecture-level soundness) and a looser Papers target for specific physics arguments. CI enforces invariants: no Lean axiom declarations, no vacuous placeholders, no unregistered assumption IDs, and no sorry regressions in Core.