Capped variance of random k-SAT: the theorem

Target T7 of phase 12. sat_variance_theorem proves sat_variance_statement of SatVarianceStatement.v: for every realType R and k >= 3, there is C > 0 with sat_capped_var R n k <= C n^(1 + 2/k) for every n >= k + 1, the power being powR. It is sat_variance_bound of RandomSAT/Variance.v, the existential form of sat_variance_bound_explicit, whose constant is C = 8 4^(k+1) k (3 k + 2^(k+2)); the headers of the files of RandomSAT describe the proof.

A Rocq formalization of the credited argument of the proposition 'Polynomial concentration' of 'A limiting satisfiability threshold for every fixed clause size' (family 235 of the OpenAI math collection, revision 1581d4cbd, source/sections/concentration.tex) and of the proposition 'Integrated forcing' of source/sections/forcing.tex, with the variance step of the Lean development of the collection in place of the lemmas 'Deletion variance bound' and 'Pivotal pairs'. The proof follows the route of that development, in lean/OAI/Probability/RandomSAT:

Lean: variance_capped (Concentration.lean, line 80)

The manuscript bounds Var(V_n) through the omission of one clause; the Lean development and the proof here use a recursion over the clauses, which gives a bound of the same form (Pivotal.v). The Lean theorem bounds the variance of the lifetime of the clause process by a constant times n (n^(1/k))^2; Model.v identifies the statistic of the statement with that lifetime.