GaussianAnalysisRocq library documentation
Main resultsGlossary
On this page
GaussianApplicationsapplicationsRandomSATForcing

Random k-SAT: integrated forcing

GaussianApplications.RandomSAT.Forcingapplications/RandomSAT/Forcing.v796 lines61 lemmas and theorems, 16 definitionssource
Imports 5 library modules and 10 external

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

Imported by 1

Part of target T7 of phase 12 (see Model.v). A Rocq formalization of the credited argument of the proposition 'Integrated forcing' of 'A limiting satisfiability threshold for every fixed clause size' (family 235 of the OpenAI math collection, revision 1581d4cbd, source/sections/forcing.tex), following the Lean development of the collection (lean/OAI/Probability/RandomSAT):

Lean: binomialMean (Binomial.lean, line 17)

Lean: binomial_replacement_sum_le (Binomial.lean, line 162)

Lean: head_forced_reduction (Forcing.lean, line 88)

Lean: deletedMean_eq_binomial (Forcing.lean, line 239)

Lean: erasedMean_replacement (Forcing.lean, line 265)

Lean: integrated_head_forcing (Forcing.lean, line 386)

Lean: forced_coordinate_mean (Forcing.lean, line 493)

Lean: forcedFractionMean_eq_head (Forcing.lean, line 525)

The clauses have size k.+1 and n.+1 variables, with k < n.

  • binom_mean p m f is the mean of f over a binomial number of successes in m trials of probability p, defined by its recursion on the first trial. binom_rep_sum_le sums the replacement differences rep_diff P g j d = P (j - d) - P (j + (g - 1) d) of a nonincreasing P with values in [0, 1], by telescoping (sum_shift_diff_le).
  • If the first variable is forced by the clauses t, then deleting it, that is dropping the clauses that contain it, leaves a satisfiable formula, and erasing it, that is removing its literal from these clauses, leaves an unsatisfiable one (head_forced_reduction).
  • The number of clauses that contain the first variable is binomial with p = k.+1 / n.+1, and the other clauses are uniform of size k.+1 on the other n variables (del_mean_binom). Erasing, then replacing each shortened clause by a block of g clauses of size k.+1 (kill_replacement of Replacement.v), costs at most a^-k per shortened clause (era_mean_replacement).
  • integrated_head_forcing: for 1 <= k < n, a > 0 with 1 / (n + 1) <= a^-k and g >= 2 (k + 1) a, the probabilities head_forced n k j that the first variable is forced by j clauses satisfy

sum_(j <= M) head_forced n k j <= g M p + (M + 1) M p a^-k.

The manuscript erases the last variable; here, as in the Lean development, the first. The manuscript bounds the binomial weights by (k M / n)^d / d!; here, as in the Lean development, the replacement differences are summed under the binomial mean of the cap M (binom_rep_sum_le), which gives the term g M p instead of the manuscript's (k M / n) e^(k M / n) g; at M = 2^(k+1) n this removes the factor e^(k 2^(k+1)) from the constant.

Main results

ResultsStatement
integrated_head_forcingforced_frac_head
For 1 <= k < n, a > 0 with 1 / (n + 1) <= a^-k, an integer g >= 2 (k + 1) a and p = (k + 1) / (n + 1), the probabilities h_j that the first variable is forced by j independent uniform clauses of size k + 1 on n + 1 variables satisfy sum_(j <= M) h_j <= g M p + (M + 1) M p a^-k for every M. The mean fraction of forced variables after j clauses is h_j.

Declarations77 exported, 12 local

lemma, theoremdefinitioninstancelocal

The mean of f over a binomial number of successes in m trials of probability p, by its recursion on the first trial.

sectionbinom_mean
Context {R : realType}.
fixpoint binom_mean source, line 75
Type
forall {R : realType}, R -> nat -> (nat -> R) -> R
Definition
Fixpoint binom_mean (p : R) (m : nat) (f : nat -> R) : R :=
  if m is m'.+1 then
    (1 - p) * binom_mean p m' f + p * binom_mean p m' (fun d => f d.+1)
  else f 0%N.
Used by 17 declarations in 1 file
lemma eq_binom_mean source, line 80 
forall {R : realType} (p : R) [m : nat] [f g : nat -> R],
(forall d : nat, (d <= m)%N -> f d = g d) -> binom_mean p m f = binom_mean p m g
Statement as written in the source
Lemma eq_binom_mean p m (f g : nat -> R) :
  (forall d, (d <= m)%N -> f d = g d) -> binom_mean p m f = binom_mean p m g.
Used by 4 declarations in 1 file
lemma binom_mean_cst source, line 88 
forall {R : realType} (p : R) (m : nat) (c : R), binom_mean p m (fun=> c) = c
Statement as written in the source
Lemma binom_mean_cst p m (c : R) : binom_mean p m (fun=> c) = c.
Used by 1 declaration in 1 file
lemma binom_meanD source, line 91 
forall {R : realType} (p : R) (m : nat) (f g : nat -> R),
binom_mean p m (fun d : nat => f d + g d) = binom_mean p m f + binom_mean p m g
Statement as written in the source
Lemma binom_meanD p m (f g : nat -> R) :
  binom_mean p m (fun d => f d + g d) = binom_mean p m f + binom_mean p m g.
Used by 3 declarations in 1 file
lemma binom_meanZ source, line 95 
forall {R : realType} (p : R) (m : nat) (c : R) (f : nat -> R),
binom_mean p m (fun d : nat => c * f d) = c * binom_mean p m f
Statement as written in the source
Lemma binom_meanZ p m (c : R) (f : nat -> R) :
  binom_mean p m (fun d => c * f d) = c * binom_mean p m f.
Used by 3 declarations in 1 file
lemma binom_meanN source, line 99 
forall {R : realType} (p : R) (m : nat) (f : nat -> R),
binom_mean p m (fun d : nat => - f d) = - binom_mean p m f
Statement as written in the source
Lemma binom_meanN p m (f : nat -> R) :
  binom_mean p m (fun d => - f d) = - binom_mean p m f.
Used by 1 declaration in 1 file
lemma binom_meanB source, line 105 
forall {R : realType} (p : R) (m : nat) (f g : nat -> R),
binom_mean p m (fun d : nat => f d - g d) = binom_mean p m f - binom_mean p m g
Statement as written in the source
Lemma binom_meanB p m (f g : nat -> R) :
  binom_mean p m (fun d => f d - g d) = binom_mean p m f - binom_mean p m g.
Used by 1 declaration in 1 file
lemma ler_binom_mean source, line 109 
forall {R : realType}
  [p : join_Num_POrderNmodule_between_Algebra_BaseAddUMagma_and_Order_Preorder R] 
  [m : nat] [f g : nat -> R],
0 <= p ->
p <= 1 ->
(forall d : nat, (d <= m)%N -> f d <= g d) -> binom_mean p m f <= binom_mean p m g
Statement as written in the source
Lemma ler_binom_mean p m (f g : nat -> R) : 0 <= p -> p <= 1 ->
  (forall d, (d <= m)%N -> f d <= g d) -> binom_mean p m f <= binom_mean p m g.
Used by 3 declarations in 1 file
lemma binom_mean_id source, line 118 
forall {R : realType} (p : R) (m : nat), binom_mean p m [eta Algebra.natmul 1] = m%:R * p
Statement as written in the source
Lemma binom_mean_id p m : binom_mean p m (fun d => d%:R) = m%:R * p.
Used by 2 declarations in 1 file
lemma binom_mean_trials_le source, line 128 
forall {R : realType}
  [p : join_Num_POrderNmodule_between_Algebra_BaseAddUMagma_and_Order_Preorder R] 
  (m : nat) [f : nat -> R],
0 <= p ->
p <= 1 ->
{homo f : d d' / (d <= d')%N >-> d <= d'} -> binom_mean p m f <= binom_mean p m.+1 f

More trials give more successes.

Statement as written in the source
Lemma binom_mean_trials_le p m (f : nat -> R) : 0 <= p -> p <= 1 ->
  {homo f : d d' / (d <= d')%N >-> d <= d'} ->
  binom_mean p m f <= binom_mean p m.+1 f.
Used by 1 declaration in 1 file
lemma binom_mean_trials source, line 138 
forall {R : realType}
  [p : join_Num_POrderNmodule_between_Algebra_BaseAddUMagma_and_Order_Preorder R]
  [m m' : nat] [f : nat -> R],
0 <= p ->
p <= 1 ->
{homo f : d d' / (d <= d')%N >-> d <= d'} ->
(m <= m')%N -> binom_mean p m f <= binom_mean p m' f
Statement as written in the source
Lemma binom_mean_trials p m m' (f : nat -> R) : 0 <= p -> p <= 1 ->
  {homo f : d d' / (d <= d')%N >-> d <= d'} -> (m <= m')%N ->
  binom_mean p m f <= binom_mean p m' f.
Used by 1 declaration in 1 file
lemma binom_mean_sum source, line 147 
forall {R : realType} (p : R) (m : nat) [I : finType] (F : I -> nat -> R),
binom_mean p m (fun d : nat => \sum_i F i d) = \sum_i binom_mean p m (F i)
Statement as written in the source
Lemma binom_mean_sum p m (I : finType) (F : I -> nat -> R) :
  binom_mean p m (fun d => \sum_i F i d) = \sum_i binom_mean p m (F i).
Used by 1 declaration in 1 file
lemma unif_mean_binom_mean source, line 154 
forall {R : realType} [T : finType] (p : R) (m : nat) (f : nat -> T -> R),
unif_mean (fun x : T => binom_mean p m (f^~ x)) =
binom_mean p m (fun d : nat => unif_mean (f d))
Statement as written in the source
Lemma unif_mean_binom_mean (T : finType) p m (f : nat -> T -> R) :
  unif_mean (fun x => binom_mean p m (fun d => f d x)) =
  binom_mean p m (fun d => unif_mean (f d)).
Used by 2 declarations in 1 file
lemma sum_shift_diff_le source, line 164 
forall {R : realType} [P : nat -> R] (l b : nat),
(forall j : nat, 0 <= P j) ->
(forall j : nat, P j <= 1) -> \sum_(j < l) (P j - P (j + b)%N) <= b%:R

Telescoping: sum_(j < l) (P j - P (j + b)) <= b for P with values in [0, 1].

Statement as written in the source
Lemma sum_shift_diff_le (P : nat -> R) l b :
  (forall j, 0 <= P j) -> (forall j, P j <= 1) ->
  \sum_(j < l) (P j - P (j + b)%N) <= b%:R.
Used by 1 declaration in 1 file
definition rep_diff source, line 187
Type
forall {R : realType}, (nat -> R) -> nat -> nat -> nat -> R
Definition
Definition rep_diff (P : nat -> R) (g j d : nat) : R :=
  P (j - d)%N - P (j + (g - 1) * d)%N.
Used by 5 declarations in 1 file
lemma rep_diff_mono source, line 190 
forall {R : realType} [P : nat -> R] (g j : nat),
{homo P : x y / (x <= y)%N >-> y <= x} ->
{homo rep_diff P g j : d d' / (d <= d')%N >-> d <= d'}
Statement as written in the source
Lemma rep_diff_mono (P : nat -> R) g j :
  {homo P : x y / (x <= y)%N >-> y <= x} ->
  {homo rep_diff P g j : d d' / (d <= d')%N >-> d <= d'}.
Used by 1 declaration in 1 file
lemma rep_diff_sum_le source, line 199 
forall {R : realType} [P : nat -> R] [g : nat] (l d : nat),
(forall j : nat, 0 <= P j) ->
(forall j : nat, P j <= 1) -> (0 < g)%N -> \sum_(j < l) rep_diff P g j d <= g%:R * d%:R
Statement as written in the source
Lemma rep_diff_sum_le (P : nat -> R) g l d :
  (forall j, 0 <= P j) -> (forall j, P j <= 1) -> (1 <= g)%N ->
  \sum_(j < l) rep_diff P g j d <= g%:R * d%:R.
Used by 1 declaration in 1 file
lemma binom_rep_sum_le source, line 219 
forall {R : realType} [P : nat -> R]
  [p : join_Num_POrderNmodule_between_Algebra_BaseAddUMagma_and_Order_Preorder R] 
  [g : nat] (M : nat),
0 <= p ->
p <= 1 ->
{homo P : x y / (x <= y)%N >-> y <= x} ->
(forall j : nat, 0 <= P j) ->
(forall j : nat, P j <= 1) ->
(0 < g)%N -> \sum_(j < M.+1) binom_mean p j (rep_diff P g j) <= g%:R * M%:R * p
Statement as written in the source
Lemma binom_rep_sum_le (P : nat -> R) p g M : 0 <= p -> p <= 1 ->
  {homo P : x y / (x <= y)%N >-> y <= x} ->
  (forall j, 0 <= P j) -> (forall j, P j <= 1) -> (1 <= g)%N ->
  \sum_(j < M.+1) binom_mean p j (rep_diff P g j) <= g%:R * M%:R * p.
Used by 1 declaration in 1 file

The first variable of an assignment on n.+1 variables, and the rest.

sectionassignment_split
Variable n : nat.
Local Notation asg := {ffun 'I_n -> bool}.
Local Notation asg1 := {ffun 'I_n.+1 -> bool}.
definition atail source, line 243
Type
forall [n : nat], {ffun 'I_n.+1 -> bool} -> {ffun 'I_n -> bool}
Definition
Definition atail (s : asg1) : asg := [ffun j => s (lift ord0 j)].
Used by 5 declarations in 1 file
definition aext source, line 245
Type
forall [n : nat], {ffun 'I_n -> bool} -> bool -> {ffun 'I_n.+1 -> bool}
Definition
Definition aext (s : asg) (b : bool) : asg1 :=
  [ffun i => if unlift ord0 i is Some j then s j else b].
Used by 4 declarations in 1 file
lemma atail_ext source, line 248 
forall [n : nat] (s : {ffun 'I_n -> bool}) (b : bool), atail (aext s b) = s
Statement as written in the source
Lemma atail_ext s b : atail (aext s b) = s.
Used by 1 declaration in 1 file
lemma aext0 source, line 251 
forall [n : nat] (s : {ffun 'I_n -> bool}) (b : bool), aext s b ord0 = b
Statement as written in the source
Lemma aext0 s b : aext s b ord0 = b.
Used by 1 declaration in 1 file
lemma exists_ordS source, line 254 
forall [n : nat] (P : pred 'I_n.+1),
[exists i, P i] = P ord0 || [exists j, P (lift ord0 j)]
Statement as written in the source
Lemma exists_ordS (P : pred 'I_n.+1) :
  [exists i, P i] = P ord0 || [exists j : 'I_n, P (lift ord0 j)].
Used by 2 declarations in 1 file
lemma sat_cabsent source, line 264 
forall [n k : nat] (s : {ffun 'I_n.+1 -> bool}) (d : clause n k),
clause_sat s (cabsent d) = clause_sat (atail s) d
Statement as written in the source
Lemma sat_cabsent k (s : asg1) (d : clause n k) :
  clause_sat s (cabsent d) = clause_sat (atail s) d.
Used by 2 declarations in 1 file
lemma sat_cpresent source, line 271 
forall [n k : nat] (s : {ffun 'I_n.+1 -> bool}) (q : clause n k) (b : bool),
clause_sat s (cpresent q b) = (b == s ord0) || clause_sat (atail s) q
Statement as written in the source
Lemma sat_cpresent k (s : asg1) (q : clause n k) b :
  clause_sat s (cpresent q b) = (b == s ord0) || clause_sat (atail s) q.
Used by 1 declaration in 1 file
sectionerasure
Context {R : realType} (n k : nat).
Local Notation asg := {ffun 'I_n -> bool}.
Local Notation asg1 := {ffun 'I_n.+1 -> bool}.
Local Notation C1 := (clause n.+1 k.+1).
definition del_ok source, line 289
Type
forall [n k : nat], {ffun 'I_n -> bool} -> clause n.+1 k.+1 -> bool
Definition
Definition del_ok (s : asg) (c : C1) : bool :=
  if csplit c is inl d then clause_sat s d else true.

The constraints left on the other variables by a clause on n.+1 variables, once the first variable is deleted (its clauses are dropped) or erased (its literal is removed from its clauses).

Used by 4 declarations in 1 file
definition era_ok source, line 292
Type
forall [n k : nat], {ffun 'I_n -> bool} -> clause n.+1 k.+1 -> bool
Definition
Definition era_ok (s : asg) (c : C1) : bool :=
  match csplit c with inl d => clause_sat s d
  | inr (q, _) => clause_sat s q end.
Used by 4 declarations in 1 file
definition deleted source, line 296
Type
forall [n k : nat],
{set {ffun 'I_n -> bool}} -> seq (clause n.+1 k.+1) -> {set {ffun 'I_n -> bool}}
Definition
Definition deleted (S : {set asg}) (t : seq C1) : {set asg} :=
  [set s in S | all (del_ok s) t].
Used by 7 declarations in 1 file
definition erased source, line 299
Type
forall [n k : nat],
{set {ffun 'I_n -> bool}} -> seq (clause n.+1 k.+1) -> {set {ffun 'I_n -> bool}}
Definition
Definition erased (S : {set asg}) (t : seq C1) : {set asg} :=
  [set s in S | all (era_ok s) t].
Used by 6 declarations in 1 file
lemma era_del_ok source, line 302 
forall [n k : nat] [s : {ffun 'I_n -> bool}] [c : clause n.+1 k.+1],
era_ok s c -> del_ok s c
Statement as written in the source
Lemma era_del_ok s c : era_ok s c -> del_ok s c.
Used by 1 declaration in 1 file
lemma erased_sub source, line 305 
forall [n k : nat] (S0 : {set {ffun 'I_n -> bool}}) (t : seq (clause n.+1 k.+1)),
erased S0 t \subset deleted S0 t
Statement as written in the source
Lemma erased_sub S t : erased S t \subset deleted S t.
Used by 1 declaration in 1 file
lemma sat_del_ok source, line 311 
forall [n k : nat] [s : {ffun 'I_n.+1 -> bool}] [c : clause n.+1 k.+1],
clause_sat s c -> del_ok (atail s) c
Statement as written in the source
Lemma sat_del_ok (s : asg1) (c : C1) : clause_sat s c -> del_ok (atail s) c.
Used by 1 declaration in 1 file
lemma era_ok_sat source, line 317 
forall [n k : nat] [s : {ffun 'I_n -> bool}] (b : bool) [c : clause n.+1 k.+1],
era_ok s c -> clause_sat (aext s b) c
Statement as written in the source
Lemma era_ok_sat (s : asg) b (c : C1) : era_ok s c -> clause_sat (aext s b) c.
Used by 1 declaration in 1 file
lemma head_forced_reduction source, line 326 
forall [n k : nat] [t : seq (clause n.+1 k.+1)],
ord0 \in forced (restrict [set: {ffun 'I_n.+1 -> bool}] t) ->
deleted [set: {ffun 'I_n -> bool}] t != set0 /\ erased [set: {ffun 'I_n -> bool}] t = set0

If the first variable is forced by the clauses t, then deleting it leaves a satisfiable formula and erasing it an unsatisfiable one.

Statement as written in the source
Lemma head_forced_reduction (t : seq C1) :
  ord0 \in forced (restrict [set: asg1] t) ->
  deleted [set: asg] t != set0 /\ erased [set: asg] t = set0.
Used by 1 declaration in 1 file
lemma head_forced_ind source, line 341 
forall {R : realType} [n k : nat] (t : seq (clause n.+1 k.+1)),
((ord0 \in forced (restrict [set: {ffun 'I_n.+1 -> bool}] t))%:R : R) <=
(alive (deleted [set: {ffun 'I_n -> bool}] t) - alive (erased [set: {ffun 'I_n -> bool}] t)
 :
 R)
Statement as written in the source
Lemma head_forced_ind (t : seq C1) :
  (ord0 \in forced (restrict [set: asg1] t))%:R <=
  alive (deleted [set: asg] t) - alive (erased [set: asg] t) :> R.
Used by 1 declaration in 1 file
lemma deleted_cons source, line 351 
forall [n k : nat] (S0 : {set {ffun 'I_n -> bool}}) (c : clause n.+1 k.+1)
  (t : seq (clause n.+1 k.+1)),
deleted S0 (c :: t) =
match csplit c with
| inl d => deleted (add_clause S0 d) t
| inr _ => deleted S0 t
end
Statement as written in the source
Lemma deleted_cons S c t :
  deleted S (c :: t) =
  if csplit c is inl d then deleted (add_clause S d) t else deleted S t.
Used by 1 declaration in 1 file
lemma erased_cons source, line 359 
forall [n k : nat] (S0 : {set {ffun 'I_n -> bool}}) (c : clause n.+1 k.+1)
  (t : seq (clause n.+1 k.+1)),
erased S0 (c :: t) =
match csplit c with
| inl d => erased (add_clause S0 d) t
| inr (q, _) => erased (add_clause S0 q) t
end
Statement as written in the source
Lemma erased_cons S c t :
  erased S (c :: t) =
  match csplit c with
  | inl d => erased (add_clause S d) t
  | inr (q, _) => erased (add_clause S q) t
  end.
Used by 1 declaration in 1 file
lemma csplit_absent source, line 372 
forall [n k : nat] (d : clause n k.+1), csplit (cabsent d) = inl d
Statement as written in the source
Lemma csplit_absent n k (d : clause n k.+1) : csplit (cabsent d) = inl d.
Used by 2 declarations in 1 file
lemma csplit_present source, line 375 
forall [n k : nat] (q : clause n k) (b : bool), csplit (cpresent q b) = inr (q, b)
Statement as written in the source
Lemma csplit_present n k (q : clause n k) b :
  csplit (cpresent q b) = inr (q, b).
Used by 2 declarations in 1 file

Means over consecutive blocks of clauses, and their commutation.

sectiontuple_avg_facts
Context {R : realType} (n : nat).
Local Notation asg := {ffun 'I_n -> bool}.
lemma restrict_add_clause source, line 384 
forall [n k r : nat] (S : {set {ffun 'I_n -> bool}}) (c : clause n r)
  (s : seq (clause n k)),
restrict (add_clause S c) s = add_clause (restrict S s) c
Statement as written in the source
Lemma restrict_add_clause k r (S : {set asg}) (c : clause n r)
    (s : seq (clause n k)) :
  restrict (add_clause S c) s = add_clause (restrict S s) c.
Used by 1 declaration in 1 file
lemma tuple_avg_add source, line 392 
forall {R : realType} [n : nat] (k t u : nat) (f : {set {ffun 'I_n -> bool}} -> R)
  (S : {set {ffun 'I_n -> bool}}),
tuple_avg k (t + u) f S = tuple_avg k t (tuple_avg k u f) S
Statement as written in the source
Lemma tuple_avg_add k t u (f : {set asg} -> R) S :
  tuple_avg k (t + u) f S = tuple_avg k t (tuple_avg k u f) S.
Used by 1 declaration in 1 file
lemma clause_avg_tuple_avg source, line 400 
forall {R : realType} [n : nat] (k r t : nat) (f : {set {ffun 'I_n -> bool}} -> R)
  (S : {set {ffun 'I_n -> bool}}),
clause_avg r (tuple_avg k t f) S = tuple_avg k t (clause_avg r f) S
Statement as written in the source
Lemma clause_avg_tuple_avg k r t (f : {set asg} -> R) S :
  clause_avg r (tuple_avg k t f) S = tuple_avg k t (clause_avg r f) S.
Used by 1 declaration in 1 file
lemma ler_tuple_avg_cst source, line 410 
forall {R : realType} [n k : nat] (t : nat) (f : {set {ffun 'I_n -> bool}} -> R) 
  (c : R) (S0 : {set {ffun 'I_n -> bool}}),
(0 < #|{: clause n k}|)%N ->
tuple_avg k t (fun T : {set {ffun 'I_n -> bool}} => f T - c) S0 = tuple_avg k t f S0 - c
Statement as written in the source
Lemma ler_tuple_avg_cst k t (f : {set asg} -> R) (c : R) S :
  (0 < #|{: clause n k}|)%N ->
  tuple_avg k t (fun T => f T - c) S = tuple_avg k t f S - c.
Used by 1 declaration in 1 file
lemma survival_antitone source, line 418 
forall {R : realType} [n k : nat] (m : nat) (S0 : {set {ffun 'I_n -> bool}}),
(0 < #|{: clause n k}|)%N -> survival k m.+1 S0 <= survival k m S0
Statement as written in the source
Lemma survival_antitone k m (S : {set asg}) : (0 < #|{: clause n k}|)%N ->
  survival k m.+1 S <= survival (R := R) k m S.
Used by 1 declaration in 1 file
sectionerasure_means
Context {R : realType} (n k : nat).
Hypothesis kn : (k < n)%N.
Local Notation asg := {ffun 'I_n -> bool}.
Local Notation C1 := (clause n.+1 k.+1).
let p section-local source, line 434 
Let p : R := k.+1%:R / n.+1%:R.
Used by 5 declarations in 1 file
let Ck section-local source, line 436 
Let Ck : (0 < #|{: clause n k}|)%N.
let Ck1 section-local source, line 439 
Let Ck1 : (0 < #|{: clause n k.+1}|)%N.
lemma p_ge0 source, line 442 
forall {R : realType} (n k : nat), 0 <= k.+1%:R / n.+1%:R
Statement as written in the source
Lemma p_ge0 : 0 <= p.
Used by 2 declarations in 1 file
lemma p_le1 source, line 445 
forall {R : realType} [n k : nat], (k < n)%N -> k.+1%:R / n.+1%:R <= 1
Statement as written in the source
Lemma p_le1 : p <= 1.
Used by 2 declarations in 1 file
definition del_mean source, line 448
Type
forall {R : realType} [n : nat], nat -> nat -> {set {ffun 'I_n -> bool}} -> R
Definition
Definition del_mean m (S : {set asg}) : R :=
  unif_mean (fun t : m.-tuple C1 => alive (deleted S t)).
Used by 4 declarations in 1 file
definition era_mean source, line 451
Type
forall {R : realType} [n : nat], nat -> nat -> {set {ffun 'I_n -> bool}} -> R
Definition
Definition era_mean m (S : {set asg}) : R :=
  unif_mean (fun t : m.-tuple C1 => alive (erased S t)).
Used by 4 declarations in 1 file
lemma del_mean0 source, line 454 
forall {R : realType} [n : nat] (k : nat) (S : {set {ffun 'I_n -> bool}}),
del_mean k 0 S = alive S
Statement as written in the source
Lemma del_mean0 S : del_mean 0 S = alive S.
Used by 1 declaration in 1 file
lemma era_mean0 source, line 460 
forall {R : realType} [n : nat] (k : nat) (S : {set {ffun 'I_n -> bool}}),
era_mean k 0 S = alive S
Statement as written in the source
Lemma era_mean0 S : era_mean 0 S = alive S.
Used by 1 declaration in 1 file
lemma del_meanS source, line 466 
forall {R : realType} [n k : nat],
(k < n)%N ->
forall (m : nat) (S0 : {set {ffun 'I_n -> bool}}),
del_mean k m.+1 S0 =
(1 - k.+1%:R / n.+1%:R) * clause_avg k.+1 (del_mean k m) S0 +
k.+1%:R / n.+1%:R * del_mean k m S0
Statement as written in the source
Lemma del_meanS m S :
  del_mean m.+1 S = (1 - p) * clause_avg k.+1 (del_mean m) S + p * del_mean m S.
Used by 1 declaration in 1 file
lemma era_meanS source, line 481 
forall {R : realType} [n k : nat],
(k < n)%N ->
forall (m : nat) (S0 : {set {ffun 'I_n -> bool}}),
era_mean k m.+1 S0 =
(1 - k.+1%:R / n.+1%:R) * clause_avg k.+1 (era_mean k m) S0 +
k.+1%:R / n.+1%:R * clause_avg k (era_mean k m) S0
Statement as written in the source
Lemma era_meanS m S :
  era_mean m.+1 S = (1 - p) * clause_avg k.+1 (era_mean m) S +
    p * clause_avg k (era_mean m) S.
Used by 1 declaration in 1 file
lemma del_mean_binom source, line 498 
forall {R : realType} [n k : nat],
(k < n)%N ->
forall (m : nat) (S0 : {set {ffun 'I_n -> bool}}),
del_mean k m S0 =
binom_mean (k.+1%:R / n.+1%:R) m (fun d : nat => survival k.+1 (m - d) S0)

Deleting the first variable: the clauses that contain it, a binomial number of them, are dropped, and the others are uniform k.+1-clauses on the remaining n variables.

Statement as written in the source
Lemma del_mean_binom m S :
  del_mean m S = binom_mean p m (fun d => survival k.+1 (m - d) S).
Used by 1 declaration in 1 file
sectionerased_replacement
Context {R : realType} (n k g : nat) (a : R).
Hypotheses (k1 : (1 <= k)%N) (kn : (k < n)%N) (a0 : 0 < a).
Hypotheses (hsmall : (n.+1%:R)^-1 <= a^-1 ^+ k) (hg : 2 * k.+1%:R * a <= g%:R).
Local Notation asg := {ffun 'I_n -> bool}.
Local Notation C1 := (clause n.+1 k.+1).
let eps section-local source, line 519 
Let eps : R := a^-1 ^+ k.
Used by 4 declarations in 1 file
let p section-local source, line 520 
Let p : R := k.+1%:R / n.+1%:R.
Used by 1 declaration in 1 file
let Ck section-local source, line 522 
Let Ck : (0 < #|{: clause n k}|)%N.
Used by 1 declaration in 1 file
let Ck1 section-local source, line 525 
Let Ck1 : (0 < #|{: clause n k.+1}|)%N.
let eps0 section-local source, line 528 
Let eps0 : 0 <= eps.
lemma g_ge1 source, line 531 
forall {R : realType} [k g : nat] [a : R], 0 < a -> 2 * k.+1%:R * a <= g%:R -> (0 < g)%N
Statement as written in the source
Lemma g_ge1 : (1 <= g)%N.
Used by 2 declarations in 1 file
lemma short_survival source, line 539 
forall {R : realType} [n k g : nat] [a : R],
(0 < k)%N ->
(k < n)%N ->
0 < a ->
n.+1%:R^-1 <= a^-1 ^+ k ->
2 * k.+1%:R * a <= g%:R ->
forall T : {set {ffun 'I_n -> bool}}, survival k.+1 g T - a^-1 ^+ k <= survival k 1 T

A block of g clauses of size k.+1 survives at most as often as one clause of size k, up to eps.

Statement as written in the source
Lemma short_survival (T : {set asg}) :
  survival k.+1 g T - eps <= survival (R := R) k 1 T.
Used by 1 declaration in 1 file
lemma clause_avg_short_survival source, line 551 
forall {R : realType} [n k g : nat] [a : R],
(0 < k)%N ->
(k < n)%N ->
0 < a ->
n.+1%:R^-1 <= a^-1 ^+ k ->
2 * k.+1%:R * a <= g%:R ->
forall (t : nat) (S0 : {set {ffun 'I_n -> bool}}),
survival k.+1 (t + g) S0 - a^-1 ^+ k <= clause_avg k (survival k.+1 t) S0
Statement as written in the source
Lemma clause_avg_short_survival t (S : {set asg}) :
  survival k.+1 (t + g) S - eps <= clause_avg k (survival k.+1 t) S.
Used by 1 declaration in 1 file
lemma clause_avg_subr source, line 561 
forall {R : realType} [n r : nat] (f : {set {ffun 'I_n -> bool}} -> R) 
  (c : R) (S0 : {set {ffun 'I_n -> bool}}),
(0 < #|{: clause n r}|)%N ->
clause_avg r (fun T : {set {ffun 'I_n -> bool}} => f T - c) S0 = clause_avg r f S0 - c
Statement as written in the source
Lemma clause_avg_subr r (f : {set asg} -> R) (c : R) S :
  (0 < #|{: clause n r}|)%N ->
  clause_avg r (fun T => f T - c) S = clause_avg r f S - c.
lemma era_mean_replacement source, line 568 
forall {R : realType} [n k g : nat] [a : R],
(0 < k)%N ->
(k < n)%N ->
0 < a ->
n.+1%:R^-1 <= a^-1 ^+ k ->
2 * k.+1%:R * a <= g%:R ->
forall (m : nat) (S0 : {set {ffun 'I_n -> bool}}),
binom_mean (k.+1%:R / n.+1%:R) m
  (fun d : nat => survival k.+1 (m - d + g * d) S0 - d%:R * a^-1 ^+ k) <=
era_mean k m S0

Erasing the first variable and replacing each shortened clause by a block of g clauses of size k.+1.

Statement as written in the source
Lemma era_mean_replacement m (S : {set asg}) :
  binom_mean p m (fun d => survival k.+1 (m - d + g * d) S - d%:R * eps) <=
  era_mean (R := R) k m S.
Used by 1 declaration in 1 file
lemma survival_le source, line 594 
forall (R : realType) [n k x y : nat] (S0 : {set {ffun 'I_n -> bool}}),
(0 < #|{: clause n k}|)%N -> (x <= y)%N -> survival k y S0 <= survival k x S0
Statement as written in the source
Lemma survival_le (R : realType) n k x y (S : {set {ffun 'I_n -> bool}}) :
  (0 < #|{: clause n k}|)%N -> (x <= y)%N ->
  survival (R := R) k y S <= survival k x S.
Used by 1 declaration in 1 file
sectionhead_forcing
Context {R : realType} (n k g : nat) (a : R).
Hypotheses (k1 : (1 <= k)%N) (kn : (k < n)%N) (a0 : 0 < a).
Hypotheses (hsmall : (n.+1%:R)^-1 <= a^-1 ^+ k) (hg : 2 * k.+1%:R * a <= g%:R).
Local Notation asg := {ffun 'I_n -> bool}.
Local Notation asg1 := {ffun 'I_n.+1 -> bool}.
Local Notation C1 := (clause n.+1 k.+1).
let eps section-local source, line 610 
Let eps : R := a^-1 ^+ k.
Used by 2 declarations in 1 file
let p section-local source, line 611 
Let p : R := k.+1%:R / n.+1%:R.
Used by 2 declarations in 1 file
let P section-local source, line 612 
Let P (j : nat) : R := survival k.+1 j [set: asg].
Used by 2 declarations in 1 file
let Ck1 section-local source, line 614 
Let Ck1 : (0 < #|{: clause n k.+1}|)%N.
definition head_forced source, line 618
Type
forall {R : realType}, nat -> nat -> nat -> R
Definition
Definition head_forced m : R :=
  unif_mean (fun t : m.-tuple C1 =>
    (ord0 \in forced (restrict [set: asg1] t))%:R).

The probability that the first variable is forced by m clauses.

Used by 5 declarations in 2 files
lemma head_forced_mean_le source, line 622 
forall {R : realType} [n k g : nat] [a : R],
(0 < k)%N ->
(k < n)%N ->
0 < a ->
n.+1%:R^-1 <= a^-1 ^+ k ->
2 * k.+1%:R * a <= g%:R ->
forall m : nat,
head_forced n k m <=
binom_mean (k.+1%:R / n.+1%:R) m
  (rep_diff ((survival k.+1)^~ [set: {ffun 'I_n -> bool}]) g m) +
m%:R * (k.+1%:R / n.+1%:R) * a^-1 ^+ k
Statement as written in the source
Lemma head_forced_mean_le m :
  head_forced m <= binom_mean p m (rep_diff P g m) + m%:R * p * eps.
Used by 1 declaration in 1 file
lemma integrated_head_forcing main result source, line 644 
forall {R : realType} [n k g : nat] [a : R],
(0 < k)%N ->
(k < n)%N ->
0 < a ->
n.+1%:R^-1 <= a^-1 ^+ k ->
2 * k.+1%:R * a <= g%:R ->
forall M : nat,
\sum_(j < M.+1) head_forced n k j <=
g%:R * M%:R * (k.+1%:R / n.+1%:R) + M.+1%:R * M%:R * (k.+1%:R / n.+1%:R) * a^-1 ^+ k
Main result, as the README states it

For 1 <= k < n, a > 0 with 1 / (n + 1) <= a^-k, an integer g >= 2 (k + 1) a and p = (k + 1) / (n + 1), the probabilities h_j that the first variable is forced by j independent uniform clauses of size k + 1 on n + 1 variables satisfy sum_(j <= M) h_j <= g M p + (M + 1) M p a^-k for every M. The mean fraction of forced variables after j clauses is h_j.

Statement as written in the source
Lemma integrated_head_forcing M :
  \sum_(j < M.+1) head_forced j <= g%:R * M%:R * p + M.+1%:R * M%:R * p * eps.
Used by 1 declaration in 1 file

Renaming the variables by a permutation preserves the uniform law of the clauses and moves the forced variables accordingly.

sectionrenaming
Variables (N k : nat) (sg : {perm 'I_N}).
Local Notation asg := {ffun 'I_N -> bool}.
definition rename_ffun source, line 673
Type
forall [N : nat], {perm 'I_N} -> {ffun 'I_N -> option bool} -> {ffun 'I_N -> option bool}
Definition
Definition rename_ffun (c : {ffun 'I_N -> option bool}) :
    {ffun 'I_N -> option bool} :=
  [ffun i => c (sg i)].
Used by 1 declaration in 1 file
lemma proper_rename source, line 677 
forall [N k : nat] (sg : {perm 'I_N}) (c : clause N k),
proper_clause k (rename_ffun sg (\val c))
Statement as written in the source
Lemma proper_rename (c : clause N k) : proper_clause k (rename_ffun (val c)).
Used by 1 declaration in 1 file
definition rename_clause source, line 687
Type
forall [N k : nat], {perm 'I_N} -> clause N k -> clause N k
Definition
Definition rename_clause (c : clause N k) : clause N k :=
  exist (fun f => proper_clause k f) _ (proper_rename c).
Used by 3 declarations in 1 file
definition rename_asg source, line 690
Type
forall [N : nat], {perm 'I_N} -> {ffun 'I_N -> bool} -> {ffun 'I_N -> bool}
Definition
Definition rename_asg (s : asg) : asg := [ffun i => s (sg i)].
Used by 4 declarations in 1 file
lemma sat_rename source, line 692 
forall [N k : nat] (sg : {perm 'I_N}) (s : {ffun 'I_N -> bool}) (c : clause N k),
clause_sat (rename_asg sg s) (rename_clause sg c) = clause_sat s c
Statement as written in the source
Lemma sat_rename (s : asg) (c : clause N k) :
  clause_sat (rename_asg s) (rename_clause c) = clause_sat s c.
Used by 1 declaration in 1 file
lemma rename_asg_bij source, line 700 
forall [N : nat] (sg : {perm 'I_N}), bijective (rename_asg sg)
Statement as written in the source
Lemma rename_asg_bij : bijective rename_asg.
lemma rename_clause_bij source, line 708 
forall [N : nat] (k : nat) (sg : {perm 'I_N}), bijective (rename_clause sg)
Statement as written in the source
Lemma rename_clause_bij N k (sg : {perm 'I_N}) :
  bijective (@rename_clause N k sg).
Used by 1 declaration in 1 file
sectionforced_symmetry
Context {R : realType} (n k : nat).
Local Notation asg1 := {ffun 'I_n.+1 -> bool}.
Local Notation C1 := (clause n.+1 k.+1).
definition rename_tuple source, line 720
Type
forall [n k m : nat],
{perm 'I_n.+1} -> m.-tuple (clause n.+1 k.+1) -> m.-tuple (clause n.+1 k.+1)
Definition
Definition rename_tuple m (sg : {perm 'I_n.+1}) (t : m.-tuple C1) :
    m.-tuple C1 :=
  map_tuple (rename_clause sg) t.
Used by 3 declarations in 1 file
lemma rename_tuple_bij source, line 724 
forall [n : nat] (k m : nat) (sg : {perm 'I_n.+1}), bijective (rename_tuple sg)
Statement as written in the source
Lemma rename_tuple_bij m sg : bijective (@rename_tuple m sg).
Used by 1 declaration in 1 file
lemma mem_restrict_rename source, line 732 
forall [n k m : nat] (sg : {perm 'I_n.+1}) (t : m.-tuple (clause n.+1 k.+1))
  (s : {ffun 'I_n.+1 -> bool}),
(s \in restrict [set: {ffun 'I_n.+1 -> bool}] (rename_tuple sg t)) =
(rename_asg sg^-1 s \in restrict [set: {ffun 'I_n.+1 -> bool}] t)
Statement as written in the source
Lemma mem_restrict_rename m sg (t : m.-tuple C1) (s : asg1) :
  (s \in restrict [set: asg1] (rename_tuple sg t)) =
  (rename_asg (sg^-1)%g s \in restrict [set: asg1] t).
Used by 1 declaration in 1 file
lemma forced_rename source, line 742 
forall [n k m : nat] (sg : {perm 'I_n.+1}) (t : m.-tuple (clause n.+1 k.+1)) (i : 'I_n.+1),
(i \in forced (restrict [set: {ffun 'I_n.+1 -> bool}] (rename_tuple sg t))) =
(sg i \in forced (restrict [set: {ffun 'I_n.+1 -> bool}] t))
Statement as written in the source
Lemma forced_rename m sg (t : m.-tuple C1) i :
  (i \in forced (restrict [set: asg1] (rename_tuple sg t))) =
  (sg i \in forced (restrict [set: asg1] t)).
Used by 1 declaration in 1 file
lemma forced_coord_mean source, line 763 
forall {R : realType} [n : nat] (k m : nat) (i : 'I_n.+1),
unif_mean
  (fun t : m.-tuple (clause n.+1 k.+1) =>
   (i \in forced (restrict [set: {ffun 'I_n.+1 -> bool}] t))%:R) =
head_forced n k m
Statement as written in the source
Lemma forced_coord_mean m (i : 'I_n.+1) :
  unif_mean (fun t : m.-tuple C1 =>
    (i \in forced (restrict [set: asg1] t))%:R) =
  head_forced (R := R) n k m.
Used by 1 declaration in 1 file
definition forced_frac source, line 774
Type
forall {R : realType}, nat -> nat -> nat -> R
Definition
Definition forced_frac m : R :=
  unif_mean (fun t : m.-tuple C1 =>
    #|forced (restrict [set: asg1] t)|%:R / n.+1%:R).

The mean fraction of forced variables.

Used by 2 declarations in 2 files
lemma card_as_sum source, line 778 
forall {R : realType} [n : nat] (A : {set 'I_n.+1}), #|A|%:R = \sum_(i < n.+1) (i \in A)%:R
Statement as written in the source
Lemma card_as_sum (A : {set 'I_n.+1}) :
  #|A|%:R = \sum_(i : 'I_n.+1) (i \in A)%:R :> R.
Used by 1 declaration in 1 file
lemma forced_frac_head main result source, line 785 
forall {R : realType} (n k m : nat), forced_frac n k m = head_forced n k m
Main result

Stated in the README together with integrated_head_forcing.

Statement as written in the source
Lemma forced_frac_head m : forced_frac m = head_forced (R := R) n k m.
Used by 1 declaration in 1 file
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.