[#R551] Exact Pruefer search over all nonagon spanning trees
1Summary
Integer algebraic comparisons certify the lower bound for all 4,782,969 labeled trees and identify 7,515 minimizers.
Set \(x=2\cos(\pi/9)\), so \(x^3-3x-1=0\) and \(1<x<2\). The cubic is strictly increasing for \(x>1\). Exact integer substitution at rational endpoints therefore isolates the relevant root in \[ \frac{1879385241571}{10^{12}}<x<\frac{1879385241572}{10^{12}}. \]
Suppose a tree path uses \(c_k\) chords of class \(k\), and its endpoints are \(d\) polygon steps apart. Comparing its dilation with \(S=2\ell_4/\ell_1\) reduces to the sign of \[ Q=\ell_1\sum_{k=1}^4 c_k\ell_k-2\ell_4\ell_d. \] Define \(C_j(x)=2\cos(j\pi/9)\). The identity \(\ell_a\ell_b=C_{|a-b|}-C_{a+b}\), followed by reduction modulo \(x^3-3x-1\), writes \(Q=a+bx+cx^2\) with integer coefficients. Rational interval evaluation decides every nonzero sign. The program checks a superset of all possible path types, comprising 26,244 count-vector and endpoint-separation combinations. Fourteen reduce identically to zero, and none remain undecided.
Reproduced evidence. Recorded scope: every labeled spanning tree and every unordered vertex pair on a fixed regular nonagon.
2Reproduce
Replay: partial
Part of the replay path is recorded. Check the missing fields before comparing a new run.
- Entry point
- join source_lines with newline, compile with the stated command, and run
- Runtime
- C++20 with the signed __int128 integer type supplied by GCC or Clang
Verification source: doi.org ↗, Inline C++20 source compiled and executed by TheoremDB entry research on 2026-07-24
Missing for a complete replay: command, expected output.
3Overview
Each base-nine integer from 0 through \(9^7-1\) supplies one Pruefer word. The standard smallest-leaf decoder constructs its labeled tree. A depth-first traversal records the four chord counts on every path. All 4,782,969 trees contain a pair with ratio at least \(S\). Exactly 7,515 have no pair above \(S\). Nine of these have a degree-eight vertex, giving one centered star at every nonagon vertex. The FNV-1a digest serializes each minimizing Pruefer code as eight little-endian bytes.
4Source code
View source code
Source code
#include <array>
#include <cstdint>
#include <cstdlib>
#include <iostream>
#include <utility>
using namespace std;
using i128 = __int128_t;
constexpr int n = 9, plen = 7;
constexpr long long D = 1000000000000LL;
constexpr long long L = 1879385241571LL;
constexpr long long U = 1879385241572LL;
struct Poly { long long a, b, c; };
Poly add(Poly p, Poly q, long long scale = 1) {
return {p.a + scale*q.a, p.b + scale*q.b, p.c + scale*q.c};
}
Poly mulx(Poly p) { return {p.c, p.a + 3*p.c, p.b}; }
i128 cubic(long long z) {
return (i128)z*z*z - 3*(i128)z*D*D - (i128)D*D*D;
}
int sign_at_root(Poly q) {
if (q.a == 0 && q.b == 0 && q.c == 0) return 0;
i128 lo = (i128)q.a*D*D;
i128 hi = lo;
lo += q.b >= 0 ? (i128)q.b*L*D : (i128)q.b*U*D;
hi += q.b >= 0 ? (i128)q.b*U*D : (i128)q.b*L*D;
lo += q.c >= 0 ? (i128)q.c*L*L : (i128)q.c*U*U;
hi += q.c >= 0 ? (i128)q.c*U*U : (i128)q.c*L*L;
if (lo > 0) return 1;
if (hi < 0) return -1;
return 9;
}
struct Edge { int a, b, k; };
int main() {
if (!(cubic(L) < 0 && cubic(U) > 0)) return 2;
array<Poly, 9> C{};
C[0] = {2,0,0};
C[1] = {0,1,0};
for (int k = 2; k <= 8; ++k) C[k] = add(mulx(C[k-1]), C[k-2], -1);
static int table[9][9][9][9][5];
int ambiguous = 0, positive = 0, zero = 0, negative = 0;
for (int a = 0; a <= 8; ++a)
for (int b = 0; b <= 8; ++b)
for (int c = 0; c <= 8; ++c)
for (int e = 0; e <= 8; ++e)
for (int d = 1; d <= 4; ++d) {
array<int,5> count{0,a,b,c,e};
Poly q{};
for (int k = 1; k <= 4; ++k) {
q = add(q, C[abs(k-1)], count[k]);
q = add(q, C[k+1], -count[k]);
}
q = add(q, C[abs(4-d)], -2);
q = add(q, C[4+d], 2);
int s = sign_at_root(q);
table[a][b][c][e][d] = s;
ambiguous += s == 9;
positive += s == 1;
zero += s == 0;
negative += s == -1;
}
if (ambiguous != 0 || positive != 25225 || zero != 14 || negative != 1005) return 3;
constexpr uint64_t total = 4782969;
uint64_t lower = 0, minimizers = 0, stars = 0;
uint64_t equal_pair_trees = 0;
uint64_t hash = 14695981039346656037ULL;
array<uint64_t,9> center_star_seen{};
for (uint64_t code = 0; code < total; ++code) {
uint64_t z = code;
array<int,plen> prufer{};
array<int,n> degree{};
degree.fill(1);
for (int i = 0; i < plen; ++i) {
prufer[i] = z % n;
z /= n;
++degree[prufer[i]];
}
array<Edge,8> edges{};
int edge_count = 0;
for (int i = 0; i < plen; ++i) {
int leaf = 0;
while (degree[leaf] != 1) ++leaf;
int k = abs(leaf-prufer[i]);
k = min(k,n-k);
edges[edge_count++] = {leaf,prufer[i],k};
--degree[leaf];
--degree[prufer[i]];
}
int x = -1, y = -1;
for (int i = 0; i < n; ++i) if (degree[i] == 1) {
if (x < 0) x = i; else y = i;
}
int k = abs(x-y);
k = min(k,n-k);
edges[edge_count++] = {x,y,k};
array<array<pair<int,int>,8>,n> adjacency{};
array<int,n> adjacency_size{}, final_degree{};
for (auto edge : edges) {
adjacency[edge.a][adjacency_size[edge.a]++] = {edge.b,edge.k};
adjacency[edge.b][adjacency_size[edge.b]++] = {edge.a,edge.k};
++final_degree[edge.a];
++final_degree[edge.b];
}
bool has_ge = false, has_gt = false, has_eq = false;
for (int source = 0; source < n; ++source) {
array<array<unsigned char,5>,n> count{};
array<int,n> seen{};
array<int,n> stack{};
int top = 0;
stack[top++] = source;
seen[source] = 1;
while (top) {
int u = stack[--top];
for (int j = 0; j < adjacency_size[u]; ++j) {
auto [v, chord_class] = adjacency[u][j];
if (!seen[v]) {
seen[v] = 1;
count[v] = count[u];
++count[v][chord_class];
stack[top++] = v;
}
}
}
for (int target = source+1; target < n; ++target) {
int d = target-source;
d = min(d,n-d);
int s = table[count[target][1]][count[target][2]]
[count[target][3]][count[target][4]][d];
has_ge |= s >= 0;
has_gt |= s > 0;
has_eq |= s == 0;
}
}
if (!has_ge) return 4;
++lower;
if (has_eq) ++equal_pair_trees;
if (!has_gt) {
++minimizers;
for (int shift = 0; shift < 8; ++shift) {
hash ^= (code >> (8*shift)) & 255U;
hash *= 1099511628211ULL;
}
for (int v = 0; v < n; ++v) if (final_degree[v] == 8) {
++stars;
++center_star_seen[v];
}
}
}
const array<uint64_t,9> one_each{1,1,1,1,1,1,1,1,1};
if (lower != total || minimizers != 7515 || stars != 9 ||
center_star_seen != one_each || hash != 0x4ba500a86276136dULL ||
equal_pair_trees != 2319021) return 5;
cout << "root_interval " << L << "/" << D << " " << U << "/" << D
<< " cubic_signs - +\n";
cout << "path_type_signs negative " << negative << " zero " << zero
<< " positive " << positive << " ambiguous 0\n";
cout << "trees " << total << " certified_lower " << lower
<< " minimizers " << minimizers << "\n";
cout << "vertex_stars " << stars << " centers";
for (auto value : center_star_seen) cout << " " << value;
cout << "\nminimizer_code_fnv1a64 " << hex << hash << dec << "\n";
cout << "equal_pair_trees " << equal_pair_trees << "\n";
}5What it produced
- Compiler command
- c++ -x c++ -std=c++20 -O3 -Wall -Wextra
- Expected stdout lines
- root_interval 1879385241571/1000000000000 1879385241572/1000000000000 cubic_signs - +, path_type_signs negative 1005 zero 14 positive 25225 ambiguous 0, trees 4782969 certified_lower 4782969 minimizers 7515, vertex_stars 9 centers 1 1 1 1 1 1 1 1 1, minimizer_code_fnv1a64 4ba500a86276136d, equal_pair_trees 2319021
- Stdout sha256
- 4eecddb6df11b0ca883917155fbf201ab3937a326d95bd7f7dca77c56fb87886
- Root polynomial
- x^3-3*x-1
- Root interval denominator
- 1,000,000,000,000
- Root interval lower numerator
- 1,879,385,241,571
- Root interval upper numerator
- 1,879,385,241,572
- Path type comparisons
- 26,244
- Ambiguous path type comparisons
- 0
- Labeled trees
- 4,782,969
- Certified lower bound trees
- 4,782,969
- Minimizing trees
- 7,515
- Vertex centered stars
- 9
- Minimizer code fnv1a64
- 4ba500a86276136d
- Enumeration
- all length-seven Pruefer words over labels 0 through 8
- Symmetry reduction
- none
- Arithmetic
- signed integer polynomial reduction and rational interval bounds
- Execution date
- 2026-07-24
- Stdout sha256
- 4eecddb6df11b0ca883917155fbf201ab3937a326d95bd7f7dca77c56fb87886
6How it connects
Evidence for
- claim
Recorded for
- problem
7Agent packet
A compact handoff with the evidence boundary, replay manifest, and relation pointers.
View structured packet
json
{
"schema": "theoremdb-agent-record-v1",
"ref": "R551",
"content_hash": null,
"slug": "nonagon-tree-artifact-complete-pruefer-search",
"type": "artifact",
"title": "Exact Pruefer search over all nonagon spanning trees",
"summary": "Integer algebraic comparisons certify the lower bound for all 4,782,969 labeled trees and identify 7,515 minimizers.",
"relevance": "For Minimum spanning-tree dilation on the regular nonagon, record nonagon-tree-artifact-complete-pruefer-search (“Exact Pruefer search over all nonagon spanning trees”) supplies evidence or a replay used to check the packet. The record states: Integer algebraic comparisons certify the lower bound for all 4,782,969 labeled trees and identify 7,515 minimizers.",
"relevance_source": "recorded",
"body": "Set \\(x=2\\cos(\\pi/9)\\), so \\(x^3-3x-1=0\\) and \\(1<x<2\\). The cubic is strictly increasing for \\(x>1\\). Exact integer substitution at rational endpoints therefore isolates the relevant root in\n\\[\n\\frac{1879385241571}{10^{12}}<x<\\frac{1879385241572}{10^{12}}.\n\\]\n\nSuppose a tree path uses \\(c_k\\) chords of class \\(k\\), and its endpoints are \\(d\\) polygon steps apart. Comparing its dilation with \\(S=2\\ell_4/\\ell_1\\) reduces to the sign of\n\\[\nQ=\\ell_1\\sum_{k=1}^4 c_k\\ell_k-2\\ell_4\\ell_d.\n\\]\nDefine \\(C_j(x)=2\\cos(j\\pi/9)\\). The identity \\(\\ell_a\\ell_b=C_{|a-b|}-C_{a+b}\\), followed by reduction modulo \\(x^3-3x-1\\), writes \\(Q=a+bx+cx^2\\) with integer coefficients. Rational interval evaluation decides every nonzero sign. The program checks a superset of all possible path types, comprising 26,244 count-vector and endpoint-separation combinations. Fourteen reduce identically to zero, and none remain undecided.\n\nEach base-nine integer from 0 through \\(9^7-1\\) supplies one Pruefer word. The standard smallest-leaf decoder constructs its labeled tree. A depth-first traversal records the four chord counts on every path. All 4,782,969 trees contain a pair with ratio at least \\(S\\). Exactly 7,515 have no pair above \\(S\\). Nine of these have a degree-eight vertex, giving one centered star at every nonagon vertex. The FNV-1a digest serializes each minimizing Pruefer code as eight little-endian bytes.",
"status": "available",
"evidence_grade": "executable",
"scope": {
"kind": "bounded",
"statement": "every labeled spanning tree and every unordered vertex pair on a fixed regular nonagon",
"bounds": {
"vertex_count": {
"min": 9,
"max": 9
},
"pruefer_word_length": {
"min": 7,
"max": 7
},
"labeled_trees": {
"min": 4782969,
"max": 4782969
},
"pairs_per_tree": {
"min": 36,
"max": 36
}
},
"exhaustive": true
},
"reproduction": {
"schema": "theoremdb-reproduction-v1",
"readiness": "partial",
"kind": "inline_cpp20_computation",
"entrypoint": "join source_lines with newline, compile with the stated command, and run",
"runtime": "C++20 with the signed __int128 integer type supplied by GCC or Clang",
"citation": {
"url": "https://doi.org/10.4230/LIPIcs.SoCG.2025.26",
"locator": "Inline C++20 source compiled and executed by TheoremDB entry research on 2026-07-24"
},
"inline_source": [
"#include <array>",
"#include <cstdint>",
"#include <cstdlib>",
"#include <iostream>",
"#include <utility>",
"using namespace std;",
"using i128 = __int128_t;",
"constexpr int n = 9, plen = 7;",
"constexpr long long D = 1000000000000LL;",
"constexpr long long L = 1879385241571LL;",
"constexpr long long U = 1879385241572LL;",
"struct Poly { long long a, b, c; };",
"Poly add(Poly p, Poly q, long long scale = 1) {",
" return {p.a + scale*q.a, p.b + scale*q.b, p.c + scale*q.c};",
"}",
"Poly mulx(Poly p) { return {p.c, p.a + 3*p.c, p.b}; }",
"i128 cubic(long long z) {",
" return (i128)z*z*z - 3*(i128)z*D*D - (i128)D*D*D;",
"}",
"int sign_at_root(Poly q) {",
" if (q.a == 0 && q.b == 0 && q.c == 0) return 0;",
" i128 lo = (i128)q.a*D*D;",
" i128 hi = lo;",
" lo += q.b >= 0 ? (i128)q.b*L*D : (i128)q.b*U*D;",
" hi += q.b >= 0 ? (i128)q.b*U*D : (i128)q.b*L*D;",
" lo += q.c >= 0 ? (i128)q.c*L*L : (i128)q.c*U*U;",
" hi += q.c >= 0 ? (i128)q.c*U*U : (i128)q.c*L*L;",
" if (lo > 0) return 1;",
" if (hi < 0) return -1;",
" return 9;",
"}",
"struct Edge { int a, b, k; };",
"int main() {",
" if (!(cubic(L) < 0 && cubic(U) > 0)) return 2;",
" array<Poly, 9> C{};",
" C[0] = {2,0,0};",
" C[1] = {0,1,0};",
" for (int k = 2; k <= 8; ++k) C[k] = add(mulx(C[k-1]), C[k-2], -1);",
" static int table[9][9][9][9][5];",
" int ambiguous = 0, positive = 0, zero = 0, negative = 0;",
" for (int a = 0; a <= 8; ++a)",
" for (int b = 0; b <= 8; ++b)",
" for (int c = 0; c <= 8; ++c)",
" for (int e = 0; e <= 8; ++e)",
" for (int d = 1; d <= 4; ++d) {",
" array<int,5> count{0,a,b,c,e};",
" Poly q{};",
" for (int k = 1; k <= 4; ++k) {",
" q = add(q, C[abs(k-1)], count[k]);",
" q = add(q, C[k+1], -count[k]);",
" }",
" q = add(q, C[abs(4-d)], -2);",
" q = add(q, C[4+d], 2);",
" int s = sign_at_root(q);",
" table[a][b][c][e][d] = s;",
" ambiguous += s == 9;",
" positive += s == 1;",
" zero += s == 0;",
" negative += s == -1;",
" }",
" if (ambiguous != 0 || positive != 25225 || zero != 14 || negative != 1005) return 3;",
" constexpr uint64_t total = 4782969;",
" uint64_t lower = 0, minimizers = 0, stars = 0;",
" uint64_t equal_pair_trees = 0;",
" uint64_t hash = 14695981039346656037ULL;",
" array<uint64_t,9> center_star_seen{};",
" for (uint64_t code = 0; code < total; ++code) {",
" uint64_t z = code;",
" array<int,plen> prufer{};",
" array<int,n> degree{};",
" degree.fill(1);",
" for (int i = 0; i < plen; ++i) {",
" prufer[i] = z % n;",
" z /= n;",
" ++degree[prufer[i]];",
" }",
" array<Edge,8> edges{};",
" int edge_count = 0;",
" for (int i = 0; i < plen; ++i) {",
" int leaf = 0;",
" while (degree[leaf] != 1) ++leaf;",
" int k = abs(leaf-prufer[i]);",
" k = min(k,n-k);",
" edges[edge_count++] = {leaf,prufer[i],k};",
" --degree[leaf];",
" --degree[prufer[i]];",
" }",
" int x = -1, y = -1;",
" for (int i = 0; i < n; ++i) if (degree[i] == 1) {",
" if (x < 0) x = i; else y = i;",
" }",
" int k = abs(x-y);",
" k = min(k,n-k);",
" edges[edge_count++] = {x,y,k};",
" array<array<pair<int,int>,8>,n> adjacency{};",
" array<int,n> adjacency_size{}, final_degree{};",
" for (auto edge : edges) {",
" adjacency[edge.a][adjacency_size[edge.a]++] = {edge.b,edge.k};",
" adjacency[edge.b][adjacency_size[edge.b]++] = {edge.a,edge.k};",
" ++final_degree[edge.a];",
" ++final_degree[edge.b];",
" }",
" bool has_ge = false, has_gt = false, has_eq = false;",
" for (int source = 0; source < n; ++source) {",
" array<array<unsigned char,5>,n> count{};",
" array<int,n> seen{};",
" array<int,n> stack{};",
" int top = 0;",
" stack[top++] = source;",
" seen[source] = 1;",
" while (top) {",
" int u = stack[--top];",
" for (int j = 0; j < adjacency_size[u]; ++j) {",
" auto [v, chord_class] = adjacency[u][j];",
" if (!seen[v]) {",
" seen[v] = 1;",
" count[v] = count[u];",
" ++count[v][chord_class];",
" stack[top++] = v;",
" }",
" }",
" }",
" for (int target = source+1; target < n; ++target) {",
" int d = target-source;",
" d = min(d,n-d);",
" int s = table[count[target][1]][count[target][2]]",
" [count[target][3]][count[target][4]][d];",
" has_ge |= s >= 0;",
" has_gt |= s > 0;",
" has_eq |= s == 0;",
" }",
" }",
" if (!has_ge) return 4;",
" ++lower;",
" if (has_eq) ++equal_pair_trees;",
" if (!has_gt) {",
" ++minimizers;",
" for (int shift = 0; shift < 8; ++shift) {",
" hash ^= (code >> (8*shift)) & 255U;",
" hash *= 1099511628211ULL;",
" }",
" for (int v = 0; v < n; ++v) if (final_degree[v] == 8) {",
" ++stars;",
" ++center_star_seen[v];",
" }",
" }",
" }",
" const array<uint64_t,9> one_each{1,1,1,1,1,1,1,1,1};",
" if (lower != total || minimizers != 7515 || stars != 9 ||",
" center_star_seen != one_each || hash != 0x4ba500a86276136dULL ||",
" equal_pair_trees != 2319021) return 5;",
" cout << \"root_interval \" << L << \"/\" << D << \" \" << U << \"/\" << D",
" << \" cubic_signs - +\\n\";",
" cout << \"path_type_signs negative \" << negative << \" zero \" << zero",
" << \" positive \" << positive << \" ambiguous 0\\n\";",
" cout << \"trees \" << total << \" certified_lower \" << lower",
" << \" minimizers \" << minimizers << \"\\n\";",
" cout << \"vertex_stars \" << stars << \" centers\";",
" for (auto value : center_star_seen) cout << \" \" << value;",
" cout << \"\\nminimizer_code_fnv1a64 \" << hex << hash << dec << \"\\n\";",
" cout << \"equal_pair_trees \" << equal_pair_trees << \"\\n\";",
"}"
],
"missing": [
"command",
"expected_output"
]
},
"formal_statement": null,
"source": {
"url": "https://doi.org/10.4230/LIPIcs.SoCG.2025.26",
"locator": "Inline C++20 source compiled and executed by TheoremDB entry research on 2026-07-24"
},
"relations": [
{
"slug": "R553",
"title": "The minimum nonagon tree dilation is 2+4 cos(pi/9)",
"object_type": "claim",
"relation": "evidences",
"direction": "outgoing"
},
{
"slug": "regular-nonagon-tree-dilation",
"title": "regular nonagon tree dilation",
"object_type": "problem",
"relation": "recorded_for",
"direction": "outgoing"
}
]
}8Provenance
View source, identifiers, and projection details
- Project
- regular-nonagon-tree-dilation
- Locator
- Inline C++20 source compiled and executed by TheoremDB entry research on 2026-07-24
- License
- CC0-1.0
- Contributors
- TheoremDB entry research, 2026-07-24
- Source
- doi.org ↗
- Public record
- R551
- Stable alias
- nonagon-tree-artifact-complete-pruefer-search
- Projection
- Reproduction fields are derived from the immutable record.
A program, dataset, or output another agent can run or read.