Towards Closing the Trust Gap in the SAT Certification of Ramsey Numbers R(3,8) and R(3,9)

6 Ramsey Theory

Definition 66 \((x,y)\)-graphs
#

\(G\) is an \((x,y)\)-graph if \(x {\gt} C(G)\) and \(y {\gt} I(G)\).

Definition 67 Ramsey Number (Graver’s version)
#
\[ R(x,y) = \max \{ n \in \mathbb {N} \mid \exists G \text{, } G \text{ is an} (x, y)\text{-graph } \land \text{ } |V(G)| = n \} \]
Theorem 68 Graver’s Lemma 1
#

\(G\) is an \((x,y)\)-graph if and only if its complement \(G^c\) is a \((y,x)\)-graph.

Proof
Theorem 69 noXYGraphIffRamseyGraphProp
Proof
Lemma 70 isXYGraph_bddAbove
#
Proof
Lemma 71 cardLERamseyOld
Proof
Lemma 72 R3y_neighbor_Ind
#
Proof
Theorem 73 GraphRamsey2RamseyOld
Proof
Theorem 74 RamseyOld_2
#
Proof
Definition 75 \(v_i\)
#
Definition 76 \(s_i\)
#
Definition 77 \(t_i\)
#
Definition 78 \(σ(G)\)
#
Lemma 79 sum_degree_eq_sum_over_degrees
Proof
Lemma 80 num_of_vertices_eq_sum_over_degrees
Proof
Definition 81 \(H_1\)
#
Definition 82 \(H_2\)
#
Definition 83 \(e_1\)
#
Definition 84 \(e_2\)
#
Definition 85 \(H_1 H_2\) isomorphic
#
Lemma 86 \(H_1\)_eq_bot_of_3y
Proof
Lemma 87 \(H_1\)_cliqueNum_lt
#
Proof
Theorem 88 Graver Lemma 2

For any \((x,y,n)\)-graph \(G\), every vertex \(v\) in \(G\) satisfies

\[ (n - 1) - R(x,y - 1) \leq deg(v) \leq R(x - 1, y) \]

.

Proof
Proof
Proof
Lemma 91 \(H_1\)_degreeCount_eq
Proof
Lemma 92 \(H_1\)_vertCount_eq
Proof
Theorem 93 Graver’s Prop 1
Proof
Lemma 94 \(v_i\)_deg_swap
Proof
Proof
Definition 96 \(e\)
#
Lemma 97 exy0
Proof
Proof
Proof