ERDŐS/DAILY

← back to the ledger

ERDőS #80 · PARTIAL

Erdős problem 80 — wave 5h report

Date: 2026-07-26 UTC

Claim labels used throughout:

certificate whose verification is transparent.

the explicitly cited theorem.

literature-search conclusion, not a theorem.

to an asymptotic theorem.

0. Mandatory live-page check

I accessed the live page through the Bright Data browser route on

2026-07-26. I separately extracted the rendered problem page, its LaTeX

view, its links and status fields, and the linked discussion thread. A

full-page screenshot agreed with the extracted text. The page says it was

last edited on 07 April 2026.

Verbatim live statement

> Let \(c>0\) and let \(f_c(n)\) be the maximal \(m\) such that every graph

> \(G\) with \(n\) vertices and at least \(cn^2\) edges, where each edge is

> contained in at least one triangle, must contain a book of size \(m\),

> that is, an edge shared by at least \(m\) different triangles.

>

> Estimate \(f_c(n)\). In particular, is it true that

> \(f_c(n)>n^{\epsilon}\) for some \(\epsilon>0\)? Or

> \(f_c(n)\gg \log n\)?

Live sources: problem page,

LaTeX view.

Verbatim listed results

> A problem of Erdős and Rothschild. Alon and Trotter showed that, provided

> \(c<1/4\), \(f_c(n)\ll_c n^{1/2}\). Szemerédi observed that his regularity

> lemma implies that \(f_c(n)\to \infty\).

>

> Edwards (unpublished) and Khadzhiivanov and Nikiforov [KhNi79] proved

> independently that \(f_c(n) \geq n/6\) when \(c>1/4\) (see [905]).

>

> Fox and Loh [FoLo12] proved that

> \[ > f_c(n) \leq n^{O(1/\log\log n)} > \]

> for all \(c<1/4\), disproving the first conjecture of Erdős.

>

> The best known lower bounds for \(f_c(n)\) are those from Szemerédi's

> regularity lemma, and as such remain very poor.

>

> See also [600] and the entry in the graphs problem collection.

The displayed references identify:

Rothschild on edges in triangles*, Combinatorica (2012), 619–628.

problem of P. Erdős about the maximum number of triangles with a common

edge*, C. R. Acad. Bulgare Sci. (1979), 1315–1318.

Sole live comment, verbatim

The page reports one comment. Its full mathematical text is:

> [Po18] by A. Potechin is another partial improvement on this problem.

>

> Moreover, this problem is also reported to be in [Er88], [Er92] and

> [Er98]

>

> [Er88]: P. Erd˝os, Problems and results in combinatorial analysis and

> graph theory, Proceedings of the First Japan Conference on Graph Theory

> and Applications (Hakone, 1986), Discrete Math. 72 (1988), p. 81-92.

>

> [Er92]: P. Erd˝os, Some of my favourite problems in various branches of

> combinatorics. Combinatorics 92 (Catania, 1992). Matematiche (Catania)

> 47 (1992), no. 2, p. 231-240

It was posted by Alfaiz at 12:26 on 04 May 2026. The rendered [Po18]

link points to https://arxiv.org/pdf/1412.1838.

Status and collaboration/proof markers

Thus the mandatory stop condition did not fire: there is no claimed proof

and no current worker.

1. Primary-source literature audit

Original problem

[b] The original six-page Erdős paper exists in the Rényi archive:

[P. Erdős, Some problems on finite and infinite graphs (1987),

PDF](https://www.renyi.hu/~p_erdos/1987-28.pdf). On printed page 226,

Problem 11 names Bruce Rothschild, defines \(f(n;c)\), records the Alon

and Szemerédi observations, and asks whether \(f(n;c)>n^\epsilon\), or at

least \(f(n;c)>\log n\). The downloaded primary PDF has SHA-256

b22809ce28667517eb39249bf54bff2140c548475306070989f3f8964870cb71.

The optional online mode of the checker downloads this PDF afresh, checks

that digest, and checks the OCR for the stable identifying tokens.

Fox–Loh upper construction

[b] The cited paper and arXiv identifier both exist:

edges in triangles*, Combinatorica 32 (2012), 619–628,

DOI 10.1007/s00493-012-2844-3,

arXiv:1106.0290.

Its Theorem 1.1 gives, for all sufficiently large \(n\), an \(n\)-vertex

graph with

\[ \frac{n^2}{4}\left(1-e^{-(\log n)^{1/6}}\right) \]

edges, every edge in a triangle, and no edge in more than

\(n^{14/\log\log n}\) triangles. Consequently, for every fixed

\(c<1/4\),

\[ f_c(n)\le n^{O(1/\log\log n)}. \]

The paper also explicitly says that Fox's improved graph-removal bound

gives

\[ f_c(n)\ge 2^{\Omega_c(\log^* n)} \]

for every fixed \(c>0\). This is still vastly below \(\log n\).

Potechin's omitted threshold-regime improvement

[b] The live comment's [Po18] link is a real primary source:

Aaron Potechin, A note on a problem of Erdos and Rothschild,

arXiv:1412.1838. The arXiv record says

it was submitted on 4 December 2014; [Po18] is the website comment's

citation label, not evidence of a 2018 journal publication. I found no

journal record and do not invent one.

Potechin defines the threshold-regime quantity with

\[ e(G)=\frac{n^2}{4}-nf(n). \]

His Theorem 1.3 states that, when \(f(n)\le n/1000\), either

\(bk(G)>n/1000\), or

\[ f(n)\bigl(f(n)+bk(G)\bigr)bk(G)\ge \frac{n^2}{1250}. \]

Corollary 1.4 gives the explicit lower bound

\[ bk(G)\ge \min\left\{ \frac{n}{50\sqrt{f(n)}}, \frac{n^2}{2500f(n)^2}, \frac{n}{1000} \right\} \]

under the paper's stated integrality hypothesis. This is a genuine

improvement near the \(n^2/4\) threshold. It does not settle fixed

\(c<1/4\), where \(f(n)\) is linear in \(n\).

Later explicit reformulation

[b] Noga Alon and Adi Shraibman,

*Algorithmic Number On the Forehead Protocols Yielding Dense

Ruzsa–Szemerédi Graphs and Hypergraphs*,

arXiv:2001.00387, gives explicit

communication-protocol versions of the dense Ruzsa–Szemerédi and

Fox–Loh-type constructions. In the graph case it recovers the same

\(n^{O(1/\log\log n)}\) scale; it does not improve the open logarithmic

lower bound.

Search conclusion

[c] I searched the exact title, the notations \(h(n,c)\),

\(\gamma(n,f)\), and \(f_c(n)\), the phrases “every edge is in/contained

in a triangle” with “booksize”, the Fox–Loh citation trail, and arXiv

records through July 2026. I found Potechin and Alon–Shraibman, but no

primary source claiming either \(f_c(n)\gg\log n\) or a counterexample to

it. This is an honest search result, not a proof that no uncatalogued

paper exists. It agrees with the live page's 2026 OPEN status.

The standalone checker has an --online-citations mode which independently

validates the arXiv metadata and abstract claims above, the Fox–Loh

Crossref record, and the original Erdős PDF.

2. A finite extremal formulation

For a graph \(G\), write

\[ b(G)=\max_{uv\in E(G)}|N(u)\cap N(v)| \]

for its booksize, with \(b(\varnothing)=0\). Define

\[ M_k(n)=\max\left\{ e(G): |V(G)|=n,\ \text{every edge of }G\text{ is in a triangle},\ b(G)\le k \right\}. \tag{2.1} \]

Also let

\[ F(n,E)=\min\left\{ b(G): |V(G)|=n,\ e(G)\ge E,\ \text{every edge is in a triangle} \right\}. \tag{2.2} \]

[a] Whenever \(1\le E\le\binom n2\),

\[ F(n,E)=\min\{k:E\le M_k(n)\}. \tag{2.3} \]

Indeed, \(E\le M_k(n)\) supplies a witness with at least \(E\) edges and

booksize at most \(k\). If \(E>M_{k-1}(n)\), no qualifying graph with at

least \(E\) edges can have booksize at most \(k-1\).

Therefore, with

\[ E_c(n)=\lceil cn^2\rceil, \]

[a]

\[ f_c(n)=F(n,E_c(n)) \tag{2.4} \]

provided \(E_c(n)\le\binom n2\). If \(E_c(n)>\binom n2\), there is no

qualifying simple graph, so the universal condition is vacuous and there

is no maximal finite \(m\).

3. A reusable degree-sum lemma

Lemma

[a] If \(G\) has \(n\) vertices, \(e>0\) edges, and

\(b(G)\le b\), then

\[ \sum_{v\in V(G)}d(v)^2\le e(n+b) \tag{3.1} \]

and consequently

\[ e\le \frac{n(n+b)}4. \tag{3.2} \]

Proof

For an edge \(uv\), let

\[ q=|N(u)\cap N(v)| \]

and let \(r\) be the number of vertices adjacent to neither \(u\) nor

\(v\). Partitioning the other \(n-2\) vertices gives

\[ d(u)+d(v)-n=q-r\le q\le b. \]

Summing over all edges,

\[ \sum_v d(v)^2 =\sum_{uv\in E(G)}(d(u)+d(v)) \le e(n+b). \]

Cauchy–Schwarz and \(\sum_vd(v)=2e\) give

\[ \frac{4e^2}{n}\le\sum_vd(v)^2\le e(n+b), \]

which yields (3.2). \(\square\)

4. Exact solution of the complete \(n=8\) finite problem

Theorem

[a] For \(n=8\),

\[ \boxed{ \bigl(M_0(8),M_1(8),\ldots,M_6(8)\bigr) =(0,12,18,21,24,24,28). } \tag{4.1} \]

The proof below is elementary. The checker independently exhausts the

two delicate upper bounds \(k=1,2\).

Sharp constructions

Each row is directly checked from its description.

| book cap \(k\) | graph | edges | actual booksize |

|---:|---|---:|---:|

| 1 | four triangles in a loose \(4\)-cycle | 12 | 1 |

| 2 | \(\overline K_2\vee C_6\) | 18 | 2 |

| 3 | \(K_{2,3,3}\) | 21 | 3 |

| 4 | \(K_8\) minus a perfect matching | 24 | 4 |

| 5 | \(K_8\) minus a perfect matching | 24 | 4 |

| 6 | \(K_8\) | 28 | 6 |

For the first row, one explicit set of triangles is

\[ 012,\quad 234,\quad 456,\quad 670. \]

For \(\overline K_2\vee C_6\), a cycle edge has the two apices as its

common neighbors, and an apex–cycle edge has the two cycle neighbors of

its cycle endpoint. Thus every edge has codegree exactly \(2\).

In a complete tripartite graph, an edge between two parts has the third

part as its common neighborhood, so \(K_{2,3,3}\) has booksize \(3\).

In \(K_8\) minus a perfect matching, an edge's endpoints have two

distinct forbidden partners, leaving exactly four common neighbors.

It remains to prove the upper bounds.

Cap \(k=1\): \(M_1(8)\le12\)

Suppose every edge lies in exactly one triangle. Then graph triangles

are edge-disjoint, and

\[ e(G)=3|\mathcal T|. \]

If \(e(G)\ge13\), then \(e(G)\ge15\), so choose five graph triangles.

Regard them as the blocks of a linear \(3\)-uniform hypergraph

\(\mathcal H\) on at most eight points. It has no Berge triangle: if

three blocks met pairwise in three distinct points, those intersection

points would form an additional graph triangle, putting its edges in

two triangles.

I now prove that no such \(\mathcal H\) exists. Let its used-point

degrees be \(r_1,\ldots,r_v>0\). There are \(15\) incidences. Linearity

gives

\[ \sum_i\binom{r_i}{2}\le\binom52=10. \tag{4.2} \]

If \(v\le6\), convexity makes the left side at least \(12\), so

\(v\in\{7,8\}\). The positive integer partitions of \(15\) satisfying

(4.2) are exactly:

| \(v\) | point-degree multiset | \(\sum\binom{r_i}{2}\) |

|---:|---|---:|

| 7 | \(3^2\,2^4\,1\) | 10 |

| 7 | \(3\,2^6\) | 9 |

| 8 | \(3^3\,2\,1^4\) | 10 |

| 8 | \(4\,2^4\,1^3\) | 10 |

| 8 | \(3^2\,2^3\,1^3\) | 9 |

| 8 | \(3\,2^5\,1^2\) | 8 |

| 8 | \(2^7\,1\) | 7 |

Build the intersection graph \(J\) on the five blocks. A point of

degree \(r\) contributes a clique \(K_r\), and these cliques are

edge-disjoint. Every triangle of \(J\) must lie in one of these

designated cliques; otherwise it is a Berge triangle.

The seven rows are impossible:

1. For \(2^7\,1\), \(J\) would be a triangle-free five-vertex graph with

seven edges, contradicting Mantel's elementary six-edge bound.

2. For \(3\,2^5\,1^2\), \(J\) has eight edges but only one permitted

triangle. Any eight-edge graph on five vertices is \(K_5\) minus two

edges and has at least \(10-2\cdot3=4\) triangles.

3. For \(3\,2^6\), \(J=K_5-e\) has seven triangles but only one

designated \(K_3\).

4. In either row with two \(K_3\)'s, the edge-disjoint triangles on five

block-vertices meet in one block. Every additional edge between the

two opposite pairs completes a non-designated triangle through that

common block. Yet the row requires three or four such edges.

5. For \(3^3\,2\,1^4\), three triangles and one edge would partition

\(E(K_5)\). Triangle contributions give even degree at every vertex,

while the final edge changes parity at its two endpoints, impossible

since all \(K_5\) degrees are even.

6. For \(4\,2^4\,1^3\), after the designated \(K_4\), the four remaining

edges join the fifth block to each \(K_4\) block. They correspond to

four distinct intersection points on that fifth block, impossible

for a three-element block.

This contradiction proves \(e(G)\le12\). The loose \(4\)-cycle shows

equality.

The checker also verifies this bound independently by inspecting all

\[ \binom{56}{5}=3{,}819{,}816 \]

five-triangle families on eight labelled vertices. Exactly 84,000

families are edge-disjoint, and every one has an additional triangle

in its edge union.

Cap \(k=2\): \(M_2(8)\le18\)

The degree-sum lemma first gives \(e(G)\le20\). Suppose

\(e(G)\in\{19,20\}\), and let \(H=\overline G\). For a nonedge \(uv\)

of \(H\), equivalently an edge of \(G\),

\[ |N_G(u)\cap N_G(v)| =6-|N_H(u)\cup N_H(v)|. \]

Every \(G\)-edge is in one or two triangles, so

\[ |N_H(u)\cup N_H(v)|\in\{4,5\} \quad\text{for every nonedge }uv\text{ of }H. \tag{4.3} \]

First, \(\delta(H)\ge2\). A degree-zero vertex and each of its seven

nonneighbors force all seven other degrees to be at least \(4\), far

above either available degree sum. If \(d_H(u)=1\), then each of the six

vertices other than \(u\) and its neighbor has degree at least \(3\) by

(4.3), again forcing degree sum at least \(20\).

If \(e(G)=20\), then \(e(H)=8\), so every \(H\)-degree is \(2\). The two

neighbors of any vertex share that vertex. If they were nonadjacent,

their neighborhood union would have size at most \(3\), contradicting

(4.3). Hence every component of the \(2\)-regular graph \(H\) is a

triangle, impossible on eight vertices.

If \(e(G)=19\), then \(e(H)=9\). Since all degrees are at least \(2\)

and sum to \(18\), the degree multiset is one of

\[ (4,2,2,2,2,2,2,2), \qquad (3,3,2,2,2,2,2,2). \tag{4.4} \]

For any vertex \(w\), its degree-two neighbors form a clique: two

nonadjacent such neighbors would share \(w\) and have neighborhood

union at most \(3\), violating (4.3). Such a clique has at most two

vertices, because each already uses one edge to \(w\).

The first sequence in (4.4) is therefore impossible: its degree-four

vertex has four degree-two neighbors. In the second sequence, call the

degree-three vertices \(x,y\). Each has at most two degree-two

neighbors, hence \(xy\in E(H)\), and each has exactly two low-degree

neighbors. Those two pairs must be disjoint; a shared low neighbor

would already have degree two from \(x,y\), but cliquehood at \(x\)

would force a third edge. Each pair is itself adjacent and therefore

saturated. The two remaining degree-two vertices can then only meet

each other, leaving them with degree one. This final contradiction

proves \(e(G)\le18\).

As an independent audit, the checker generates every labelled

complement with the degree sequences surviving the argument:

None satisfies (4.3).

Cap \(k=3\): \(M_3(8)\le21\)

The degree-sum lemma gives \(e\le22\). If \(e=22\), the degree sum is

\(44\). Among eight integer degrees with this sum, the minimum square

sum is attained by four \(5\)'s and four \(6\)'s:

\[ \sum_vd(v)^2\ge4\cdot25+4\cdot36=244. \]

But (3.1) gives

\[ \sum_vd(v)^2\le22(8+3)=242, \]

a contradiction. Thus \(e\le21\), sharply attained by \(K_{2,3,3}\).

Cap \(k=4\): \(M_4(8)\le24\)

Equation (3.2) immediately gives

\[ e\le\frac{8(8+4)}4=24, \]

sharply attained by \(K_8\) minus a perfect matching.

Cap \(k=5\): \(M_5(8)\le24\)

Equation (3.2) first gives \(e\le26\). If \(e=25\) or \(26\), then

\(\overline G\) has only three or two edges. Those missing edges touch

at most six vertices, so at least two vertices are isolated in

\(\overline G\). Their edge in \(G\) has all other six vertices as

common neighbors, giving a book of size \(6\), contrary to the cap.

Thus \(e\le24\), again attained by \(K_8\) minus a perfect matching.

Cap \(k=6\)

The complete graph \(K_8\) has 28 edges and booksize 6, and no simple

eight-vertex graph has more edges.

This completes the proof of (4.1).

Exact value of \(f_c(8)\)

Combining (2.3) with (4.1), [a]

\[ F(8,E)= \begin{cases} 1,&1\le E\le12,\\ 2,&13\le E\le18,\\ 3,&19\le E\le21,\\ 4,&22\le E\le24,\\ 6,&25\le E\le28. \end{cases} \tag{4.5} \]

In particular, there is no edge threshold for which the forced value is

exactly \(5\).

Since \(E=\lceil64c\rceil\), [a]

\[ \boxed{ f_c(8)= \begin{cases} 1,&0For \(c>7/16\), no simple graph on eight vertices has \(64c\) edges, so

the defining universal class is empty.

5. Independent exact census for \(3\le n\le7\)

The checker uses two independent exhaustive methods.

1. Union generation. Start with \(\{0\}\) and repeatedly adjoin the

bitwise union with each triangle edge-mask. This produces exactly all

unions of triangles.

2. All-mask scan. Inspect all \(2^{\binom n2}\) labelled graphs,

retain a graph iff the union of its present triangles equals its full

edge set, and compute all edge codegrees directly from bit-set

neighborhoods.

[a] The completeness observation is exact: every edge of \(G\) lies

in a triangle iff \(G\) is the union of its triangles. Thus the first

method omits no admissible graph, and the second is an independent

cross-check.

Both methods return the following frontiers. These rows are

[d] computational-only for \(n\le7\); the \(n=8\) row is the

elementary theorem proved above.

| \(n\) | \(M_0(n),M_1(n),\ldots,M_{n-2}(n)\) |

|---:|---|

| 3 | \(0,3\) |

| 4 | \(0,3,6\) |

| 5 | \(0,6,8,10\) |

| 6 | \(0,6,12,12,15\) |

| 7 | \(0,9,15,16,18,21\) |

| 8 | \(0,12,18,21,24,24,28\) |

The exact numbers of admissible labelled graphs by exact booksize are:

| \(n\) | booksize \(0,1,\ldots,n-2\) |

|---:|---|

| 3 | \(1,1\) |

| 4 | \(1,4,7\) |

| 5 | \(1,25,110,51\) |

| 6 | \(1,120,2487,2796,711\) |

| 7 | \(1,1155,78956,193396,118692,17725\) |

The total admissible labelled graph counts are

\[ 2,\ 12,\ 187,\ 6115,\ 409925 \]

for \(n=3,4,5,6,7\), respectively. The two methods also agree on a

SHA-256 digest of the full increasing mask list at each \(n\), not only

on these aggregate statistics.

6. Exact reduction to the quantitative triangle-removal bottleneck

Let \(\delta_\triangle(\varepsilon)\) denote any valid triangle-removal

function in the following convention:

> Every \(n\)-vertex graph requiring deletion of at least

> \(\varepsilon n^2\) edges to become triangle-free contains at least

> \(\delta_\triangle(\varepsilon)n^3\) triangles.

Suppose \(G\) has \(e(G)\ge cn^2\), every edge lies in a triangle, and

\(b(G)\le b\). Let \(T\) be its number of triangles and let

\(\tau_\triangle(G)\) be the minimum number of edges meeting every

triangle.

[a] Since every edge is covered,

\[ 3T=\sum_{uv\in E(G)}|N(u)\cap N(v)|\ge e(G). \]

Since a single edge meets at most \(b\) triangles, every triangle edge

cover has size at least

\[ \tau_\triangle(G)\ge\frac{T}{b} \ge\frac{e(G)}{3b} \ge\frac{c}{3b}n^2. \tag{6.1} \]

On the other hand,

\[ 3T\le b\,e(G)\le b\binom n2<\frac{bn^2}{2}, \]

so \(T

Applying the triangle-removal lemma at

\(\varepsilon=c/(3b)\) gives the exact implicit obstruction

\[ \boxed{ \delta_\triangle\!\left(\frac{c}{3b}\right) <\frac{b}{6n}. } \tag{6.2} \]

Thus any \(b\) for which the reverse strict inequality holds is too

small to be the booksize of a qualifying graph.

What would make the logarithmic bound follow by this route

[b] Fox's quantitative graph-removal theorem, substituted into

(6.2), yields the known \(2^{\Omega_c(\log^*n)}\) lower bound. Its tower

dependence does not reach \(\log n\).

[a] A bound of the form

\[ \delta_\triangle(\varepsilon)\ge \exp(-C/\varepsilon) \tag{6.3} \]

for all sufficiently small \(\varepsilon\) would be enough. Indeed, put

\(b=\alpha\log n\). Then (6.3) gives

\[ \delta_\triangle(c/(3b)) \ge n^{-3C\alpha/c}. \]

Choosing, for example, \(\alpha

\(n^{-1/2}\), which is eventually larger than

\(b/(6n)=O(\log n/n)\), contradicting (6.2). Hence (6.3) would imply

\(f_c(n)\gg_c\log n\).

[c] I do not prove (6.3), and do not claim that a general removal

bound of precisely this strength is necessary. The exact missing input

for this standard route is the scale-specific inequality

\[ \delta_\triangle(c/(3b))>\frac{b}{6n} \quad\text{for }b\asymp\log n. \]

A theorem tailored to triangle-covered, bounded-book graphs could also

supply it without improving the full triangle-removal lemma.

This identifies the genuine uniformity gap: the finite frontiers and

explicit \(n=8\) solution do not give a bound uniform in \(n\). In

particular, the \(b=1\) case is already tied to the

Ruzsa–Szemerédi \((6,3)\) phenomenon; finite exclusion is not the

asymptotic density statement.

7. Reproducibility and cost

The standalone checker is

runs/erdos80_wave5h_verify.py.

It uses only the Python standard library. Run:

python runs/erdos80_wave5h_verify.py

On this VM it completed all finite checks in about 20 seconds. It:

  • cross-checks every \(n\le7\) result by union generation and an

independent scan of every labelled graph mask;

  • verifies all six \(n=8\) extremal constructions;
  • checks all 3,819,816 five-triangle families for the \(M_1(8)\) upper

bound;

  • generates and checks all 143,927 complement graphs in the degree

classes relevant to \(M_2(8)\);

  • checks every two- or three-edge complement relevant to \(M_5(8)\);
  • recomputes the edge-threshold and \(c\)-interval translations.

To re-fetch and validate the primary-source citation records as well,

run:

python runs/erdos80_wave5h_verify.py --online-citations

That mode completed in about 23 seconds and reported every citation

audit PASS.

I did not perform a naive \(n=9\) all-graph scan. It would inspect

\[ 2^{\binom{9}{2}}=2^{36}=68{,}719{,}476{,}736 \]

masks. Scaling the measured \(n=7\) scan gives roughly 109 single-core

hours at the same per-mask throughput, about 4.5 core-days (roughly

\$5.50–\$16.50 at \$0.05–\$0.15/core-hour). Since a nine-vertex mask

has more triangles to inspect, this is optimistic. It would still be

only a finite result. Structural generation or certified SAT would be

the appropriate next computational method.

8. Outcome

The asymptotic logarithmic question remains open. The concrete progress

is a complete, elementary exact solution at \(n=8\), explicit extremal

graphs at every book cap, an independently reproduced \(n\le7\) census,

and the precise quantitative triangle-removal inequality that the

standard lower-bound route must beat.

PARTIAL: Proved the exact frontier \(M_k(8)=(0,12,18,21,24,24,28)\), independently verified the full \(n\le7\) census, and isolated the removal-lemma scale needed for \(f_c(n)\gg\log n\); the asymptotic problem remains open.

This is the AI working report, labelled by outcome — not an independently verified claim unless marked PROVED. ← ledger