def TriangleIntersecting.IsTriangleIntersecting {n : ℕ} (F : Finset (SimpleGraph (Fin n))) : Prop

A family $F$ of graphs on a common vertex set is triangle-intersecting if every pair of graphs in $F$ shares at least one triangle, i.e. $G_1 \cap G_2$ contains a 3-clique.

theorem TriangleIntersecting.cliqueFree_three_of_card_le_two {n : ℕ} (hn : n ≤ 2) (G : SimpleGraph (Fin n)) : G.CliqueFree 3

Any graph on at most 2 vertices is triangle-free (3-clique-free).

theorem TriangleIntersecting.triangle_intersecting_bound_small {n : ℕ} (hn : n ≤ 2) (F : Finset (SimpleGraph (Fin n))) (hF : IsTriangleIntersecting F) : F.card < 2 ^ (n.choose 2 - 2)

Base case of the triangle-intersecting bound for $n \le 2$: such a family must be empty.

theorem TriangleIntersecting.complete_of_not_cliqueFree_fin3 (G : SimpleGraph (Fin 3)) (h : ¬G.CliqueFree 3) : G = ⊤

A graph on 3 vertices that contains a 3-clique must be the complete graph $K_3$.

theorem TriangleIntersecting.triangle_intersecting_bound_three (F : Finset (SimpleGraph (Fin 3))) (hF : IsTriangleIntersecting F) : F.card < 2 ^ (Nat.choose 3 2 - 2)

The triangle-intersecting bound for $n = 3$: the family contains only $K_3$, so its cardinality is at most $1 < 2$.

theorem TriangleIntersecting.coverage_arithmetic {r s m k : ℕ} (hr : 1 ≤ r) (hcov : k * m = r * s) (hlt : 2 * r < m) (hk : 0 < k) : (r - 1) * s < (m - 2) * k

Arithmetic lemma extracting the exponent gain from the covering relation $k m = r s$ together with $2r < m$: $(r-1) s < (m-2) k$.

theorem TriangleIntersecting.bound_from_pow_bound {F_card r s m k : ℕ} (hpow : F_card ^ k ≤ (2 ^ (r - 1)) ^ s) (harith : (r - 1) * s < (m - 2) * k) : F_card < 2 ^ (m - 2)

From the Shearer-style power inequality $|F|^k \le (2^{r-1})^s$ combined with the arithmetic gap $(r-1) s < (m-2) k$, deduce the desired bound $|F| < 2^{m-2}$.

theorem TriangleIntersecting.shearer_bipartition_bound {n : ℕ} (hn : 4 ≤ n) (F : Finset (SimpleGraph (Fin n))) (hF : IsTriangleIntersecting F) (hne : F.Nonempty) : ∃ (r : ℕ) (s : ℕ) (k : ℕ), 1 ≤ r ∧ 0 < k ∧ 2 * r < n.choose 2 ∧ k * n.choose 2 = r * s ∧ F.card ^ k ≤ (2 ^ (r - 1)) ^ s

Existence of a Shearer-style bipartition covering for any non-empty triangle-intersecting family on $n \ge 4$ vertices, providing parameters $r,s,k$ along with the projection bound $|F|^k \le (2^{r-1})^s$ used to derive the main theorem.

theorem TriangleIntersecting.triangle_intersecting_bound (n : ℕ) (F : Finset (SimpleGraph (Fin n))) (hF : IsTriangleIntersecting F) : F.card < 2 ^ (n.choose 2 - 2)

Chung-Graham-Frankl-Shearer (Theorem 10.4.9): every triangle-intersecting family of graphs on $n$ labeled vertices has size strictly less than $2^{\binom{n}{2} - 2}$.