{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R5",
  "content_hash": null,
  "slug": "ac0123-artifact-updown-constructor",
  "type": "artifact",
  "title": "Deterministic Up-and-Down finite-word constructor",
  "summary": "A self-contained C++17 program implements exact suffix checks, alternating letter priorities, fixed retreats, and a full internal scan.",
  "relevance": "For Additive-cube avoidance on the alphabet zero through three, record ac0123-artifact-updown-constructor (“Deterministic Up-and-Down finite-word constructor”) supplies evidence or a replay used to check the packet. The record states: A self-contained C++17 program implements exact suffix checks, alternating letter priorities, fixed retreats, and a full internal scan.",
  "relevance_source": "recorded",
  "body": "The constructor stores exact unsigned 64-bit prefix sums. A candidate letter is accepted precisely when no additive cube ends at the new final position. In Up-and-Down mode it starts with priority \\(0,1,2,3\\), switches to \\(3,2,1,0\\) after 1,209 rejected candidates or at each 10,000-letter checkpoint, retreats 100 letters, and repeats. The thesis's displayed main directly switches direction and retreats at the checkpoints. It fixes the failure threshold at 1,209 and uses a retreat of 100 in the threshold-tuning code, while also saying that the retreat changed during the long construction. The program therefore records the exact 100-letter retreat as a source-informed choice specific to this reconstruction.\n\nAfter construction, the program scans every end position and every admissible block length again before printing the word. The execution is deterministic and uses no randomness, floating point, network, or external service. Its implementation was written independently from the unavailable thesis source and should be treated as a source-informed reconstruction.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "the deterministic Up-and-Down execution recorded here on the integer alphabet {0,1,2,3}",
    "bounds": {
      "word_length": {
        "min": 1000000,
        "max": 1000000
      },
      "alphabet_size": {
        "min": 4,
        "max": 4
      }
    },
    "exhaustive": false
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "complete",
    "kind": "inline_cpp17_deterministic_constructor_and_internal_verifier",
    "command": "clang++ -O3 -std=c++17 -Wall -Wextra -pedantic additive_cube_replay.cpp -o additive_cube_replay && /usr/bin/time -lp ./additive_cube_replay updown 1000000 1209 100 10000 10000000000 > acube_updown_1000000.txt",
    "entrypoint": "Join source_lines with LF characters and append one terminal LF as additive_cube_replay.cpp; source_sha256 includes that terminal LF",
    "runtime": "Apple clang version 21.0.0, target arm64-apple-darwin25.2.0, ISO C++17, standard library only",
    "citation": {
      "locator": "Inline C++17 source prepared and executed on 2026-07-28; method parameters traced to Lietard thesis Sections 6.2.4 and 6.4.1"
    },
    "dependencies": [
      {
        "name": "Apple clang",
        "version": "21.0.0",
        "license": "Apache-2.0 WITH LLVM-exception"
      },
      {
        "name": "Apple libc++",
        "version": "system toolchain for arm64-apple-darwin25.2.0",
        "license": "Apache-2.0 WITH LLVM-exception"
      }
    ],
    "outputs": {
      "source_sha256": "853fc455b9c4932707d8baf68da1014a7a938fa3310a6ae4f56b2e6cb42cd1e2",
      "word_file_sha256_including_final_lf": "15d439b42fefa8501203775cf0b4457f7eaf19bae14ae5797b5d405e03ed1846",
      "word_length": 1000000,
      "valid": true,
      "checked_pairs_internal": 166666500000,
      "tested_letters": 2480028,
      "rejected_letters": 1271032,
      "backtracks": 208996,
      "direction_changes": 1097,
      "constructor_seconds_before_full_scan": 96.2857,
      "maximum_resident_bytes": 18382848
    },
    "runtime_seconds": 180.38,
    "inline_source": [
      "#include <algorithm>",
      "#include <chrono>",
      "#include <cstdint>",
      "#include <cstdlib>",
      "#include <iostream>",
      "#include <string>",
      "#include <vector>",
      "",
      "using u64 = std::uint64_t;",
      "",
      "struct Search {",
      "    std::vector<u64> sums;",
      "    u64 length = 0;",
      "    u64 tested_letters = 0;",
      "    u64 rejected_letters = 0;",
      "    u64 backtracks = 0;",
      "    u64 direction_changes = 0;",
      "",
      "    explicit Search(u64 target) : sums(target + 1, 0) {}",
      "",
      "    bool safe_end(u64 n) const {",
      "        for (u64 k = 1; 3 * k <= n; ++k) {",
      "            const u64 a = sums[n] - sums[n - k];",
      "            const u64 b = sums[n - k] - sums[n - 2 * k];",
      "            if (a != b) continue;",
      "            const u64 c = sums[n - 2 * k] - sums[n - 3 * k];",
      "            if (b == c) return false;",
      "        }",
      "        return true;",
      "    }",
      "",
      "    bool extend_ascending(u64 &failed, u64 max_tested) {",
      "        int start = 0;",
      "        while (true) {",
      "            for (int c = start; c <= 3; ++c) {",
      "                if (tested_letters >= max_tested) return false;",
      "                sums[length + 1] = sums[length] + static_cast<u64>(c);",
      "                ++tested_letters;",
      "                if (safe_end(length + 1)) {",
      "                    ++length;",
      "                    return true;",
      "                }",
      "                ++failed;",
      "                ++rejected_letters;",
      "            }",
      "            if (length == 0) return false;",
      "            const int old = static_cast<int>(sums[length] - sums[length - 1]);",
      "            --length;",
      "            ++backtracks;",
      "            start = old + 1;",
      "        }",
      "    }",
      "",
      "    bool extend_descending(u64 &failed, u64 max_tested) {",
      "        int start = 3;",
      "        while (true) {",
      "            for (int c = start; c >= 0; --c) {",
      "                if (tested_letters >= max_tested) return false;",
      "                sums[length + 1] = sums[length] + static_cast<u64>(c);",
      "                ++tested_letters;",
      "                if (safe_end(length + 1)) {",
      "                    ++length;",
      "                    return true;",
      "                }",
      "                ++failed;",
      "                ++rejected_letters;",
      "            }",
      "            if (length == 0) return false;",
      "            const int old = static_cast<int>(sums[length] - sums[length - 1]);",
      "            --length;",
      "            ++backtracks;",
      "            start = old - 1;",
      "        }",
      "    }",
      "",
      "    std::string word() const {",
      "        std::string out;",
      "        out.reserve(length);",
      "        for (u64 i = 1; i <= length; ++i)",
      "            out.push_back(static_cast<char>('0' + sums[i] - sums[i - 1]));",
      "        return out;",
      "    }",
      "};",
      "",
      "static bool verify(const std::string &word, u64 &checks, u64 &bad_end, u64 &bad_k) {",
      "    std::vector<u64> sums(word.size() + 1, 0);",
      "    for (u64 i = 0; i < word.size(); ++i) {",
      "        if (word[i] < '0' || word[i] > '3') return false;",
      "        sums[i + 1] = sums[i] + static_cast<u64>(word[i] - '0');",
      "    }",
      "    checks = 0;",
      "    for (u64 n = 1; n <= word.size(); ++n) {",
      "        for (u64 k = 1; 3 * k <= n; ++k) {",
      "            ++checks;",
      "            const u64 a = sums[n] - sums[n - k];",
      "            const u64 b = sums[n - k] - sums[n - 2 * k];",
      "            const u64 c = sums[n - 2 * k] - sums[n - 3 * k];",
      "            if (a == b && b == c) {",
      "                bad_end = n;",
      "                bad_k = k;",
      "                return false;",
      "            }",
      "        }",
      "    }",
      "    return true;",
      "}",
      "",
      "int main(int argc, char **argv) {",
      "    if (argc < 3) {",
      "        std::cerr << \"usage: additive_cube_replay MODE TARGET \"",
      "                     \"[FAIL_THRESHOLD BACKTRACK CHECKPOINT MAX_TESTED]\\n\";",
      "        return 2;",
      "    }",
      "    const std::string mode = argv[1];",
      "    const u64 target = std::strtoull(argv[2], nullptr, 10);",
      "    const u64 fail_threshold = argc > 3 ? std::strtoull(argv[3], nullptr, 10) : 1209;",
      "    const u64 backtrack_size = argc > 4 ? std::strtoull(argv[4], nullptr, 10) : 100;",
      "    const u64 checkpoint = argc > 5 ? std::strtoull(argv[5], nullptr, 10) : 10000;",
      "    const u64 max_tested = argc > 6 ? std::strtoull(argv[6], nullptr, 10) : UINT64_MAX;",
      "    Search search(target);",
      "    bool ascending = true;",
      "    u64 next_checkpoint = checkpoint;",
      "    const auto start = std::chrono::steady_clock::now();",
      "    while (search.length < target && search.tested_letters < max_tested) {",
      "        u64 failed = 0;",
      "        const u64 phase_stop = mode == \"updown\" ? std::min(target, next_checkpoint) : target;",
      "        while (search.length < phase_stop && failed < fail_threshold) {",
      "            const bool moved = ascending",
      "                ? search.extend_ascending(failed, max_tested)",
      "                : search.extend_descending(failed, max_tested);",
      "            if (!moved) break;",
      "        }",
      "        if (search.length >= target || search.tested_letters >= max_tested) break;",
      "        if (mode == \"direct\") break;",
      "        if (search.length >= next_checkpoint) next_checkpoint += checkpoint;",
      "        const u64 retreat = std::min(backtrack_size, search.length);",
      "        search.length -= retreat;",
      "        search.backtracks += retreat;",
      "        ascending = !ascending;",
      "        ++search.direction_changes;",
      "    }",
      "    const auto stop = std::chrono::steady_clock::now();",
      "    const double seconds =",
      "        std::chrono::duration<double>(stop - start).count();",
      "    const std::string word = search.word();",
      "    u64 checks = 0, bad_end = 0, bad_k = 0;",
      "    const bool valid = verify(word, checks, bad_end, bad_k);",
      "    std::cerr << \"mode=\" << mode",
      "              << \" target=\" << target",
      "              << \" reached=\" << search.length",
      "              << \" valid=\" << (valid ? \"true\" : \"false\")",
      "              << \" checked_pairs=\" << checks",
      "              << \" tested_letters=\" << search.tested_letters",
      "              << \" rejected_letters=\" << search.rejected_letters",
      "              << \" backtracks=\" << search.backtracks",
      "              << \" direction_changes=\" << search.direction_changes",
      "              << \" seconds=\" << seconds;",
      "    if (!valid) std::cerr << \" bad_end=\" << bad_end << \" bad_k=\" << bad_k;",
      "    std::cerr << '\\n';",
      "    std::cout << word << '\\n';",
      "    return valid ? 0 : 1;",
      "}"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": null,
    "locator": "Inline C++17 source prepared and executed on 2026-07-28; method parameters traced to Lietard thesis Sections 6.2.4 and 6.4.1"
  },
  "models": [],
  "continuation": null,
  "relations": [
    {
      "slug": "R9",
      "title": "The source-informed finite construction reaches one million",
      "object_type": "attempt",
      "relation": "uses",
      "direction": "incoming"
    },
    {
      "slug": "R10",
      "title": "The reconstructed method produces a checked million-letter word",
      "object_type": "claim",
      "relation": "evidences",
      "direction": "outgoing"
    },
    {
      "slug": "R8",
      "title": "Direct ascending search stalls near the thesis hard boundary",
      "object_type": "attempt",
      "relation": "uses",
      "direction": "incoming"
    },
    {
      "slug": "additive-cube-four-term-progression-alphabet",
      "title": "additive cube four term progression alphabet",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}