---

Claim. With $n_0(r)$ the least $N$ such that for every $n>N$ some family of subsets of $\{1,\ldots,n\}$, none containing another and each occurring size occurring at least $r$ times, has exactly $n-3$ distinct sizes, the write-up states that $n_0(4)=12$. As the forum entry describes the argument, no such family exists at $n=12$: the four sets on each of the two extreme levels are classified, and once the centers they force are removed, what remains on the middle levels comes down to four finite statements about antichains on seven points, the last of which is also checked exhaustively. Explicit families cover $13\le n\le19$. For $n\ge20$ the label construction of He and Tang ([HeTa26b] on the problem page; the source card records their results) applies: with $k=\lfloor n/2\rfloor$ and $m$ least with $\binom{m}{\lfloor m/2\rfloor}\ge k$, the inequality $\binom{k-5}{2}\ge k$ for $k\ge10$ gives $m\le k-5$, the room the construction needs.

Submission note. Posted to erdosproblems.com as a proof claim by Gilad Ronen (account H_Murdock) on 21 July 2026, giving "OpenAI Codex (initial draft); Hermes Agent / gpt-5.6-sol (audit and verifier hardening)" as the AI used:

This proves the exact threshold n_0(4)=12. Nonexistence at n=12 follows by classifying four sets on the two extreme levels; removing forced centres reduces the middle levels to four finite antichain assertions on seven points, the last also checked exhaustively. Explicit witnesses cover 13<=n<=19. For n>=20 the He--Tang label construction applies: with k=floor(n/2) and m minimal such that C(m,floor(m/2))>=k, the inequality C(k-5,2)>=k for k>=10 gives m<=k-5, its required room condition. Notes: Submitted as a partial result for r=4, not as a claim to settle Problem 776 in full. This is not a novelty or priority claim: proof claim #78 (17 July 2026) already states a broader exact theorem implying n_0(4)=12. The immutable commit includes explicit witnesses, strict verifiers (including under Python -O), an exhaustive checker, SAT search code, a publication manifest, and an audit record.

Depends on. [[problems/set_systems/E0776/claims/2026_02_10_he_tang|He and Tang's thresholds at r equal to 2 and 3]]: the write-up uses their level construction for $n\ge20$ and their bound $g(n,r)\le n-3$, the facts that confine the threshold to a finite range.

Covers. The case $r=4$ of Problem 776: the exact threshold $n_0(4)=12$, above He and Tang's lower bound $2r+2=10$ and agreeing at $r=4$ with the value $2r+4$ of the pending full claim, [[problems/set_systems/E0776/claims/2026_07_17_thiim|Thiim's determination of the threshold]]. Every $r\ge5$ is outside it.

Claimant. Gilad Ronen, whose write-up, "A candidate exact value for an Erdős–Trotter antichain threshold", is a Markdown document in a GitHub repository, linked at the commit the forum entry pins; the document itself names no author or tools. The entry was posted on 21 July 2026 under the username H_Murdock and names OpenAI Codex for the initial draft and Hermes Agent with gpt-5.6-sol for the audit and the hardening of a verifier. No formalization is reported.

Acceptance. None: the write-up is not refereed, the forum entry has no comments, no outside reviewer has endorsed it, no Lean audited by the corpus checks it, and the site labels the problem OPEN (page last edited 10 April 2026) and does not credit this result.