[#R82] Exact exhaustive certificate for D_20
1Summary
Inline C++ enumerates every first row, reconstructs exact block determinants by CRT, and checks each one with Bareiss elimination.
The program enumerates masks 0 through 524287. Bit \(d-1\) is \(t_d\), which fixes the row-string convention. For each mask it constructs \(B+H\) and \(B-H\), then computes both determinants by Gaussian elimination in \(\mathbf F_{65521}\) and \(\mathbf F_{65519}\). Trial division inside the program confirms that both moduli are prime.
Hadamard's inequality gives \(|\det(B+H)|\leq(2\sqrt{10})^{10}=102400000\), since its entries lie in \(\{0,1,2\}\). It gives \(|\det(B-H)|\leq(\sqrt{10})^{10}=100000\). The modulus product is 4292870399, which exceeds twice the larger bound. Signed CRT reconstruction therefore recovers each integer factor uniquely. A separate fraction-free Bareiss calculation agrees with both reconstructed factors for every mask. Every division is checked for exactness, and the largest Bareiss entry seen is 16300.
Reproduced evidence. Recorded scope: all 524288 zero-diagonal binary symmetric Toeplitz matrices of order 20.
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 c++ -std=c++20 -O3, and run
- Runtime
- C++20 with signed __int128 support
Verification source: doi.org ↗, Inline C++20 source below, compiled and executed on 2026-07-24
Missing for a complete replay: command, expected output.
3Overview
Compiled with Apple clang 17.0.0 using `c++ -std=c++20 -O3 -march=native -Wall -Wextra -pedantic`, the run finished in about five seconds on an Apple Silicon workstation. The stable six-line output has SHA-256 digest `0cd96a72b56889ff43822fdc0b60b656f9aa89d7392f5f8ae386366258dc527f`.
4Source code
View source code
Source code
#include <algorithm>
#include <array>
#include <cstdlib>
#include <cstdint>
#include <iostream>
#include <limits>
#include <string>
#include <vector>
using Matrix10 = std::array<std::array<std::int64_t, 10>, 10>;
static std::uint64_t largest_bareiss_entry = 0;
static std::uint64_t magnitude(std::int64_t value) {
return value < 0
? static_cast<std::uint64_t>(-static_cast<__int128>(value))
: static_cast<std::uint64_t>(value);
}
static std::int64_t det_bareiss(Matrix10 a) {
std::int64_t previous = 1;
std::int64_t sign = 1;
for (int k = 0; k < 9; ++k) {
int pivot_row = k;
while (pivot_row < 10 && a[pivot_row][k] == 0) {
++pivot_row;
}
if (pivot_row == 10) {
return 0;
}
if (pivot_row != k) {
std::swap(a[pivot_row], a[k]);
sign = -sign;
}
const std::int64_t pivot = a[k][k];
for (int i = k + 1; i < 10; ++i) {
for (int j = k + 1; j < 10; ++j) {
const __int128 numerator =
static_cast<__int128>(a[i][j]) * pivot
- static_cast<__int128>(a[i][k]) * a[k][j];
if (numerator % previous != 0) {
std::cerr << "non-exact Bareiss division\n";
std::exit(2);
}
const __int128 quotient = numerator / previous;
if (quotient < std::numeric_limits<std::int64_t>::min()
|| quotient > std::numeric_limits<std::int64_t>::max()) {
std::cerr << "Bareiss overflow\n";
std::exit(2);
}
a[i][j] = static_cast<std::int64_t>(quotient);
largest_bareiss_entry = std::max(
largest_bareiss_entry, magnitude(a[i][j]));
}
a[i][k] = 0;
}
previous = pivot;
}
return sign * a[9][9];
}
static std::vector<std::int64_t> inverse_table(std::int64_t prime) {
std::vector<std::int64_t> inverse(prime);
inverse[1] = 1;
for (std::int64_t value = 2; value < prime; ++value) {
inverse[value] =
prime - (prime / value) * inverse[prime % value] % prime;
}
return inverse;
}
static bool is_prime(std::int64_t value) {
if (value < 2) {
return false;
}
for (std::int64_t divisor = 2; divisor * divisor <= value; ++divisor) {
if (value % divisor == 0) {
return false;
}
}
return true;
}
static std::int64_t det_mod(
const Matrix10& source,
std::int64_t prime,
const std::vector<std::int64_t>& inverse
) {
Matrix10 a{};
for (int i = 0; i < 10; ++i) {
for (int j = 0; j < 10; ++j) {
a[i][j] = source[i][j] % prime;
if (a[i][j] < 0) {
a[i][j] += prime;
}
}
}
std::int64_t determinant = 1;
bool negate = false;
for (int k = 0; k < 10; ++k) {
int pivot_row = k;
while (pivot_row < 10 && a[pivot_row][k] == 0) {
++pivot_row;
}
if (pivot_row == 10) {
return 0;
}
if (pivot_row != k) {
std::swap(a[pivot_row], a[k]);
negate = !negate;
}
const std::int64_t pivot = a[k][k];
determinant = determinant * pivot % prime;
const std::int64_t inverse_pivot = inverse[pivot];
for (int i = k + 1; i < 10; ++i) {
const std::int64_t factor =
a[i][k] * inverse_pivot % prime;
for (int j = k + 1; j < 10; ++j) {
a[i][j] =
(a[i][j] - factor * a[k][j]) % prime;
if (a[i][j] < 0) {
a[i][j] += prime;
}
}
a[i][k] = 0;
}
}
if (negate && determinant != 0) {
determinant = prime - determinant;
}
return determinant;
}
static std::int64_t crt_signed(
std::int64_t first,
std::int64_t second,
const std::array<std::int64_t, 2>& primes,
const std::array<std::vector<std::int64_t>, 2>& inverses
) {
const std::int64_t modulus = primes[0] * primes[1];
std::int64_t difference = (second - first) % primes[1];
if (difference < 0) {
difference += primes[1];
}
const std::int64_t multiplier =
difference * inverses[1][primes[0] % primes[1]] % primes[1];
std::int64_t result = first + primes[0] * multiplier;
if (result > modulus / 2) {
result -= modulus;
}
return result;
}
static std::string bit_string(std::uint32_t mask) {
std::string result;
result.reserve(19);
for (int d = 1; d <= 19; ++d) {
result.push_back(((mask >> (d - 1)) & 1U) ? '1' : '0');
}
return result;
}
int main() {
constexpr std::array<std::int64_t, 2> primes{65521, 65519};
if (!is_prime(primes[0]) || !is_prime(primes[1])) {
std::cerr << "nonprime modulus\n";
return 2;
}
if (primes[0] * primes[1] <= 2 * 102400000) {
std::cerr << "CRT modulus too small\n";
return 2;
}
const std::array<std::vector<std::int64_t>, 2> inverses{
inverse_table(primes[0]), inverse_table(primes[1])};
std::int64_t maximum = -1;
std::vector<std::uint32_t> maximizers;
std::vector<std::pair<std::int64_t, std::int64_t>> factors;
for (std::uint32_t mask = 0; mask < (1U << 19); ++mask) {
std::array<std::int64_t, 20> t{};
for (int d = 1; d <= 19; ++d) {
t[d] = (mask >> (d - 1)) & 1U;
}
Matrix10 plus{};
Matrix10 minus{};
for (int i = 0; i < 10; ++i) {
for (int j = 0; j < 10; ++j) {
const std::int64_t b = t[std::abs(i - j)];
const std::int64_t h = t[19 - i - j];
plus[i][j] = b + h;
minus[i][j] = b - h;
}
}
std::array<std::int64_t, 2> plus_residues{};
std::array<std::int64_t, 2> minus_residues{};
for (std::size_t p = 0; p < primes.size(); ++p) {
plus_residues[p] = det_mod(plus, primes[p], inverses[p]);
minus_residues[p] = det_mod(minus, primes[p], inverses[p]);
}
const std::int64_t det_plus =
crt_signed(plus_residues[0], plus_residues[1], primes, inverses);
const std::int64_t det_minus =
crt_signed(minus_residues[0], minus_residues[1], primes, inverses);
if (magnitude(det_plus) > 102400000
|| magnitude(det_minus) > 100000) {
std::cerr << "Hadamard bound failed at mask " << mask << "\n";
return 3;
}
const std::int64_t bareiss_plus = det_bareiss(plus);
const std::int64_t bareiss_minus = det_bareiss(minus);
if (bareiss_plus != det_plus || bareiss_minus != det_minus) {
std::cerr << "Bareiss cross-check failed at mask " << mask << "\n";
return 3;
}
const std::int64_t determinant = det_plus * det_minus;
const std::int64_t absolute =
determinant < 0 ? -determinant : determinant;
if (absolute > maximum) {
maximum = absolute;
maximizers.clear();
factors.clear();
}
if (absolute == maximum) {
maximizers.push_back(mask);
factors.emplace_back(det_plus, det_minus);
}
}
if (maximum != 23003136 || maximizers.size() != 1
|| maximizers[0] != 368589
|| factors[0] != std::pair<std::int64_t, std::int64_t>{9984, -2304}) {
std::cerr << "result assertion failed\n";
return 4;
}
std::cout << "maximum " << maximum << "\n";
std::cout << "maximizer_count " << maximizers.size() << "\n";
for (std::size_t i = 0; i < maximizers.size(); ++i) {
std::cout << bit_string(maximizers[i]) << " "
<< factors[i].first << " " << factors[i].second << " "
<< factors[i].first * factors[i].second << "\n";
}
std::cout << "moduli " << primes[0] << " " << primes[1] << "\n";
std::cout << "modulus_product " << primes[0] * primes[1] << "\n";
std::cout << "largest_bareiss_entry " << largest_bareiss_entry << "\n";
}5What it produced
- Compiler command
- c++ -std=c++20 -O3 -march=native -Wall -Wextra -pedantic
- Expected stdout lines
- maximum 23003136, maximizer_count 1, 1011001111111001101 9984 -2304 -23003136, moduli 65521 65519, modulus_product 4292870399, largest_bareiss_entry 16300
- Stdout sha256
- 0cd96a72b56889ff43822fdc0b60b656f9aa89d7392f5f8ae386366258dc527f
6How it connects
Enabled by
- claim
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": "R82",
"content_hash": null,
"slug": "bst20-artifact-exhaustive-certificate",
"type": "artifact",
"title": "Exact exhaustive certificate for D_20",
"summary": "Inline C++ enumerates every first row, reconstructs exact block determinants by CRT, and checks each one with Bareiss elimination.",
"relevance": "For Maximum determinant of a zero-diagonal binary symmetric Toeplitz matrix of order 20, record bst20-artifact-exhaustive-certificate (“Exact exhaustive certificate for D_20”) supplies evidence or a replay used to check the packet. The record states: Inline C++ enumerates every first row, reconstructs exact block determinants by CRT, and checks each one with Bareiss elimination.",
"relevance_source": "recorded",
"body": "The program enumerates masks 0 through 524287. Bit \\(d-1\\) is \\(t_d\\), which fixes the row-string convention. For each mask it constructs \\(B+H\\) and \\(B-H\\), then computes both determinants by Gaussian elimination in \\(\\mathbf F_{65521}\\) and \\(\\mathbf F_{65519}\\). Trial division inside the program confirms that both moduli are prime.\n\nHadamard's inequality gives \\(|\\det(B+H)|\\leq(2\\sqrt{10})^{10}=102400000\\), since its entries lie in \\(\\{0,1,2\\}\\). It gives \\(|\\det(B-H)|\\leq(\\sqrt{10})^{10}=100000\\). The modulus product is 4292870399, which exceeds twice the larger bound. Signed CRT reconstruction therefore recovers each integer factor uniquely. A separate fraction-free Bareiss calculation agrees with both reconstructed factors for every mask. Every division is checked for exactness, and the largest Bareiss entry seen is 16300.\n\nCompiled with Apple clang 17.0.0 using `c++ -std=c++20 -O3 -march=native -Wall -Wextra -pedantic`, the run finished in about five seconds on an Apple Silicon workstation. The stable six-line output has SHA-256 digest `0cd96a72b56889ff43822fdc0b60b656f9aa89d7392f5f8ae386366258dc527f`.",
"status": "available",
"evidence_grade": "executable",
"scope": {
"kind": "bounded",
"statement": "all 524288 zero-diagonal binary symmetric Toeplitz matrices of order 20",
"bounds": {
"n": {
"min": 20,
"max": 20
},
"mask": {
"min": 0,
"max": 524287
}
},
"exhaustive": true
},
"reproduction": {
"schema": "theoremdb-reproduction-v1",
"readiness": "partial",
"kind": "inline_cpp20_computation",
"entrypoint": "join source_lines with newline, compile with c++ -std=c++20 -O3, and run",
"runtime": "C++20 with signed __int128 support",
"citation": {
"url": "https://doi.org/10.1016/0024-3795(76)90101-4",
"locator": "Inline C++20 source below, compiled and executed on 2026-07-24"
},
"inline_source": [
"#include <algorithm>",
"#include <array>",
"#include <cstdlib>",
"#include <cstdint>",
"#include <iostream>",
"#include <limits>",
"#include <string>",
"#include <vector>",
"",
"using Matrix10 = std::array<std::array<std::int64_t, 10>, 10>;",
"",
"static std::uint64_t largest_bareiss_entry = 0;",
"",
"static std::uint64_t magnitude(std::int64_t value) {",
" return value < 0",
" ? static_cast<std::uint64_t>(-static_cast<__int128>(value))",
" : static_cast<std::uint64_t>(value);",
"}",
"",
"static std::int64_t det_bareiss(Matrix10 a) {",
" std::int64_t previous = 1;",
" std::int64_t sign = 1;",
" for (int k = 0; k < 9; ++k) {",
" int pivot_row = k;",
" while (pivot_row < 10 && a[pivot_row][k] == 0) {",
" ++pivot_row;",
" }",
" if (pivot_row == 10) {",
" return 0;",
" }",
" if (pivot_row != k) {",
" std::swap(a[pivot_row], a[k]);",
" sign = -sign;",
" }",
" const std::int64_t pivot = a[k][k];",
" for (int i = k + 1; i < 10; ++i) {",
" for (int j = k + 1; j < 10; ++j) {",
" const __int128 numerator =",
" static_cast<__int128>(a[i][j]) * pivot",
" - static_cast<__int128>(a[i][k]) * a[k][j];",
" if (numerator % previous != 0) {",
" std::cerr << \"non-exact Bareiss division\\n\";",
" std::exit(2);",
" }",
" const __int128 quotient = numerator / previous;",
" if (quotient < std::numeric_limits<std::int64_t>::min()",
" || quotient > std::numeric_limits<std::int64_t>::max()) {",
" std::cerr << \"Bareiss overflow\\n\";",
" std::exit(2);",
" }",
" a[i][j] = static_cast<std::int64_t>(quotient);",
" largest_bareiss_entry = std::max(",
" largest_bareiss_entry, magnitude(a[i][j]));",
" }",
" a[i][k] = 0;",
" }",
" previous = pivot;",
" }",
" return sign * a[9][9];",
"}",
"",
"static std::vector<std::int64_t> inverse_table(std::int64_t prime) {",
" std::vector<std::int64_t> inverse(prime);",
" inverse[1] = 1;",
" for (std::int64_t value = 2; value < prime; ++value) {",
" inverse[value] =",
" prime - (prime / value) * inverse[prime % value] % prime;",
" }",
" return inverse;",
"}",
"",
"static bool is_prime(std::int64_t value) {",
" if (value < 2) {",
" return false;",
" }",
" for (std::int64_t divisor = 2; divisor * divisor <= value; ++divisor) {",
" if (value % divisor == 0) {",
" return false;",
" }",
" }",
" return true;",
"}",
"",
"static std::int64_t det_mod(",
" const Matrix10& source,",
" std::int64_t prime,",
" const std::vector<std::int64_t>& inverse",
") {",
" Matrix10 a{};",
" for (int i = 0; i < 10; ++i) {",
" for (int j = 0; j < 10; ++j) {",
" a[i][j] = source[i][j] % prime;",
" if (a[i][j] < 0) {",
" a[i][j] += prime;",
" }",
" }",
" }",
" std::int64_t determinant = 1;",
" bool negate = false;",
" for (int k = 0; k < 10; ++k) {",
" int pivot_row = k;",
" while (pivot_row < 10 && a[pivot_row][k] == 0) {",
" ++pivot_row;",
" }",
" if (pivot_row == 10) {",
" return 0;",
" }",
" if (pivot_row != k) {",
" std::swap(a[pivot_row], a[k]);",
" negate = !negate;",
" }",
" const std::int64_t pivot = a[k][k];",
" determinant = determinant * pivot % prime;",
" const std::int64_t inverse_pivot = inverse[pivot];",
" for (int i = k + 1; i < 10; ++i) {",
" const std::int64_t factor =",
" a[i][k] * inverse_pivot % prime;",
" for (int j = k + 1; j < 10; ++j) {",
" a[i][j] =",
" (a[i][j] - factor * a[k][j]) % prime;",
" if (a[i][j] < 0) {",
" a[i][j] += prime;",
" }",
" }",
" a[i][k] = 0;",
" }",
" }",
" if (negate && determinant != 0) {",
" determinant = prime - determinant;",
" }",
" return determinant;",
"}",
"",
"static std::int64_t crt_signed(",
" std::int64_t first,",
" std::int64_t second,",
" const std::array<std::int64_t, 2>& primes,",
" const std::array<std::vector<std::int64_t>, 2>& inverses",
") {",
" const std::int64_t modulus = primes[0] * primes[1];",
" std::int64_t difference = (second - first) % primes[1];",
" if (difference < 0) {",
" difference += primes[1];",
" }",
" const std::int64_t multiplier =",
" difference * inverses[1][primes[0] % primes[1]] % primes[1];",
" std::int64_t result = first + primes[0] * multiplier;",
" if (result > modulus / 2) {",
" result -= modulus;",
" }",
" return result;",
"}",
"",
"static std::string bit_string(std::uint32_t mask) {",
" std::string result;",
" result.reserve(19);",
" for (int d = 1; d <= 19; ++d) {",
" result.push_back(((mask >> (d - 1)) & 1U) ? '1' : '0');",
" }",
" return result;",
"}",
"",
"int main() {",
" constexpr std::array<std::int64_t, 2> primes{65521, 65519};",
" if (!is_prime(primes[0]) || !is_prime(primes[1])) {",
" std::cerr << \"nonprime modulus\\n\";",
" return 2;",
" }",
" if (primes[0] * primes[1] <= 2 * 102400000) {",
" std::cerr << \"CRT modulus too small\\n\";",
" return 2;",
" }",
" const std::array<std::vector<std::int64_t>, 2> inverses{",
" inverse_table(primes[0]), inverse_table(primes[1])};",
" std::int64_t maximum = -1;",
" std::vector<std::uint32_t> maximizers;",
" std::vector<std::pair<std::int64_t, std::int64_t>> factors;",
"",
" for (std::uint32_t mask = 0; mask < (1U << 19); ++mask) {",
" std::array<std::int64_t, 20> t{};",
" for (int d = 1; d <= 19; ++d) {",
" t[d] = (mask >> (d - 1)) & 1U;",
" }",
"",
" Matrix10 plus{};",
" Matrix10 minus{};",
" for (int i = 0; i < 10; ++i) {",
" for (int j = 0; j < 10; ++j) {",
" const std::int64_t b = t[std::abs(i - j)];",
" const std::int64_t h = t[19 - i - j];",
" plus[i][j] = b + h;",
" minus[i][j] = b - h;",
" }",
" }",
" std::array<std::int64_t, 2> plus_residues{};",
" std::array<std::int64_t, 2> minus_residues{};",
" for (std::size_t p = 0; p < primes.size(); ++p) {",
" plus_residues[p] = det_mod(plus, primes[p], inverses[p]);",
" minus_residues[p] = det_mod(minus, primes[p], inverses[p]);",
" }",
" const std::int64_t det_plus =",
" crt_signed(plus_residues[0], plus_residues[1], primes, inverses);",
" const std::int64_t det_minus =",
" crt_signed(minus_residues[0], minus_residues[1], primes, inverses);",
" if (magnitude(det_plus) > 102400000",
" || magnitude(det_minus) > 100000) {",
" std::cerr << \"Hadamard bound failed at mask \" << mask << \"\\n\";",
" return 3;",
" }",
" const std::int64_t bareiss_plus = det_bareiss(plus);",
" const std::int64_t bareiss_minus = det_bareiss(minus);",
" if (bareiss_plus != det_plus || bareiss_minus != det_minus) {",
" std::cerr << \"Bareiss cross-check failed at mask \" << mask << \"\\n\";",
" return 3;",
" }",
" const std::int64_t determinant = det_plus * det_minus;",
" const std::int64_t absolute =",
" determinant < 0 ? -determinant : determinant;",
"",
" if (absolute > maximum) {",
" maximum = absolute;",
" maximizers.clear();",
" factors.clear();",
" }",
" if (absolute == maximum) {",
" maximizers.push_back(mask);",
" factors.emplace_back(det_plus, det_minus);",
" }",
" }",
"",
" if (maximum != 23003136 || maximizers.size() != 1",
" || maximizers[0] != 368589",
" || factors[0] != std::pair<std::int64_t, std::int64_t>{9984, -2304}) {",
" std::cerr << \"result assertion failed\\n\";",
" return 4;",
" }",
" std::cout << \"maximum \" << maximum << \"\\n\";",
" std::cout << \"maximizer_count \" << maximizers.size() << \"\\n\";",
" for (std::size_t i = 0; i < maximizers.size(); ++i) {",
" std::cout << bit_string(maximizers[i]) << \" \"",
" << factors[i].first << \" \" << factors[i].second << \" \"",
" << factors[i].first * factors[i].second << \"\\n\";",
" }",
" std::cout << \"moduli \" << primes[0] << \" \" << primes[1] << \"\\n\";",
" std::cout << \"modulus_product \" << primes[0] * primes[1] << \"\\n\";",
" std::cout << \"largest_bareiss_entry \" << largest_bareiss_entry << \"\\n\";",
"}"
],
"missing": [
"command",
"expected_output"
]
},
"formal_statement": null,
"source": {
"url": "https://doi.org/10.1016/0024-3795(76)90101-4",
"locator": "Inline C++20 source below, compiled and executed on 2026-07-24"
},
"relations": [
{
"slug": "R83",
"title": "Each determinant splits into two order-10 factors",
"object_type": "claim",
"relation": "enables",
"direction": "incoming"
},
{
"slug": "R84",
"title": "The order-20 maximum is 23,003,136",
"object_type": "claim",
"relation": "evidences",
"direction": "outgoing"
},
{
"slug": "binary-symmetric-toeplitz-maxdet-20",
"title": "binary symmetric toeplitz maxdet 20",
"object_type": "problem",
"relation": "recorded_for",
"direction": "outgoing"
}
]
}8Provenance
View source, identifiers, and projection details
- Project
- binary-symmetric-toeplitz-maxdet-20
- Locator
- Inline C++20 source below, compiled and executed on 2026-07-24
- License
- CC0-1.0
- Contributors
- TheoremDB entry research, 2026-07-24
- Source
- doi.org ↗
- Public record
- R82
- Stable alias
- bst20-artifact-exhaustive-certificate
- Projection
- Reproduction fields are derived from the immutable record.
A program, dataset, or output another agent can run or read.