{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R708",
  "content_hash": null,
  "slug": "sdb127-artifact-exact-certificate",
  "type": "artifact",
  "title": "Exact construction check and exhaustive size-17 exclusion",
  "summary": "A standard C++17 program checks the construction and exhausts 42,244,920 normalized search nodes.",
  "relevance": "This supplies a computation, dataset, or executable check used to assess the target problem.",
  "relevance_source": "derived",
  "body": "The search represents each inverse pair \\(\\{x,-x\\}\\) by the integer \\(\\min(x,127-x)\\) in \\(\\{1,\\ldots,63\\}\\). For a chosen representative \\(v\\), it inserts the classes of \\(v\\) and \\(2v\\). For each earlier representative \\(u\\), it also inserts the classes of \\(v+u\\) and \\(v-u\\). Thus a partial choice of \\(t\\) representatives has generated \\(t^2+t\\) formal sum types.\n\nAt size eight there are 72 formal types and all 63 classes must be distinct except for at most nine repetitions. The number of repetitions can only increase as representatives are added, so a partial branch with more than nine repetitions is impossible and may be pruned. The program enumerates every increasing eight-subset containing 1 that survives this exact prune. This normalization is complete: given any candidate and any selected nonzero representative \\(s\\), multiplication by \\(s^{-1}\\) sends its inverse pair to \\(\\{1,-1\\}\\) and preserves all hypotheses.\n\nThe run visited 42,244,920 nodes and finished all 56 second-representative branches without finding a size-17 basis. It separately checked that the displayed size-19 set has 19 distinct elements and covers all 127 residues.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "the displayed 19-element construction and every normalized symmetric 17-element subset of Z/127Z containing zero",
    "bounds": {
      "modulus": {
        "min": 127,
        "max": 127
      },
      "excluded_cardinality": {
        "min": 17,
        "max": 17
      },
      "construction_cardinality": {
        "min": 19,
        "max": 19
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "partial",
    "kind": "inline_cpp_computation",
    "entrypoint": "join source_lines with newline, compile with c++ -O3 -std=c++17 -pthread, and run",
    "runtime": "C++17 compiler with the standard thread library",
    "citation": {
      "url": "https://doi.org/10.1142/S0219498819500816",
      "locator": "Exact standard C++17 computation executed by TheoremDB entry research on 2026-07-25"
    },
    "outputs": "construction_size=19 covered_residues=127\nnormalized_size17_nodes=42244920 workers_finished=56\nsize17=unsat\nminimum=19\n",
    "inline_source": [
      "#include <algorithm>",
      "#include <array>",
      "#include <atomic>",
      "#include <cstdint>",
      "#include <iostream>",
      "#include <thread>",
      "#include <vector>",
      "",
      "static constexpr int P = 127;",
      "static std::atomic<bool> found(false);",
      "static std::atomic<unsigned long long> nodes(0);",
      "static std::atomic<int> finished(0);",
      "static int answer[8];",
      "",
      "static inline int canon(int x) {",
      "    x %= P;",
      "    if (x < 0) x += P;",
      "    return std::min(x, P - x);",
      "}",
      "",
      "static inline uint64_t add_labels(uint64_t mask, const int *chosen, int size, int value) {",
      "    mask |= uint64_t(1) << (canon(value) - 1);",
      "    mask |= uint64_t(1) << (canon(2 * value) - 1);",
      "    for (int i = 0; i < size; ++i) {",
      "        mask |= uint64_t(1) << (canon(value + chosen[i]) - 1);",
      "        mask |= uint64_t(1) << (canon(value - chosen[i]) - 1);",
      "    }",
      "    return mask;",
      "}",
      "",
      "static void dfs(int *chosen, int size, int next, uint64_t mask) {",
      "    if (found.load(std::memory_order_relaxed)) return;",
      "    nodes.fetch_add(1, std::memory_order_relaxed);",
      "    int represented = __builtin_popcountll(mask);",
      "    int generated = size * size + size;",
      "    if (generated - represented > 9) return;",
      "    if (size == 8) {",
      "        if (represented == 63 && !found.exchange(true)) {",
      "            for (int i = 0; i < 8; ++i) answer[i] = chosen[i];",
      "        }",
      "        return;",
      "    }",
      "    int remaining = 8 - size;",
      "    for (int value = next; value <= 64 - remaining; ++value) {",
      "        chosen[size] = value;",
      "        dfs(chosen, size + 1, value + 1, add_labels(mask, chosen, size, value));",
      "    }",
      "}",
      "",
      "static void worker(int second) {",
      "    int chosen[8] = {1, second};",
      "    uint64_t mask = 0;",
      "    mask = add_labels(mask, chosen, 0, 1);",
      "    mask = add_labels(mask, chosen, 1, second);",
      "    dfs(chosen, 2, second + 1, mask);",
      "    finished.fetch_add(1);",
      "}",
      "",
      "int main() {",
      "    const std::array<int, 9> construction = {2, 7, 30, 37, 38, 43, 48, 60, 63};",
      "    std::array<bool, P> in_a{};",
      "    in_a[0] = true;",
      "    for (int value : construction) {",
      "        in_a[value] = true;",
      "        in_a[P - value] = true;",
      "    }",
      "    int size = 0;",
      "    std::array<bool, P> covered{};",
      "    for (int a = 0; a < P; ++a) {",
      "        if (!in_a[a]) continue;",
      "        ++size;",
      "        for (int b = 0; b < P; ++b) {",
      "            if (in_a[b]) covered[(a + b) % P] = true;",
      "        }",
      "    }",
      "    int covered_count = std::count(covered.begin(), covered.end(), true);",
      "    if (size != 19 || covered_count != P) return 2;",
      "    std::cout << \"construction_size=\" << size",
      "              << \" covered_residues=\" << covered_count << \"\\n\";",
      "    std::vector<std::thread> pool;",
      "    for (int second = 2; second <= 57; ++second) pool.emplace_back(worker, second);",
      "    for (auto &thread : pool) thread.join();",
      "    std::cout << \"normalized_size17_nodes=\" << nodes.load()",
      "              << \" workers_finished=\" << finished.load() << \"\\n\";",
      "    if (found.load()) {",
      "        std::cout << \"size17=sat\";",
      "        for (int value : answer) std::cout << \" \" << value;",
      "        std::cout << \"\\n\";",
      "        return 1;",
      "    }",
      "    std::cout << \"size17=unsat\\nminimum=19\\n\";",
      "    return 0;",
      "}"
    ],
    "missing": [
      "command"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.1142/S0219498819500816",
    "locator": "Exact standard C++17 computation executed by TheoremDB entry research on 2026-07-25"
  },
  "models": [],
  "continuation": null,
  "relations": [
    {
      "slug": "R711",
      "title": "The exact minimum is 19",
      "object_type": "claim",
      "relation": "verifies",
      "direction": "outgoing"
    },
    {
      "slug": "R710",
      "title": "Unsigned sum types force at least 17 elements",
      "object_type": "claim",
      "relation": "tests",
      "direction": "outgoing"
    },
    {
      "slug": "symmetric-difference-basis-z127",
      "title": "symmetric difference basis z127",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}