Erdős Problem #561

`F(s,n)` is the disjoint union of the stars \(K_{1,n_i}\). The vertex \((i,0)\) is the center of component \(i\); its other \(n_i\) vertices are leaves. -/ local notation "F(" s ", " n ")" => fromRel (fun (u v : Σ i : Fin s, Fin (n i + 1)) ↦ Sigma.fst u = Sigma.fst v ∧ (Fin.val (Sigma.snd u) = 0 ∨ Fin.val (Sigma.snd v) = 0)) /-- Let \(\hat{R}(G)\) denote the size Ramsey number, the minimal number of edges \(m\) such that there is a graph \(H\) with \(m\) edges such that in any \(2\)-colouring of the edges of \(H\) there is a monochromatic copy of \(G\). Let \(F_1\) and \(F_2\) be the union of stars. More precisely, let \(F_1=\cup_{i\leq s}K_{1,n_i}\) and \(F_2=\cup_{j\leq t}K_{1,m_j}\) with \(n_1\geq\cdots\geq n_s\geq1\) and \(m_1\geq\cdots\geq m_t\geq1\). Prove that \[\hat{R}(F_1,F_2)=\sum_{2\leq k\leq s+t}l_k\] where \[l_k=\max\{n_i+m_j-1:i+j=k\}.\] The unions are vertex-disjoint, and \(s,t\geq1\). Lean indices start at zero, so the condition \(i+j=k\) is represented by \((i+1)+(j+1)=k\).