On this page

GaussianApplicationsapplicationsRandomSATVariance

Random k-SAT: the capped variance bound

GaussianApplications.RandomSAT.Varianceapplications/RandomSAT/Variance.v272 lines13 lemmas and theoremssource

Imports 6 library modules and 10 external

External: HB.structures, mathcomp.classical.all_ssreflect_compat, mathcomp.algebra.algebraic_hierarchy.ssralg, mathcomp.algebra.numeric_hierarchy.ssrnum, mathcomp.reals.reals, mathcomp.algebra.archimedean, mathcomp.analysis.exp, mathcomp.algebra.arithmetic_tactic, mathcomp.algebra.ring_tactic, mathcomp.algebra.field_tactic

Imported by 1

GaussianApplications.SatVarianceTheorem

Part of target T7 of phase 12 (see Model.v). 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), assembled as in the Lean development of the collection (lean/OAI/Probability/RandomSAT):

Lean: truncatedKilling_le_forced (Variance.lean, line 412)

Lean: lifetimeVariance_forcing_bound (Variance.lean, line 487)

Lean: replacementScale (Replacement.lean, line 282)

Lean: integrated_forcing_capped (Concentration.lean, line 49)

Lean: variance_capped (Concentration.lean, line 80)

trunc_le_forced: if M <= c^k, then min(M kill k S, 1) <= c b / n, with b the number of forced variables of S, since the killing probability is at most (b / (2 n))^k <= (b / n)^k (kfrac_le_pow).
sat_capped_varE: sat_capped_var R n k, the variance of the statistic of the statement, is life_var k (sat_cap k n) of the set of all assignments (sat_prefix_lenE of Model.v).
sat_variance_bound_explicit: for K >= 3 and N >= K + 1, sat_capped_var R N K <= C N^(1 + 2/K), with C = 8 4^(K+1) K (3 K + 2^(K+2)); sat_variance_bound is its existential form, the form of the statement. The proof takes a = N^(1/K), the block g = floor(2 K a) + 1 <= 3 K a and c = 4 a, so that the cap M = 2^(K+1) N is at most c^K; life_var_le_occ of Pivotal.v, trunc_le_forced, forced_frac_head and integrated_head_forcing of Forcing.v then bound the variance by 2 M c (g M p + (M + 1) M p a^-(K-1)), with p = K / N, and N a^-(K-1) = a, N a^2 = N^(1 + 2/K).

The statement and the manuscript bound Var(V_n) by C n^(1 + 2/k); the Lean theorem bounds the variance of the lifetime by a constant times n (n^(1/k))^2, with a block of size ceil(2 k n^(1/k)). The constant here is explicit (sat_variance_bound_explicit) and holds for every n >= k + 1.

Main results

Results	Statement
sat_capped_varEtrunc_le_forcedsat_variance_bound_explicitsat_variance_bound	`sat_capped_var R n k` is the variance of the lifetime of the set of all assignments over `sat_cap k n` clauses. For `0 < k <= n`, `c >= 0` and `M <= c^k`, `min(M q, 1) <= c b / n`, where `q` is the probability that a uniform clause of size `k` empties a set of assignments with `b` forced variables. `sat_variance_bound_explicit`: for `K >= 3` and `N >= K + 1`, `sat_capped_var R N K <= 8 4^(K+1) K (3 K + 2^(K+2)) N^(1 + 2/K)`; `sat_variance_bound` is its existential form, the form of the statement.

Declarations13 exported, 1 local

sectionbounds

Context {R : realType}.

lemma min_le_lin source, line 58

forall {R : realType} [M q y c : R] [K : nat],
(0 < K)%N ->
0 <= q ->
0 <= y -> 0 <= c -> 0 <= M -> q <= y ^+ K -> M <= c ^+ K -> Num.min (M * q) 1 <= c * y

min (M q, 1) <= c y when q <= y^K, M <= c^K and K >= 1.

Statement as written in the source

Lemma min_le_lin (M q y c : R) K : (0 < K)%N -> 0 <= q -> 0 <= y -> 0 <= c ->
  0 <= M -> q <= y ^+ K -> M <= c ^+ K -> Num.min (M * q) 1 <= c * y.

Used by 1 declaration in 1 file

this file: trunc_le_forced

lemma trunc_le_forced main result source, line 72

forall {R : realType} [n k M : nat] [c : R] (S0 : {set {ffun 'I_n -> bool}}),
(0 < k)%N ->
(k <= n)%N -> 0 <= c -> M%:R <= c ^+ k -> trunc k M S0 <= c * (#|forced S0|%:R / n%:R)

The truncated killing chance is at most c times the forced fraction.

Main result

Stated in the README together with sat_capped_varE.

Statement as written in the source

Lemma trunc_le_forced n k M (c : R) (S : {set {ffun 'I_n -> bool}}) :
  (0 < k)%N -> (k <= n)%N -> 0 <= c -> M%:R <= c ^+ k ->
  trunc k M S <= c * (#|forced S|%:R / n%:R).

Used by 1 declaration in 1 file

this file: sat_variance_bound_explicit

sectionsat_variance

Context {R : realType}.

lemma sat_capped_varE main result source, line 102

forall {R : realType} (n k : nat),
sat_capped_var R n k = life_var k (sat_cap k n) [set: {ffun 'I_n -> bool}]

Main result, as the README states it

sat_capped_var R n k is the variance of the lifetime of the set of all assignments over sat_cap k n clauses. For 0 < k <= n, c >= 0 and M <= c^k, min(M q, 1) <= c b / n, where q is the probability that a uniform clause of size k empties a set of assignments with b forced variables. sat_variance_bound_explicit: for K >= 3 and N >= K + 1, sat_capped_var R N K <= 8 4^(K+1) K (3 K + 2^(K+2)) N^(1 + 2/K); sat_variance_bound is its existential form, the form of the statement.

Statement as written in the source

Lemma sat_capped_varE n k :
  sat_capped_var R n k = life_var k (sat_cap k n) [set: {ffun 'I_n -> bool}].

Used by 1 declaration in 1 file

this file: sat_variance_bound_explicit

The root a = n^(1/K) of the manuscript's block size and error.

sectionroot

Variables (n k : nat).

let a section-local source, line 114

Let a : R := n.+1%:R `^ (k.+1%:R)^-1.

Used by 6 declarations in 1 file

this file: root_gt0, root_pow, root_ge1, root_small, root_err, root_sqr

lemma root_gt0 source, line 116

forall {R : realType} (n k : nat), 0 < n.+1%:R `^ k.+1%:R^-1

Statement as written in the source

Lemma root_gt0 : 0 < a.

Used by 4 declarations in 1 file

this file: root_ge1, root_small, root_err, sat_variance_bound_explicit

lemma root_pow source, line 119

forall {R : realType} (n k : nat), n.+1%:R `^ k.+1%:R^-1 ^+ k.+1 = n.+1%:R

Statement as written in the source

Lemma root_pow : a ^+ k.+1 = n.+1%:R.

Used by 4 declarations in 1 file

this file: root_ge1, root_small, root_err, sat_variance_bound_explicit

lemma root_ge1 source, line 125

forall {R : realType} (n k : nat), 1 <= n.+1%:R `^ k.+1%:R^-1

Statement as written in the source

Lemma root_ge1 : 1 <= a.

Used by 2 declarations in 1 file

this file: root_small, sat_variance_bound_explicit

lemma root_small source, line 132

forall {R : realType} (n k : nat), n.+1%:R^-1 <= (n.+1%:R `^ k.+1%:R^-1)^-1 ^+ k

Statement as written in the source

Lemma root_small : (n.+1%:R)^-1 <= a^-1 ^+ k.

Used by 1 declaration in 1 file

this file: sat_variance_bound_explicit

lemma root_err source, line 139

forall {R : realType} (n k : nat),
n.+1%:R * (n.+1%:R `^ k.+1%:R^-1)^-1 ^+ k = n.+1%:R `^ k.+1%:R^-1

Statement as written in the source

Lemma root_err : n.+1%:R * a^-1 ^+ k = a.

Used by 1 declaration in 1 file

this file: sat_variance_bound_explicit

lemma root_sqr source, line 146

forall {R : realType} (n k : nat),
n.+1%:R * n.+1%:R `^ k.+1%:R^-1 ^+ 2 = n.+1%:R `^ (1 + 2 / k.+1%:R)

Statement as written in the source

Lemma root_sqr : n.+1%:R * a ^+ 2 = n.+1%:R `^ (1 + 2 / k.+1%:R).

Used by 1 declaration in 1 file

this file: sat_variance_bound_explicit

lemma trunc_block source, line 158

forall {R : realType} [x : R], 1 <= x -> (Num.Def.truncn (2 * x)).+1%:R <= 3 * x

Statement as written in the source

Lemma trunc_block (x : R) : 1 <= x -> (Num.truncn (2 * x)).+1%:R <= 3 * x.

Used by 1 declaration in 1 file

this file: sat_variance_bound_explicit

lemma variance_arith source, line 166

forall {R : realType} [V Sg m N K a g e t : R],
0 < N ->
0 <= a ->
0 <= K ->
0 <= e ->
0 <= t ->
1 <= m ->
m = t * N ->
N * e = a ->
g <= 3 * (K * a) ->
V <= 2 * m * (4 * a * Sg) ->
Sg <= g * m * (K / N) + (m + 1) * m * (K / N) * e ->
V <= 8 * t * t * K * (3 * K + 2 * t) * (N * a ^+ 2)

The arithmetic of the final bound, over plain real numbers.

Statement as written in the source

Lemma variance_arith (V Sg m N K a g e t : R) :
  0 < N -> 0 <= a -> 0 <= K -> 0 <= e -> 0 <= t -> 1 <= m -> m = t * N ->
  N * e = a -> g <= 3 * (K * a) ->
  V <= 2 * m * (4 * a * Sg) ->
  Sg <= g * m * (K / N) + (m + 1) * m * (K / N) * e ->
  V <= 8 * t * t * K * (3 * K + 2 * t) * (N * a ^+ 2).

Used by 1 declaration in 1 file

this file: sat_variance_bound_explicit

theorem sat_variance_bound_explicit main result source, line 196

forall {R : realType} [K N : nat],
(2 < K)%N ->
(K < N)%N ->
sat_capped_var R N K <=
8 * 4 ^+ K.+1 * K%:R * (3 * K%:R + 2 ^+ K.+2) * N%:R `^ (1 + 2 / K%:R)

The bound with its explicit constant.

Main result

Stated in the README together with sat_capped_varE.

Statement as written in the source

Theorem sat_variance_bound_explicit K N : (3 <= K)%N -> (K.+1 <= N)%N ->
  sat_capped_var R N K <=
    8 * 4 ^+ K.+1 * K%:R * (3 * K%:R + 2 ^+ K.+2) * N%:R `^ (1 + 2 / K%:R).

Used by 1 declaration in 1 file

this file: sat_variance_bound

theorem sat_variance_bound main result source, line 259

forall {R : realType} [K : nat],
(2 < K)%N ->
exists C : R,
  0 < C /\
  (forall N : nat, (K < N)%N -> sat_capped_var R N K <= C * N%:R `^ (1 + 2 / K%:R))

The existential form, the form of the statement.

Main result

Stated in the README together with sat_capped_varE.

Statement as written in the source

Theorem sat_variance_bound K : (3 <= K)%N ->
  exists C : R, 0 < C /\ forall N, (K.+1 <= N)%N ->
    sat_capped_var R N K <= C * N%:R `^ (1 + 2 / K%:R).

Used by 1 declaration in 1 file

GaussianApplications.SatVarianceTheorem: sat_variance_theorem

Generated from commit 9046883 (tag phase12) of the ellipsoid fitting repository. Signatures are printed by Rocq 9.1.1; links in the source statements come from the compiled .glob files. The source links open the files on GitHub at this commit, in the now-public repository.