\(V \ S\) is \(S^{c}\). Independent sets and coverings are complementary, which is why the book’s figure 7.1 shows independent sets visibly complementing coverings.

The largest independent set and the smallest covering are exact complements: choosing one is the same problem as choosing the other.

The striking parallel with Corollary 7.1 — even though matchings and edge coverings are not complementary the way independent sets and coverings are. The book is explicit about this (§7.1, p. 110):

König’s min-max equality transported across the two Gallai identities. The book introduces it with (§7.1, p. 110):

(\(\Rightarrow \)) Every subgraph of a bipartite graph is bipartite, and the larger side of a bipartition is an independent set with at least half the vertices.

(\(\Leftarrow \)) If \(G\) were not bipartite it would contain an odd cycle (Thm 1.2). That cycle on \(2k+1\) vertices has \(\alpha = k\), and \(2k \lt 2k+1\), so the condition fails at that subgraph.

Stated as \(\nu (H) \le 2\cdot \alpha (H)\) to avoid division.

"Subgraph \(H\) of \(G\)" is H : G.Subgraph, which carries its own verts — so \(\nu (H)\) genuinely shrinks and the odd-cycle witness is expressible. H.coe is the subgraph viewed as a SimpleGraph ↥H.verts, and H.verts.ncard is used in place of Fintype.card ↥H.verts to avoid an instance that [Fintype V] alone does not supply.

(\(\Rightarrow \)) Theorem 7.3 applied subgraph-wise, every subgraph of a bipartite graph being bipartite.

(\(\Leftarrow \)) Contrapositive: an odd cycle \(H\) on \(2k+1\) vertices has \(\delta (H) = 2 \gt 0\), \(\alpha (H) = k\) and \(\beta '(H) = k + 1\), so the equality fails there.

So the identity \(\alpha = \beta '\) — which Theorem 7.3 gives for bipartite graphs — actually characterises them.

! The instance binders [Fintype H.verts] \(\to \) [DecidableRel H.coe.Adj] \(\to \) sit inside the \(\forall H\), as hypotheses rather than instance arguments. That is unusual and means a user must supply them explicitly at each application; it also means the (\(\Leftarrow \)) direction gets to assume them for its witness, which is harmless here but worth noticing.

Suppose \(v\) is a cut vertex, so \(G - v\) splits. Independent sets can be chosen per component, and one shows some edge at \(v\) is deletable without increasing \(\alpha \) — contradicting criticality, where every deletion must raise it.

So \(\alpha \)-criticality forces a structure that cannot be pieced together at a single articulation point.

Corollary 7.1 gives \(\alpha + \beta = \nu \) for every graph on the vertex type, and edge deletion leaves \(\nu \) fixed. So \(\beta (G - e) \lt \beta (G)\) \(\iff \) \(\alpha (G - e) \gt \alpha (G)\), and \(\beta \)-critical is the same condition as \(\alpha \)-critical.

Stated as \(2\beta \le \varepsilon + 1\) to avoid division.

A minimum covering touches every edge, and in a connected graph the edges are linked tightly enough that each covering vertex can be charged at least two edges, with one left over for a spanning tree’s root.

! Note the book states this under 7.1.3, whose preamble defines \(\beta \)-critical — but part (b) does not assume \(\beta \)-criticality, only connectivity, and the Lean signature correctly reflects that. (The docstring previously implied the \(\beta \)-critical hypothesis carried over; it does not.)

Connectivity is essential: a disjoint union of \(k\) edges has \(\beta = k = \varepsilon \), which violates the bound for \(k \ge 2\).

A bigger graph contains a smaller one: restrict a graph on \(m\) vertices to any \(n\) of them, get a \(k\)-clique or \(l\)-independent set there, and it survives in the larger graph.

No matter how a graph is drawn, if it is large enough it cannot avoid both a big clique and a big independent set.

The book can be informal about existence because \(r(k,l)\) is only ever used comparatively. In Lean, ramseyNumber is sInf over a set that this lemma proves nonempty — so until this is proved, every ramseyNumber in the file is provably \(0\) and every result below is vacuous. It gates all of §7.2 and, via Schur, §7.4.

ramseyNumber is an sInf. Once the set is nonempty (exists_isRamseyBound) it contains its infimum (Nat.sInf_mem), so \(r(k,l)\) genuinely has the defining property.

Note isRamseyBound_mono is not needed for this — Nat.sInf_mem alone suffices — but it is what makes \(r(k,l)\) the sharp threshold rather than merely a bound.

A 1-clique is a single vertex, which any nonempty graph has. So one vertex suffices.

! \(n = 1\) must genuinely satisfy IsRamseyBound 1 1 l and no smaller \(n\) must — but \(n = 0\) also satisfies it vacuously only if Fin 0 graphs have a 1-clique, which they do not. So the sInf really is \(1\), but the \(n = 0\) case has to be ruled out explicitly rather than assumed.

A 1-element independent set is a single vertex. The mirror image of ramseyNumber_one_left, and derivable from it via ramseyNumber_comm (Ex 7.2.1) — though proving it directly is just as short.

A 2-clique is an edge. On \(l\) vertices either some edge is present — a 2-clique — or there are none, and all \(l\) vertices are independent. So \(l\) suffices; and \(l - 1\) does not, since \(\bot \) on Fin (l-1) has no edge and no \(l\)-element independent set.

A 2-element independent set is a non-adjacent pair. On \(k\) vertices either some pair is non-adjacent, or every pair is adjacent and all \(k\) form a clique. The complete graph on \(k - 1\) vertices shows \(k\) is needed.

The mirror of ramseyNumber_two_left under ramseyNumber_comm.

The engine behind both the exact values in the book’s table and the binomial bound of Theorem 7.5.

! \(l - 1\) and \(k - 1\) are \(\mathbb {N}\) subtraction; \(hk\), \(hl\) keep them from truncating, but the proof must still convert \(l - 1 + 1 = l\) explicitly at each use.

The parity refinement that pins down \(r(3,4) = 9\): \(r(3,3) = 6\) and \(r(2,4) = 4\) are both even, so \(r(3,4) \le 6 + 4 - 1 = 9\).

! The book’s "in particular, \(v\) cannot be adjacent to precisely \(r(k-1,l) - 1\) vertices" is the crux and compresses a parity computation: with both summands even, \(r(k-1,l) - 1\) is odd, so a vertex of even degree cannot have exactly that degree. That one configuration is precisely the one where neither (i) nor (ii) holds, so ruling it out restores the case analysis.

\(C_{5}\) has girth 5, so no triangle: each vertex has two neighbours and they are not adjacent to each other.

Any three of five cyclic positions include two consecutive ones, hence adjacent. So \(\alpha (C_{5}) = 2\).

\(C_{5}\) is self-complementary, which is what makes it work on both sides at once — the book conjectures (§7.2, p. 114) that all \((k,k)\)-Ramsey graphs are.

\(C_{5}\) witnesses that five vertices do not force either structure, so the threshold is \(\ge 6\). Combined with Thm 7.4 this is the exact value: among any six people, three are mutual acquaintances or three mutual strangers.

! Only the lower bound is stated here; the file does not state \(r(3,3) = 6\). Same for \(r(3,5)\) and \(r(4,4)\) below — all three exact values in the book’s worked examples are left unstated.

A triangle needs three residues pairwise differing by an element of \({1, 5, 8, 12}\); the arithmetic rules it out. The graph is 4-regular and triangle-free.

Five pairwise non-adjacent vertices would be five residues no two differing by an element of \({1, 5, 8, 12}\). With thirteen residues and four forbidden differences, no such set exists.

Thirteen vertices do not suffice, so the threshold is \(\ge 14\).

! The book’s upper bound chain routes through \(r(3,4) = 9\), which itself needs the strict form of Theorem 7.4 (\(r(3,3)\) and \(r(2,4)\) both even). Neither \(r(3,4) = 9\) nor its ingredients are stated in this file, so the exact value \(r(3,5) = 14\) is not reachable from what is here even once everything is proved.

Four vertices pairwise differing by quadratic residues would be a \(K_{4}\); the arithmetic of \({1,2,4,8,9,13,15,16}\) prevents it, so \(\omega = 3\).

+ The slick route: the Paley graph of order 17 is self-complementary (the book notes this), so a 4-element independent set would be a \(K_{4}\) in the complement, i.e. in an isomorphic copy — ruled out by the previous lemma.

! But that route costs a self-complementarity proof (an explicit isomorphism \(x \mapsto gx\) for \(g\) a non-residue), which is more work than the direct check.

Seventeen vertices do not suffice, so the threshold is \(\ge 18\) — and with the upper bound, exactly \(18\), the largest value in the book’s table.

! As with \(r(3,5)\), only the lower bound is stated here, and the upper bound would need \(r(3,4) = 9\) — itself unstated and requiring the strict form of Theorem 7.4.

\(r(k, l) \le C(k + l - 2, k - 1)\).

Theorem 7.4’s recursion is exactly Pascal’s rule, so the Ramsey numbers are dominated by binomial coefficients. Setting \(k = l\) gives roughly \(r(k,k) \le 4^k\); Theorem 7.6 gives \(2^{k/2}\) below, and closing that gap is still open.

! Three \(\mathbb {N}\) subtractions in the statement (\(k + l - 2\), \(k - 1\), and \(m - 2\) in the proof). The Pascal step \(C(m+n-3, m-1) + C(m+n-3, m-2) = C(m+n-2, m-1)\) is Nat.choose_succ_succ only after the indices are massaged into succ form — budget for that.

A simple graph on a labelled vertex set is determined by which of the \(C(n,2)\) possible edges are present.

! Mathlib has a Fintype (SimpleGraph (Fin n)) instance but no cardinality lemma, so this genuinely has to be proved. The route is an equiv SimpleGraph (Fin n) \(\simeq \) (Sym2 (Fin n) \{} diagonal \(\to \) Bool), or via Finset.powerset on the non-diagonal Sym2s — the Sym2 bookkeeping is the work, not the arithmetic.

The counting fact underlying Erdős’ probabilistic proof of Theorem 7.6.

The probabilistic method, which the book introduces as (§7.2, p. 115):

The exponent \(k/2\) is real, hence the \(\mathbb {R}\)-valued statement — the one place in this chapter where \(\mathbb {N}\) will not do.

Ramsey numbers are monotone in both arguments, so \(r(k,l) \ge r(m,m)\) for m = min(k,l); then Theorem 7.6.

! Monotonicity of ramseyNumber in its arguments is not stated in this file. isRamseyBound_mono is monotonicity in \(n\), a different thing. The needed lemma — \(k \le k' \to l \le l' \to r(k,l) \le r(k',l')\) — has to be added; it follows from IsRamseyBound n k’ l’ \(\to \) IsRamseyBound n k l (a bigger clique contains a smaller one).

Generalises Theorem 7.4’s recursion. Fix \(v\) in a large \(K_{n}\) and classify the other vertices by the colour of their edge to \(v\). If every colour class were smaller than \(r(\dots , k_{i}-1, \dots )\), the classes could not cover all vertices — which is exactly what the bound arranges. Some class is then big enough for a monochromatic complete subgraph, and \(v\) extends it in colour \(i\).

Stated additively (\(+ m\) on the left, \(+ 2\) on the right) to avoid the \(\mathbb {N}\) subtraction \(- m + 2\).

! Function.update c i (c i - 1) still has an inner \(\mathbb {N}\) subtraction; \(hc : \forall i, 2 \le c i\) keeps it from truncating.

Iterating Theorem 7.7 gives exactly the multinomial recursion, as the two-colour case gave binomials in Theorem 7.5.

With \(m = 2\) this is Theorem 7.5, since \((k_{1}+k_{2})!/(k_{1}!k_{2}!) = C(k_{1}+k_{2}, k_{1})\).

! The division is exact but is \(\mathbb {N}\) division in Lean; as with card_perfectMatching_completeGraph in chapter 5, the proof should establish the multiplied form \(r(\dots ) * \prod k_{i}! \le (\sum k_{i})!\) and divide only at the end.

Complementation swaps cliques and independent sets, so a graph with no \(k\)-clique and no \(l\)-independent set becomes one with no \(l\)-clique and no \(k\)-independent set. The thresholds coincide.

Why the book’s table is symmetric about its diagonal.

Theorem 7.7 with all targets \(3\). Fix \(v\) in a \(K_{n}\) on \(n(r_{n-1}-1) + 2\) vertices; its \(n(r_{n-1}-1) + 1\) neighbours split among \(n\) colours, so some class has \(\ge r_{n-1}\) vertices. Either two of them are joined in that same colour — a monochromatic triangle with \(v\) — or the class avoids that colour and its induced colouring uses only \(n-1\) colours, where \(r_{n-1}\) vertices force a triangle.

Stated additively (\(+ n\) on the left) to avoid \(\mathbb {N}\) subtraction.

Unwinding \(r_{n} \le n(r_{n-1} - 1) + 2\) from \(r_{2} = 6\) and dividing by \(n!\) gives a telescoping sum of reciprocals \(1/k!\), which converge to \(e\). Hence \(r_{n} - 1 \le n! e\).

\(e\) appears precisely as \(\sum 1/k!\).

Part (a) at \(n = 3\) with \(r_{2} = 6\): \(r_{3} \le 3(6-1) + 2 = 17\). (Part (b) also gives \(\lfloor 6e\rfloor + 1 = 16 + 1 = 17\).)

So among any seventeen points, any 3-colouring of the pairs forces a monochromatic triangle.

Let \(S\) be independent in \(G[H]\). Its first-coordinate projection is independent in \(G\) (two \(S\)-vertices in different copies force those \(G\)-vertices non-adjacent), so at most \(\alpha (G)\) copies are touched; within each, at most \(\alpha (H)\) vertices. Multiply.

Take \((k+1,k+1)\)- and \((l+1,l+1)\)-Ramsey graphs \(G\), \(H\) — so \(\omega , \alpha \le k\) and \(\le l\) respectively — and form \(G[H]\), which has the product vertex count. Part (a) gives \(\alpha (G[H]) \le kl\); complementing gives \(\omega (G[H]) \le kl\). So \(G[H]\) avoids both a \((kl+1)\)-clique and a \((kl+1)\)-independent set.

Stated additively (\(\dots + 1 \le r(\dots )\)) to avoid \(\mathbb {N}\) subtraction on the outside — though the two inner \(- 1\)s remain.

! The complement step needs \((G[H])^{c} \cong G^{c}[H^{c}]\), which is true but not obvious and is not stated in this file. Without it, part (a) bounds only \(\alpha \) and the clique side has to be argued separately.

Iterate part (b) from \(r(3,3) = 6\), so \(r(3,3) - 1 = 5\). Taking \(k = l = 2^{n-1}\) each step multiplies by \(5\). The witness is the \(n\)-fold composition of \(C_{5}\) with itself.

The best constructive bound, versus Corollary 7.6’s probabilistic one. With \(k = 2^{n}\), 5\(^{n}\) = k^{log\(_{2}\)5} \(\approx \) k^{2.32} is merely polynomial in \(k\), while \(2^{k/2}\) is exponential — the gap the book remarks on.

(absent from Mathlib). If \(\delta (G) \ge m - 1\) then every tree \(T\) on \(m\) vertices embeds in \(G\).*

Build the embedding greedily. A tree on \(m\) vertices can be listed so each new vertex attaches to exactly one already-placed vertex (peel leaves). Placing the \(j\)-th, its unique placed neighbour has \(\ge m - 1\) neighbours in \(G\), of which at most \(j - 1 \le m - 2\) are used — a fresh image always exists.

The standard "minimum degree forces every small tree" lemma; it is what makes tree-target Ramsey numbers exactly computable.

! \(m\) is a free variable in the signature, tied to \(W\) only through hm : Fintype.card W = m — so \(m\) is determined but Lean will not infer it; callers must supply it.

\(K_{1,n}\) is the star with \(n\) leaves, so a blue copy is a vertex with \(n\) blue edges. On \(m + n - 1\) points, if no vertex has \(n\) blue edges then every vertex has \(\ge (m+n-2) - (n-1) = m - 1\) red edges, and tree_isContained_of_minDegree_le embeds \(T\) in red.

Lower bound: a colouring of \(K_{m+n-2}\) with no red \(T\) and no blue star. The divisibility \((m-1) \mid (n-1)\) is exactly what lets the red graph be \((m-2)\)-regular — too sparse for \(T\), while leaving every vertex under \(n\) blue edges.

! The two targets live on different carriers (\(W\) and Fin 1 \(\oplus \) Fin n), so \(![T, K_{1,n}]\) cannot elaborate — Matrix.vecCons is homogeneous. Hence the dependent spelling Fin.cons T (Fin.cons _ finZeroElim) with an explicit type family W := ![W, Fin 1 \(\oplus \) Fin n], and W : Type rather than Type*.

One of the cleanest results in generalised Ramsey theory: the answer depends on the tree only through its number of vertices, not its shape.

Lower bound. Partition \((m-1)(n-1)\) points into \(n-1\) groups of \(m-1\); red inside groups, blue between. Red is a disjoint union of \(K_{m-1}\)s, too small for a tree on \(m\) vertices; blue is complete \((n-1)\)-partite, so its largest clique has \(n-1\) vertices — no \(K_{n}\).

Upper bound. On \((m-1)(n-1) + 1\) points, if blue has no \(K_{n}\) then Turán-type reasoning gives red minimum degree \(\ge m-1\) somewhere, and the sub-lemma embeds \(T\).

! Same heterogeneous-carrier spelling as part (b).

! The upper bound’s "Turán-type reasoning" is genuinely §7.3’s Theorem 7.9 — so this exercise depends on the next section, not just on §7.2.

The book remarks (§7.3, p. 118) on the parallel with Theorem 4.6:

! Blocked on degreeSequence being unsorted — see the warning there. The book’s DegreeMajorised compares nondecreasing sequences; against this file’s unsorted list the predicate is not even isomorphism-invariant, so the equality clause (same degree sequence \(\to \) G \(\cong \) H) cannot be right as stated. Fix degreeSequence first.

! The carrier changes: \(H\) is existentially quantified over a fresh type \(W\), so DegreeMajorised G H compares across types via the Fintype.card V = Fintype.card W conjunct.

(absent from Mathlib). *If \(d_G(v) \le d_H(v)\) for every vertex \(v\), then \(G\) is degree-majorised by \(H\).*

Degree-majorisation compares sorted sequences entrywise. Pointwise domination survives sorting: the \(i\)-th smallest degree of \(G\) cannot exceed the \(i\)-th smallest of \(H\).

! Two problems with this as stated.

1. degreeSequence in this file is unsorted, so "sorting preserves domination" is not what the predicate says — the entrywise comparison is against Finset.univ.toList’s arbitrary order. With both graphs on the same \(V\) that order is at least the same on both sides, so pointwise domination does happen to give the conclusion — but only by accident of the shared carrier, not because the lemma is right. 2. It is stated for G H : SimpleGraph V on the same carrier, whereas Theorem 7.8 needs it across different carriers (\(G\) on \(V\), \(H\) on \(W\)). So it does not actually discharge the step it was extracted for.

The balanced complete multipartite graph is not merely an extremal example but the unique one, up to isomorphism.

Turán at \(m = 2\) — Mantel’s 1907 case, half a century before the generalisation. Extremal example: balanced \(K_{\lfloor \nu /2\rfloor ,\lceil \nu /2\rceil }\) with \(\lfloor \nu ^{2}/4\rfloor \) edges.

Cleared to \(\nu ^{2} \lt 4\varepsilon \) to avoid division.

Forbidding bipartiteness on top of triangle-freeness drops the cap from \(\nu ^{2}/4\) to \((\nu -1)^{2}/4 + 1\). A triangle-free non-bipartite graph contains an odd cycle of length \(\ge 5\), which is an inefficient use of vertices; the densest such graph is essentially \(C_{5}\) blown up.

The stability phenomenon of extremal graph theory: near-extremal graphs all resemble the extremal one, so departing from it costs edges.

Cleared to \((\nu -1)^{2} + 4 \lt 4\varepsilon \).

Double-count cherries (paths of length two). Each \(v\) centres \(C(d(v),2)\) of them, so the total is \(\sum _v C(d(v),2)\); each is determined by its two endpoints, an unordered pair from \(C(\nu ,2)\). If no pair had \(m\) common neighbours, each pair would host \(\le m-1\) cherries, capping the total at \((m-1)C(\nu ,2)\).

The prototype for Kővári–Sós–Turán (exercise 7.3.5).

Convert part (a)’s degree condition into an edge count. By convexity, \(\sum _v C(d(v),2)\) is minimised at fixed \(\varepsilon \) when all degrees equal \(2\varepsilon /\nu \), so \(\sum _v C(d(v),2) \ge \nu \cdot C(2\varepsilon /\nu , 2)\); demanding this exceed \((m-1)C(\nu ,2)\) and solving for \(\varepsilon \) gives the threshold.

A genuinely sub-quadratic threshold (\(\nu ^{3/2}\)), unlike Turán’s for cliques.

! Real-valued with rpow exponents, so the proof leaves \(\mathbb {N}\) early. Mathlib’s inner_mul_le_norm_mul_norm or Finset.inner_mul_le_norm_mul_norm / sq_sum_le_card_mul_sum_sq supply the convexity step; Finset.inner_card_le_... is the usual shape for "sum of \(C(d_{v},2)\) versus the average".

Two distinct points have \(\le 2\) common unit-distance neighbours (two unit circles meet in \(\le 2\) points), so the graph is \(K_{2,3}\)-free; 7.3.4(b) at \(m = 3\) gives \(\varepsilon \le (\sqrt2 \cdot n^{3/2})/2 + n/4 = n^{3/2}/\sqrt2 + n/4\).

A purely combinatorial bound on a geometric quantity, obtained by turning a fact about circles into a forbidden subgraph. The true order of growth of the unit-distance problem is still open (Erdős).

Generalises 7.3.4 from \(K_{2,m}\) to \(K_{m,m}\). Count stars — a vertex with \(m\) of its neighbours — two ways: each \(v\) contributes \(C(d(v), m)\), and each \(m\)-set can be the leaf-set of \(\le m-1\) stars unless a \(K_{m,m}\) appears. Convexity converts the degree sum into an edge count.

The exponent \(2 - 1/m\) is the point: forbidding a complete bipartite subgraph caps \(\varepsilon \) at strictly sub-quadratic order, unlike Turán’s constant fraction of \(\nu ^{2}\). Whether the exponent is tight for every \(m\) is the Zarankiewicz problem, still open.

! The rpow exponent varies with \(m\), so this is irreducibly real-valued; and \((m - 1 : \mathbb {R})\) with \(hm : 1 \le m\) means the base can be \(0\) at \(m = 1\), where \(0 ^(1/1) = 0\) — check that boundary case does not make the hypothesis vacuous.

The classical bridge from Ramsey theory to additive number theory. Schur’s original motivation was Fermat’s Last Theorem mod \(p\).

The book’s motivating example (§7.4, p. 120):

! Note "not necessarily distinct" — so \(x = y\) is allowed, and the Lean statement correctly does not require distinctness.

! hpart says every \(k \in [1, r_{n}]\) lies in exactly one part, and hsub that no part escapes the range — together a genuine partition. But nothing forces the parts nonempty, which is fine (empty parts are harmless).

Lower bound from the book’s opening partition \(({1,4,10,13}, {2,3,11,12}, {5,6,7,8,9})\) of \({1,\dots ,13}\).

Compare \(s_{3} \le r_{3} = 17\): the Schur number is strictly below the Ramsey number it is derived from, so Theorem 7.10’s bound is not tight.

From a sum-free \((n-1)\)-partition of \({1,\dots ,s_{n-1}-1}\), build an \(n\)-partition of a roughly three-times-longer interval by scaling: keep the old parts tripled, and give the new \(n\)-th part the leftover residues.

Stated additively as \(3s_{n-1} \le s_{n} + 1\).

Iterate \(s_{n} \ge 3s_{n-1} - 1\) from \(s_{3} = 14\); solving the linear recurrence gives \(s_{n} \ge (27\cdot 3^{n-3} + 1)/2\).

Cleared to \(27\cdot 3^{n-3} + 1 \le 2s_{n}\).

Schur numbers grow at least exponentially with ratio \(3\); the upper bound \(s_{n} \le r_{n} \le \lfloor n!e\rfloor + 1\) grows factorially, and the true rate is unknown.

Two genuinely geometric inputs, neither in Mathlib: 1. Any four points in the plane determine an angle \(\ge 90^{\circ }\) — a convex-hull case analysis (line / triangle / quadrilateral). 2. The law of cosines consequence: an angle \(\ge 90^{\circ }\) at \(x_{j}\) with both adjacent sides \(\gt 1/\sqrt2\) forces the opposite side \(\gt 1\).

Given those, farGraph is \(K_{4}\)-free and turan_edge_bound at \(m = 3\) finishes.

The far-pairs graph of this configuration is exactly the balanced complete tripartite \(T_{3,n}\), with \(\lfloor n^{2}/3\rfloor \) edges — so the Turán bound is attained and the geometric optimum is realised by the graph-theoretic extremal configuration.

In a diameter-1 set, a pair at distance exactly \(1\) is a diameter pair. The key geometric fact: two diameter pairs must cross or share a point — if \(ab\) and \(cd\) were disjoint diameters, one of the four cross distances would exceed \(1\).

That crossing property forces the diameter graph to have \(\le n\) edges.

Contrast exercise 7.3.4(c), where without the diameter restriction the bound is of order \(n^{3/2}\); bounding the diameter collapses it to linear.