feat(ErdosProblems/567): Ramsey size linearity of Q3, K33, H5

[ruskaruma]

This PR adds the formal statement for Erdős Problem 567 (Issue #796) and refactors the sizeRamsey definition for code reuse.

Changes

New Files

• ForMathlib/Combinatorics/SimpleGraph/SizeRamsey.lean: Shared definitions for sizeRamsey and IsRamseySizeLinear
• ErdosProblems/567.lean: Formalization of Problem 567

Modified Files

• ErdosProblems/566.lean: Updated to import shared sizeRamsey from ForMathlib

Problem Statement

Let $G$ be either $Q_3$ (3-cube), $K_{3,3}$, or $H_5$ ($C_5$ with two vertex-disjoint chords). Is $G$ Ramsey size linear?

Implementation Details

• Q3: 3-dimensional hypercube (8 vertices, 12 edges)
• K33: Complete bipartite graph (6 vertices, 9 edges)
• H5: Cycle $C_5$ with chords {0,2} and {1,3} (5 vertices, 7 edges)

Follows the sizeRamsey definition established in #1567.

Closes #796

[ruskaruma]

Quick question before the review:

I have defined the H5 constructively as C5 with chords {0,2} and {1,3}. The problem statement mentions that it can also be described as K4 with one edge subdivided (K4*). Should I add a comment or lemma noting these are isomorphic, or is the current definition sufficient?

[YaelDillies]

A comment is certainly enough. The subdivision definition is much more complicated than your current one

[ruskaruma]

A comment is certainly enough. The subdivision definition is much more complicated than your current one

Got it. Thanks.

[YaelDillies]

Thanks!

[ruskaruma]

Thanks!

Thankyou so much for the help on this one.