Formal verification study demonstrates rigorous path-integral formulations for bosonic and fermionic reservoirs in Lean 4, highlighting exact mathematical foundations for open quantum dynamics.
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.
No takes yet. Share an insight, caveat, or question.
Berdinsky et al. (2026) studied this question.
Synapse has enriched 5 closely related papers on similar clinical questions. Consider them for comparative context: