GaussianAnalysisRocq library documentation
Main resultsGlossary
On this page
GaussianApplicationsapplicationsSKGapTwoSpin

The uniform two-spin inequality

GaussianApplications.SKGap.TwoSpinapplications/SKGap/TwoSpin.v769 lines47 lemmas and theorems, 13 definitionssource
Imports 3 library modules and 14 external

External: HB.structures, mathcomp.classical.all_ssreflect_compat, mathcomp.algebra.algebraic_hierarchy.ssralg, mathcomp.algebra.numeric_hierarchy.ssrnum, mathcomp.algebra.ssrint, mathcomp.algebra.matrix, mathcomp.algebra.sesquilinear, mathcomp.classical.boolp, mathcomp.reals.reals, mathcomp.analysis.sequences, mathcomp.analysis.exp, mathcomp.algebra.ring_tactic, mathcomp.algebra.field_tactic, mathcomp.algebra.arithmetic_tactic

Imported by 1

Part of target T4 of phase 12 (AGENTS.md, section Phase 12). A Rocq formalization of the credited argument of the lemma 'Uniform two-spin inequality' of 'Cutoff throughout the high-temperature Sherrington-Kirkpatrick phase' (family 227 of the OpenAI math collection, revision 1581d4cbd, appendices/entropy.tex). The remainder of the expansion in t is bounded by a real polynomial certificate instead of the manuscript's complex Cauchy estimate, as the Lean module of the collection does:

Lean: pair_cubic_signed_bound (SKRatio/Calculus/TwoSpin.lean)

The coefficients of the certificate are those of the unique polynomial R with t^3 R equal to the numerator of C - L; they were computed independently and agree with those of the Lean module. Nothing is copied from the Lean code.

  • The pair law: for |a|, |b| <= 1 and |t| <= 1/4, plaw a b t F is the mean of F under the law proportional to (1 + a x)(1 + b y)(1 + t x y) on {-1, 1}^2; pcm and pcv are the conditional means and variances, and pg1, pg2 the half-differences p + r (y - b) and q + r (x - a).
  • ts_certificate, ts_coef_bound: the coefficient C of the manuscript is the leading term L = 1 + a b t + (1 - a^2 - b^2 + 2 a^2 b^2) t^2 up to 30000 |t|^3.
  • pair_factorization: the mixed energy plus the correction term is P_0 Q, as in the manuscript; pair_signed_mean_lower: Q >= - 30000 |t|^3 (p^2 + q^2) for |t| <= 1/1000.
  • plaw_energy_ge, pprefactor_bounds: the energies are at least (3/5) (1 - a^2) p^2 and (3/5) (1 - b^2) q^2, and 0 <= P_0 <= (4/3) (1 - a^2) (1 - b^2).
  • pair_two_spin: the inequality of the lemma for the pair law, with t_0 = 1/1000 and C_0 = 70000 (the manuscript's example is t_0 = 1/100, C_0 = 22000; the Lean theorem has C_0 = 1920000).
  • ising_two_spin: the inequality of the lemma for the Ising law of a symmetric A with zero diagonal, for i != j with |tanh A_ij| <= 1/1000: nu[D_i f D_j f] >= - nu[(t + 2 t^2 m_i m_j) v_i v_j d_i f d_j f] - 70000 |t|^3 (nu[v_i (d_i f)^2] + nu[v_j (d_j f)^2]), with t = tanh A_ij. The proof conditions on the spins outside i and j (ising_mean_block, ising_weight_block).

Main results

ResultsStatement
pair_two_spinising_two_spin
The uniform two-spin inequality. For the pair law proportional to (1 + a x)(1 + b y)(1 + t x y) with |a|, |b| <= 1 and |t| <= 1/1000: the mixed energy plus the correction term (t + 2 t^2 m_i m_j) v_i v_j d_i f d_j f is at least - 70000 |t|^3 times the sum of the two energies (pair_two_spin; the remainder in t by a real polynomial certificate, ts_coef_bound). For the Ising law of a symmetric A with zero diagonal and i != j with |tanh A_ij| <= 1/1000: nu[D_i f D_j f] >= - nu[(t + 2 t^2 m_i m_j) v_i v_j d_i f d_j f] - 70000 |t|^3 (nu[v_i (d_i f)^2] + nu[v_j (d_j f)^2]) with t = tanh A_ij (ising_two_spin).

Declarations60 exported

lemma, theoremdefinitioninstancelocal
sectiontwo_spin_certificate
Variable R : realType.
Implicit Types a b t : R.
definition ts_lead source, line 60
Type
forall [R : realType], R -> R -> R -> R
Definition
Definition ts_lead a b t : R :=
  1 + a * b * t + (1 - a ^+ 2 - b ^+ 2 + 2 * a ^+ 2 * b ^+ 2) * t ^+ 2.
Used by 7 declarations in 1 file
definition ts_coef source, line 63
Type
forall [R : realType], R -> R -> R -> R
Definition
Definition ts_coef a b t : R :=
  (1 - t) / ((1 + a * t) * (1 + b * t)) +
  (t + 2 * t ^+ 2 * ((a + t) / (1 + a * t)) * ((b + t) / (1 + b * t))) *
    ((1 - t ^+ 2) * (1 + a) * (1 + b) * (1 + t)) /
    ((1 + a * t) ^+ 2 * (1 + b * t) ^+ 2).
Used by 3 declarations in 1 file
definition ts_monomials source, line 69
Type
seq (int * nat * nat * nat)
Definition
Definition ts_monomials : seq (int * nat * nat * nat) :=
  [:: (Negz 0, 0, 0, 0); (Negz 0, 0, 1, 0); (Posz 2, 0, 2, 0);
     (Posz 2, 0, 3, 0); (Negz 0, 1, 0, 0); (Posz 4, 1, 1, 0);
     (Posz 2, 1, 2, 0); (Negz 2, 1, 3, 0); (Posz 2, 2, 0, 0);
     (Posz 2, 2, 1, 0); (Negz 5, 2, 2, 0); (Negz 5, 2, 3, 0);
     (Posz 2, 3, 0, 0); (Negz 2, 3, 1, 0); (Negz 5, 3, 2, 0);
     (Posz 1, 0, 0, 1); (Posz 2, 0, 1, 1); (Negz 1, 0, 2, 1);
     (Posz 3, 0, 4, 1); (Posz 2, 1, 0, 1); (Negz 6, 1, 1, 1);
     (Negz 1, 1, 2, 1); (Posz 6, 1, 3, 1); (Negz 0, 1, 4, 1);
     (Negz 1, 2, 0, 1); (Negz 1, 2, 1, 1); (Negz 2, 2, 2, 1);
     (Negz 8, 2, 3, 1); (Negz 5, 2, 4, 1); (Posz 6, 3, 1, 1);
     (Negz 8, 3, 2, 1); (Negz 17, 3, 3, 1); (Posz 3, 4, 0, 1);
     (Negz 0, 4, 1, 1); (Negz 5, 4, 2, 1); (Posz 2, 0, 0, 2);
     (Negz 0, 0, 1, 2); (Negz 2, 0, 2, 2); (Negz 0, 0, 3, 2);
     (Posz 1, 0, 5, 2); (Negz 0, 1, 0, 2); (Negz 6, 1, 1, 2);
     (Negz 14, 1, 2, 2); (Posz 9, 1, 4, 2); (Negz 2, 2, 0, 2);
     (Negz 14, 2, 1, 2); (Negz 3, 2, 2, 2); (Posz 7, 2, 3, 2);
     (Negz 2, 2, 4, 2); (Negz 1, 2, 5, 2); (Negz 0, 3, 0, 2);
     (Posz 7, 3, 2, 2); (Negz 8, 3, 3, 2); (Negz 17, 3, 4, 2);
     (Posz 9, 4, 1, 2); (Negz 2, 4, 2, 2); (Negz 17, 4, 3, 2);
     (Posz 1, 5, 0, 2); (Negz 1, 5, 2, 2); (Negz 1, 0, 0, 3);
     (Negz 3, 0, 1, 3); (Negz 1, 0, 2, 3); (Negz 3, 1, 0, 3);
     (Negz 6, 1, 1, 3); (Negz 2, 1, 2, 3); (Negz 2, 1, 3, 3);
     (Posz 3, 1, 5, 3); (Negz 1, 2, 0, 3); (Negz 2, 2, 1, 3);
     (Negz 9, 2, 2, 3); (Posz 9, 2, 4, 3); (Negz 2, 3, 1, 3);
     (Posz 5, 3, 3, 3); (Negz 2, 3, 4, 3); (Negz 5, 3, 5, 3);
     (Posz 9, 4, 2, 3); (Negz 2, 4, 3, 3); (Negz 17, 4, 4, 3);
     (Posz 3, 5, 1, 3); (Negz 5, 5, 3, 3); (Negz 1, 0, 0, 4);
     (Negz 1, 0, 1, 4); (Negz 1, 1, 0, 4); (Negz 1, 1, 1, 4);
     (Negz 2, 2, 3, 4); (Posz 3, 2, 5, 4); (Negz 2, 3, 2, 4);
     (Posz 3, 3, 4, 4); (Posz 3, 4, 3, 4); (Negz 0, 4, 4, 4);
     (Negz 5, 4, 5, 4); (Posz 3, 5, 2, 4); (Negz 5, 5, 4, 4);
     (Negz 0, 3, 3, 5); (Posz 1, 3, 5, 5); (Posz 1, 5, 3, 5);
     (Negz 1, 5, 5, 5)].
Used by 3 declarations in 1 file
definition ts_rem source, line 104
Type
forall [R : realType], R -> R -> R -> R
Definition
Definition ts_rem a b t : R :=
  \sum_(m <- ts_monomials) m.1.1.1%:~R * a ^+ m.1.1.2 * b ^+ m.1.2 * t ^+ m.2.
Used by 4 declarations in 1 file
lemma ts_certificate source, line 107 
forall [R : realType] (a b t : R),
(1 - t) * (1 + a * t) ^+ 2 * (1 + b * t) ^+ 2 +
(t * (1 + a * t) * (1 + b * t) + 2 * t ^+ 2 * (a + t) * (b + t)) *
((1 - t ^+ 2) * (1 + a) * (1 + b) * (1 + t)) -
ts_lead a b t * ((1 + a * t) ^+ 3 * (1 + b * t) ^+ 3) = t ^+ 3 * ts_rem a b t
Statement as written in the source
Lemma ts_certificate a b t :
  (1 - t) * (1 + a * t) ^+ 2 * (1 + b * t) ^+ 2 +
  (t * (1 + a * t) * (1 + b * t) + 2 * t ^+ 2 * (a + t) * (b + t)) *
    ((1 - t ^+ 2) * (1 + a) * (1 + b) * (1 + t)) -
  ts_lead a b t * ((1 + a * t) ^+ 3 * (1 + b * t) ^+ 3) =
  t ^+ 3 * ts_rem a b t.
Used by 1 declaration in 1 file
lemma monomials_bound source, line 118 
forall [R : realType] (l : seq (int * nat * nat * nat)) [a b t : R],
`|a| <= 1 ->
`|b| <= 1 ->
`|t| <= 1 ->
`|\sum_(m <- l) m.1.1.1%:~R * a ^+ m.1.1.2 * b ^+ m.1.2 * t ^+ m.2| <=
\sum_(m <- l) `|m.1.1.1%:~R : R|
Statement as written in the source
Lemma monomials_bound (l : seq (int * nat * nat * nat)) a b t :
  `|a| <= 1 -> `|b| <= 1 -> `|t| <= 1 ->
  `|\sum_(m <- l) m.1.1.1%:~R * a ^+ m.1.1.2 * b ^+ m.1.2 * t ^+ m.2| <=
  \sum_(m <- l) `|m.1.1.1%:~R : R|.
Used by 1 declaration in 1 file
lemma ts_rem_bound source, line 128 
forall [R : realType] [a b t : R],
`|a| <= 1 -> `|b| <= 1 -> `|t| <= 1 -> `|ts_rem a b t| <= 428
Statement as written in the source
Lemma ts_rem_bound a b t : `|a| <= 1 -> `|b| <= 1 -> `|t| <= 1 ->
  `|ts_rem a b t| <= 428.
Used by 1 declaration in 1 file
lemma affine_half source, line 138 
forall [R : realType] [a t : R], `|a| <= 1 -> `|t| <= 1 / 4 -> 1 / 2 <= 1 + a * t
Statement as written in the source
Lemma affine_half a t : `|a| <= 1 -> `|t| <= 1 / 4 -> 1 / 2 <= 1 + a * t.
Used by 3 declarations in 1 file
lemma ts_coef_remainder source, line 145 
forall [R : realType] [a b t : R],
`|a| <= 1 ->
`|b| <= 1 ->
`|t| <= 1 / 4 ->
ts_coef a b t - ts_lead a b t =
t ^+ 3 * ts_rem a b t / ((1 + a * t) ^+ 3 * (1 + b * t) ^+ 3)
Statement as written in the source
Lemma ts_coef_remainder a b t : `|a| <= 1 -> `|b| <= 1 -> `|t| <= 1 / 4 ->
  ts_coef a b t - ts_lead a b t =
  t ^+ 3 * ts_rem a b t / ((1 + a * t) ^+ 3 * (1 + b * t) ^+ 3).
Used by 1 declaration in 1 file
lemma ts_coef_bound source, line 155 
forall [R : realType] [a b t : R],
`|a| <= 1 ->
`|b| <= 1 -> `|t| <= 1 / 4 -> `|ts_coef a b t - ts_lead a b t| <= 3 * 10 ^+ 4 * `|t| ^+ 3
Statement as written in the source
Lemma ts_coef_bound a b t : `|a| <= 1 -> `|b| <= 1 -> `|t| <= 1 / 4 ->
  `|ts_coef a b t - ts_lead a b t| <= 3 * 10 ^+ 4 * `|t| ^+ 3.
Used by 1 declaration in 1 file
sectiontwo_spin_pair
Variable R : realType.
Implicit Types (a b t p q r : R) (x y : bool).
definition pmean source, line 184
Type
forall [R : realType], R -> R -> (bool -> bool -> R) -> R
Definition
Definition pmean a b (F : bool -> bool -> R) : R :=
  ((1 + a) * (1 + b) * F true true + (1 + a) * (1 - b) * F true false +
   (1 - a) * (1 + b) * F false true + (1 - a) * (1 - b) * F false false) / 4.
Used by 14 declarations in 1 file
definition plaw source, line 188
Type
forall [R : realType], R -> R -> R -> (bool -> bool -> R) -> R
Definition
Definition plaw a b t (F : bool -> bool -> R) : R :=
  pmean a b (fun x y => (1 + t * spin x * spin y) / (1 + t * a * b) * F x y).
Used by 8 declarations in 1 file
definition pcm source, line 191
Type
forall [R : realType], R -> R -> bool -> R
Definition
Definition pcm a t y : R := (a + t * spin y) / (1 + t * a * spin y).
Used by 6 declarations in 1 file
definition pcv source, line 193
Type
forall [R : realType], R -> R -> bool -> R
Definition
Definition pcv a t y : R :=
  (1 - a ^+ 2) * (1 - t ^+ 2) / (1 + t * a * spin y) ^+ 2.
Used by 7 declarations in 1 file
definition pg1 source, line 196
Type
forall [R : realType], R -> R -> R -> bool -> R
Definition
Definition pg1 b p r y : R := p + r * (spin y - b).
Used by 8 declarations in 1 file
definition pg2 source, line 198
Type
forall [R : realType], R -> R -> R -> bool -> R
Definition
Definition pg2 a q r x : R := q + r * (spin x - a).
Used by 7 declarations in 1 file
definition psign source, line 200
Type
forall [R : realType], R -> R -> R -> bool -> bool -> R
Definition
Definition psign a b t x y : R :=
  (spin x * spin y - t) / ((1 + t * a * spin y) * (1 + t * b * spin x)) +
  (t + 2 * t ^+ 2 * pcm a t y * pcm b t x) *
    ((1 - t ^+ 2) * (1 + a * spin x) * (1 + b * spin y) * (1 + t * spin x * spin y)) /
    ((1 + t * a * spin y) ^+ 2 * (1 + t * b * spin x) ^+ 2).
Used by 4 declarations in 1 file
definition pprefactor source, line 206
Type
forall [R : realType], R -> R -> R -> R
Definition
Definition pprefactor a b t : R :=
  (1 - a ^+ 2) * (1 - b ^+ 2) * (1 - t ^+ 2) / (1 + t * a * b).
Used by 3 declarations in 1 file
lemma affine_half' source, line 209 
forall [R : realType] [a t : R] (x : bool),
`|a| <= 1 -> `|t| <= 1 / 4 -> 1 / 2 <= 1 + t * a * spin x
Statement as written in the source
Lemma affine_half' a t x : `|a| <= 1 -> `|t| <= 1 / 4 -> 1 / 2 <= 1 + t * a * spin x.
Used by 5 declarations in 1 file
lemma pcv_eq source, line 215 
forall [R : realType] [a t : R] (y : bool),
`|a| <= 1 -> `|t| <= 1 / 4 -> pcv a t y = 1 - pcm a t y ^+ 2
Statement as written in the source
Lemma pcv_eq a t y : `|a| <= 1 -> `|t| <= 1 / 4 -> pcv a t y = 1 - pcm a t y ^+ 2.
Used by 1 declaration in 1 file
lemma psign_eq source, line 224 
forall [R : realType] [a b t : R] (x y : bool),
`|a| <= 1 ->
`|b| <= 1 ->
`|t| <= 1 / 4 ->
psign a b t x y = spin x * spin y * ts_coef (a * spin x) (b * spin y) (t * spin x * spin y)
Statement as written in the source
Lemma psign_eq a b t x y : `|a| <= 1 -> `|b| <= 1 -> `|t| <= 1 / 4 ->
  psign a b t x y =
  spin x * spin y * ts_coef (a * spin x) (b * spin y) (t * spin x * spin y).
Used by 1 declaration in 1 file
lemma ts_lead_sign source, line 240 
forall [R : realType] (a b t : R) (x y : bool),
ts_lead (a * spin x) (b * spin y) (t * spin x * spin y) = ts_lead a b t
Statement as written in the source
Lemma ts_lead_sign a b t x y :
  ts_lead (a * spin x) (b * spin y) (t * spin x * spin y) = ts_lead a b t.
Used by 1 declaration in 1 file
lemma psign_bound source, line 244 
forall [R : realType] [a b t : R] (x y : bool),
`|a| <= 1 ->
`|b| <= 1 ->
`|t| <= 1 / 4 ->
`|psign a b t x y - spin x * spin y * ts_lead a b t| <= 3 * 10 ^+ 4 * `|t| ^+ 3
Statement as written in the source
Lemma psign_bound a b t x y : `|a| <= 1 -> `|b| <= 1 -> `|t| <= 1 / 4 ->
  `|psign a b t x y - spin x * spin y * ts_lead a b t| <= 3 * 10 ^+ 4 * `|t| ^+ 3.
Used by 1 declaration in 1 file
lemma pair_factorization source, line 253 
forall [R : realType] [a b t : R] (p q r : R),
`|a| <= 1 ->
`|b| <= 1 ->
`|t| <= 1 / 4 ->
plaw a b t
  (fun x y : bool =>
   (spin x - pcm a t y) * pg1 b p r y * ((spin y - pcm b t x) * pg2 a q r x)) +
plaw a b t
  (fun x y : bool =>
   (t + 2 * t ^+ 2 * pcm a t y * pcm b t x) * pcv a t y * pcv b t x * pg1 b p r y *
   pg2 a q r x) =
pprefactor a b t *
pmean 0 0 (fun x y : bool => pg1 b p r y * pg2 a q r x * psign a b t x y)
Statement as written in the source
Lemma pair_factorization a b t p q r : `|a| <= 1 -> `|b| <= 1 -> `|t| <= 1 / 4 ->
  plaw a b t (fun x y => (spin x - pcm a t y) * pg1 b p r y *
    ((spin y - pcm b t x) * pg2 a q r x)) +
  plaw a b t (fun x y => (t + 2 * t ^+ 2 * pcm a t y * pcm b t x) *
    pcv a t y * pcv b t x * pg1 b p r y * pg2 a q r x) =
  pprefactor a b t *
    pmean 0 0 (fun x y => pg1 b p r y * pg2 a q r x * psign a b t x y).
Used by 1 declaration in 1 file
lemma pair_cross_mean source, line 278 
forall [R : realType] (a b p q r : R),
pmean 0 0 (fun x y : bool => spin x * spin y * pg1 b p r y * pg2 a q r x) = r ^+ 2
Statement as written in the source
Lemma pair_cross_mean a b p q r :
  pmean 0 0 (fun x y => spin x * spin y * pg1 b p r y * pg2 a q r x) = r ^+ 2.
Used by 1 declaration in 1 file
lemma pair_grad_bound source, line 282 
forall [R : realType] [a b : R] (p q r : R) (x y : bool),
`|a| <= 1 -> `|b| <= 1 -> `|pg1 b p r y * pg2 a q r x| <= p ^+ 2 + q ^+ 2 + 8 * r ^+ 2
Statement as written in the source
Lemma pair_grad_bound a b p q r x y : `|a| <= 1 -> `|b| <= 1 ->
  `|pg1 b p r y * pg2 a q r x| <= p ^+ 2 + q ^+ 2 + 8 * r ^+ 2.
Used by 1 declaration in 1 file
lemma ts_lead_ge source, line 310 
forall [R : realType] [a b : R] (t : R),
`|a| <= 1 -> `|b| <= 1 -> 1 - `|t| <= ts_lead a b t
Statement as written in the source
Lemma ts_lead_ge a b t : `|a| <= 1 -> `|b| <= 1 -> 1 - `|t| <= ts_lead a b t.
Used by 1 declaration in 1 file
lemma pmean_le source, line 323 
forall [R : realType] [a b : R] [F G : bool -> bool -> R],
`|a| <= 1 -> `|b| <= 1 -> (forall x y : bool, F x y <= G x y) -> pmean a b F <= pmean a b G
Statement as written in the source
Lemma pmean_le a b (F G : bool -> bool -> R) : `|a| <= 1 -> `|b| <= 1 ->
  (forall x y, F x y <= G x y) -> pmean a b F <= pmean a b G.
Used by 1 declaration in 1 file
lemma pmean_add source, line 333 
forall [R : realType] (a b : R) (F G : bool -> bool -> R),
pmean a b (fun x y : bool => F x y + G x y) = pmean a b F + pmean a b G
Statement as written in the source
Lemma pmean_add a b (F G : bool -> bool -> R) :
  pmean a b (fun x y => F x y + G x y) = pmean a b F + pmean a b G.
Used by 1 declaration in 1 file
lemma pmean_scale source, line 337 
forall [R : realType] (a b c : R) (F : bool -> bool -> R),
pmean a b (fun x y : bool => c * F x y) = c * pmean a b F
Statement as written in the source
Lemma pmean_scale a b c (F : bool -> bool -> R) :
  pmean a b (fun x y => c * F x y) = c * pmean a b F.
lemma pmean_const source, line 341 
forall [R : realType] (a b c : R), pmean a b (fun=> (fun=> c)) = c
Statement as written in the source
Lemma pmean_const a b c : pmean a b (fun _ _ => c) = c.
lemma plaw_add source, line 344 
forall [R : realType] (a b t : R) (F G : bool -> bool -> R),
plaw a b t (fun x y : bool => F x y + G x y) = plaw a b t F + plaw a b t G
Statement as written in the source
Lemma plaw_add a b t (F G : bool -> bool -> R) :
  plaw a b t (fun x y => F x y + G x y) = plaw a b t F + plaw a b t G.
lemma pmean_swap source, line 348 
forall [R : realType] (a b : R) (F : bool -> bool -> R),
pmean a b F = pmean b a (fun x : bool => F^~ x)
Statement as written in the source
Lemma pmean_swap a b (F : bool -> bool -> R) :
  pmean a b F = pmean b a (fun x y => F y x).
Used by 1 declaration in 1 file
lemma plaw_swap source, line 352 
forall [R : realType] (a b t : R) (F : bool -> bool -> R),
plaw a b t F = plaw b a t (fun x : bool => F^~ x)
Statement as written in the source
Lemma plaw_swap a b t (F : bool -> bool -> R) :
  plaw a b t F = plaw b a t (fun x y => F y x).
Used by 1 declaration in 1 file
lemma pair_signed_mean_lower source, line 359 
forall [R : realType] [a b t : R] (p q r : R),
`|a| <= 1 ->
`|b| <= 1 ->
`|t| <= 1 / 10 ^+ 3 ->
- (3 * 10 ^+ 4 * `|t| ^+ 3 * (p ^+ 2 + q ^+ 2)) <=
pmean 0 0 (fun x y : bool => pg1 b p r y * pg2 a q r x * psign a b t x y)
Statement as written in the source
Lemma pair_signed_mean_lower a b t p q r :
  `|a| <= 1 -> `|b| <= 1 -> `|t| <= 1 / 10 ^+ 3 ->
  - (3 * 10 ^+ 4 * `|t| ^+ 3 * (p ^+ 2 + q ^+ 2)) <=
  pmean 0 0 (fun x y => pg1 b p r y * pg2 a q r x * psign a b t x y).
Used by 1 declaration in 1 file
sectiontwo_spin_energy
Variable R : realType.
Implicit Types (a b t p q r : R) (x y : bool).
lemma sqr_le1 source, line 403 
forall [R : realType] [a : R], `|a| <= 1 -> a ^+ 2 <= 1
Statement as written in the source
Lemma sqr_le1 a : `|a| <= 1 -> a ^+ 2 <= 1.
Used by 3 declarations in 1 file
lemma sqr_le_norm source, line 406 
forall [R : realType] [a : R]
  [c : join_Num_POrderNmodule_between_Algebra_BaseAddUMagma_and_Order_Preorder
         {|
           Num.POrderZmodule.sort := R;
           Num.POrderZmodule.class :=
             {|
               Num.POrderZmodule.choice_hasChoice_mixin := Real.class R;
               Num.POrderZmodule.eqtype_hasDecEq_mixin := Real.class R;
               Num.POrderZmodule.Order_isDuallyPreorder_mixin := Real.class R;
               Num.POrderZmodule.Order_Preorder_isDuallyPOrder_mixin := Real.class R;
               Num.POrderZmodule.Algebra_hasOpp_mixin := Real.class R;
               Num.POrderZmodule.Algebra_hasZero_mixin := Real.class R;
               Num.POrderZmodule.Algebra_hasAdd_mixin := Real.class R;
               Num.POrderZmodule.Algebra_BaseZmoduleNmodule_isZmodule_mixin := Real.class R;
               Num.POrderZmodule.Algebra_BaseAddUMagma_isAddUMagma_mixin := Real.class R;
               Num.POrderZmodule.Algebra_BaseAddMagma_isAddMagma_mixin := Real.class R;
               Num.POrderZmodule.Algebra_AddMagma_isAddSemigroup_mixin := Real.class R
             |}
         |}],
0 <= c -> `|a| <= c -> a ^+ 2 <= c ^+ 2
Statement as written in the source
Lemma sqr_le_norm a c : 0 <= c -> `|a| <= c -> a ^+ 2 <= c ^+ 2.
Used by 2 declarations in 1 file
lemma plaw_energy source, line 409 
forall [R : realType] [a b t : R] (p r : R),
`|a| <= 1 ->
`|b| <= 1 ->
`|t| <= 1 / 4 ->
plaw a b t (fun=> (fun y : bool => pcv a t y * pg1 b p r y ^+ 2)) =
(1 - a ^+ 2) * (1 - t ^+ 2) / (2 * (1 + t * a * b)) *
((1 + b) * pg1 b p r true ^+ 2 / (1 + t * a) + (1 - b) * pg1 b p r false ^+ 2 / (1 - t * a))
Statement as written in the source
Lemma plaw_energy a b t p r : `|a| <= 1 -> `|b| <= 1 -> `|t| <= 1 / 4 ->
  plaw a b t (fun x y => pcv a t y * pg1 b p r y ^+ 2) =
  (1 - a ^+ 2) * (1 - t ^+ 2) / (2 * (1 + t * a * b)) *
    ((1 + b) * pg1 b p r true ^+ 2 / (1 + t * a) +
     (1 - b) * pg1 b p r false ^+ 2 / (1 - t * a)).
Used by 1 declaration in 1 file
lemma energy_bound_aux source, line 428 
forall [R : realType] [A0 c u v X1 X2 P : R],
0 <= A0 ->
3 / 8 <= c ->
4 / 5 <= u ->
4 / 5 <= v ->
0 <= X1 ->
0 <= X2 -> 0 <= P -> 2 * P <= X1 + X2 -> 3 / 5 * A0 * P <= A0 * c * (X1 * u + X2 * v)
Statement as written in the source
Lemma energy_bound_aux (A0 c u v X1 X2 P : R) : 0 <= A0 -> 3 / 8 <= c ->
  4 / 5 <= u -> 4 / 5 <= v -> 0 <= X1 -> 0 <= X2 -> 0 <= P ->
  2 * P <= X1 + X2 -> 3 / 5 * A0 * P <= A0 * c * (X1 * u + X2 * v).
Used by 1 declaration in 1 file
lemma plaw_energy_ge source, line 438 
forall [R : realType] [a b t : R] (p r : R),
`|a| <= 1 ->
`|b| <= 1 ->
`|t| <= 1 / 4 ->
3 / 5 * (1 - a ^+ 2) * p ^+ 2 <=
plaw a b t (fun=> (fun y : bool => pcv a t y * pg1 b p r y ^+ 2))
Statement as written in the source
Lemma plaw_energy_ge a b t p r : `|a| <= 1 -> `|b| <= 1 -> `|t| <= 1 / 4 ->
  3 / 5 * (1 - a ^+ 2) * p ^+ 2 <=
  plaw a b t (fun x y => pcv a t y * pg1 b p r y ^+ 2).
Used by 2 declarations in 1 file
lemma pprefactor_bounds source, line 473 
forall [R : realType] [a b t : R],
`|a| <= 1 ->
`|b| <= 1 ->
`|t| <= 1 / 4 ->
0 <= pprefactor a b t /\ pprefactor a b t <= 4 / 3 * ((1 - a ^+ 2) * (1 - b ^+ 2))
Statement as written in the source
Lemma pprefactor_bounds a b t : `|a| <= 1 -> `|b| <= 1 -> `|t| <= 1 / 4 ->
  0 <= pprefactor a b t /\
  pprefactor a b t <= 4 / 3 * ((1 - a ^+ 2) * (1 - b ^+ 2)).
Used by 1 declaration in 1 file
lemma plaw_energy_ge' source, line 498 
forall [R : realType] [a b t : R] (q r : R),
`|a| <= 1 ->
`|b| <= 1 ->
`|t| <= 1 / 4 ->
3 / 5 * (1 - b ^+ 2) * q ^+ 2 <=
plaw a b t (fun x : bool => fun=> pcv b t x * pg2 a q r x ^+ 2)
Statement as written in the source
Lemma plaw_energy_ge' a b t q r : `|a| <= 1 -> `|b| <= 1 -> `|t| <= 1 / 4 ->
  3 / 5 * (1 - b ^+ 2) * q ^+ 2 <=
  plaw a b t (fun x y => pcv b t x * pg2 a q r x ^+ 2).
Used by 1 declaration in 1 file
lemma pair_two_spin main result source, line 506 
forall [R : realType] [a b t : R] (p q r : R),
`|a| <= 1 ->
`|b| <= 1 ->
`|t| <= 1 / 10 ^+ 3 ->
-
plaw a b t
  (fun x y : bool =>
   (t + 2 * t ^+ 2 * pcm a t y * pcm b t x) * pcv a t y * pcv b t x * pg1 b p r y *
   pg2 a q r x) -
7 * 10 ^+ 4 * `|t| ^+ 3 *
(plaw a b t (fun=> (fun y : bool => pcv a t y * pg1 b p r y ^+ 2)) +
 plaw a b t (fun x : bool => fun=> pcv b t x * pg2 a q r x ^+ 2)) <=
plaw a b t
  (fun x y : bool =>
   (spin x - pcm a t y) * pg1 b p r y * ((spin y - pcm b t x) * pg2 a q r x))
Main result, as the README states it

The uniform two-spin inequality. For the pair law proportional to (1 + a x)(1 + b y)(1 + t x y) with |a|, |b| <= 1 and |t| <= 1/1000: the mixed energy plus the correction term (t + 2 t^2 m_i m_j) v_i v_j d_i f d_j f is at least - 70000 |t|^3 times the sum of the two energies (pair_two_spin; the remainder in t by a real polynomial certificate, ts_coef_bound). For the Ising law of a symmetric A with zero diagonal and i != j with |tanh A_ij| <= 1/1000: nu[D_i f D_j f] >= - nu[(t + 2 t^2 m_i m_j) v_i v_j d_i f d_j f] - 70000 |t|^3 (nu[v_i (d_i f)^2] + nu[v_j (d_j f)^2]) with t = tanh A_ij (ising_two_spin).

Statement as written in the source
Lemma pair_two_spin a b t p q r : `|a| <= 1 -> `|b| <= 1 -> `|t| <= 1 / 10 ^+ 3 ->
  - plaw a b t (fun x y => (t + 2 * t ^+ 2 * pcm a t y * pcm b t x) *
      pcv a t y * pcv b t x * pg1 b p r y * pg2 a q r x) -
  7 * 10 ^+ 4 * `|t| ^+ 3 * (plaw a b t (fun x y => pcv a t y * pg1 b p r y ^+ 2) +
                       plaw a b t (fun x y => pcv b t x * pg2 a q r x ^+ 2)) <=
  plaw a b t (fun x y => (spin x - pcm a t y) * pg1 b p r y *
    ((spin y - pcm b t x) * pg2 a q r x)).
Used by 1 declaration in 1 file
lemma spinT source, line 556 
forall R : realType, spin true = 1
Statement as written in the source
Lemma spinT (R : realType) : spin true = 1 :> R.
Used by 1 declaration in 1 file
lemma spinF source, line 559 
forall R : realType, spin false = -1
Statement as written in the source
Lemma spinF (R : realType) : spin false = -1 :> R.
Used by 1 declaration in 1 file
sectionising_two_spin
Variables (R : realType) (n : nat) (A : 'M[R]_n) (theta : 'cV[R]_n).
Hypothesis Asym : A \is symmetricmx.
Hypothesis Adiag : forall k, A k k = 0.
Local Notation cube := {ffun 'I_n -> bool}.
Local Notation w := (ising_weight A theta).
Local Notation E := (ising_mean A theta).
Implicit Types (x : cube) (i j : 'I_n) (f G : cube -> R).
Local Notation blk x i j c d := (spin_set (spin_set x i c) j d).
definition bsum source, line 573
Type
forall [R : realType] [n : nat],
'M_n -> 'cV_n -> {ffun 'I_n -> bool} -> 'I_n -> 'I_n -> ({ffun 'I_n -> bool} -> R) -> R
Definition
Definition bsum x i j G : R :=
  w (blk x i j true true) * G (blk x i j true true) +
  w (blk x i j true false) * G (blk x i j true false) +
  w (blk x i j false true) * G (blk x i j false true) +
  w (blk x i j false false) * G (blk x i j false false).
Used by 3 declarations in 1 file
lemma ising_mean_block source, line 579 
forall [R : realType] [n : nat] (A : 'M_n) (theta : 'cV_n) [i j : 'I_n]
  (G : {ffun 'I_n -> bool} -> R),
i != j ->
ising_mean A theta G = (\sum_x bsum A theta x i j G) / 4 / \sum_x ising_weight A theta x
Statement as written in the source
Lemma ising_mean_block i j G : i != j ->
  E G = (\sum_x bsum x i j G) / 4 / \sum_x w x.
Used by 1 declaration in 1 file
lemma block_set_i source, line 594 
forall [n : nat] (x : {ffun 'I_n -> bool}) [i j : 'I_n] (c d c' : bool),
i != j -> spin_set (spin_set (spin_set x i c) j d) i c' = spin_set (spin_set x i c') j d
Statement as written in the source
Lemma block_set_i x i j c d c' : i != j ->
  spin_set (blk x i j c d) i c' = blk x i j c' d.
Used by 1 declaration in 1 file
lemma block_set_j source, line 598 
forall [n : nat] (x : {ffun 'I_n -> bool}) (i j : 'I_n) (c d d' : bool),
spin_set (spin_set (spin_set x i c) j d) j d' = spin_set (spin_set x i c) j d'
Statement as written in the source
Lemma block_set_j x i j c d d' : spin_set (blk x i j c d) j d' = blk x i j c d'.
Used by 1 declaration in 1 file
lemma block_val_i source, line 601 
forall [n : nat] (x : {ffun 'I_n -> bool}) [i j : 'I_n] (c d : bool),
i != j -> spin_set (spin_set x i c) j d i = c
Statement as written in the source
Lemma block_val_i x i j c d : i != j -> blk x i j c d i = c.
Used by 1 declaration in 1 file
lemma block_val_j source, line 604 
forall [n : nat] (x : {ffun 'I_n -> bool}) (i j : 'I_n) (c d : bool),
spin_set (spin_set x i c) j d j = d
Statement as written in the source
Lemma block_val_j x i j c d : blk x i j c d j = d.
Used by 1 declaration in 1 file
lemma bsum_plaw source, line 607 
forall [R : realType] [n : nat] [A : 'M_n] [theta : 'cV_n] [x : {ffun 'I_n -> bool}]
  [i j : 'I_n] [G : {ffun 'I_n -> bool} -> R] [K a b t : R] [g : bool -> bool -> R],
1 + t * a * b != 0 ->
(forall c d : bool,
 ising_weight A theta (spin_set (spin_set x i c) j d) =
 K * ((1 + a * spin c) * (1 + b * spin d) * (1 + t * spin c * spin d))) ->
(forall c d : bool, G (spin_set (spin_set x i c) j d) = g c d) ->
bsum A theta x i j G = 4 * K * (1 + t * a * b) * plaw a b t g
Statement as written in the source
Lemma bsum_plaw x i j G K a b t (g : bool -> bool -> R) :
  1 + t * a * b != 0 ->
  (forall c d, w (blk x i j c d) =
     K * ((1 + a * spin c) * (1 + b * spin d) * (1 + t * spin c * spin d))) ->
  (forall c d, G (blk x i j c d) = g c d) ->
  bsum x i j G = 4 * K * (1 + t * a * b) * plaw a b t g.
Used by 1 declaration in 1 file
lemma pcm_block_i source, line 618 
forall [R : realType] [K a b t s : R],
K != 0 ->
1 + b * s != 0 ->
1 + t * a * s != 0 ->
(K * ((1 + a) * (1 + b * s) * (1 + t * s)) - K * ((1 - a) * (1 + b * s) * (1 - t * s))) /
(K * ((1 + a) * (1 + b * s) * (1 + t * s)) + K * ((1 - a) * (1 + b * s) * (1 - t * s))) =
(a + t * s) / (1 + t * a * s)
Statement as written in the source
Lemma pcm_block_i (K a b t s : R) : K != 0 -> 1 + b * s != 0 -> 1 + t * a * s != 0 ->
  (K * ((1 + a) * (1 + b * s) * (1 + t * s)) -
     K * ((1 - a) * (1 + b * s) * (1 - t * s))) /
  (K * ((1 + a) * (1 + b * s) * (1 + t * s)) +
     K * ((1 - a) * (1 + b * s) * (1 - t * s))) =
  (a + t * s) / (1 + t * a * s).
Used by 1 declaration in 1 file
lemma pcm_block_j source, line 635 
forall [R : realType] [K a b t s : R],
K != 0 ->
1 + a * s != 0 ->
1 + t * b * s != 0 ->
(K * ((1 + a * s) * (1 + b) * (1 + t * s)) - K * ((1 + a * s) * (1 - b) * (1 - t * s))) /
(K * ((1 + a * s) * (1 + b) * (1 + t * s)) + K * ((1 + a * s) * (1 - b) * (1 - t * s))) =
(b + t * s) / (1 + t * b * s)
Statement as written in the source
Lemma pcm_block_j (K a b t s : R) : K != 0 -> 1 + a * s != 0 -> 1 + t * b * s != 0 ->
  (K * ((1 + a * s) * (1 + b) * (1 + t * s)) -
     K * ((1 + a * s) * (1 - b) * (1 - t * s))) /
  (K * ((1 + a * s) * (1 + b) * (1 + t * s)) +
     K * ((1 + a * s) * (1 - b) * (1 - t * s))) =
  (b + t * s) / (1 + t * b * s).
Used by 1 declaration in 1 file
lemma affine_pos source, line 652 
forall [R : realType] [a s : R], `|a| < 1 -> `|s| = 1 -> 0 < 1 + a * s
Statement as written in the source
Lemma affine_pos (a s : R) : `|a| < 1 -> `|s| = 1 -> 0 < 1 + a * s.
Used by 1 declaration in 1 file
lemma div_le4 source, line 658 
forall [R : realType] [Z K a b c d : R],
0 < Z -> - b - K * (c + d) <= a -> - (b / 4 / Z) - K * (c / 4 / Z + d / 4 / Z) <= a / 4 / Z
Statement as written in the source
Lemma div_le4 (Z K a b c d : R) : 0 < Z -> - b - K * (c + d) <= a ->
  - (b / 4 / Z) - K * (c / 4 / Z + d / 4 / Z) <= a / 4 / Z.
Used by 1 declaration in 1 file
lemma sum_combine source, line 669 
forall [R : realType] [I : finType] [F1 F2 F3 F4 : I -> R] [K : R],
(forall k : I, - F2 k - K * (F3 k + F4 k) <= F1 k) ->
- \sum_k F2 k - K * (\sum_k F3 k + \sum_k F4 k) <= \sum_k F1 k
Statement as written in the source
Lemma sum_combine (I : finType) (F1 F2 F3 F4 : I -> R) (K : R) :
  (forall k, - F2 k - K * (F3 k + F4 k) <= F1 k) ->
  - (\sum_k F2 k) - K * (\sum_k F3 k + \sum_k F4 k) <= \sum_k F1 k.
Used by 1 declaration in 1 file
lemma scale_ineq source, line 680 
forall [R : realType] [c K P1 P2 P3 P4 : R],
0 <= c -> - P2 - K * (P3 + P4) <= P1 -> - (c * P2) - K * (c * P3 + c * P4) <= c * P1
Statement as written in the source
Lemma scale_ineq (c K P1 P2 P3 P4 : R) : 0 <= c ->
  - P2 - K * (P3 + P4) <= P1 -> - (c * P2) - K * (c * P3 + c * P4) <= c * P1.
Used by 1 declaration in 1 file
Local Notation m := (ising_cond_mean A theta).
Local Notation v := (ising_cond_var A theta).
Local Notation D := (ising_dproj A theta).
lemma ising_two_spin_block source, line 691 
forall [R : realType] [n : nat] [A : 'M_n] (theta : 'cV_n),
A \is symmetricmx ->
(forall k : 'I_n, A k k = 0) ->
forall (x : {ffun 'I_n -> bool}) [i j : 'I_n] (f : {ffun 'I_n -> bool} -> R),
i != j ->
`|sk_tanh (A i j)| <= 1 / 10 ^+ 3 ->
-
bsum A theta x i j
  (fun y : {ffun 'I_n -> bool} =>
   (sk_tanh (A i j) +
    2 * sk_tanh (A i j) ^+ 2 * ising_cond_mean A theta i y * ising_cond_mean A theta j y) *
   ising_cond_var A theta i y * ising_cond_var A theta j y * half_diff i f y *
   half_diff j f y) -
7 * 10 ^+ 4 * `|sk_tanh (A i j)| ^+ 3 *
(bsum A theta x i j
   (fun y : {ffun 'I_n -> bool} => ising_cond_var A theta i y * half_diff i f y ^+ 2) +
 bsum A theta x i j
   (fun y : {ffun 'I_n -> bool} => ising_cond_var A theta j y * half_diff j f y ^+ 2)) <=
bsum A theta x i j
  (fun y : {ffun 'I_n -> bool} => ising_dproj A theta i f y * ising_dproj A theta j f y)
Statement as written in the source
Lemma ising_two_spin_block x i j f : i != j ->
  `|sk_tanh (A i j)| <= 1 / 10 ^+ 3 ->
  - bsum x i j (fun y => (sk_tanh (A i j) + 2 * sk_tanh (A i j) ^+ 2 * m i y * m j y) *
       v i y * v j y * half_diff i f y * half_diff j f y) -
  7 * 10 ^+ 4 * `|sk_tanh (A i j)| ^+ 3 *
    (bsum x i j (fun y => v i y * half_diff i f y ^+ 2) +
     bsum x i j (fun y => v j y * half_diff j f y ^+ 2)) <=
  bsum x i j (fun y => D i f y * D j f y).
Used by 1 declaration in 1 file
lemma ising_two_spin main result source, line 756 
forall [R : realType] [n : nat] [A : 'M_n] (theta : 'cV_n),
A \is symmetricmx ->
(forall k : 'I_n, A k k = 0) ->
forall [i j : 'I_n] (f : {ffun 'I_n -> bool} -> R),
i != j ->
`|sk_tanh (A i j)| <= 1 / 10 ^+ 3 ->
-
ising_mean A theta
  (fun y : {ffun 'I_n -> bool} =>
   (sk_tanh (A i j) +
    2 * sk_tanh (A i j) ^+ 2 * ising_cond_mean A theta i y * ising_cond_mean A theta j y) *
   ising_cond_var A theta i y * ising_cond_var A theta j y * half_diff i f y *
   half_diff j f y) -
7 * 10 ^+ 4 * `|sk_tanh (A i j)| ^+ 3 *
(ising_mean A theta
   (fun y : {ffun 'I_n -> bool} => ising_cond_var A theta i y * half_diff i f y ^+ 2) +
 ising_mean A theta
   (fun y : {ffun 'I_n -> bool} => ising_cond_var A theta j y * half_diff j f y ^+ 2)) <=
ising_mean A theta
  (fun y : {ffun 'I_n -> bool} => ising_dproj A theta i f y * ising_dproj A theta j f y)
Main result

Stated in the README together with pair_two_spin.

Statement as written in the source
Lemma ising_two_spin i j f : i != j -> `|sk_tanh (A i j)| <= 1 / 10 ^+ 3 ->
  - E (fun y => (sk_tanh (A i j) + 2 * sk_tanh (A i j) ^+ 2 * m i y * m j y) *
       v i y * v j y * half_diff i f y * half_diff j f y) -
  7 * 10 ^+ 4 * `|sk_tanh (A i j)| ^+ 3 *
    (E (fun y => v i y * half_diff i f y ^+ 2) +
     E (fun y => v j y * half_diff j f y ^+ 2)) <=
  E (fun y => D i f y * D j f y).
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.