On this page

GaussianApplicationsapplicationsRandomSATModel

Random k-SAT: solution sets and the lifetime of a clause sequence

GaussianApplications.RandomSAT.Modelapplications/RandomSAT/Model.v447 lines43 lemmas and theorems, 10 definitionssource

Imports 2 library modules and 7 external

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

Imported by 4

Part of target T7 of phase 12, the capped variance bound for random k-SAT of SatVarianceStatement.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 and forcing.tex). The files of RandomSAT follow the route of the Lean development of the collection (lean/OAI/Probability/RandomSAT, paths below relative to it): the variance by a recursion over the clauses, and the forced variables by the erasure of one variable. This file follows:

Lean: addClause (ClauseProcess.lean, line 76)

Lean: restrictSolutions (ClauseProcess.lean, line 91)

Lean: alive (ClauseProcess.lean, line 129)

Lean: lifetime (Variance.lean, line 37)

Lean: clauseHeadEquiv (ClauseProcess.lean, line 50)

Lean: clauseHead_mean (ClauseProcess.lean, line 394)

The clauses, the cap and the statistic V_n are those of SatVarianceDefinitions.v. The assignments on n variables are {ffun 'I_n -> bool}, and S is a set of assignments.

add_clause S c is the set of the elements of S that satisfy the clause c, restrict S s the set of those that satisfy every clause of the sequence s, and alive S is 1 if S is not empty and 0 otherwise.
life S s, the lifetime, is the number of nonempty sets among the solution sets of the nonempty prefixes of s (life_sum).
sat_prefix_lenE: for every tuple t of M clauses, sat_prefix_len t is life [set: _] t. The statistic of the statement, the largest satisfiable prefix length up to the cap, is the lifetime of the set of all assignments. The Lean development states its variance bound for the lifetime; this identity transfers it to the statistic of the statement.
The first variable of a clause: a clause of size k.+1 on n.+1 variables either does not contain the first variable, and is cabsent c for a clause c of size k.+1 on the other n variables, or contains it with a sign b, and is cpresent c b for a clause c of size k. The map cjoin of the two cases is a bijection (cjoin_bij). Hence #|clause n k| = 'C(n, k) 2^k (card_clause), and the uniform mean over clause n.+1 k.+1 is the mixture of the two cases with weights 1 - k.+1/n.+1 and k.+1/n.+1 (unif_mean_clause_split).

Main results

Results	Statement
sat_prefix_lenEcard_clauseunif_mean_clause_split	For a tuple `t` of `M` clauses, the largest satisfiable prefix length `sat_prefix_len t`, the cap `M` included, is the lifetime `life [set: _] t`: the number of nonempty solution sets among those of the nonempty prefixes of `t`. `#\|clause n k\| = 'C(n, k) 2^k`. For `k <= n`, the uniform mean over `clause n.+1 k.+1` is the mixture, with weights `1 - k.+1/n.+1` and `k.+1/n.+1`, of the clauses without the first variable (a uniform clause of size `k.+1` on the other `n` variables) and of the clauses with it (a uniform sign and a uniform clause of size `k` on the others).

Declarations53 exported

sectionsolutions

Context {R : realType}.

definition add_clause source, line 62

Type

forall {n k : nat}, {set {ffun 'I_n -> bool}} -> clause n k -> {set {ffun 'I_n -> bool}}

Definition

Definition add_clause n k (S : {set {ffun 'I_n -> bool}}) (c : clause n k) :
    {set {ffun 'I_n -> bool}} :=
  [set s in S | clause_sat s c].

The assignments of a formula on n variables that satisfy a clause.

Used by 27 declarations in 4 files

this file: restrict, life, add_clause_sub, add_clause_mono, add_clauseC, add_clause0
GaussianApplications.RandomSAT.Pivotal: clause_avg, kill, kill_le1, alive_restrict_le, survival_le_geom, delay, delay_cons, pivot_sqr, delay_cross, delay_cons_sqr, secondS, life_var_succ_le
GaussianApplications.RandomSAT.Replacement: kills_frozen, frozen_kills, card_kills, killE_forced
GaussianApplications.RandomSAT.Forcing: deleted_cons, erased_cons, restrict_add_clause, clause_avg_tuple_avg, del_mean_binom

definition alive source, line 66

Type

forall {R : realType} {n : nat}, {set {ffun 'I_n -> bool}} -> R

Definition

Definition alive n (S : {set {ffun 'I_n -> bool}}) : R := (S != set0)%:R.

Used by 30 declarations in 4 files

this file: life, alive_ge0, alive_le1, alive_mono, alive0, alive_sqr, life_sum, sat_prefix_lenE
GaussianApplications.RandomSAT.Pivotal: survival, kill, killE, alive_restrict_le, survival_le_geom, life_meanS, delay, delay_cons, pivot_sqr, delay_cross, delay_cons_sqr, secondS, life_var_succ_le
GaussianApplications.RandomSAT.Replacement: killE_forced
GaussianApplications.RandomSAT.Forcing: head_forced_ind, del_mean, era_mean, del_mean0, era_mean0, del_meanS, short_survival, clause_avg_short_survival

fixpoint restrict source, line 69

Type

forall {n k : nat},
{set {ffun 'I_n -> bool}} -> seq (clause n k) -> {set {ffun 'I_n -> bool}}

Definition

Fixpoint restrict n k (S : {set {ffun 'I_n -> bool}}) (s : seq (clause n k)) :
    {set {ffun 'I_n -> bool}} :=
  if s is c :: s' then restrict (add_clause S c) s' else S.

The solutions in S of a sequence of clauses.

Used by 16 declarations in 3 files

this file: restrictE, restrict_sub, restrict_mono, life_sum, prefix_satE
GaussianApplications.RandomSAT.Pivotal: tuple_avg, alive_restrict_le
GaussianApplications.RandomSAT.Forcing: head_forced_reduction, head_forced_ind, restrict_add_clause, clause_avg_tuple_avg, head_forced, mem_restrict_rename, forced_rename, forced_coord_mean, forced_frac

fixpoint life source, line 74

Type

forall {R : realType} {n k : nat}, {set {ffun 'I_n -> bool}} -> seq (clause n k) -> R

Definition

Fixpoint life n k (S : {set {ffun 'I_n -> bool}}) (s : seq (clause n k)) : R :=
  if s is c :: s' then alive (add_clause S c) + life (add_clause S c) s' else 0.

The number of nonempty solution sets along the sequence: the lifetime.

Used by 13 declarations in 2 files

this file: life0, life_ge0, life_le, life_mono, life_sum, sat_prefix_lenE
GaussianApplications.RandomSAT.Pivotal: life_mean, life_var, delay, delay_cross, delay_cons_sqr, secondS, life_var_succ_le

lemma add_clause_sub source, line 77

forall [n k : nat] (S : {set {ffun 'I_n -> bool}}) (c : clause n k),
add_clause S c \subset S

Statement as written in the source

Lemma add_clause_sub n k (S : {set {ffun 'I_n -> bool}}) (c : clause n k) :
  add_clause S c \subset S.

Used by 4 declarations in 2 files

GaussianApplications.RandomSAT.Pivotal: kill_ge0, alive_restrict_le, delay_cons_sqr
GaussianApplications.RandomSAT.Forcing: survival_antitone

lemma add_clause_mono source, line 81

forall [n k : nat] [S T : {set {ffun 'I_n -> bool}}] (c : clause n k),
S \subset T -> add_clause S c \subset add_clause T c

Statement as written in the source

Lemma add_clause_mono n k (S T : {set {ffun 'I_n -> bool}}) (c : clause n k) :
  S \subset T -> add_clause S c \subset add_clause T c.

Used by 3 declarations in 2 files

this file: life_mono
GaussianApplications.RandomSAT.Pivotal: alive_restrict_le, delay_cross

lemma add_clauseC source, line 88

forall [n k r : nat] (S : {set {ffun 'I_n -> bool}}) (c : clause n k) (d : clause n r),
add_clause (add_clause S c) d = add_clause (add_clause S d) c

Statement as written in the source

Lemma add_clauseC n k r (S : {set {ffun 'I_n -> bool}}) (c : clause n k)
    (d : clause n r) :
  add_clause (add_clause S c) d = add_clause (add_clause S d) c.

Used by 1 declaration in 1 file

GaussianApplications.RandomSAT.Pivotal: delay_cons

lemma add_clause0 source, line 93

forall [n k : nat] (c : clause n k), add_clause set0 c = set0

Statement as written in the source

Lemma add_clause0 n k (c : clause n k) : add_clause set0 c = set0.

Used by 4 declarations in 2 files

this file: life0
GaussianApplications.RandomSAT.Pivotal: kill0, pivot_sqr, delay_cross

lemma restrictE source, line 96

forall [n k : nat] (S : {set {ffun 'I_n -> bool}}) (s : seq (clause n k)),
restrict S s = [set x in S | all (clause_sat x) s]

Statement as written in the source

Lemma restrictE n k (S : {set {ffun 'I_n -> bool}}) (s : seq (clause n k)) :
  restrict S s = [set x in S | all (clause_sat x) s].

Used by 8 declarations in 3 files

this file: restrict_sub, restrict_mono, prefix_satE, prefix_sat_le
GaussianApplications.RandomSAT.Pivotal: survival0_set
GaussianApplications.RandomSAT.Forcing: head_forced_reduction, restrict_add_clause, mem_restrict_rename

lemma restrict_sub source, line 103

forall [n k : nat] (S : {set {ffun 'I_n -> bool}}) (s : seq (clause n k)),
restrict S s \subset S

Statement as written in the source

Lemma restrict_sub n k (S : {set {ffun 'I_n -> bool}}) (s : seq (clause n k)) :
  restrict S s \subset S.

Used by 1 declaration in 1 file

GaussianApplications.RandomSAT.Pivotal: alive_restrict_le

lemma restrict_mono source, line 107

forall [n k : nat] [S T : {set {ffun 'I_n -> bool}}] (s : seq (clause n k)),
S \subset T -> restrict S s \subset restrict T s

Statement as written in the source

Lemma restrict_mono n k (S T : {set {ffun 'I_n -> bool}})
    (s : seq (clause n k)) :
  S \subset T -> restrict S s \subset restrict T s.

Used by 1 declaration in 1 file

GaussianApplications.RandomSAT.Pivotal: survival_mono

lemma alive_ge0 source, line 115

forall {R : realType} [n : nat] (S : {set {ffun 'I_n -> bool}}), 0 <= alive S

Statement as written in the source

Lemma alive_ge0 n (S : {set {ffun 'I_n -> bool}}) : 0 <= alive S.

Used by 4 declarations in 2 files

this file: life_ge0
GaussianApplications.RandomSAT.Pivotal: survival_ge0, kill_le1, alive_restrict_le

lemma alive_le1 source, line 118

forall {R : realType} [n : nat] (S : {set {ffun 'I_n -> bool}}), alive S <= 1

Statement as written in the source

Lemma alive_le1 n (S : {set {ffun 'I_n -> bool}}) : alive S <= 1.

Used by 4 declarations in 2 files

this file: life_le
GaussianApplications.RandomSAT.Pivotal: survival_le1, kill_le1, alive_restrict_le

lemma alive_mono source, line 121

forall {R : realType} [n : nat] [S T : {set {ffun 'I_n -> bool}}],
S \subset T -> alive S <= alive T

Statement as written in the source

Lemma alive_mono n (S T : {set {ffun 'I_n -> bool}}) :
  S \subset T -> alive S <= alive T.

Used by 5 declarations in 3 files

this file: life_mono
GaussianApplications.RandomSAT.Pivotal: survival_mono, kill_ge0, alive_restrict_le
GaussianApplications.RandomSAT.Forcing: head_forced_ind

lemma alive0 source, line 131

forall {R : realType} (n : nat), alive (set0 : {set {ffun 'I_n -> bool}}) = 0

Statement as written in the source

Lemma alive0 n : alive (set0 : {set {ffun 'I_n -> bool}}) = 0.

Used by 4 declarations in 2 files

this file: life0
GaussianApplications.RandomSAT.Pivotal: survival0_set, alive_restrict_le, delay_cross

lemma alive_sqr source, line 134

forall {R : realType} [n : nat] (S0 : {set {ffun 'I_n -> bool}}), alive S0 ^+ 2 = alive S0

Statement as written in the source

Lemma alive_sqr n (S : {set {ffun 'I_n -> bool}}) : alive S ^+ 2 = alive S.

lemma life0 source, line 137

forall {R : realType} [n k : nat] (s : seq (clause n k)), life set0 s = 0

Statement as written in the source

Lemma life0 n k (s : seq (clause n k)) : life set0 s = 0.

Used by 1 declaration in 1 file

GaussianApplications.RandomSAT.Pivotal: delay_cross

lemma life_ge0 source, line 140

forall {R : realType} [n k : nat] (S : {set {ffun 'I_n -> bool}}) (s : seq (clause n k)),
0 <= life S s

Statement as written in the source

Lemma life_ge0 n k (S : {set {ffun 'I_n -> bool}}) (s : seq (clause n k)) :
  0 <= life S s.

Used by 1 declaration in 1 file

GaussianApplications.RandomSAT.Pivotal: life_mean_ge0

lemma life_le source, line 144

forall {R : realType} [n k : nat] (S : {set {ffun 'I_n -> bool}}) (s : seq (clause n k)),
life S s <= (size s)%:R

Statement as written in the source

Lemma life_le n k (S : {set {ffun 'I_n -> bool}}) (s : seq (clause n k)) :
  life S s <= (size s)%:R.

lemma life_mono source, line 151

forall {R : realType} [n k : nat] [S T : {set {ffun 'I_n -> bool}}] (s : seq (clause n k)),
S \subset T -> life S s <= life T s

Statement as written in the source

Lemma life_mono n k (S T : {set {ffun 'I_n -> bool}}) (s : seq (clause n k)) :
  S \subset T -> life S s <= life T s.

lemma life_sum source, line 159

forall {R : realType} [n k : nat] (S0 : {set {ffun 'I_n -> bool}}) (s : seq (clause n k)),
life S0 s = \sum_(j < size s) alive (restrict S0 (take j.+1 s))

The lifetime counts the nonempty solution sets of the prefixes.

Statement as written in the source

Lemma life_sum n k (S : {set {ffun 'I_n -> bool}}) (s : seq (clause n k)) :
  life S s = \sum_(j < size s) alive (restrict S (take j.+1 s)).

Used by 1 declaration in 1 file

this file: sat_prefix_lenE

Arguments add_clause {n k} S c.
Arguments alive {R n} S.
Arguments restrict {n k} S s.
Arguments life {R n k} S s.

sectionprefix

Context {R : realType}.

lemma all_take_tnth source, line 176

forall [T : Type] [M : nat] (t : M.-tuple T) (p : pred T) (m : nat),
all p (take m t) = [forall i, (i < m)%N ==> p (tnth t i)]

Statement as written in the source

Lemma all_take_tnth (T : Type) M (t : M.-tuple T) (p : pred T) m :
  all p (take m t) = [forall i : 'I_M, (i < m)%N ==> p (tnth t i)].

Used by 1 declaration in 1 file

this file: prefix_satE

lemma prefix_satE source, line 194

forall [n k M : nat] (t : M.-tuple (clause n k)) (m : nat),
prefix_sat t m = (restrict [set: {ffun 'I_n -> bool}] (take m t) != set0)

Statement as written in the source

Lemma prefix_satE n k M (t : M.-tuple (clause n k)) m :
  prefix_sat t m = (restrict [set: {ffun 'I_n -> bool}] (take m t) != set0).

Used by 3 declarations in 1 file

this file: prefix_sat0, prefix_sat_le, sat_prefix_lenE

lemma prefix_sat0 source, line 202

forall [n k M : nat] (t : M.-tuple (clause n k)), prefix_sat t 0

Statement as written in the source

Lemma prefix_sat0 n k M (t : M.-tuple (clause n k)) : prefix_sat t 0.

Used by 1 declaration in 1 file

this file: sat_prefix_lenE

lemma prefix_sat_le source, line 205

forall [n k M : nat] [t : M.-tuple (clause n k)] [m m' : nat],
(m' <= m)%N -> prefix_sat t m -> prefix_sat t m'

Statement as written in the source

Lemma prefix_sat_le n k M (t : M.-tuple (clause n k)) m m' :
  (m' <= m)%N -> prefix_sat t m -> prefix_sat t m'.

Used by 1 declaration in 1 file

this file: sat_prefix_lenE

lemma sum_ltn_ord source, line 213

forall [M V : nat], (V <= M)%N -> (\sum_(j < M) (j < V))%N = V

Statement as written in the source

Lemma sum_ltn_ord M V : (V <= M)%N -> (\sum_(j < M) (j < V)%N)%N = V.

Used by 1 declaration in 1 file

this file: sat_prefix_lenE

lemma sat_prefix_lenE main result source, line 228

forall {R : realType} [n k M : nat] (t : M.-tuple (clause n k)),
(sat_prefix_len t)%:R = life [set: {ffun 'I_n -> bool}] t

The length of the longest satisfiable prefix is the lifetime of the full solution set.

Main result, as the README states it

For a tuple t of M clauses, the largest satisfiable prefix length sat_prefix_len t, the cap M included, is the lifetime life [set: _] t: the number of nonempty solution sets among those of the nonempty prefixes of t. #|clause n k| = 'C(n, k) 2^k. For k <= n, the uniform mean over clause n.+1 k.+1 is the mixture, with weights 1 - k.+1/n.+1 and k.+1/n.+1, of the clauses without the first variable (a uniform clause of size k.+1 on the other n variables) and of the clauses with it (a uniform sign and a uniform clause of size k on the others).

Statement as written in the source

Lemma sat_prefix_lenE n k M (t : M.-tuple (clause n k)) :
  (sat_prefix_len t)%:R = life [set: {ffun 'I_n -> bool}] t :> R.

Used by 1 declaration in 1 file

GaussianApplications.RandomSAT.Variance: sat_capped_varE

The first variable of a clause: a clause on n.+1 variables is a clause on the last n variables, with the first variable absent or present with a sign.

sectionclause_split

definition prepend source, line 258

Type

forall [n : nat],
option bool -> {ffun 'I_n -> option bool} -> {ffun 'I_n.+1 -> option bool}

Definition

Definition prepend n (b : option bool) (c : {ffun 'I_n -> option bool}) :
    {ffun 'I_n.+1 -> option bool} :=
  [ffun i => if unlift ord0 i is Some j then c j else b].

Used by 8 declarations in 1 file

this file: prepend0, prepend_lift, ftail_prepend, prepend_ftail, card_support_prepend, proper_prepend, cabsent, cpresent

definition ftail source, line 262

Type

forall [n : nat], {ffun 'I_n.+1 -> option bool} -> {ffun 'I_n -> option bool}

Definition

Definition ftail n (c : {ffun 'I_n.+1 -> option bool}) :
    {ffun 'I_n -> option bool} :=
  [ffun j => c (lift ord0 j)].

Used by 7 declarations in 1 file

this file: ftail_prepend, prepend_ftail, proper_ftail, proper_ftail_None, proper_ftail_Some, csplit, cjoin_surj

lemma prepend0 source, line 266

forall [n : nat] (b : option bool) (c : {ffun 'I_n -> option bool}), prepend b c ord0 = b

Statement as written in the source

Lemma prepend0 n b (c : {ffun 'I_n -> option bool}) : prepend b c ord0 = b.

Used by 4 declarations in 2 files

this file: card_support_prepend, cjoinK
GaussianApplications.RandomSAT.Forcing: sat_cabsent, sat_cpresent

lemma prepend_lift source, line 269

forall [n : nat] (b : option bool) (c : {ffun 'I_n -> option bool}) (j : 'I_n.+1.-1),
prepend b c (lift ord0 j) = c j

Statement as written in the source

Lemma prepend_lift n b (c : {ffun 'I_n -> option bool}) j :
  prepend b c (lift ord0 j) = c j.

Used by 4 declarations in 2 files

this file: ftail_prepend, card_support_prepend
GaussianApplications.RandomSAT.Forcing: sat_cabsent, sat_cpresent

lemma ftail_prepend source, line 273

forall [n : nat] (b : option bool) (c : {ffun 'I_n -> option bool}),
ftail (prepend b c) = c

Statement as written in the source

Lemma ftail_prepend n b (c : {ffun 'I_n -> option bool}) :
  ftail (prepend b c) = c.

Used by 1 declaration in 1 file

this file: cjoinK

lemma prepend_ftail source, line 277

forall [n : nat] (c : {ffun 'I_n.+1 -> option bool}), prepend (c ord0) (ftail c) = c

Statement as written in the source

Lemma prepend_ftail n (c : {ffun 'I_n.+1 -> option bool}) :
  prepend (c ord0) (ftail c) = c.

Used by 2 declarations in 1 file

this file: proper_ftail, cjoin_surj

lemma card_support source, line 284

forall [n : nat] (c : {ffun 'I_n -> option bool}),
#|[set i | c i != None]| = (\sum_i (c i != None))%N

Statement as written in the source

Lemma card_support n (c : {ffun 'I_n -> option bool}) :
  #|[set i | c i != None]| = (\sum_i (c i != None))%N.

Used by 3 declarations in 1 file

this file: card_support_prepend, card_clause0, card_clause0S

lemma card_support_prepend source, line 288

forall [n : nat] (b : option bool) (c : {ffun 'I_n -> option bool}),
#|[set i | prepend b c i != None]| = ((b != None) + #|[set i | c i != None]|)%N

Statement as written in the source

Lemma card_support_prepend n b (c : {ffun 'I_n -> option bool}) :
  #|[set i | prepend b c i != None]| =
    ((b != None) + #|[set i | c i != None]|)%N.

Used by 2 declarations in 1 file

this file: proper_prepend, proper_ftail

lemma proper_prepend source, line 296

forall [n k : nat]
  (b : option bool)
  [c : {ffun 'I_n -> option bool}],
proper_clause k c -> proper_clause ((b != None) + k) (prepend b c)

Statement as written in the source

Lemma proper_prepend n k b (c : {ffun 'I_n -> option bool}) :
  proper_clause k c -> proper_clause ((b != None) + k) (prepend b c).

Used by 2 declarations in 1 file

this file: cabsent, cpresent

lemma proper_ftail source, line 300

forall [n k : nat] [c : {ffun 'I_n.+1 -> option bool}],
proper_clause ((c ord0 != None) + k) c -> proper_clause k (ftail c)

Statement as written in the source

Lemma proper_ftail n k (c : {ffun 'I_n.+1 -> option bool}) :
  proper_clause ((c ord0 != None) + k) c -> proper_clause k (ftail c).

Used by 2 declarations in 1 file

this file: proper_ftail_None, proper_ftail_Some

definition cabsent source, line 307

Type

forall [n k : nat], clause n k -> clause n.+1 k

Definition

Definition cabsent n k (c : clause n k) : clause n.+1 k :=
  exist _ (prepend None (val c)) (proper_prepend None (valP c)).

Used by 5 declarations in 2 files

this file: cjoin, cjoinK, unif_mean_clause_split
GaussianApplications.RandomSAT.Forcing: sat_cabsent, csplit_absent

definition cpresent source, line 310

Type

forall [n k : nat], clause n k -> bool -> clause n.+1 k.+1

Definition

Definition cpresent n k (c : clause n k) (b : bool) : clause n.+1 k.+1 :=
  exist _ (prepend (Some b) (val c)) (proper_prepend (Some b) (valP c)).

Used by 5 declarations in 2 files

this file: cjoin, cjoinK, unif_mean_clause_split
GaussianApplications.RandomSAT.Forcing: sat_cpresent, csplit_present

lemma proper_ftail_None source, line 313

forall [n k : nat] [c : clause n.+1 k],
\val c ord0 = None -> proper_clause k (ftail (\val c))

Statement as written in the source

Lemma proper_ftail_None n k (c : clause n.+1 k) :
  val c ord0 = None -> proper_clause k (ftail (val c)).

Used by 3 declarations in 1 file

this file: csplit, cjoinK, cjoin_surj

lemma proper_ftail_Some source, line 319

forall [n k : nat] [c : clause n.+1 k.+1] [b : bool],
\val c ord0 = Some b -> proper_clause k (ftail (\val c))

Statement as written in the source

Lemma proper_ftail_Some n k (c : clause n.+1 k.+1) b :
  val c ord0 = Some b -> proper_clause k (ftail (val c)).

Used by 3 declarations in 1 file

this file: csplit, cjoinK, cjoin_surj

definition csplit source, line 325

Type

forall [n k : nat], clause n.+1 k.+1 -> clause n k.+1 + clause n k * bool

Definition

Definition csplit n k (c : clause n.+1 k.+1) :
    clause n k.+1 + clause n k * bool :=
  match val c ord0 as o return val c ord0 = o -> _ with
  | None => fun e => inl (exist _ (ftail (val c)) (proper_ftail_None e))
  | Some b => fun e => inr (exist _ (ftail (val c)) (proper_ftail_Some e), b)
  end erefl.

Used by 12 declarations in 2 files

this file: cjoinK, csplitK, cjoin_bij
GaussianApplications.RandomSAT.Forcing: del_ok, era_ok, era_del_ok, sat_del_ok, era_ok_sat, deleted_cons, erased_cons, csplit_absent, csplit_present

definition cjoin source, line 332

Type

forall [n k : nat], clause n k.+1 + clause n k * bool -> clause n.+1 k.+1

Definition

Definition cjoin n k (x : clause n k.+1 + clause n k * bool) :
    clause n.+1 k.+1 :=
  match x with
  | inl c => cabsent c
  | inr (c, b) => cpresent c b
  end.

Used by 5 declarations in 1 file

this file: cjoinK, cjoin_surj, csplitK, cjoin_bij, unif_mean_clause_split

lemma cjoinK source, line 339

forall [n k : nat], cancel (cjoin (k:=k)) (csplit (k:=k))

Statement as written in the source

Lemma cjoinK n k : cancel (@cjoin n k) (@csplit n k).

Used by 4 declarations in 2 files

this file: csplitK, cjoin_bij
GaussianApplications.RandomSAT.Forcing: csplit_absent, csplit_present

lemma cjoin_surj source, line 352

forall [n k : nat] (c : clause n.+1 k.+1),
exists x : clause n k.+1 + clause n k * bool, cjoin x = c

Statement as written in the source

Lemma cjoin_surj n k (c : clause n.+1 k.+1) : exists x, cjoin x = c.

Used by 1 declaration in 1 file

this file: csplitK

lemma csplitK source, line 361

forall [n k : nat], cancel (csplit (k:=k)) (cjoin (k:=k))

Statement as written in the source

Lemma csplitK n k : cancel (@csplit n k) (@cjoin n k).

Used by 3 declarations in 2 files

this file: cjoin_bij
GaussianApplications.RandomSAT.Forcing: sat_del_ok, era_ok_sat

lemma cjoin_bij source, line 364

forall n k : nat, bijective (cjoin (k:=k))

Statement as written in the source

Lemma cjoin_bij n k : bijective (@cjoin n k).

Used by 2 declarations in 1 file

this file: card_clauseSS, unif_mean_clause_split

lemma card_clause0 source, line 368

forall n : nat, #|{: clause n 0}| = 1%N

The number of proper signed k-clauses on n variables.

Statement as written in the source

Lemma card_clause0 n : #|{: clause n 0}| = 1%N.

Used by 1 declaration in 1 file

this file: card_clause

lemma card_clause0S source, line 382

forall k : nat, #|{: clause 0 k.+1}| = 0%N

Statement as written in the source

Lemma card_clause0S k : #|{: clause 0 k.+1}| = 0%N.

Used by 1 declaration in 1 file

this file: card_clause

lemma card_clauseSS source, line 388

forall n k : nat,
#|{: clause n.+1 k.+1}| = (#|{: clause n k.+1}| + #|{: clause n k}| * 2)%N

Statement as written in the source

Lemma card_clauseSS n k :
  #|{: clause n.+1 k.+1}| = (#|{: clause n k.+1}| + #|{: clause n k}| * 2)%N.

Used by 1 declaration in 1 file

this file: card_clause

lemma card_clause main result source, line 394

forall n k : nat, #|{: clause n k}| = ('C(n, k) * 2 ^ k)%N

Main result

Stated in the README together with sat_prefix_lenE.

Statement as written in the source

Lemma card_clause n k : #|{: clause n k}| = ('C(n, k) * 2 ^ k)%N.

Used by 3 declarations in 2 files

this file: card_clause_gt0, unif_mean_clause_split
GaussianApplications.RandomSAT.Replacement: killE_forced

lemma card_clause_gt0 source, line 403

forall [n k : nat], (k <= n)%N -> (0 < #|{: clause n k}|)%N

Statement as written in the source

Lemma card_clause_gt0 n k : (k <= n)%N -> (0 < #|{: clause n k}|)%N.

Used by 8 declarations in 3 files

GaussianApplications.RandomSAT.Replacement: kill_replacement
GaussianApplications.RandomSAT.Forcing: Ck, Ck1, Ck, Ck1, Ck1
GaussianApplications.RandomSAT.Variance: trunc_le_forced, sat_variance_bound_explicit

lemma unif_mean_clause_split main result source, line 412

forall [R : realType] [n k : nat] (f : clause n.+1 k.+1 -> R),
(k <= n)%N ->
unif_mean f =
(1 - k.+1%:R / n.+1%:R) * unif_mean (fun c : clause n k.+1 => f (cabsent c)) +
k.+1%:R / n.+1%:R *
unif_mean (fun c : clause n k => unif_mean (fun b : bool => f (cpresent c b)))

The uniform clause on n.+1 variables: its first variable is absent with probability 1 - k.+1 / n.+1, and the rest is a uniform clause of size k.+1; or present with probability k.+1 / n.+1, with a uniform sign, and the rest is a uniform clause of size k.

Main result

Stated in the README together with sat_prefix_lenE.

Statement as written in the source

Lemma unif_mean_clause_split (R : realType) n k (f : clause n.+1 k.+1 -> R) :
  (k <= n)%N ->
  unif_mean f =
  (1 - k.+1%:R / n.+1%:R) * unif_mean (fun c : clause n k.+1 => f (cabsent c)) +
  k.+1%:R / n.+1%:R *
    unif_mean (fun c : clause n k =>
      unif_mean (fun b : bool => f (cpresent c b))).

Used by 2 declarations in 1 file

GaussianApplications.RandomSAT.Forcing: del_meanS, era_meanS

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.