The good disorder of the SK model

Part of target T4 of phase 12 (AGENTS.md, section Phase 12), the spectral gap of the heat-bath dynamics of the Sherrington-Kirkpatrick model for beta < 1/2. A Rocq formalization of the credited argument of the proposition 'Good disorder' (rcut:prop:good-disorder) of 'Cutoff throughout the high-temperature Sherrington-Kirkpatrick phase' (family 227 of the OpenAI math collection, revision 1581d4cbd, file appendices/entropy.tex). It follows the TeX, not a Lean module of the collection.

For beta >= 0, delta > 0 and the coupling J = sk_coupling beta a of SKGapDefinitions.v, sk_good_disorder n beta delta is the set of the a of 'rV[R]_(n * n) such that

opnorm J <= 2 beta + delta,
sum_j J_ij^2 <= beta^2 + delta for every i,
|J_ij| <= delta for every i and j.

It is measurable (sk_good_disorder_measurable), and its probability under gauss (n * n) tends to one (sk_good_disorder_prob). R is implicit in the three; their other arguments are explicit.

The proof is the manuscript's. If beta = 0, then J = 0 and the event is the whole space. If beta > 0, then J = beta (W - Diag W) with W = goe_mx a, and the event holds outside four failure events of random_matrix/goe_entries.v and random_matrix/goe_edge.v, where t = delta / (2 beta), u = delta / beta^2 and s = delta / beta:

• opnorm W >= 2 + t, of probability at most 2 exp (- n t^2 / 4) by the sharp edge goe_opnorm_edge_tail. Outside it, and when the diagonal of W is at most t, opnorm J <= beta (opnorm W + t) <= 2 beta + delta (sk_coupling_opnorm_le);
• |W_ii| >= t for some i, of probability at most 2 n exp (- n t^2 / 4), by Gaussian tails and a union bound;
• sum_(j != i) W_ij^2 >= 1 + u for some i, of probability at most n exp (- n u^2 / (4 (1 + u))), by the tail of a chi-square with n - 1 degrees of freedom and a union bound;
• |W_ij| >= s for some i != j, of probability at most 2 n^2 exp (- n s^2 / 2), by Gaussian tails and a union bound.

As n^k exp (- n c) <= 6 / (c^3 n) for c > 0, k <= 2 and n >= 1 (exprn_expRN_le of random_matrix/goe_entries.v), the four probabilities sum to at most K / n, with K depending only on beta and delta.

The manuscript lets delta = n^(-1/4) tend to zero. Here delta > 0 is fixed, which is what the assembly of T4 uses, and no rate is needed. The manuscript's consequence for the cubic row sums is not part of this file.