Note that the expectation of fermionic operators, when taken with respect to the computational-basis states, can be exactly computed using the so-called Wick's theorem [1]}, [2]}. However, this approach would introduce unnecessary term reordering which actually complicates our proof. In contrast, the underlying idea of path counting is conceptually simpler and may have potential applications in other contexts beyond the analysis of Trotter error.
