A computer-assisted sufficient condition for Edwards–Anderson order in the square-lattice ±J model

Consider the zero-field nearest-neighbor Ising model on the square lattice with independent couplings J_e ∈ {−1,+1}, where p = ℙ(J_e = +1). We give a computer-assisted sufficient condition for a positive thermodynamic Edwards–Anderson response: p ≥ 0.9537 and inverse temperature β ≥ 10⁶. The proof combines local contour-flip estimates, a gauge transformation applied to one checkerboard class, and a finite-memory matrix retaining correlations within transformed bond stars. The local estimates are an arm-flip family at contour corners (Lemma A), strict local deformations of the contour (Lemma S) and cap flips; one constant, the sign-monotonicity ratio of the weight, is established by an exact finite computation rather than by hand. A positive integer vector certifies every row of a 453,233,520-state rational matrix below a contraction factor 0.9999, and two exact verifiers accept it with the same maximum row ratio. A favorable finite patch converts contour summability into positive mean overlap for a specified disorder-dependent boundary. Convexity then gives a boundary-independent thermodynamic order parameter; compactness and ergodicity give almost-sure Gibbs nonuniqueness at each fixed temperature in the stated range. The conclusion does not distinguish a ferromagnet from a phase with zero magnetization and nonzero overlap.