Henstock-Kurzweil Path Integrals for Open Quantum Systems: Bosonic and Fermionic Reservoirs — A Machine-Verified Approach

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.