This preprint develops a rigorous, machine-checked construction of non-Gaussian functional integrals using the Henstock–Kurzweil (HK) gauge integral and Chernoff product approximations. The central object is a finite family of bosonic modes with an action containing a quartic self-interaction λ∑iφi4λ∑iφi4. We show that the one-mode non-Gaussian integral is finite, positive, monotone and infinitely differentiable in the coupling λλ on [0,∞)[0,∞), with derivatives given by convergent integrals rather than by the divergent perturbative series. The MM-mode influence functional factorises into one-mode integrals and is bounded by its Gaussian value. A Chernoff/Lie–Trotter splitting handles non-commutativity of the free and non-Gaussian generators. All statements are formalised in Lean 4 / Mathlib and are free of sorry, using only the standard axioms propext, Classical.choice, Quot.sound. The accompanying Lean file HkNonGaussian.lean is included. Illustrative applications are worked out at the level of explicit formulas: the Duffing oscillator, local volatility (CEV) in finance, Wilson–Cowan neural fields, and non-Gaussian quantum reservoirs. This work is a direct continuation of the author’s programme on machine-verified path integrals without Wick rotation.
This preprint develops a rigorous, machine-checked construction of non-Gaussian functional integrals using the Henstock–Kurzweil (HK) gauge integral and Chernoff product approximations. The central object is a finite family of bosonic modes with an action containing a quartic self-interaction λ∑iφi4λ∑iφi4. We show that the one-mode non-Gaussian integral is finite, positive, monotone and infinitely differentiable in the coupling λλ on [0,∞)[0,∞), with derivatives given by convergent integrals rather than by the divergent perturbative series. The MM-mode influence functional factorises into one-mode integrals and is bounded by its Gaussian value. A Chernoff/Lie–Trotter splitting handles non-commutativity of the free and non-Gaussian generators. All statements are formalised in Lean 4 / Mathlib and are free of sorry, using only the standard axioms propext, Classical.choice, Quot.sound. The accompanying Lean file HkNonGaussian.lean is included. Illustrative applications are worked out at the level of explicit formulas: the Duffing oscillator, local volatility (CEV) in finance, Wilson–Cowan neural fields, and non-Gaussian quantum reservoirs. This work is a direct continuation of the author’s programme on machine-verified path integrals without Wick rotation.
We unify the Henstock-Kurzweil treatment of open quantum systems with bosonic Gaussian reservoirs and fermionic Grassmann reservoirs. Finite cylindrical gauge integrals yield determinant and covariance identities for bosons, while Berezin integration yields Pfaffian identities for fermions. In both sectors the reservoir is eliminated into an influence functional and the reduced dynamics is organised by Chernoff splitting. The accompanying Lean 4 developments verify the finite-dimensional Gaussian, operator, exterior-algebra, and Pfaffian steps. This upload contains the paper and the accompanying Lean 4 formalisation. The Lean development is free of sorry, admit, and newly introduced axioms. Kernel axiom inspection of the headline results reports only propext, Classical.choice, and Quot.sound. The finite-mode formulas are exact and machine-checked; continuum and unbounded-generator qualifications are kept explicit in the paper.
In order to preserve the leading role of the action principle in formulating all field theories one needs quantum field theory, with the associated BRST symmetry, and Feynman–DeWitt–Faddeev–Popov ghost fields. Such fields result from the fiber-bundle structure of the space of histories, but the physics-oriented literature used them formally because a rigorous theory of measure and integration was lacking. Motivated by this framework, this paper exploits the previous work of Gill and Zachary, where the use of Banach spaces for the Feynman integral was proposed. The Henstock–Kurzweil integral is first introduced, because it makes it possible to integrate functions like [Formula: see text]. The Lebesgue measure on [Formula: see text] is then built and used to define the measure on every separable Hilbert space. The subsequent step is the construction of a new Hilbert space [Formula: see text], which contains [Formula: see text] as a continuous dense embedding, and contains both the test functions [Formula: see text] and their dual [Formula: see text], the Schwartz space of distributions, as continuous embeddings. This space allows us to construct the Feynman path integral in a manner that maintains its intuitive and computational advantages. We also extend this space to [Formula: see text], where [Formula: see text] is any separable Hilbert space. Last, the existence of a unique universal definition of time, [Formula: see text], that we call historical time, is proven. We use [Formula: see text] as the order parameter for our construction of Feynman’s time ordered operator calculus, which in turn is used to extend the path integral in order to include all time-dependent groups and semigroups with a reproducing kernel representation.
Abstract In this work, the perturbative aspects of quantum mechanics (QM) and quantum field theory (QFT), to a large extent, are studied with functional (path or field) integrals and functional techniques. This physics textbook thus begins with a discussion of algebraic properties of Gaussian measures, and Gaussian expectation values for a finite number of variables. The important role of Gaussian measures is not unrelated to the central limit theorem of probabilities, although the interesting physics is generally hidden in essential deviations from Gaussian distributions. A few algebraic identities about Gaussian expectation values, in particular Wick's theorem are recalled. Integrals over some type of formally complex conjugate variables, directly relevant for boson systems are defined. Fermion systems require the introduction of Grassmann or exterior algebras, and the corresponding generalization of the notions of differentiation and integration. Both for complex and Grassmann integrals, Gaussian integrals, and Gaussian expectation values are calculated, and generalized Wick's theorems proven. The concepts of generating functions and Legendre transformation are recalled.
I present a numerical algorithm for direct evaluation of multiple Grassmann integrals. The approach is exact and suffers no Fermion sign problems. Memory requirements grow exponentially with the interaction range and the transverse size of the system. Low dimensional systems of order a thousand Grassmann variables can be evaluated on a workstation. In quantum field theory fermions are usually treated via integrals over anti-commuting Grassmann variables [2], providing an elegant framework for the formal establishment of Feynman perturbation theory. With non-perturbative approaches, such as Monte Carlo studies on the lattice, these objects are more problematic. Essentially all approaches formally integrate the fermionic fields in terms of determinants depending only on bosonic fields. When a background
We present a machine-verified formalization, in Lean 4 with Mathlib, of the hypothesisthat matter is an emergent invariant of computation. The framework models a quantumcellular automaton as a unitary operator on a finite-dimensional Hilbert space equippedwith a conserved energy functional and a physical-subspace projector. Matter is identifiedwith the quotient of the fixed-point subspace of the evolution by a global-phase equivalencerelation. We prove: (1) unitarity preserves inner products and norms; (2) the energy func-tional is conserved under iterated evolution; (3) nontrivial fixed-point subspaces exist; and(4) coarse-grained dynamics converge to a stable effective theory. All proofs compile withzero sorry statements and use only the standard axioms of dependent type theory (propext,Classical.choice, Quot.sound).
The Feynman–Bijl argument bounds the lowest excitation energy of a Bose fluid at wavevector k by ħ2k2/(2mS(k)), with S(k) the static structure factor. This preprint formalises its single-mode core in Lean 4.34.1 with Mathlib and applies the one-sided diffraction test S(k) ≤ √(k/2k*) (k* = 2mc/ħ) of an earlier preprint to published data. Every claim is filed in an Elenchus claim ledger with tiers A (kernel-checked Lean), L (cited literature; excerpts: prose as extracted, mathematics transcribed linearly), C (human argument, not machine-checked) and X (floating-point arithmetic or values read from a figure, which never supports a claim). Tier A (Lean 4.34.1 and Mathlib, pinned toolchain; axioms within propext, Classical.choice, Quot.sound; planted sorry and planted-axiom controls caught; independently recompiled by a separate AI auditor with a private olean build, axioms identical, planted controls and two auditor mutations caught; no human audit): on a finite-dimensional complex inner product space with a symmetric H and an eigenvector ψ, the identity ⟨ψ,[ρ†,[H,ρ]]ψ⟩ = A(ρ) + A(ρ†) holds with no extra hypothesis. With the k ↔ −k symmetry and the f-sum value taken as hypotheses, the trial state ρψ/||ρψ|| has excess energy f/(2NS) and an eigenvector overlapping ρψ obeys λ − E0 ≤ ħ2k2/(2mS); a gap form gives 0 < λ − E0 under two further hypotheses. A kernel-checked counterexample shows that the symmetry hypothesis cannot be dropped from the halving step (A(ρ) = 1 ≠ 1/2 = f/2); that the final bound also fails in that example is a hand computation (Tier C), not a Lean theorem. A kernel-checked witness shows that all hypotheses hold together and the bound is attained. The Bogoliubov link (the Feynman energy from SB equals the Bogoliubov energy; SB ≤ √(k/2k*)) is re-proved on the pinned stack. The physics (f-sum rule from the canonical commutation relations, the symmetry, momentum conservation) is not in Lean. Tier X data analysis, Tier C reading: for 4He, 99 points of Table 14.1 of the Donnelly–Barenghi compilation (a secondary source; 1.4–4 K, not T = 0; no printed error bars) with k* = 3.00379 Å-1 from c = 238.3 m/s: 63 points refuted, 29 consistent, 7 undecided, all 21 points in the roton/peak region 1.7–2.4 Å-1 refuted by a factor 1.62–2.49. The refutation threshold (0.082, the gap between the two datasets' peak maxima) was defined after seeing the data and is a deviation from the preregistration; the strict-run endpoint (Q = 5.129 is refuted by 0.0830) and the counts above 2.4 Å-1 depend on its third decimal (refuted 60–64 for thresholds 0.07–0.10), while the roton-region result does not (smallest margin 0.328, about 4 thresholds) and also holds on the Donnelly–Barenghi recommended subset (X-ray for Q < 1, neutron for Q > 1). Read conditionally, this says only that 4He is not a Bogoliubov gas, which is textbook; no novelty is claimed for the physics or for the Feynman–Bijl argument. For trapped Bose gases only values read from figures exist (Tier X): the three absolute points of Stamper-Kurn et al. lie below a local-density-averaged bound with low test power (no ‘BEC consistent’ claim), and the Steinhauer et al. points were multiplied by 2.3 by the authors, so no decisive test is possible. A trapped-gas positive control shows that single-k* bounds fail their own control and only the LDA-averaged bound is valid. No rusty-SUNDIALS or LeanFlow change was made in this lane (the numerics are Python), so none is claimed. The Elenchus ledger gate reports 0 blocking findings and 11 flags (exit code 1), one for each Tier A row whose statement adequacy no human has audited. The work was produced by AI agents (Claude) under the author's direction and was audited by a separate AI agent (verdict ACCEPT_WITH_CORRECTIONS, corrections applied); no human has audited it; the author is responsible for the content.