TheoremDB

Problem packetResearch packetR82

R82Executable evidence

Exact exhaustive certificate for D_20

View replayOpen source ↗
Link to a section

Authored summary

Inline C++ enumerates every first row, reconstructs exact block determinants by CRT, and checks each one with Bareiss elimination.

Executable material is recorded. Successful replay is a separate check.

Recorded status: available

Recorded scope: all 524288 zero-diagonal binary symmetric Toeplitz matrices of order 20

Complete recorded scope and conditions
{
  "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
}

Originating problem: Maximum determinant of a zero-diagonal binary symmetric Toeplitz matrix of order 20

Read the full authored explanationInspect the parent problem’s formal coverageFull source

Recorded relationships: The order-20 maximum is 23,003,136

Authored record and scope
Authored title
Exact exhaustive certificate for D_20
Record type
artifact
Stored status
available
Evidence grade
executable
Recorded scope data
{ "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 }
Linked research record IDs
R84

2Authored explanation

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.

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`.

Files and source

Files embedded in this record. Matching a file hash confirms its identity.

  • R82.txt8,276 bytes · No SHA-256 recorded
    Preview R82.txt
    #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";
}
    File identity
    Recorded filename
    R82.txt
    Download SHA-256
    7e7dd207a0794217ab7ff9fcef6e86bda87f2dcf2af430d9dd9f36239c61843c
Continue this work
Replay material: partial

4Reproduce

Replay package: 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.

Recorded artifact fields
Kind
inline_cpp20_computation
Entry point
join source_lines with newline, compile with c++ -std=c++20 -O3, and run
Environment
C++20 with signed __int128 support

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

Evidence for

Recorded for

Machine-readable record

Copy the structured record when continuing this work with an agent.

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"
  },
  "models": [],
  "continuation": null,
  "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.

Sign in to follow

Sign in in another tab, then return here.

Open sign-in in another tab

Report a problem

Report location:

Your ChatGPT account

Opening ChatGPT

ChatGPT is opening in a new tab.