Negative correlation of steps for walks in symmetric windows

Consider closed ±1 walks D_0, D_1, …, D_n = D_0 confined to symmetric time-dependent windows |D_t| ≤ L_t, with the starting height free within a parity class, and give every such walk the same weight. We prove that any two distinct steps are non-positively correlated. For a fixed starting and ending height the walks in arbitrary windows are the bases of a lattice path matroid, so negative correlation is then an instance of the theorem of Cohen, Tetali and Yeliussizov; our measure is instead a mixture of such matroid measures over the starting height, and mixtures of negatively correlated measures are not negatively correlated in general. The symmetry of the windows is what makes the mixture work: the proof orders conditional drifts by total positivity, shows by reflection that the conditioning weights decay away from height 0, and concludes by Abel summation. The core inequality is certified in the Lean 4 proof assistant. We record extensions (vertex weights decreasing in |x|, lazy walks, box windows in ℤ², open walks with even parity-wise unimodal start and end weights, and a Brownian limit in continuous symmetric tubes), examples showing that each hypothesis is needed, an exact witness that the open-walk measures are not strongly Rayleigh, and open problems. Every result carries an explicit status label.