I.9 Exact effective dynamics
On this page · Permalink · Source line 892
I.9.1 Schur–Feshbach reduction
On this page · Permalink · Source line 894
Let \(P\) be a retained packet projector and \(Q=I-P\). In packet coordinates,
Theorem I.9.1: Exact Feshbach resolvent
Assume that both \(zI_Q-H_{QQ}\) and \(zI-H\) are invertible. Define
Then
where the left side is restricted to \(P{\mathcal H}\), the right side is an inverse on that retained space, and both are written in the same orthonormal basis. Here \(z-H_{QQ}\) and \(z-H_{\mathrm{eff}}\) abbreviate the appropriately sized scalar matrices minus the indicated blocks.
Read proof · Read statement and proof side by side · Permalink · Source line 905 · Claim record · Lean coverage · Code · Worked examples
Proof of Theorem I.9.1
The block in the lower right corner of \(z-H\) is \(z-H_{QQ}\). Gaussian block elimination produces the Schur complement
The assumed invertibility of this block and of the full matrix implies that the Schur complement is invertible. The block in the upper left corner of the full inverse is the inverse of that Schur complement, which is exactly the displayed operator.
Back to statement · Read statement and proof side by side · Permalink · Source line 926 · Claim record · Lean coverage · Code · Worked examples
The second premise cannot be dropped: at \(z=0\) and \(H=\operatorname{diag}(0,-1)\), the eliminated block is \(1\) but \(zI-H\) is singular. This counterexample is also included in the Lean module.
The self-energy
contains the complete influence of the eliminated packet. Bare truncation drops \(\Sigma_P(z)\) and is therefore exact only when the coupling between packets vanishes or the self-energy cancels for another stated reason.
Text description
A logarithmic bar chart compares projected resolvent error. The exact Feshbach bar is near numerical precision, while the bare-truncation bar is substantially larger. The comparison retains the influence of the eliminated coordinates in one finite example.
Text description
A two-by-two heatmap places source parity on columns and target parity on rows. The two diagonal blocks have positive displayed norms; the off-diagonal blocks are zero in this example. The color scale represents block Frobenius norms.
Numerical certificate I.9.2: Effective resolvent
In the reported test with a random Hermitian matrix of dimension six, the exact Feshbach residual was \(3.2291\times10^{-17}\). The corresponding residual for bare truncation was \(1.3091\times10^{-2}\).
Permalink · Source line 959 · Claim record · Lean coverage · Code · Worked examples
I.9.2 The hidden packet as memory
On this page · Permalink · Source line 963
For a time-independent finite Hamiltonian \(H\) and fixed projectors \(P,Q\), write \(\psi=x+y\), with \(x=P\psi\) and \(y=Q\psi\). Then
Solving the second equation gives
Substitution yields the exact Volterra equation
with memory kernel
The influence of the eliminated degrees of freedom is therefore retained in a self-energy that depends on frequency, or equivalently in an exact memory term. For forward evolution the integral is causal. When the Hamiltonian depends on time, the corresponding propagator between two times replaces the stationary exponential used here. This Volterra derivation is not a separate entry in the finite Lean register.