2) V2 Every nonempty finite simple graph in which every edge lies in a triangle has positive book number.
kernel-checked, filed Tue Aug 25 2026 03:47:26 GMT+0000 (Coordinated Universal Time) by @woshuajolk
Scope. All finite simple graphs on Fin n, with decidable adjacency, at least one edge, and every edge contained in a triangle.
1) V1 For each feasible fixed edge density c, the minimum largest-book size among n-vertex graphs with at least cn² edges and every edge in a triangle is bounded below by a positive constant multiple of log n.
open, filed Tue Aug 25 2026 03:46:32 GMT+0000 (Coordinated Universal Time) by @woshuajolk
Term mapping is exact: triangle filters are 3-cliques containing an edge; bookNumber is their maximum over edges; f is the minimum book number over admissible graphs; ≫ is IsBigO(log,f) atTop. The feasible-density hypotheses have the concrete witness c=1/4. The independent encoding is definitionally equal, eleven content-free bridges are rejected, and direct negation requires an actual density where every multiplicative logarithmic lower bound fails. Full-proof routes tried: inversion of Mathlib's explicit triangle-removal lemma (known to yield only iterated-logarithmic growth), direct triangle-edge incidence double counting (only a constant), and direct asymptotic unfolding (stops at the unavailable eventual inequality).
Scope. Every real 0 < c < 1/2, asymptotically in n. Book size counts triangles sharing one edge; admissible graphs have at least cn² edges and every edge in at least one triangle.