diff --git a/.github/workflows/c4-h7-d2-three-source-past.yml b/.github/workflows/c4-h7-d2-three-source-past.yml new file mode 100644 index 0000000..d4cf34e --- /dev/null +++ b/.github/workflows/c4-h7-d2-three-source-past.yml @@ -0,0 +1,242 @@ +name: Audit c4 h7 three-source zero-debt pasts +run-name: Exact c4 k2 h7 past restoration and independent initial-state audit + +on: + push: + branches: [codex/c4-h7-global-bypass] + workflow_dispatch: + +permissions: + contents: read + +concurrency: + group: c4-h7-d2-three-source-past-${{ github.ref }} + cancel-in-progress: true + +jobs: + formal-past-restoration: + runs-on: ubuntu-latest + timeout-minutes: 360 + steps: + - uses: actions/checkout@v5 + - uses: actions/setup-python@v5 + with: + python-version: "3.12" + + - name: Configure and build the two solvers plus certificate tools + run: | + cmake -S . -B build \ + -DCMAKE_BUILD_TYPE=Release \ + -DWSC_WARNINGS_AS_ERRORS=ON + cmake --build build \ + --target \ + water-c4-h7-d2-three-source \ + water-c4-h7-d2-three-source-past \ + water-oracle \ + water-verify \ + --parallel 2 + + - name: Rebuild the complete 1106490-future checkpoint + run: | + mkdir -p out/checkpoint + set -o pipefail + build/water-c4-h7-d2-three-source \ + --self-test --output-dir out/checkpoint 2>&1 \ + | tee out/checkpoint/production.log + python scripts/validate_c4_h7_d2_three_source_report.py \ + out/checkpoint/report.json --negative-tests + + - name: Independently reproduce every checkpoint row + run: | + set -o pipefail + python tests/check_c4_h7_d2_three_source.py \ + --report out/checkpoint/report.json \ + --json out/checkpoint/independent-audit.json \ + --local-no-ledger out/checkpoint/independent-local-no-ledger.jsonl 2>&1 \ + | tee out/checkpoint/independent.log + + - name: Prove the unified all-local-NO bypass symbolically and against the artifact + run: | + set -o pipefail + python tests/check_c4_h7_d2_three_source_all_local_no_bypass.py 2>&1 \ + | tee out/checkpoint/all-local-no-bypass-symbolic.log + python tests/check_c4_h7_d2_three_source_all_local_no_bypass.py \ + --report out/checkpoint/report.json \ + --ledger out/checkpoint/local-no-ledger.jsonl 2>&1 \ + | tee out/checkpoint/all-local-no-bypass-artifact.log + + - name: Verify the sparse early-low continuation kernels + run: | + set -o pipefail + python tests/check_c4_h7_sparse_all_q_continuation.py \ + --checkpoint-report out/checkpoint/report.json 2>&1 \ + | tee out/checkpoint/sparse-all-q-continuation.log + + - name: Run a bounded past-restoration row differential first + run: | + mkdir -p out/past-bounded + set -o pipefail + build/water-c4-h7-d2-three-source-past \ + --checkpoint-report out/checkpoint/report.json \ + --output-dir out/past-bounded \ + --limit-restorations 64 \ + --self-test 2>&1 \ + | tee out/past-bounded/production.log + python scripts/validate_c4_h7_d2_three_source_past_report.py \ + out/past-bounded/report.json --negative-tests + python tests/check_c4_h7_d2_three_source_past.py \ + --checkpoint-report out/checkpoint/report.json \ + --production-report out/past-bounded/report.json \ + --limit 64 \ + --json out/past-bounded/independent-audit.json + + - name: Solve the complete 285600 balanced restoration superset + run: | + mkdir -p out/past-full + set -o pipefail + build/water-c4-h7-d2-three-source-past \ + --checkpoint-report out/checkpoint/report.json \ + --output-dir out/past-full \ + --self-test 2>&1 \ + | tee out/past-full/production.log + python scripts/validate_c4_h7_d2_three_source_past_report.py \ + out/past-full/report.json --negative-tests + + - name: Independently rebuild and compare all restored initial layouts + run: | + set -o pipefail + python tests/check_c4_h7_d2_three_source_past.py \ + --checkpoint-report out/checkpoint/report.json \ + --production-report out/past-full/report.json \ + --full \ + --json out/past-full/independent-audit.json 2>&1 \ + | tee out/past-full/independent.log + + - name: Gate all-YES and candidate outcomes at their exact claim boundary + run: | + python - <<'PY' + import json + from pathlib import Path + + production = json.loads(Path("out/past-full/report.json").read_text()) + independent = json.loads(Path("out/past-full/independent-audit.json").read_text()) + if independent["run"]["row_by_row_agreement"] is not True: + raise SystemExit("the independent implementation did not compare every row") + if independent["run"]["production_rows_compared"] != 285_600: + raise SystemExit("the independent implementation did not cover the full superset") + if production["status"] != independent["status"]: + raise SystemExit("the two initial-state implementations disagree on status") + status = production["status"] + if status == "THREE_SOURCE_PAST_FAMILY_ELIMINATED": + if production["run"]["initial_no"] != 0: + raise SystemExit("all-YES status contains a NO") + if independent["claims"]["restoration_family_eliminated"] is not True: + raise SystemExit("independent implementation did not prove the finite-family result") + elif status == "INITIAL_NO_CANDIDATES_EXPORTED": + if production["run"]["initial_no"] == 0: + raise SystemExit("candidate status contains no candidate") + if independent["run"]["initial_no"] != production["run"]["initial_no"]: + raise SystemExit("the two implementations disagree on candidate count") + else: + raise SystemExit(f"formal past run ended in unsafe status {status!r}") + Path("out/past-full/pre-certificate-status.txt").write_text(status + "\n") + PY + + - name: Independently certify any complete-layout NO candidate + run: | + status="$(cat out/past-full/pre-certificate-status.txt)" + if test "$status" = INITIAL_NO_CANDIDATES_EXPORTED; then + set -o pipefail + build/water-oracle \ + --input out/past-full/initial-no-candidate.txt \ + --count 1 \ + --certificate out/past-full/global-no-candidate.wscert 2>&1 \ + | tee out/past-full/water-oracle.log + grep -Eq '^border_sequences=0([[:space:]]|$)' out/past-full/water-oracle.log + grep -Fxq UNSOLVABLE out/past-full/water-oracle.log + test -s out/past-full/global-no-candidate.wscert + build/water-verify \ + --input out/past-full/initial-no-candidate.txt \ + --certificate out/past-full/global-no-candidate.wscert 2>&1 \ + | tee out/past-full/water-verify.log + grep -Fxq 'VALID NO CERTIFICATE' out/past-full/water-verify.log + fi + + - name: Emit only the conclusion justified by both implementations + run: | + python - <<'PY' + import hashlib + import json + from pathlib import Path + + directory = Path("out/past-full") + production = json.loads((directory / "report.json").read_text()) + independent = json.loads((directory / "independent-audit.json").read_text()) + candidate = production["status"] == "INITIAL_NO_CANDIDATES_EXPORTED" + certificate = directory / "global-no-candidate.wscert" + if candidate and not certificate.is_file(): + raise SystemExit("a DP NO was not promoted because no verified certificate exists") + status = "GLOBAL_NO_CERTIFIED" if candidate else "THREE_SOURCE_PAST_FAMILY_ELIMINATED" + result = { + "schema_version": 1, + "experiment": "c4_h7_d2_three_source_past_formal_gate", + "status": status, + "evidence": { + "production_status": production["status"], + "independent_status": independent["status"], + "rows_compared": independent["run"]["production_rows_compared"], + "oracle_count_cap": 1 if candidate else None, + "water_verify_passed": candidate, + "certificate_sha256": hashlib.sha256(certificate.read_bytes()).hexdigest() if candidate else None, + }, + "scope": { + "balanced_restoration_superset": 285_600, + "parent_reachable_subset": 281_904, + "universal_c4_h7_solvability": False, + }, + "claims": { + "three_source_past_family_eliminated": not candidate, + "global_no_certified": candidate, + "universal_c4_h7_solvability": False, + }, + } + (directory / "formal-result.json").write_text(json.dumps(result, indent=2, sort_keys=True) + "\n") + (directory / "status.txt").write_text(status + "\n") + PY + + - name: Record the exact finite-family conclusion + if: success() + run: | + python - <<'PY' >> "$GITHUB_STEP_SUMMARY" + import json + from pathlib import Path + + result = json.loads(Path("out/past-full/formal-result.json").read_text()) + if result["status"] == "GLOBAL_NO_CERTIFIED": + print( + "> A complete balanced c4/h7 layout from this restoration family is NO: " + "the independent oracle found zero solutions and water-verify accepted its closure certificate." + ) + else: + print( + "> Both independent implementations found all 285,600 balanced restorations YES. " + "This eliminates exactly the restored three-source residual family; it is not a universal c4/h7 proof." + ) + PY + cat out/past-full/report.md >> "$GITHUB_STEP_SUMMARY" + + - name: Create and verify the evidence manifest + if: always() + run: | + find out -type f ! -name SHA256SUMS -print0 \ + | sort -z \ + | xargs -0 -r sha256sum > out/SHA256SUMS + sha256sum --check out/SHA256SUMS + + - uses: actions/upload-artifact@v6 + if: always() + with: + name: c4-h7-d2-three-source-past-${{ github.run_id }} + path: out/ + if-no-files-found: error + retention-days: 30 diff --git a/.github/workflows/c4-h7-d2-three-source.yml b/.github/workflows/c4-h7-d2-three-source.yml new file mode 100644 index 0000000..ac26a45 --- /dev/null +++ b/.github/workflows/c4-h7-d2-three-source.yml @@ -0,0 +1,188 @@ +name: Audit c4 h7 three-source D2 checkpoints +run-name: Exact c4 k2 h7 three-legal-source fixed-future checkpoint audit + +on: + push: + branches: [codex/c4-h7-global-bypass] + workflow_dispatch: + +permissions: + contents: read + +concurrency: + group: c4-h7-d2-three-source-${{ github.ref }} + cancel-in-progress: true + +jobs: + build-and-bounded-differential: + runs-on: ubuntu-latest + timeout-minutes: 30 + steps: + - uses: actions/checkout@v5 + - uses: actions/setup-python@v5 + with: + python-version: "3.12" + - name: Configure Release with warnings as errors + run: >- + cmake -S . -B build + -DCMAKE_BUILD_TYPE=Release + -DWSC_WARNINGS_AS_ERRORS=ON + - name: Build the focused executable + run: >- + cmake --build build + --target water-c4-h7-d2-three-source + --parallel 2 + - name: Run the focused C++ smoke test + run: >- + ctest --test-dir build --output-on-failure + --no-tests=error + -R '^water-c4-h7-d2-three-source-smoke$' + - name: Differentially rebuild and solve a bounded prefix + run: | + mkdir -p out/bounded + set -o pipefail + python tests/check_c4_h7_d2_three_source.py \ + --program build/water-c4-h7-d2-three-source \ + --limit 64 \ + --json out/bounded/independent-64.json 2>&1 \ + | tee out/bounded/independent-64.log + - name: Preserve and strictly validate the same bounded prefix + run: | + set -o pipefail + build/water-c4-h7-d2-three-source \ + --self-test --limit 64 --output-dir out/bounded/production 2>&1 \ + | tee out/bounded/production.log + python scripts/validate_c4_h7_d2_three_source_report.py \ + out/bounded/production/report.json --negative-tests + test "$(python -c 'import json; print(json.load(open("out/bounded/production/report.json"))["status"])')" = INCOMPLETE + - name: Configure Clang ASan and UBSan + run: >- + cmake -S . -B build-sanitize + -DCMAKE_BUILD_TYPE=Debug + -DCMAKE_CXX_COMPILER=clang++ + -DWSC_WARNINGS_AS_ERRORS=ON + -DCMAKE_CXX_FLAGS='-fsanitize=address,undefined -fno-omit-frame-pointer' + -DCMAKE_EXE_LINKER_FLAGS='-fsanitize=address,undefined' + - name: Run bounded sanitizer self-tests + env: + ASAN_OPTIONS: detect_leaks=1:halt_on_error=1 + UBSAN_OPTIONS: halt_on_error=1:print_stacktrace=1 + run: | + cmake --build build-sanitize \ + --target water-c4-h7-d2-three-source --parallel 2 + build-sanitize/water-c4-h7-d2-three-source \ + --self-test --limit 8 --output-dir out/bounded/sanitized + - name: Create and verify the bounded SHA-256 manifest + if: always() + run: | + mkdir -p out/bounded + find out/bounded -type f ! -name SHA256SUMS -print0 \ + | sort -z \ + | xargs -0 -r sha256sum > out/bounded/SHA256SUMS + sha256sum --check out/bounded/SHA256SUMS + - uses: actions/upload-artifact@v6 + if: always() + with: + name: c4-h7-d2-three-source-bounded-${{ github.run_id }} + path: out/bounded/ + if-no-files-found: error + retention-days: 30 + + full-fixed-future-checkpoint-audit: + runs-on: ubuntu-latest + timeout-minutes: 240 + steps: + - uses: actions/checkout@v5 + - uses: actions/setup-python@v5 + with: + python-version: "3.12" + - name: Configure and build Release with warnings as errors + run: | + cmake -S . -B build \ + -DCMAKE_BUILD_TYPE=Release \ + -DWSC_WARNINGS_AS_ERRORS=ON + cmake --build build \ + --target water-c4-h7-d2-three-source --parallel 2 + - name: Enumerate and solve all 1106490 fixed futures + run: | + mkdir -p out/full + set -o pipefail + build/water-c4-h7-d2-three-source \ + --self-test --output-dir out/full 2>&1 \ + | tee out/full/production.log + - name: Strictly validate schema, ledgers, and claim boundaries + run: | + python scripts/validate_c4_h7_d2_three_source_report.py \ + out/full/report.json --negative-tests + python - <<'PY' + import json + from pathlib import Path + + report = json.loads(Path("out/full/report.json").read_text()) + if report["status"] != "LOCAL_NO_RESIDUALS_EXPORTED": + raise SystemExit(f"unexpected full status: {report['status']}") + if report["claims"] != { + "three_source_checkpoint_family_eliminated": False, + "zero_debt_initial_family_eliminated": False, + "universal_c4_h7_solvability": False, + }: + raise SystemExit("full report crossed its checkpoint-only claim boundary") + Path("out/full/status.txt").write_text(report["status"] + "\n") + PY + - name: Independently rebuild, solve, and compare every fixed future + run: | + set -o pipefail + python tests/check_c4_h7_d2_three_source.py \ + --report out/full/report.json \ + --json out/full/independent-audit.json \ + --local-no-ledger out/full/independent-local-no-ledger.jsonl 2>&1 \ + | tee out/full/independent.log + - name: Verify independent NO rows remain explicitly local-only + run: | + python - <<'PY' + import json + from pathlib import Path + + path = Path("out/full/independent-local-no-ledger.jsonl") + rows = [json.loads(line) for line in path.read_text().splitlines()] + if not rows: + raise SystemExit("expected at least one independently reproduced checkpoint local NO") + for index, row in enumerate(rows): + if row.get("scope") != "nonzero_debt_parent_checkpoint_fixed_future": + raise SystemExit(f"independent NO {index} lost its local scope") + if row.get("zero_debt_past_restored") is not False: + raise SystemExit(f"independent NO {index} claims restored zero debt") + if row.get("global_counterexample") is not False: + raise SystemExit(f"independent NO {index} claims a global counterexample") + report = json.loads(Path("out/full/report.json").read_text()) + if len(rows) != report["run"]["local_no"]: + raise SystemExit("independent local-NO ledger count drifted") + PY + - name: Record the intentionally narrow conclusion + run: | + python - <<'PY' >> "$GITHUB_STEP_SUMMARY" + import json + from pathlib import Path + + report = json.loads(Path("out/full/report.json").read_text()) + print("> Exact full result: " + f"{report['run']['local_no']} of {report['run']['fixed_futures_checked']} " + "fixed futures are local NO at nonzero-debt parent checkpoints. " + "They are exported for a later zero-debt past-restoration analysis; " + "this job proves no balanced initial-layout NO and no global c4/h7 theorem.") + PY + cat out/full/report.md >> "$GITHUB_STEP_SUMMARY" + - name: Create and verify the full SHA-256 manifest + if: always() + run: | + find out/full -type f ! -name SHA256SUMS -print0 \ + | sort -z \ + | xargs -0 -r sha256sum > out/full/SHA256SUMS + sha256sum --check out/full/SHA256SUMS + - uses: actions/upload-artifact@v6 + if: always() + with: + name: c4-h7-d2-three-source-full-${{ github.run_id }} + path: out/full/ + if-no-files-found: error + retention-days: 30 diff --git a/.github/workflows/c4-h7-global-bypass.yml b/.github/workflows/c4-h7-global-bypass.yml new file mode 100644 index 0000000..6e98515 --- /dev/null +++ b/.github/workflows/c4-h7-global-bypass.yml @@ -0,0 +1,120 @@ +name: Audit c4 h7 global bypass lemmas +run-name: Check the critical-pair, anchor-pair, and rainbow-lift reductions + +on: + push: + branches: [codex/c4-h7-global-bypass] + workflow_dispatch: + +permissions: + contents: read + +concurrency: + group: c4-h7-global-bypass-${{ github.ref }} + cancel-in-progress: true + +jobs: + mathematical-reductions: + runs-on: ubuntu-latest + timeout-minutes: 30 + steps: + - uses: actions/checkout@v5 + - uses: actions/setup-python@v5 + with: + python-version: "3.12" + - name: Compile the independent audit programs + run: >- + python -m py_compile + tests/check_c4_h7_critical_pair_bypass.py + tests/check_c4_h7_rainbow_lift.py + tests/check_c4_h7_anchor_pair_potential.py + tests/check_c4_h7_anchor_pair_graph.py + tests/check_c4_h7_e2_a_not_q_four_source.py + tests/check_c4_h7_d2_four_source_q5_bypass.py + - name: Build the certified first-exhaustion census producer + run: | + cmake -S . -B build \ + -DCMAKE_BUILD_TYPE=Release \ + -DWSC_WARNINGS_AS_ERRORS=ON + cmake --build build \ + --target water-c4-h7-tq-exhaust-siblings --parallel 2 + - name: Rebuild the complete first-exhaustion ledger + run: | + mkdir -p out/anchor + build/water-c4-h7-tq-exhaust-siblings \ + --output-dir out/anchor + test "$(jq -r .status out/anchor/report.json)" = NEXT_RUN_CENSUS_COMPLETE + - name: Check every stated critical-pair and past-bypass formula + run: | + mkdir -p out/critical + set -o pipefail + python tests/check_c4_h7_critical_pair_bypass.py 2>&1 \ + | tee out/critical/audit.log + - name: Check rainbow factorization and exact token-lift fixtures + run: | + mkdir -p out/rainbow + set -o pipefail + python tests/check_c4_h7_rainbow_lift.py \ + --json out/rainbow/audit.json 2>&1 \ + | tee out/rainbow/audit.log + - name: Check the two-anchor potential and its complete ledger + run: | + set -o pipefail + python tests/check_c4_h7_anchor_pair_potential.py \ + --report out/anchor/report.json 2>&1 \ + | tee out/anchor/potential-audit.json + - name: Check anchor-pair switching and the height-seven saturation cut + run: | + mkdir -p out/anchor-graph + set -o pipefail + python tests/check_c4_h7_anchor_pair_graph.py 2>&1 \ + | tee out/anchor-graph/audit.log + - name: Check the E=2 A-form fixed-future four-source continuation + run: | + mkdir -p out/four-source-a + set -o pipefail + python tests/check_c4_h7_e2_a_not_q_four_source.py 2>&1 \ + | tee out/four-source-a/audit.log + { + printf '%s\n' '### E=2 A-form four-source audit' '' '```text' + cat out/four-source-a/audit.log + printf '%s\n' '```' + } >> "$GITHUB_STEP_SUMMARY" + - name: Check the E=2 Q-form q5 later-rotor bypass + run: | + mkdir -p out/four-source-q5 + set -o pipefail + python tests/check_c4_h7_d2_four_source_q5_bypass.py 2>&1 \ + | tee out/four-source-q5/audit.log + { + printf '%s\n' '### E=2 Q-form q5 four-source audit' '' '```text' + cat out/four-source-q5/audit.log + printf '%s\n' '```' + } >> "$GITHUB_STEP_SUMMARY" + - name: Record the exact claim boundary + run: | + cat >> "$GITHUB_STEP_SUMMARY" <<'EOF' + These checks certify three mathematical reductions: the exact + critical-pair disable formula plus the past/future bypass, the + two-anchor vector potential and first-sweep inequalities, and the + rainbow-transversal/token-error formula. It also checks the clean + two-switch return saturation cut, the fixed-future E=2 A-form + four-source continuation, and the scoped E=2 Q-form q5 later-rotor + bypass. They deliberately do not claim universal c4/k2/h7 + solvability. + EOF + - name: Hash the complete audit bundle + if: always() + run: | + mkdir -p out + find out -type f ! -name SHA256SUMS -print0 \ + | sort -z \ + | xargs -0 -r sha256sum > out/SHA256SUMS + sha256sum --check out/SHA256SUMS + - uses: actions/upload-artifact@v6 + if: always() + with: + name: c4-h7-global-bypass-audit-${{ github.run_id }} + path: out/ + if-no-files-found: error + retention-days: 30 diff --git a/CMakeLists.txt b/CMakeLists.txt index 4dd0627..7c1b451 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -141,6 +141,34 @@ else() endif() endif() +add_executable(water-c4-h7-d2-three-source apps/c4_h7_d2_three_source.cpp) +if(MSVC) + target_compile_options(water-c4-h7-d2-three-source PRIVATE /W4) + if(WSC_WARNINGS_AS_ERRORS) + target_compile_options(water-c4-h7-d2-three-source PRIVATE /WX) + endif() +else() + target_compile_options(water-c4-h7-d2-three-source PRIVATE -Wall -Wextra -Wpedantic) + if(WSC_WARNINGS_AS_ERRORS) + target_compile_options(water-c4-h7-d2-three-source PRIVATE -Werror) + endif() +endif() + +add_executable(water-c4-h7-d2-three-source-past + apps/c4_h7_d2_three_source_past.cpp) +if(MSVC) + target_compile_options(water-c4-h7-d2-three-source-past PRIVATE /W4) + if(WSC_WARNINGS_AS_ERRORS) + target_compile_options(water-c4-h7-d2-three-source-past PRIVATE /WX) + endif() +else() + target_compile_options(water-c4-h7-d2-three-source-past PRIVATE + -Wall -Wextra -Wpedantic) + if(WSC_WARNINGS_AS_ERRORS) + target_compile_options(water-c4-h7-d2-three-source-past PRIVATE -Werror) + endif() +endif() + include(CTest) if(BUILD_TESTING) add_executable(water-sort-tests tests/test_main.cpp) @@ -168,6 +196,13 @@ if(BUILD_TESTING) --self-test --limit 64 --output-dir ${CMAKE_CURRENT_BINARY_DIR}/test-c4-h7-d2-two-source-output) + add_test(NAME water-c4-h7-d2-three-source-smoke + COMMAND water-c4-h7-d2-three-source + --self-test + --limit 64 + --output-dir ${CMAKE_CURRENT_BINARY_DIR}/test-c4-h7-d2-three-source-output) + add_test(NAME water-c4-h7-d2-three-source-past-self-test + COMMAND water-c4-h7-d2-three-source-past --self-test) file(GLOB WSC_EXPERIMENT_INSTANCES "${CMAKE_CURRENT_SOURCE_DIR}/experiments/*.txt") foreach(WSC_EXPERIMENT_INSTANCE IN LISTS WSC_EXPERIMENT_INSTANCES) get_filename_component(WSC_EXPERIMENT_NAME ${WSC_EXPERIMENT_INSTANCE} NAME_WE) diff --git a/apps/c4_h7_d2_three_source.cpp b/apps/c4_h7_d2_three_source.cpp new file mode 100644 index 0000000..2e27703 --- /dev/null +++ b/apps/c4_h7_d2_three_source.cpp @@ -0,0 +1,1395 @@ +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include + +namespace { + +constexpr int kHeight = 7; +constexpr int kColors = 4; +constexpr int kEmpty = 2; +constexpr std::uint64_t kExpectedTqTerminals = 71; +constexpr std::uint64_t kExpectedLabeledCandidates = 624; +constexpr std::uint64_t kExpectedCanonicalParents = 418; +constexpr std::uint64_t kExpectedCanonicalEdges = 429; +constexpr std::uint64_t kExpectedSiblingEdges = 423; +constexpr std::uint64_t kExpectedSelectedEdges = 12; +constexpr std::uint64_t kExpectedDecorations = 1535; +constexpr std::uint64_t kExpectedResidualWords = 1106490; + +using Debts = std::array; +using Counts = std::array; +using Caps = std::array, kColors>; + +struct Options { + std::filesystem::path output_dir; + std::uint64_t limit = 0; + bool self_test = false; +}; + +struct Bucket { + int debt = 0; + std::vector caps; + + bool operator<(const Bucket& other) const { + return std::tie(debt, caps) < std::tie(other.debt, other.caps); + } + bool operator==(const Bucket& other) const { + return debt == other.debt && caps == other.caps; + } +}; + +using State = std::array; + +struct Source { + int color = 0; + int cap = 0; +}; + +struct ExhaustAction { + int old_color = 0; + int old_cap = 0; + int final_color = 0; + + bool operator<(const ExhaustAction& other) const { + return std::tie(old_color, old_cap, final_color) < + std::tie(other.old_color, other.old_cap, other.final_color); + } +}; + +struct Card { + int color = 0; + int endpoint = 0; +}; + +struct Edge { + std::size_t ordinal = 0; + State parent; + State terminal; + ExhaustAction bad; + Debts terminal_debts{}; + int q_color = -1; + std::array q_caps{}; + int legal_source_count = 0; +}; + +struct Bridge { + std::vector edges; + std::uint64_t terminal_count = 0; + std::uint64_t labeled_candidates = 0; + std::uint64_t canonical_parent_count = 0; + std::uint64_t canonical_edge_count = 0; + std::uint64_t sibling_edge_count = 0; +}; + +struct Decoration { + std::size_t ordinal = 0; + std::size_t edge_index = 0; + std::array cards{}; + Counts residual_after_forced{}; + std::array free_tail_lengths{}; + std::uint64_t residual_words_expected = 0; +}; + +struct FixedFixture { + Debts debts{}; + std::array sources{}; + std::array, kColors> hidden_bottom_to_top; +}; + +struct EdgeStats { + std::size_t edge_ordinal = 0; + std::uint64_t decorations = 0; + std::uint64_t residual_words_expected = 0; + std::uint64_t residual_words_checked = 0; + std::uint64_t local_yes = 0; + std::uint64_t local_no = 0; + std::uint64_t states = 0; + std::uint64_t transitions = 0; + std::map safe_mask_distribution; +}; + +struct Sample { + bool present = false; + std::uint64_t future_index = 0; + std::size_t decoration_index = 0; + std::size_t edge_ordinal = 0; + bool solvable = false; + std::uint32_t safe_mask = 0; + std::string path; + std::array hidden_words_bottom_to_top; +}; + +struct RunStats { + bool self_checks_passed = false; + bool universe_complete = false; + std::uint64_t limit_requested = 0; + std::uint64_t decorations_expected = 0; + std::uint64_t residual_words_expected = 0; + std::uint64_t residual_words_checked = 0; + std::uint64_t local_yes = 0; + std::uint64_t local_no = 0; + std::uint64_t winning_paths_replayed = 0; + std::uint64_t states = 0; + std::uint64_t transitions = 0; + std::uint64_t ledger_hash = 1469598103934665603ULL; + std::vector per_edge; + std::optional first_yes; + std::optional first_no; + double elapsed_seconds = 0.0; +}; + +void require(bool condition, const std::string& message) { + if (!condition) throw std::runtime_error("self-check failed: " + message); +} + +void usage() { + std::cerr << "Usage: water-c4-h7-d2-three-source --output-dir DIR " + "[--limit N] [--self-test]\n"; +} + +Options parse_options(int argc, char** argv) { + Options options; + for (int index = 1; index < argc; ++index) { + const std::string argument = argv[index]; + if (argument == "--output-dir" && index + 1 < argc) { + options.output_dir = argv[++index]; + } else if (argument == "--limit" && index + 1 < argc) { + options.limit = std::stoull(argv[++index]); + } else if (argument == "--self-test") { + options.self_test = true; + } else if (argument == "--help") { + usage(); + std::exit(0); + } else { + usage(); + throw std::runtime_error("unknown or incomplete argument: " + argument); + } + } + if (options.output_dir.empty() && !options.self_test) { + usage(); + throw std::runtime_error("--output-dir is required unless --self-test is used"); + } + return options; +} + +int positive_count(const Debts& debts) { + return static_cast(std::count_if( + debts.begin(), debts.end(), [](int value) { return value > 0; })); +} + +State canonical_state(const Debts& debts, Caps caps) { + State result; + for (int color = 0; color < kColors; ++color) { + std::sort(caps[color].begin(), caps[color].end()); + result[static_cast(color)] = {debts[color], caps[color]}; + } + std::sort(result.begin(), result.end()); + return result; +} + +Debts state_debts(const State& state) { + Debts result{}; + for (int color = 0; color < kColors; ++color) result[color] = state[color].debt; + return result; +} + +Caps state_caps(const State& state) { + Caps result; + for (int color = 0; color < kColors; ++color) result[color] = state[color].caps; + return result; +} + +Counts exposed_counts(const State& state) { + Counts result{}; + for (int color = 0; color < kColors; ++color) { + result[color] = state[color].debt; + for (const int cap : state[color].caps) result[color] += cap; + } + return result; +} + +bool algebraically_consistent(const State& state, int exhausted) { + if (!std::is_sorted(state.begin(), state.end())) return false; + int cap_count = 0; + int debt_sum = 0; + Counts multiplicity{}; + for (int color = 0; color < kColors; ++color) { + debt_sum += state[color].debt; + multiplicity[color] = static_cast(state[color].caps.size()); + cap_count += multiplicity[color]; + for (const int cap : state[color].caps) { + if (cap < 1 || cap >= kHeight) return false; + } + } + if (cap_count != kColors - exhausted || debt_sum != exhausted * kHeight) { + return false; + } + const Counts exposed = exposed_counts(state); + Counts remaining{}; + for (int color = 0; color < kColors; ++color) { + if (exposed[color] < multiplicity[color] || exposed[color] > kHeight) { + return false; + } + remaining[color] = kHeight - exposed[color]; + } + for (int color = 0; color < kColors; ++color) { + int allowed = 0; + for (int other = 0; other < kColors; ++other) { + if (other != color) allowed += remaining[other]; + } + if (multiplicity[color] > allowed) return false; + } + return true; +} + +bool source_is_legal(const Debts& debts, int exhausted, int color, int cap) { + Debts tested = debts; + tested[color] += cap; + return positive_count(tested) <= kEmpty + exhausted; +} + +bool source_is_legal(const State& state, int exhausted, int color, int cap) { + return source_is_legal(state_debts(state), exhausted, color, cap); +} + +std::vector sources(const State& state) { + std::vector result; + for (int color = 0; color < kColors; ++color) { + for (const int cap : state[color].caps) result.push_back({color, cap}); + } + return result; +} + +std::vector legal_sources(const State& state, int exhausted) { + std::vector result; + for (const Source source : sources(state)) { + if (source_is_legal(state, exhausted, source.color, source.cap)) { + result.push_back(source); + } + } + return result; +} + +bool is_tq_terminal(const State& state) { + if (!algebraically_consistent(state, 1) || !legal_sources(state, 1).empty()) { + return false; + } + int positive = 0; + int nonpositive = 0; + int topped_nonpositive = 0; + int topped_positive = 0; + for (const Bucket& bucket : state) { + if (bucket.debt > 0) { + ++positive; + topped_positive += !bucket.caps.empty(); + } else { + ++nonpositive; + topped_nonpositive += !bucket.caps.empty(); + } + } + return positive == 3 && nonpositive == 1 && topped_nonpositive == 1 && + topped_positive == 0; +} + +std::vector enumerate_tq_terminals() { + std::set terminals; + for (int energy = 0; energy <= 2; ++energy) { + for (int c0 = 1; c0 < kHeight; ++c0) { + for (int c1 = c0; c1 < kHeight; ++c1) { + for (int c2 = c1; c2 < kHeight; ++c2) { + if (c0 <= energy || c0 + c1 + c2 - energy > kHeight) continue; + for (int p0 = 1; p0 <= kHeight; ++p0) { + for (int p1 = p0; p1 <= kHeight; ++p1) { + for (int p2 = p1; p2 <= kHeight; ++p2) { + if (p0 + p1 + p2 - energy != kHeight) continue; + Debts debts{{-energy, p0, p1, p2}}; + Caps caps; + caps[0] = {c0, c1, c2}; + State state = canonical_state(debts, caps); + if (is_tq_terminal(state)) terminals.insert(state); + } + } + } + } + } + } + } + return {terminals.begin(), terminals.end()}; +} + +std::optional apply_exhausting_action(const State& state, int exhausted, + const ExhaustAction& action) { + if (action.old_color < 0 || action.old_color >= kColors || + action.final_color < 0 || action.final_color >= kColors || + action.old_color == action.final_color || action.old_cap < 1 || + action.old_cap >= kHeight || + !source_is_legal(state, exhausted, action.old_color, action.old_cap)) { + return std::nullopt; + } + Debts debts = state_debts(state); + Caps caps = state_caps(state); + auto& old_caps = caps[action.old_color]; + const auto found = std::find(old_caps.begin(), old_caps.end(), action.old_cap); + if (found == old_caps.end()) return std::nullopt; + old_caps.erase(found); + debts[action.old_color] += action.old_cap; + debts[action.final_color] += kHeight - action.old_cap; + State successor = canonical_state(debts, caps); + if (!algebraically_consistent(successor, exhausted + 1)) return std::nullopt; + return successor; +} + +std::vector reverse_exhausting_candidates(const State& terminal) { + std::vector candidates; + for (int old_cap = 1; old_cap < kHeight; ++old_cap) { + for (int old_color = 0; old_color < kColors; ++old_color) { + for (int final_color = 0; final_color < kColors; ++final_color) { + if (old_color == final_color) continue; + Debts debts = state_debts(terminal); + Caps caps = state_caps(terminal); + debts[old_color] -= old_cap; + debts[final_color] -= kHeight - old_cap; + caps[old_color].push_back(old_cap); + Debts tested = debts; + tested[old_color] += old_cap; + if (positive_count(tested) > kEmpty) continue; + State parent = canonical_state(debts, caps); + if (algebraically_consistent(parent, 0)) candidates.push_back(parent); + } + } + } + std::sort(candidates.begin(), candidates.end()); + return candidates; +} + +std::vector exhausting_actions_to(const State& parent, + const State& terminal) { + std::set actions; + for (int old_color = 0; old_color < kColors; ++old_color) { + const std::set unique_caps(parent[old_color].caps.begin(), + parent[old_color].caps.end()); + for (const int old_cap : unique_caps) { + for (int final_color = 0; final_color < kColors; ++final_color) { + ExhaustAction action{old_color, old_cap, final_color}; + const auto successor = apply_exhausting_action(parent, 0, action); + if (successor && *successor == terminal) actions.insert(action); + } + } + } + return {actions.begin(), actions.end()}; +} + +Bridge build_bridge() { + Bridge bridge; + const auto terminals = enumerate_tq_terminals(); + bridge.terminal_count = terminals.size(); + std::vector> labeled; + std::set> pairs; + for (const State& terminal : terminals) { + for (const State& parent : reverse_exhausting_candidates(terminal)) { + labeled.emplace_back(parent, terminal); + pairs.emplace(parent, terminal); + } + } + bridge.labeled_candidates = labeled.size(); + bridge.canonical_edge_count = pairs.size(); + std::set parents; + for (const auto& pair : pairs) parents.insert(pair.first); + bridge.canonical_parent_count = parents.size(); + + for (const auto& pair : pairs) { + const State& parent = pair.first; + const State& terminal = pair.second; + const auto legal = legal_sources(parent, 0); + const auto actions = exhausting_actions_to(parent, terminal); + require(actions.size() == 1, "bridge edge does not have a unique bad action"); + const ExhaustAction bad = actions.front(); + if (legal.size() == 1) continue; + ++bridge.sibling_edge_count; + + Debts labeled_terminal = state_debts(parent); + Caps remaining_caps = state_caps(parent); + auto& bad_caps = remaining_caps[bad.old_color]; + const auto found = std::find(bad_caps.begin(), bad_caps.end(), bad.old_cap); + require(found != bad_caps.end(), "bridge bad source is absent"); + bad_caps.erase(found); + labeled_terminal[bad.old_color] += bad.old_cap; + labeled_terminal[bad.final_color] += kHeight - bad.old_cap; + require(canonical_state(labeled_terminal, remaining_caps) == terminal, + "labeled bridge replay does not reach its terminal"); + + int q_color = -1; + for (int color = 0; color < kColors; ++color) { + if (remaining_caps[color].size() == 3) { + require(q_color == -1, "bridge has two three-column colors"); + q_color = color; + } else { + require(remaining_caps[color].empty(), + "bridge remainder is not an all-q triple"); + } + } + require(q_color >= 0, "bridge has no terminal q color"); + std::sort(remaining_caps[q_color].begin(), remaining_caps[q_color].end()); + Edge edge; + edge.ordinal = bridge.edges.size(); + edge.parent = parent; + edge.terminal = terminal; + edge.bad = bad; + edge.terminal_debts = labeled_terminal; + edge.q_color = q_color; + std::copy(remaining_caps[q_color].begin(), remaining_caps[q_color].end(), + edge.q_caps.begin()); + edge.legal_source_count = static_cast(legal.size()); + bridge.edges.push_back(std::move(edge)); + } + + require(bridge.terminal_count == kExpectedTqTerminals, + "Tq terminal count is not 71"); + require(bridge.labeled_candidates == kExpectedLabeledCandidates, + "labeled first-exhaust candidate count is not 624"); + require(bridge.canonical_parent_count == kExpectedCanonicalParents, + "canonical parent count is not 418"); + require(bridge.canonical_edge_count == kExpectedCanonicalEdges, + "canonical edge count is not 429"); + require(bridge.sibling_edge_count == kExpectedSiblingEdges, + "sibling edge count is not 423"); + return bridge; +} + +std::vector cards_for(int q_color, int cap) { + std::vector cards; + for (int color = 0; color < kColors; ++color) { + if (color == q_color) continue; + for (int endpoint = cap + 1; endpoint <= kHeight; ++endpoint) { + cards.push_back({color, endpoint}); + } + } + return cards; +} + +std::uint64_t multinomial(const Counts& counts) { + static constexpr std::array factorial{{ + 1ULL, 1ULL, 2ULL, 6ULL, 24ULL, 120ULL, 720ULL, 5040ULL, + 40320ULL, 362880ULL, 3628800ULL, 39916800ULL, 479001600ULL, + 6227020800ULL, 87178291200ULL, 1307674368000ULL, + 20922789888000ULL, 355687428096000ULL, 6402373705728000ULL, + 121645100408832000ULL, 2432902008176640000ULL}}; + int total = 0; + for (const int count : counts) { + if (count < 0) return 0; + total += count; + } + require(total >= 0 && total <= 20, "multinomial total exceeds table"); + std::uint64_t result = factorial[static_cast(total)]; + for (const int count : counts) { + result /= factorial[static_cast(count)]; + } + return result; +} + +std::uint64_t count_completions(const Counts& residual, + const std::array& tail_lengths, + const std::array& cards) { + int positions = 0; + int residual_total = 0; + for (const int length : tail_lengths) { + if (length < 0) return 0; + positions += length; + } + for (const int value : residual) { + if (value < 0) return 0; + residual_total += value; + } + if (positions != residual_total) return 0; + + Counts remaining = residual; + std::uint64_t result = 0; + const auto choose_boundaries = [&](const auto& self, int slot) -> void { + while (slot < 3 && tail_lengths[slot] == 0) ++slot; + if (slot == 3) { + result += multinomial(remaining); + return; + } + for (int color = 0; color < kColors; ++color) { + if (color == cards[slot].color || remaining[color] == 0) continue; + --remaining[color]; + self(self, slot + 1); + ++remaining[color]; + } + }; + choose_boundaries(choose_boundaries, 0); + return result; +} + +bool q_source_is_legal(const Edge& edge, int cap) { + return source_is_legal(edge.parent, 0, edge.q_color, cap); +} + +bool bad_source_legal_after_live(const Edge& edge, int q_cap, const Card& card) { + Debts debts = state_debts(edge.parent); + debts[edge.q_color] += q_cap; + debts[card.color] -= q_cap; + return source_is_legal(debts, 0, edge.bad.old_color, edge.bad.old_cap); +} + +bool immediate_tq_after_sibling_exhaust(const Edge& edge, int slot, + const Card& card) { + if (card.endpoint != kHeight) return false; + Debts debts = state_debts(edge.parent); + Caps caps = state_caps(edge.parent); + auto& q_caps = caps[edge.q_color]; + const auto found = std::find(q_caps.begin(), q_caps.end(), edge.q_caps[slot]); + require(found != q_caps.end(), "direct sibling cap is absent"); + q_caps.erase(found); + debts[edge.q_color] += edge.q_caps[slot]; + debts[card.color] += kHeight - edge.q_caps[slot]; + return is_tq_terminal(canonical_state(debts, caps)); +} + +bool is_exact_live_tq_corner(const Edge& edge, int slot, + const std::array& cards, int n_value) { + if (n_value != 0 || cards[slot].endpoint != 3) return false; + for (int other = 0; other < 3; ++other) { + if (other == slot) continue; + if (edge.q_caps[other] != 1 || + cards[other].color != cards[slot].color || + cards[other].endpoint != 3) { + return false; + } + } + return true; +} + +bool is_refined_d2_reduction(const Edge& edge, + const std::array& cards) { + bool direct_certified = false; + bool n_ge_3 = false; + bool n_le_2_noncorner = false; + bool nonhandoff = false; + for (int slot = 0; slot < 3; ++slot) { + const int q_cap = edge.q_caps[slot]; + if (!q_source_is_legal(edge, q_cap)) continue; + const Card& card = cards[slot]; + if (card.endpoint == kHeight) { + direct_certified = direct_certified || + !immediate_tq_after_sibling_exhaust(edge, slot, card); + continue; + } + if (!bad_source_legal_after_live(edge, q_cap, card)) { + nonhandoff = true; + continue; + } + const int n_value = q_cap - edge.terminal_debts[card.color]; + require(n_value >= 0, "live handoff has negative N"); + if (n_value >= 3) { + n_ge_3 = true; + } else if (!is_exact_live_tq_corner(edge, slot, cards, n_value)) { + n_le_2_noncorner = true; + } + } + return !direct_certified && !n_ge_3 && !n_le_2_noncorner && nonhandoff; +} + +std::vector enumerate_decorations(const Bridge& bridge) { + static constexpr std::array, 12> expected{{ + {116, 198, 64680}, {117, 732, 252252}, {174, 263, 620928}, + {175, 192, 51744}, {178, 104, 19404}, {184, 6, 462}, + {236, 8, 72072}, {237, 6, 11088}, {238, 4, 924}, + {242, 8, 11088}, {244, 6, 924}, {248, 8, 924}}}; + + std::map> rows; + std::vector decorations; + for (const Edge& edge : bridge.edges) { + if (edge.legal_source_count != 3) continue; + const auto cards0 = cards_for(edge.q_color, edge.q_caps[0]); + const auto cards1 = cards_for(edge.q_color, edge.q_caps[1]); + const auto cards2 = cards_for(edge.q_color, edge.q_caps[2]); + for (const Card& card0 : cards0) { + for (const Card& card1 : cards1) { + for (const Card& card2 : cards2) { + const std::array cards{{card0, card1, card2}}; + Counts residual{}; + const Counts exposed = exposed_counts(edge.parent); + for (int color = 0; color < kColors; ++color) { + residual[color] = kHeight - exposed[color]; + } + residual[edge.bad.final_color] -= kHeight - edge.bad.old_cap; + std::array tails{}; + for (int slot = 0; slot < 3; ++slot) { + residual[cards[slot].color] -= + cards[slot].endpoint - edge.q_caps[slot]; + tails[slot] = kHeight - cards[slot].endpoint; + } + const std::uint64_t completions = + count_completions(residual, tails, cards); + if (completions == 0 || + !is_refined_d2_reduction(edge, cards)) { + continue; + } + Decoration decoration; + decoration.ordinal = decorations.size(); + decoration.edge_index = edge.ordinal; + decoration.cards = cards; + decoration.residual_after_forced = residual; + decoration.free_tail_lengths = tails; + decoration.residual_words_expected = completions; + decorations.push_back(decoration); + auto& row = rows[edge.ordinal]; + ++row.first; + row.second += completions; + } + } + } + } + + require(rows.size() == kExpectedSelectedEdges, + "three-source D2 edge count is not 12"); + for (const auto& item : expected) { + const std::size_t edge = std::get<0>(item); + const auto found = rows.find(edge); + require(found != rows.end(), "expected three-source edge is absent"); + require(found->second.first == std::get<1>(item) && + found->second.second == std::get<2>(item), + "three-source per-edge decoration ledger drifted"); + } + require(decorations.size() == kExpectedDecorations, + "three-source D2 decoration count is not 1535"); + const std::uint64_t words = std::accumulate( + decorations.begin(), decorations.end(), std::uint64_t{0}, + [](std::uint64_t sum, const Decoration& decoration) { + return sum + decoration.residual_words_expected; + }); + require(words == kExpectedResidualWords, + "three-source residual-word weight is not 1106490"); + return decorations; +} + +class FixedFutureSolver { +public: + struct Result { + bool solvable = false; + std::uint32_t safe_mask = 0; + std::string path; + std::uint64_t states = 0; + std::uint64_t transitions = 0; + }; + + FixedFutureSolver(const Debts& debts, + const std::array& sources, + const std::array, kColors>& words) + : initial_debts_(debts), sources_(sources) { + std::uint32_t multiplier = 1; + for (std::size_t column = 0; column < kColors; ++column) { + build_events(column, words[column]); + multipliers_[column] = multiplier; + multiplier *= static_cast(events_[column].size() + 1); + } + memo_.assign(multiplier, -1); + } + + Result solve() { + Result result; + result.solvable = visit(0); + for (std::size_t column = 0; column < kColors; ++column) { + if (safe_from(0, column)) result.safe_mask |= 1U << column; + } + if (result.solvable) { + std::uint32_t state = 0; + while (!goal(state)) { + bool advanced = false; + for (std::size_t column = 0; column < kColors; ++column) { + if (!safe_from(state, column)) continue; + result.path.push_back(static_cast('0' + column)); + state += multipliers_[column]; + advanced = true; + break; + } + require(advanced, "winning fixed future has no safe successor"); + } + } + result.states = states_; + result.transitions = transitions_; + return result; + } + + bool replay(const std::string& path) const { + std::uint32_t state = 0; + for (const char value : path) { + const std::size_t column = static_cast(value - '0'); + if (column >= kColors || !legal(state, column)) return false; + state += multipliers_[column]; + } + return goal(state); + } + +private: + struct Event { + int old_color = 0; + int old_cap = 0; + int next_color = 0; + int next_cap = 0; + }; + + Debts initial_debts_{}; + std::array sources_{}; + std::array, kColors> events_; + std::array, kColors> deltas_; + std::array multipliers_{}; + std::vector memo_; + std::uint64_t states_ = 0; + std::uint64_t transitions_ = 0; + + void build_events(std::size_t column, const std::vector& word) { + int old_color = sources_[column].color; + int old_cap = sources_[column].cap; + int cursor = static_cast(word.size()) - 1; + while (cursor >= 0) { + const int next_color = word[static_cast(cursor)]; + require(next_color != old_color, "hidden word repeats current top color"); + int first = cursor; + while (first > 0 && + word[static_cast(first - 1)] == next_color) { + --first; + } + const int length = cursor - first + 1; + const int next_cap = old_cap + length; + events_[column].push_back({old_color, old_cap, next_color, next_cap}); + old_color = next_color; + old_cap = next_cap; + cursor = first - 1; + } + require(!events_[column].empty() && + events_[column].back().next_cap == kHeight, + "fixed future does not exhaust its column at height seven"); + deltas_[column].assign(events_[column].size() + 1, Debts{}); + for (std::size_t index = 0; index < events_[column].size(); ++index) { + deltas_[column][index + 1] = deltas_[column][index]; + const Event& event = events_[column][index]; + deltas_[column][index + 1][event.old_color] += event.old_cap; + if (event.next_cap == kHeight) { + deltas_[column][index + 1][event.next_color] += + kHeight - event.old_cap; + } else { + deltas_[column][index + 1][event.next_color] -= event.old_cap; + } + } + } + + std::array decode(std::uint32_t state) const { + std::array ranks{}; + for (std::size_t column = 0; column < kColors; ++column) { + ranks[column] = (state / multipliers_[column]) % + (events_[column].size() + 1); + } + return ranks; + } + + int exhausted(const std::array& ranks) const { + int result = 0; + for (std::size_t column = 0; column < kColors; ++column) { + result += ranks[column] == events_[column].size(); + } + return result; + } + + bool goal(std::uint32_t state) const { + return exhausted(decode(state)) >= kEmpty; + } + + bool legal(std::uint32_t state, std::size_t column) const { + const auto ranks = decode(state); + if (ranks[column] == events_[column].size()) return false; + Debts debts = initial_debts_; + for (std::size_t other = 0; other < kColors; ++other) { + for (int color = 0; color < kColors; ++color) { + debts[color] += deltas_[other][ranks[other]][color]; + } + } + const Event& event = events_[column][ranks[column]]; + debts[event.old_color] += event.old_cap; + return positive_count(debts) <= kEmpty + exhausted(ranks); + } + + bool safe_from(std::uint32_t state, std::size_t column) { + if (goal(state) || !legal(state, column)) return false; + ++transitions_; + return visit(state + multipliers_[column]); + } + + bool visit(std::uint32_t state) { + if (goal(state)) return true; + std::int8_t& memo = memo_[state]; + if (memo >= 0) return memo != 0; + ++states_; + for (std::size_t column = 0; column < kColors; ++column) { + if (safe_from(state, column)) { + memo = 1; + return true; + } + } + memo = 0; + return false; + } +}; + +std::string digits(const std::vector& values) { + std::string result; + result.reserve(values.size()); + for (const int value : values) { + result.push_back(static_cast('0' + value)); + } + return result; +} + +FixedFixture make_fixture(const Edge& edge, + const std::array, 3>& q_words) { + FixedFixture fixture; + fixture.debts = state_debts(edge.parent); + fixture.sources[0] = {edge.bad.old_color, edge.bad.old_cap}; + fixture.hidden_bottom_to_top[0].assign( + static_cast(kHeight - edge.bad.old_cap), + edge.bad.final_color); + for (std::size_t slot = 0; slot < 3; ++slot) { + fixture.sources[slot + 1] = {edge.q_color, edge.q_caps[slot]}; + fixture.hidden_bottom_to_top[slot + 1] = q_words[slot]; + } + + Counts used{}; + for (std::size_t column = 0; column < kColors; ++column) { + const auto& word = fixture.hidden_bottom_to_top[column]; + require(word.size() == static_cast( + kHeight - fixture.sources[column].cap), + "fixture hidden word has the wrong length"); + require(!word.empty() && word.back() != fixture.sources[column].color, + "fixture does not begin at a genuine run boundary"); + for (const int color : word) ++used[color]; + } + const Counts exposed = exposed_counts(edge.parent); + for (int color = 0; color < kColors; ++color) { + require(used[color] == kHeight - exposed[color], + "fixture does not realize the parent color inventory"); + } + return fixture; +} + +template +bool for_each_fixed_future(const Decoration& decoration, const Edge& edge, + Callback&& callback) { + Counts remaining = decoration.residual_after_forced; + std::array boundaries{{-1, -1, -1}}; + std::uint64_t emitted = 0; + bool stopped = false; + + const auto choose_boundaries = [&](const auto& self, int slot) -> void { + if (stopped) return; + while (slot < 3 && decoration.free_tail_lengths[slot] == 0) ++slot; + if (slot < 3) { + for (int color = 0; color < kColors; ++color) { + if (color == decoration.cards[slot].color || remaining[color] == 0) { + continue; + } + --remaining[color]; + boundaries[slot] = color; + self(self, slot + 1); + boundaries[slot] = -1; + ++remaining[color]; + if (stopped) return; + } + return; + } + + std::vector pool; + for (int color = 0; color < kColors; ++color) { + pool.insert(pool.end(), static_cast(remaining[color]), color); + } + std::array, 3> free_top_to_bottom; + int free_slots = 0; + for (int q_slot = 0; q_slot < 3; ++q_slot) { + const int length = decoration.free_tail_lengths[q_slot]; + free_top_to_bottom[q_slot].assign(static_cast(length), -1); + if (length > 0) { + require(boundaries[q_slot] >= 0, "free tail has no boundary color"); + free_top_to_bottom[q_slot][0] = boundaries[q_slot]; + free_slots += length - 1; + } + } + require(static_cast(pool.size()) == free_slots, + "free-tail pool has the wrong size"); + + do { + std::size_t cursor = 0; + for (int q_slot = 0; q_slot < 3; ++q_slot) { + for (std::size_t position = 1; + position < free_top_to_bottom[q_slot].size(); ++position) { + free_top_to_bottom[q_slot][position] = pool[cursor++]; + } + } + require(cursor == pool.size(), "free-tail permutation was not consumed"); + + std::array, 3> q_words_bottom_to_top; + for (int q_slot = 0; q_slot < 3; ++q_slot) { + q_words_bottom_to_top[q_slot].assign( + free_top_to_bottom[q_slot].rbegin(), + free_top_to_bottom[q_slot].rend()); + const int forced = decoration.cards[q_slot].endpoint - + edge.q_caps[q_slot]; + q_words_bottom_to_top[q_slot].insert( + q_words_bottom_to_top[q_slot].end(), + static_cast(forced), + decoration.cards[q_slot].color); + } + ++emitted; + if (!callback(q_words_bottom_to_top, free_top_to_bottom)) { + stopped = true; + return; + } + } while (std::next_permutation(pool.begin(), pool.end())); + }; + choose_boundaries(choose_boundaries, 0); + if (!stopped) { + require(emitted == decoration.residual_words_expected, + "fixed-future enumeration disagrees with its exact weight"); + } + return !stopped; +} + +std::string join_words(const std::array, kColors>& words, + char separator) { + std::ostringstream output; + for (std::size_t column = 0; column < kColors; ++column) { + if (column != 0) output << separator; + output << digits(words[column]); + } + return output.str(); +} + +std::string cards_text(const std::array& cards) { + std::ostringstream output; + for (std::size_t slot = 0; slot < 3; ++slot) { + if (slot != 0) output << ','; + output << cards[slot].color << ':' << cards[slot].endpoint; + } + return output.str(); +} + +void update_hash(std::uint64_t& hash, const std::string& text) { + static constexpr std::uint64_t prime = 1099511628211ULL; + for (const unsigned char value : text) { + hash ^= value; + hash *= prime; + } + hash ^= static_cast('\n'); + hash *= prime; +} + +Sample make_sample(std::uint64_t future_index, const Decoration& decoration, + const Edge& edge, const FixedFixture& fixture, + const FixedFutureSolver::Result& result) { + Sample sample; + sample.present = true; + sample.future_index = future_index; + sample.decoration_index = decoration.ordinal; + sample.edge_ordinal = edge.ordinal; + sample.solvable = result.solvable; + sample.safe_mask = result.safe_mask; + sample.path = result.path; + for (std::size_t column = 0; column < kColors; ++column) { + sample.hidden_words_bottom_to_top[column] = + digits(fixture.hidden_bottom_to_top[column]); + } + return sample; +} + +void write_local_no(std::ostream& output, const Sample& sample, + const Edge& edge, const Decoration& decoration) { + output << "{\"future_index\":" << sample.future_index + << ",\"decoration_index\":" << sample.decoration_index + << ",\"bridge_edge\":" << sample.edge_ordinal + << ",\"parent_debts\":["; + const Debts debts = state_debts(edge.parent); + for (int color = 0; color < kColors; ++color) { + if (color != 0) output << ','; + output << debts[color]; + } + output << "],\"bad_source\":[" << edge.bad.old_color << ',' + << edge.bad.old_cap << ',' << edge.bad.final_color + << "],\"q_color\":" << edge.q_color << ",\"q_caps\":["; + for (std::size_t slot = 0; slot < 3; ++slot) { + if (slot != 0) output << ','; + output << edge.q_caps[slot]; + } + output << "],\"cards\":["; + for (std::size_t slot = 0; slot < 3; ++slot) { + if (slot != 0) output << ','; + output << '[' << decoration.cards[slot].color << ',' + << decoration.cards[slot].endpoint << ']'; + } + output << "],\"hidden_words_bottom_to_top\":["; + for (std::size_t column = 0; column < kColors; ++column) { + if (column != 0) output << ','; + output << '"' << sample.hidden_words_bottom_to_top[column] << '"'; + } + output << "],\"local_status\":\"NO\",\"safe_source_mask\":0}\n"; +} + +void run_solver_self_tests() { + { + const Debts debts{{-5, 0, 2, 3}}; + const std::array sources{{ + Source{0, 3}, Source{0, 3}, Source{0, 3}, Source{0, 3}}}; + const std::array, kColors> words{{ + std::vector{2, 2, 2, 1}, + std::vector{3, 3, 2, 1}, + std::vector{3, 3, 2, 1}, + std::vector{1, 1, 1, 1}}}; + FixedFutureSolver solver(debts, sources, words); + const auto result = solver.solve(); + require(!result.solvable && result.safe_mask == 0 && result.path.empty(), + "known four-way local lock did not solve as local NO"); + } + { + const Debts debts{}; + const std::array sources{{ + Source{0, 6}, Source{1, 6}, Source{2, 6}, Source{3, 6}}}; + const std::array, kColors> words{{ + std::vector{1}, std::vector{2}, + std::vector{3}, std::vector{0}}}; + FixedFutureSolver solver(debts, sources, words); + const auto result = solver.solve(); + require(result.solvable && result.safe_mask != 0, + "synthetic two-exhaustion fixture is not YES"); + require(solver.replay(result.path), + "synthetic winning path did not replay"); + } +} + +RunStats run(const Options& options, const Bridge& bridge, + const std::vector& decorations) { + RunStats stats; + stats.limit_requested = options.limit; + stats.decorations_expected = decorations.size(); + for (const Decoration& decoration : decorations) { + stats.residual_words_expected += decoration.residual_words_expected; + } + require(stats.decorations_expected == kExpectedDecorations, + "run decoration universe is not 1535"); + require(stats.residual_words_expected == kExpectedResidualWords, + "run fixed-future universe is not 1106490"); + + std::map row_for_edge; + for (const Decoration& decoration : decorations) { + const std::size_t edge_ordinal = bridge.edges[decoration.edge_index].ordinal; + auto found = row_for_edge.find(edge_ordinal); + if (found == row_for_edge.end()) { + const std::size_t row = stats.per_edge.size(); + row_for_edge.emplace(edge_ordinal, row); + EdgeStats edge_stats; + edge_stats.edge_ordinal = edge_ordinal; + stats.per_edge.push_back(edge_stats); + found = row_for_edge.find(edge_ordinal); + } + EdgeStats& edge_stats = stats.per_edge[found->second]; + ++edge_stats.decorations; + edge_stats.residual_words_expected += decoration.residual_words_expected; + } + require(stats.per_edge.size() == kExpectedSelectedEdges, + "run edge universe is not 12"); + + std::optional result_ledger; + std::optional local_no_ledger; + if (!options.output_dir.empty()) { + std::filesystem::create_directories(options.output_dir); + result_ledger.emplace(options.output_dir / "fixed-future-results.tsv", + std::ios::binary); + local_no_ledger.emplace(options.output_dir / "local-no-ledger.jsonl", + std::ios::binary); + require(*result_ledger && *local_no_ledger, + "could not open fixed-future ledgers"); + *result_ledger << "future_index\tdecoration_index\tbridge_edge\tcards" + "\thidden_words_bottom_to_top\tlocal_status" + "\tsafe_source_mask\tescape_columns\n"; + } + + const std::uint64_t effective_limit = options.limit == 0 + ? stats.residual_words_expected + : std::min(options.limit, stats.residual_words_expected); + const auto started = std::chrono::steady_clock::now(); + bool stop = false; + for (const Decoration& decoration : decorations) { + if (stop) break; + const Edge& edge = bridge.edges[decoration.edge_index]; + EdgeStats& edge_stats = stats.per_edge[row_for_edge.at(edge.ordinal)]; + std::uint64_t decoration_checked = 0; + const bool complete_decoration = for_each_fixed_future( + decoration, edge, + [&](const std::array, 3>& q_words, + const std::array, 3>&) { + if (stats.residual_words_checked >= effective_limit) return false; + const FixedFixture fixture = make_fixture(edge, q_words); + FixedFutureSolver solver(fixture.debts, fixture.sources, + fixture.hidden_bottom_to_top); + const auto result = solver.solve(); + const std::uint64_t future_index = stats.residual_words_checked; + ++stats.residual_words_checked; + ++edge_stats.residual_words_checked; + ++decoration_checked; + stats.states += result.states; + stats.transitions += result.transitions; + edge_stats.states += result.states; + edge_stats.transitions += result.transitions; + ++edge_stats.safe_mask_distribution[result.safe_mask]; + + if (result.solvable) { + require(result.safe_mask != 0 && !result.path.empty(), + "local YES has no safe first source or path"); + require(solver.replay(result.path), + "local YES escape path did not replay"); + ++stats.local_yes; + ++edge_stats.local_yes; + ++stats.winning_paths_replayed; + if (!stats.first_yes) { + stats.first_yes = make_sample( + future_index, decoration, edge, fixture, result); + } + } else { + require(result.safe_mask == 0 && result.path.empty(), + "local NO unexpectedly has a winning first source"); + ++stats.local_no; + ++edge_stats.local_no; + const Sample sample = make_sample( + future_index, decoration, edge, fixture, result); + if (!stats.first_no) stats.first_no = sample; + if (local_no_ledger) { + write_local_no(*local_no_ledger, sample, edge, decoration); + } + } + + std::ostringstream row; + row << future_index << '\t' << decoration.ordinal << '\t' + << edge.ordinal << '\t' << cards_text(decoration.cards) << '\t' + << join_words(fixture.hidden_bottom_to_top, ',') << '\t' + << (result.solvable ? "YES" : "NO") << '\t' + << result.safe_mask << '\t' << result.path; + const std::string row_text = row.str(); + update_hash(stats.ledger_hash, row_text); + if (result_ledger) *result_ledger << row_text << '\n'; + + if (stats.residual_words_checked % 100000 == 0) { + std::cout << "progress fixed_futures=" + << stats.residual_words_checked << '/' + << stats.residual_words_expected + << " local_no=" << stats.local_no << '\n'; + } + return true; + }); + if (complete_decoration) { + require(decoration_checked == decoration.residual_words_expected, + "complete decoration did not enumerate its exact weight"); + } + if (stats.residual_words_checked >= effective_limit) stop = true; + } + + stats.elapsed_seconds = std::chrono::duration( + std::chrono::steady_clock::now() - started).count(); + stats.universe_complete = + stats.residual_words_checked == stats.residual_words_expected; + stats.self_checks_passed = true; + require(stats.local_yes + stats.local_no == stats.residual_words_checked, + "local YES/NO counts do not partition checked futures"); + require(stats.winning_paths_replayed == stats.local_yes, + "not every local YES path replayed"); + for (const EdgeStats& edge_stats : stats.per_edge) { + require(edge_stats.local_yes + edge_stats.local_no == + edge_stats.residual_words_checked, + "per-edge YES/NO counts do not partition checked futures"); + if (stats.universe_complete) { + require(edge_stats.residual_words_checked == + edge_stats.residual_words_expected, + "full run did not cover a selected edge"); + } + } + return stats; +} + +std::string status(const RunStats& stats) { + if (!stats.universe_complete) return "INCOMPLETE"; + if (stats.local_no != 0) return "LOCAL_NO_RESIDUALS_EXPORTED"; + return "THREE_SOURCE_D2_CHECKPOINT_FAMILY_ELIMINATED"; +} + +std::string bool_json(bool value) { + return value ? "true" : "false"; +} + +std::string hex_u64(std::uint64_t value) { + static constexpr char digits_table[] = "0123456789abcdef"; + std::string result(16, '0'); + for (int index = 15; index >= 0; --index) { + result[static_cast(index)] = digits_table[value & 15U]; + value >>= 4U; + } + return result; +} + +void write_sample_json(std::ostream& output, const std::optional& sample) { + if (!sample) { + output << "null"; + return; + } + output << "{\"future_index\":" << sample->future_index + << ",\"decoration_index\":" << sample->decoration_index + << ",\"bridge_edge\":" << sample->edge_ordinal + << ",\"local_status\":\"" + << (sample->solvable ? "YES" : "NO") + << "\",\"safe_source_mask\":" << sample->safe_mask + << ",\"escape_columns\":\"" << sample->path + << "\",\"hidden_words_bottom_to_top\":["; + for (std::size_t column = 0; column < kColors; ++column) { + if (column != 0) output << ','; + output << '"' << sample->hidden_words_bottom_to_top[column] << '"'; + } + output << "]}"; +} + +void write_report(const Options& options, const Bridge& bridge, + const RunStats& stats) { + require(!options.output_dir.empty(), "report output directory is empty"); + const std::string run_status = status(stats); + const bool eliminated = stats.universe_complete && stats.local_no == 0; + std::ofstream json(options.output_dir / "report.json", std::ios::binary); + require(static_cast(json), "could not create report.json"); + json << "{\n" + << " \"schema_version\": 1,\n" + << " \"experiment\": \"c4_h7_d2_three_source_checkpoint\",\n" + << " \"status\": \"" << run_status << "\",\n" + << " \"parameters\": {\"colors\":4,\"height\":7,\"empty\":2},\n" + << " \"scope\": {\n" + << " \"parent_checkpoint_only\": true,\n" + << " \"fixed_hidden_futures\": true,\n" + << " \"zero_debt_past_restored\": false,\n" + << " \"full_h7_theorem\": false\n" + << " },\n" + << " \"bridge_reconstruction\": {\"tq_terminals\":" + << bridge.terminal_count << ",\"labeled_candidates\":" + << bridge.labeled_candidates << ",\"canonical_parents\":" + << bridge.canonical_parent_count << ",\"canonical_edges\":" + << bridge.canonical_edge_count << ",\"sibling_edges\":" + << bridge.sibling_edge_count << "},\n" + << " \"universe\": {\"selected_edges\":" << stats.per_edge.size() + << ",\"decorations\":" << stats.decorations_expected + << ",\"labeled_fixed_futures\":" << stats.residual_words_expected + << "},\n" + << " \"run\": {\"limit_requested\":" << stats.limit_requested + << ",\"universe_complete\":" << bool_json(stats.universe_complete) + << ",\"fixed_futures_checked\":" << stats.residual_words_checked + << ",\"local_yes\":" << stats.local_yes + << ",\"local_no\":" << stats.local_no + << ",\"winning_paths_replayed\":" << stats.winning_paths_replayed + << ",\"states\":" << stats.states + << ",\"transitions\":" << stats.transitions + << ",\"elapsed_seconds\":" << stats.elapsed_seconds << "},\n" + << " \"claims\": {\"three_source_checkpoint_family_eliminated\":" + << bool_json(eliminated) + << ",\"zero_debt_initial_family_eliminated\":false," + "\"universal_c4_h7_solvability\":false},\n" + << " \"ledgers\": {\"fixed_future_results\":" + "\"fixed-future-results.tsv\",\"local_no\":" + "\"local-no-ledger.jsonl\",\"result_rows_fnv1a64\":\"" + << hex_u64(stats.ledger_hash) << "\"},\n" + << " \"first_local_yes\": "; + write_sample_json(json, stats.first_yes); + json << ",\n \"first_local_no\": "; + write_sample_json(json, stats.first_no); + json << ",\n \"per_edge\": [\n"; + for (std::size_t index = 0; index < stats.per_edge.size(); ++index) { + const EdgeStats& row = stats.per_edge[index]; + if (index != 0) json << ",\n"; + json << " {\"bridge_edge\":" << row.edge_ordinal + << ",\"decorations\":" << row.decorations + << ",\"fixed_futures_expected\":" << row.residual_words_expected + << ",\"fixed_futures_checked\":" << row.residual_words_checked + << ",\"local_yes\":" << row.local_yes + << ",\"local_no\":" << row.local_no + << ",\"states\":" << row.states + << ",\"transitions\":" << row.transitions + << ",\"safe_mask_distribution\":{"; + bool first = true; + for (const auto& mask : row.safe_mask_distribution) { + if (!first) json << ','; + first = false; + json << '"' << mask.first << "\":" << mask.second; + } + json << "}}"; + } + json << "\n ],\n \"self_checks_passed\": " + << bool_json(stats.self_checks_passed) << "\n}\n"; + require(static_cast(json), "failed while writing report.json"); + + std::ofstream markdown(options.output_dir / "report.md", std::ios::binary); + require(static_cast(markdown), "could not create report.md"); + markdown << "# c=4, h=7 three-source D2 checkpoint audit\n\n" + << "- Status: `" << run_status << "`.\n" + << "- Exact target universe: 12 bridge edges, 1,535 decorations, " + "1,106,490 labeled fixed futures.\n" + << "- Checked fixed futures: " << stats.residual_words_checked + << ".\n" + << "- Parent-checkpoint local YES / NO: " << stats.local_yes + << " / " << stats.local_no << ".\n" + << "- Replayed winning paths: " << stats.winning_paths_replayed + << ".\n\n" + << "This audit starts at the nonzero-debt first-exhaustion parent. " + "It does not restore any zero-debt past, eliminate an initial-layout " + "family, or prove the full c=4,h=7 theorem.\n\n" + << "| Bridge edge | Decorations | Expected futures | Checked | " + "Local YES | Local NO |\n" + << "|---:|---:|---:|---:|---:|---:|\n"; + for (const EdgeStats& row : stats.per_edge) { + markdown << '|' << row.edge_ordinal << '|' << row.decorations << '|' + << row.residual_words_expected << '|' + << row.residual_words_checked << '|' << row.local_yes << '|' + << row.local_no << "|\n"; + } + require(static_cast(markdown), "failed while writing report.md"); +} + +} // namespace + +int main(int argc, char** argv) { + try { + const Options options = parse_options(argc, argv); + if (options.self_test) run_solver_self_tests(); + const Bridge bridge = build_bridge(); + const auto decorations = enumerate_decorations(bridge); + const RunStats stats = run(options, bridge, decorations); + if (!options.output_dir.empty()) write_report(options, bridge, stats); + std::cout << "status=" << status(stats) + << " edges=" << stats.per_edge.size() + << " decorations=" << stats.decorations_expected + << " fixed_futures=" << stats.residual_words_checked << '/' + << stats.residual_words_expected + << " local_yes=" << stats.local_yes + << " local_no=" << stats.local_no + << " elapsed_seconds=" << stats.elapsed_seconds << '\n'; + return 0; + } catch (const std::exception& error) { + std::cerr << "error: " << error.what() << '\n'; + return 2; + } +} diff --git a/apps/c4_h7_d2_three_source_past.cpp b/apps/c4_h7_d2_three_source_past.cpp new file mode 100644 index 0000000..0aaef4b --- /dev/null +++ b/apps/c4_h7_d2_three_source_past.cpp @@ -0,0 +1,1382 @@ +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include + +namespace { + +constexpr int kHeight = 7; +constexpr int kColors = 4; +constexpr int kEmpty = 2; +constexpr std::uint64_t kCheckpointFutures = 1'106'490; +constexpr std::uint64_t kCheckpointLocalNo = 14'784; +constexpr std::uint64_t kBalancedRestorations = 285'600; +constexpr std::uint64_t kReachableRestorations = 281'904; +constexpr std::uint64_t kFNVOffset = 1'469'598'103'934'665'603ULL; +constexpr std::uint64_t kFNVPrime = 1'099'511'628'211ULL; + +using Debts = std::array; +using Words = std::array; + +struct Options { + std::filesystem::path checkpoint_report; + std::filesystem::path output_dir; + std::uint64_t limit_restorations = 0; + bool self_test = false; +}; + +struct ParentSpec { + int edge = 0; + Debts debts{}; + std::array bad{}; // old colour, old cap, final colour + int q_color = 0; + std::array q_caps{}; + std::uint64_t local_no_rows = 0; + std::uint64_t prefix_candidates = 0; + std::uint64_t prefix_reachable = 0; + std::uint64_t legal_histories = 0; + + std::array caps() const { + return {{bad[1], q_caps[0], q_caps[1], q_caps[2]}}; + } +}; + +struct PastEvent { + int old_color = 0; + int old_cap = 0; + int next_color = 0; +}; + +struct PrefixTemplate { + std::size_t ordinal = 0; + Words words_top_to_bottom; + bool reachable = false; + std::uint64_t legal_histories = 0; + std::string first_witness; +}; + +struct LedgerRow { + std::uint64_t future_index = 0; + std::uint64_t decoration_index = 0; + std::size_t spec_index = 0; + Words hidden_bottom_to_top; +}; + +struct SolverResult { + bool solvable = false; + std::uint32_t safe_mask = 0; + std::string path; + std::uint64_t states = 0; + std::uint64_t transitions = 0; +}; + +struct CanonicalLayout { + Words columns_top_to_bottom; + std::array canonical_to_original{}; + std::string key; +}; + +struct Sample { + bool present = false; + std::uint64_t restoration_index = 0; + std::uint64_t future_index = 0; + int edge = 0; + std::size_t prefix_index = 0; + bool reachable = false; + bool solvable = false; + Words columns_top_to_bottom; + Words columns_bottom_to_top; + std::uint32_t safe_mask = 0; + std::string path; +}; + +struct EdgeStats { + int edge = 0; + std::uint64_t local_no_rows = 0; + std::uint64_t prefix_candidates = 0; + std::uint64_t prefix_reachable = 0; + std::uint64_t legal_histories = 0; + std::uint64_t balanced_expected = 0; + std::uint64_t reachable_expected = 0; + std::uint64_t checked = 0; + std::uint64_t reachable_checked = 0; + std::uint64_t initial_yes = 0; + std::uint64_t initial_no = 0; +}; + +struct RunStats { + std::uint64_t limit_requested = 0; + bool universe_complete = false; + std::uint64_t restorations_checked = 0; + std::uint64_t reachable_checked = 0; + std::uint64_t unreachable_checked = 0; + std::uint64_t initial_yes = 0; + std::uint64_t initial_no = 0; + std::uint64_t witnesses_replayed = 0; + std::uint64_t canonical_classes_solved = 0; + std::uint64_t symmetry_cache_hits = 0; + std::uint64_t states = 0; + std::uint64_t transitions = 0; + std::uint64_t result_hash = kFNVOffset; + double elapsed_seconds = 0.0; + bool self_checks_passed = false; + std::vector per_edge; + std::optional first_yes; + std::optional first_no; +}; + +void require(bool condition, const std::string& message) { + if (!condition) throw std::runtime_error("self-check failed: " + message); +} + +std::vector expected_specs() { + return { + {116, {{-4, 0, 1, 3}}, {{0, 4, 1}}, 0, {{1, 1, 5}}, + 210, 140, 140, 1184}, + {117, {{-4, 0, 2, 2}}, {{0, 4, 1}}, 0, {{1, 1, 5}}, + 252, 210, 210, 2076}, + {184, {{-3, 0, 1, 2}}, {{0, 2, 1}}, 0, {{2, 2, 4}}, + 462, 60, 60, 348}, + {236, {{-2, 0, 1, 1}}, {{0, 2, 1}}, 0, {{1, 1, 3}}, + 924, 6, 6, 12}, + {242, {{-2, 0, 1, 1}}, {{0, 2, 1}}, 0, {{1, 2, 3}}, + 11088, 12, 12, 26}, + {244, {{-2, 0, 1, 1}}, {{0, 2, 1}}, 0, {{1, 2, 4}}, + 924, 20, 16, 30}, + {248, {{-2, 0, 1, 1}}, {{0, 2, 1}}, 0, {{2, 2, 3}}, + 924, 20, 20, 44}, + }; +} + +void usage() { + std::cerr + << "Usage: water-c4-h7-d2-three-source-past " + "--checkpoint-report PATH --output-dir DIR " + "[--limit-restorations N] [--self-test]\n"; +} + +Options parse_options(int argc, char** argv) { + Options options; + for (int index = 1; index < argc; ++index) { + const std::string argument = argv[index]; + if (argument == "--checkpoint-report" && index + 1 < argc) { + options.checkpoint_report = argv[++index]; + } else if (argument == "--output-dir" && index + 1 < argc) { + options.output_dir = argv[++index]; + } else if (argument == "--limit-restorations" && index + 1 < argc) { + options.limit_restorations = std::stoull(argv[++index]); + } else if (argument == "--self-test") { + options.self_test = true; + } else if (argument == "--help") { + usage(); + std::exit(0); + } else { + usage(); + throw std::runtime_error("unknown or incomplete argument: " + argument); + } + } + return options; +} + +std::string read_text(const std::filesystem::path& path) { + std::ifstream input(path, std::ios::binary); + if (!input) throw std::runtime_error("cannot open " + path.string()); + std::ostringstream buffer; + buffer << input.rdbuf(); + return buffer.str(); +} + +std::size_t key_position(const std::string& text, const std::string& key) { + const std::string needle = "\"" + key + "\""; + const std::size_t found = text.find(needle); + if (found == std::string::npos) { + throw std::runtime_error("JSON key is missing: " + key); + } + const std::size_t colon = text.find(':', found + needle.size()); + if (colon == std::string::npos) { + throw std::runtime_error("JSON key has no value: " + key); + } + std::size_t value = colon + 1; + while (value < text.size() && + std::isspace(static_cast(text[value])) != 0) { + ++value; + } + return value; +} + +std::string json_object(const std::string& text, const std::string& key) { + const std::size_t start = key_position(text, key); + require(start < text.size() && text[start] == '{', key + " is not an object"); + int depth = 0; + bool quoted = false; + bool escaped = false; + for (std::size_t cursor = start; cursor < text.size(); ++cursor) { + const char value = text[cursor]; + if (quoted) { + if (escaped) escaped = false; + else if (value == '\\') escaped = true; + else if (value == '"') quoted = false; + continue; + } + if (value == '"') quoted = true; + else if (value == '{') ++depth; + else if (value == '}' && --depth == 0) { + return text.substr(start, cursor - start + 1); + } + } + throw std::runtime_error("unterminated JSON object: " + key); +} + +std::int64_t json_integer(const std::string& text, const std::string& key) { + std::size_t cursor = key_position(text, key); + const std::size_t begin = cursor; + if (cursor < text.size() && text[cursor] == '-') ++cursor; + while (cursor < text.size() && + std::isdigit(static_cast(text[cursor])) != 0) { + ++cursor; + } + require(cursor > begin && !(cursor == begin + 1 && text[begin] == '-'), + key + " is not an integer"); + return std::stoll(text.substr(begin, cursor - begin)); +} + +bool json_boolean(const std::string& text, const std::string& key) { + const std::size_t cursor = key_position(text, key); + if (text.compare(cursor, 4, "true") == 0) return true; + if (text.compare(cursor, 5, "false") == 0) return false; + throw std::runtime_error(key + " is not a Boolean"); +} + +std::string json_string(const std::string& text, const std::string& key) { + std::size_t cursor = key_position(text, key); + require(cursor < text.size() && text[cursor] == '"', key + " is not a string"); + ++cursor; + std::string result; + bool escaped = false; + for (; cursor < text.size(); ++cursor) { + const char value = text[cursor]; + if (escaped) { + result.push_back(value); + escaped = false; + } else if (value == '\\') { + escaped = true; + } else if (value == '"') { + return result; + } else { + result.push_back(value); + } + } + throw std::runtime_error("unterminated JSON string: " + key); +} + +std::vector json_integer_array(const std::string& text, + const std::string& key) { + std::size_t cursor = key_position(text, key); + require(cursor < text.size() && text[cursor] == '[', key + " is not an array"); + ++cursor; + std::vector result; + while (cursor < text.size()) { + while (cursor < text.size() && + (std::isspace(static_cast(text[cursor])) != 0 || + text[cursor] == ',')) { + ++cursor; + } + if (cursor < text.size() && text[cursor] == ']') return result; + const std::size_t begin = cursor; + if (cursor < text.size() && text[cursor] == '-') ++cursor; + while (cursor < text.size() && + std::isdigit(static_cast(text[cursor])) != 0) { + ++cursor; + } + require(cursor > begin, key + " contains a non-integer"); + result.push_back(std::stoi(text.substr(begin, cursor - begin))); + } + throw std::runtime_error("unterminated integer array: " + key); +} + +std::vector json_string_array(const std::string& text, + const std::string& key) { + std::size_t cursor = key_position(text, key); + require(cursor < text.size() && text[cursor] == '[', key + " is not an array"); + ++cursor; + std::vector result; + while (cursor < text.size()) { + while (cursor < text.size() && + (std::isspace(static_cast(text[cursor])) != 0 || + text[cursor] == ',')) { + ++cursor; + } + if (cursor < text.size() && text[cursor] == ']') return result; + require(cursor < text.size() && text[cursor] == '"', + key + " contains a non-string"); + ++cursor; + std::string value; + while (cursor < text.size() && text[cursor] != '"') { + require(text[cursor] != '\\', key + " uses an unsupported escape"); + value.push_back(text[cursor++]); + } + require(cursor < text.size(), "unterminated string in " + key); + ++cursor; + result.push_back(value); + } + throw std::runtime_error("unterminated string array: " + key); +} + +std::vector> prefix_events(const Words& words) { + std::vector> result(kColors); + for (int column = 0; column < kColors; ++column) { + const std::string& word = words[static_cast(column)]; + require(!word.empty(), "past prefix column is empty"); + int old_color = word.front() - '0'; + int old_cap = 1; + std::size_t cursor = 1; + while (cursor < word.size()) { + const int next_color = word[cursor] - '0'; + std::size_t end = cursor + 1; + while (end < word.size() && word[end] == word[cursor]) ++end; + const int next_cap = static_cast(end); + if (next_color != old_color) { + result[static_cast(column)].push_back( + {old_color, old_cap, next_color}); + } + old_color = next_color; + old_cap = next_cap; + cursor = end; + } + } + return result; +} + +struct PastResult { + std::uint64_t histories = 0; + std::string witness; + Debts final_debts{}; +}; + +PastResult past_reachability(const Words& words) { + const auto events = prefix_events(words); + std::array multipliers{}; + std::uint32_t states = 1; + for (int column = 0; column < kColors; ++column) { + multipliers[static_cast(column)] = states; + states *= static_cast( + events[static_cast(column)].size() + 1); + } + std::vector memo(states, -1); + std::vector first(states, -1); + const auto decode = [&](std::uint32_t state) { + std::array ranks{}; + for (int column = 0; column < kColors; ++column) { + const auto size = events[static_cast(column)].size() + 1; + ranks[static_cast(column)] = + (state / multipliers[static_cast(column)]) % size; + } + return ranks; + }; + const auto debts_at = [&](const std::array& ranks) { + Debts debts{}; + for (int column = 0; column < kColors; ++column) { + const auto& chain = events[static_cast(column)]; + for (std::size_t index = 0; + index < ranks[static_cast(column)]; ++index) { + const PastEvent& event = chain[index]; + debts[event.old_color] += event.old_cap; + debts[event.next_color] -= event.old_cap; + } + } + return debts; + }; + const auto visit = [&](const auto& self, std::uint32_t state) -> std::uint64_t { + const auto ranks = decode(state); + bool goal = true; + for (int column = 0; column < kColors; ++column) { + goal = goal && ranks[static_cast(column)] == + events[static_cast(column)].size(); + } + if (goal) return 1; + std::int64_t& known = memo[state]; + if (known >= 0) return static_cast(known); + const Debts debts = debts_at(ranks); + std::uint64_t count = 0; + for (int column = 0; column < kColors; ++column) { + const std::size_t rank = ranks[static_cast(column)]; + const auto& chain = events[static_cast(column)]; + if (rank == chain.size()) continue; + const PastEvent& event = chain[rank]; + Debts tested = debts; + tested[event.old_color] += event.old_cap; + const int positives = static_cast(std::count_if( + tested.begin(), tested.end(), [](int value) { return value > 0; })); + if (positives > kEmpty) continue; + const std::uint64_t child = self( + self, state + multipliers[static_cast(column)]); + if (child != 0 && first[state] < 0) first[state] = column; + count += child; + } + known = static_cast(count); + return count; + }; + + PastResult result; + result.histories = visit(visit, 0); + if (result.histories != 0) { + std::uint32_t state = 0; + while (true) { + const auto ranks = decode(state); + bool goal = true; + for (int column = 0; column < kColors; ++column) { + goal = goal && ranks[static_cast(column)] == + events[static_cast(column)].size(); + } + if (goal) { + result.final_debts = debts_at(ranks); + break; + } + require(first[state] >= 0, "reachable past has no witness successor"); + const int column = first[state]; + result.witness.push_back(static_cast('0' + column)); + state += multipliers[static_cast(column)]; + } + } else { + std::array final_ranks{}; + for (int column = 0; column < kColors; ++column) { + final_ranks[static_cast(column)] = + events[static_cast(column)].size(); + } + result.final_debts = debts_at(final_ranks); + } + return result; +} + +std::vector enumerate_prefixes(const ParentSpec& spec) { + const auto caps = spec.caps(); + Debts exposed = spec.debts; + for (const int cap : caps) exposed[spec.q_color] += cap; + Debts remaining = exposed; + remaining[spec.q_color] -= kColors; + require(std::all_of(remaining.begin(), remaining.end(), + [](int value) { return value >= 0; }), + "reserved final q items exceed exposed inventory"); + int free_positions = 0; + for (const int cap : caps) free_positions += cap - 1; + require(std::accumulate(remaining.begin(), remaining.end(), 0) == + free_positions, + "past residual inventory has the wrong size"); + + std::vector flat(static_cast(free_positions), 0); + std::vector templates; + const auto visit = [&](const auto& self, int position, Debts counts) -> void { + if (position == free_positions) { + PrefixTemplate item; + item.ordinal = templates.size(); + int cursor = 0; + for (int column = 0; column < kColors; ++column) { + std::string word; + for (int index = 0; index < caps[static_cast(column)] - 1; + ++index) { + word.push_back(static_cast('0' + + flat[static_cast(cursor++)])); + } + word.push_back(static_cast('0' + spec.q_color)); + item.words_top_to_bottom[static_cast(column)] = + std::move(word); + } + require(cursor == free_positions, "past prefix did not consume its pool"); + const PastResult past = past_reachability(item.words_top_to_bottom); + item.reachable = past.histories != 0; + item.legal_histories = past.histories; + item.first_witness = past.witness; + require(past.final_debts == spec.debts, + "past prefix final debts differ from its parent"); + templates.push_back(std::move(item)); + return; + } + for (int color = 0; color < kColors; ++color) { + if (counts[static_cast(color)] == 0) continue; + flat[static_cast(position)] = color; + --counts[static_cast(color)]; + self(self, position + 1, counts); + ++counts[static_cast(color)]; + } + }; + visit(visit, 0, remaining); + + const std::uint64_t reachable = static_cast(std::count_if( + templates.begin(), templates.end(), + [](const PrefixTemplate& item) { return item.reachable; })); + std::uint64_t histories = 0; + for (const PrefixTemplate& item : templates) histories += item.legal_histories; + require(templates.size() == spec.prefix_candidates, + "balanced prefix candidate census drifted on edge " + + std::to_string(spec.edge)); + require(reachable == spec.prefix_reachable, + "reachable prefix census drifted on edge " + + std::to_string(spec.edge)); + require(histories == spec.legal_histories, + "past-history census drifted on edge " + + std::to_string(spec.edge)); + return templates; +} + +class InitialSolver { +public: + explicit InitialSolver(const Words& columns) { + std::uint32_t size = 1; + for (int column = 0; column < kColors; ++column) { + build_events(column, columns[static_cast(column)]); + multipliers_[static_cast(column)] = size; + size *= static_cast( + events_[static_cast(column)].size() + 1); + } + memo_.assign(size, -1); + } + + SolverResult solve() { + SolverResult result; + result.solvable = visit(0); + for (int column = 0; column < kColors; ++column) { + if (safe_from(0, column)) result.safe_mask |= 1U << column; + } + if (result.solvable) { + std::uint32_t state = 0; + while (!goal(state)) { + bool advanced = false; + for (int column = 0; column < kColors; ++column) { + if (!safe_from(state, column)) continue; + result.path.push_back(static_cast('0' + column)); + state += multipliers_[static_cast(column)]; + advanced = true; + break; + } + require(advanced, "initial YES has no safe successor"); + } + } + result.states = states_; + result.transitions = transitions_; + return result; + } + + bool replay(const std::string& path) const { + std::uint32_t state = 0; + for (const char value : path) { + const int column = value - '0'; + if (column < 0 || column >= kColors || !legal(state, column)) { + return false; + } + state += multipliers_[static_cast(column)]; + } + return goal(state); + } + +private: + struct Event { + int old_color = 0; + int old_cap = 0; + int next_color = 0; + int next_cap = 0; + }; + + std::array, kColors> events_; + std::array, kColors> deltas_; + std::array multipliers_{}; + std::vector memo_; + std::uint64_t states_ = 0; + std::uint64_t transitions_ = 0; + + void build_events(int column, const std::string& word) { + require(word.size() == kHeight, "initial column does not have height seven"); + require(std::all_of(word.begin(), word.end(), [](char value) { + return value >= '0' && value < '0' + kColors; + }), + "initial column has an invalid colour"); + int old_color = word.front() - '0'; + std::size_t cursor = 1; + while (cursor < word.size() && word[cursor] == word.front()) ++cursor; + int old_cap = static_cast(cursor); + while (cursor < word.size()) { + const int next_color = word[cursor] - '0'; + std::size_t end = cursor + 1; + while (end < word.size() && word[end] == word[cursor]) ++end; + const int next_cap = static_cast(end); + events_[static_cast(column)].push_back( + {old_color, old_cap, next_color, next_cap}); + old_color = next_color; + old_cap = next_cap; + cursor = end; + } + auto& deltas = deltas_[static_cast(column)]; + const auto& events = events_[static_cast(column)]; + deltas.assign(events.size() + 1, Debts{}); + for (std::size_t index = 0; index < events.size(); ++index) { + deltas[index + 1] = deltas[index]; + const Event& event = events[index]; + deltas[index + 1][event.old_color] += event.old_cap; + if (event.next_cap == kHeight) { + deltas[index + 1][event.next_color] += + kHeight - event.old_cap; + } else { + deltas[index + 1][event.next_color] -= event.old_cap; + } + } + } + + std::array decode(std::uint32_t state) const { + std::array ranks{}; + for (int column = 0; column < kColors; ++column) { + ranks[static_cast(column)] = + (state / multipliers_[static_cast(column)]) % + (events_[static_cast(column)].size() + 1); + } + return ranks; + } + + int exhausted(const std::array& ranks) const { + int count = 0; + for (int column = 0; column < kColors; ++column) { + count += ranks[static_cast(column)] == + events_[static_cast(column)].size(); + } + return count; + } + + bool goal(std::uint32_t state) const { + return exhausted(decode(state)) >= kEmpty; + } + + bool legal(std::uint32_t state, int column) const { + const auto ranks = decode(state); + const std::size_t rank = ranks[static_cast(column)]; + const auto& events = events_[static_cast(column)]; + if (rank == events.size()) return false; + Debts debts{}; + for (int other = 0; other < kColors; ++other) { + const Debts& delta = deltas_[static_cast(other)] + [ranks[static_cast(other)]]; + for (int color = 0; color < kColors; ++color) { + debts[static_cast(color)] += + delta[static_cast(color)]; + } + } + const Event& event = events[rank]; + debts[event.old_color] += event.old_cap; + const int positives = static_cast(std::count_if( + debts.begin(), debts.end(), [](int value) { return value > 0; })); + return positives <= kEmpty + exhausted(ranks); + } + + bool safe_from(std::uint32_t state, int column) { + if (goal(state) || !legal(state, column)) return false; + ++transitions_; + return visit(state + multipliers_[static_cast(column)]); + } + + bool visit(std::uint32_t state) { + if (goal(state)) return true; + std::int8_t& known = memo_[state]; + if (known >= 0) return known != 0; + ++states_; + for (int column = 0; column < kColors; ++column) { + if (safe_from(state, column)) { + known = 1; + return true; + } + } + known = 0; + return false; + } +}; + +CanonicalLayout canonicalize(const Words& original) { + CanonicalLayout best; + bool present = false; + std::array colors{{0, 1, 2, 3}}; + do { + std::vector> columns; + for (int column = 0; column < kColors; ++column) { + std::string recolored; + for (const char value : original[static_cast(column)]) { + recolored.push_back(static_cast( + '0' + colors[static_cast(value - '0')])); + } + columns.emplace_back(std::move(recolored), column); + } + std::sort(columns.begin(), columns.end()); + std::string key; + for (const auto& item : columns) key += item.first; + if (!present || key < best.key) { + present = true; + best.key = key; + for (int index = 0; index < kColors; ++index) { + best.columns_top_to_bottom[static_cast(index)] = + columns[static_cast(index)].first; + best.canonical_to_original[static_cast(index)] = + columns[static_cast(index)].second; + } + } + } while (std::next_permutation(colors.begin(), colors.end())); + require(present && best.key.size() == kColors * kHeight, + "layout canonicalization failed"); + return best; +} + +std::uint32_t map_mask(std::uint32_t canonical_mask, + const std::array& mapping) { + std::uint32_t result = 0; + for (int column = 0; column < kColors; ++column) { + if ((canonical_mask & (1U << column)) != 0) { + result |= 1U << mapping[static_cast(column)]; + } + } + return result; +} + +std::string map_path(const std::string& canonical_path, + const std::array& mapping) { + std::string result; + for (const char value : canonical_path) { + const int column = value - '0'; + require(column >= 0 && column < kColors, + "canonical path contains an invalid source"); + result.push_back(static_cast( + '0' + mapping[static_cast(column)])); + } + return result; +} + +std::string reversed(std::string value) { + std::reverse(value.begin(), value.end()); + return value; +} + +void update_hash(std::uint64_t& hash, const std::string& row) { + for (const unsigned char value : row + "\n") { + hash ^= value; + hash *= kFNVPrime; + } +} + +std::string hex_u64(std::uint64_t value) { + static constexpr char digits[] = "0123456789abcdef"; + std::string result(16, '0'); + for (int index = 15; index >= 0; --index) { + result[static_cast(index)] = digits[value & 15U]; + value >>= 4U; + } + return result; +} + +std::size_t find_spec(const std::vector& specs, int edge) { + const auto found = std::find_if( + specs.begin(), specs.end(), + [edge](const ParentSpec& spec) { return spec.edge == edge; }); + require(found != specs.end(), "local-NO ledger contains unexpected edge " + + std::to_string(edge)); + return static_cast(std::distance(specs.begin(), found)); +} + +std::filesystem::path validate_checkpoint_report( + const std::filesystem::path& report_path) { + const std::string report = read_text(report_path); + require(json_integer(report, "schema_version") == 1, + "checkpoint report schema drifted"); + require(json_string(report, "experiment") == + "c4_h7_d2_three_source_checkpoint", + "checkpoint experiment drifted"); + require(json_string(report, "status") == "LOCAL_NO_RESIDUALS_EXPORTED", + "checkpoint report is not the complete local-NO artifact"); + const std::string run = json_object(report, "run"); + require(json_boolean(run, "universe_complete"), + "checkpoint universe is incomplete"); + require(json_integer(run, "fixed_futures_checked") == + static_cast(kCheckpointFutures), + "checkpoint fixed-future count drifted"); + require(json_integer(run, "local_no") == + static_cast(kCheckpointLocalNo), + "checkpoint local-NO count drifted"); + const std::string scope = json_object(report, "scope"); + require(json_boolean(scope, "parent_checkpoint_only"), + "checkpoint scope lost its parent boundary"); + require(!json_boolean(scope, "zero_debt_past_restored"), + "input unexpectedly claims a restored past"); + require(!json_boolean(scope, "full_h7_theorem"), + "input unexpectedly claims the full h7 theorem"); + const std::string claims = json_object(report, "claims"); + require(!json_boolean(claims, "zero_debt_initial_family_eliminated") && + !json_boolean(claims, "universal_c4_h7_solvability"), + "checkpoint artifact overclaims its conclusion"); + require(json_boolean(report, "self_checks_passed"), + "checkpoint self-checks did not pass"); + const std::string ledgers = json_object(report, "ledgers"); + const std::string filename = json_string(ledgers, "local_no"); + require(filename == "local-no-ledger.jsonl", + "checkpoint local-NO ledger name drifted"); + return report_path.parent_path() / filename; +} + +std::vector load_ledger(const std::filesystem::path& path, + const std::vector& specs) { + std::ifstream input(path); + if (!input) throw std::runtime_error("cannot open " + path.string()); + std::vector rows; + std::vector counts(specs.size(), 0); + std::string line; + std::uint64_t previous_future = 0; + bool first = true; + while (std::getline(input, line)) { + if (line.empty()) continue; + require(json_string(line, "local_status") == "NO" && + json_integer(line, "safe_source_mask") == 0, + "local-NO ledger row is not local NO"); + LedgerRow row; + row.future_index = static_cast( + json_integer(line, "future_index")); + row.decoration_index = static_cast( + json_integer(line, "decoration_index")); + const int edge = static_cast(json_integer(line, "bridge_edge")); + row.spec_index = find_spec(specs, edge); + const ParentSpec& spec = specs[row.spec_index]; + if (!first) require(row.future_index > previous_future, + "local-NO future indices are not increasing"); + first = false; + previous_future = row.future_index; + + const auto debts = json_integer_array(line, "parent_debts"); + const auto bad = json_integer_array(line, "bad_source"); + const auto q_caps = json_integer_array(line, "q_caps"); + require(debts.size() == kColors && + std::equal(debts.begin(), debts.end(), spec.debts.begin()), + "parent debts drifted on edge " + std::to_string(edge)); + require(bad.size() == 3 && + std::equal(bad.begin(), bad.end(), spec.bad.begin()), + "bad source drifted on edge " + std::to_string(edge)); + require(json_integer(line, "q_color") == spec.q_color, + "q colour drifted on edge " + std::to_string(edge)); + require(q_caps.size() == 3 && + std::equal(q_caps.begin(), q_caps.end(), spec.q_caps.begin()), + "q caps drifted on edge " + std::to_string(edge)); + const auto words = json_string_array(line, "hidden_words_bottom_to_top"); + require(words.size() == kColors, + "local-NO fixture does not have four hidden words"); + for (int column = 0; column < kColors; ++column) { + row.hidden_bottom_to_top[static_cast(column)] = + words[static_cast(column)]; + } + + const auto caps = spec.caps(); + Debts hidden_counts{}; + for (int column = 0; column < kColors; ++column) { + const std::string& word = + row.hidden_bottom_to_top[static_cast(column)]; + require(word.size() == static_cast( + kHeight - caps[static_cast(column)]), + "hidden word length drifted on edge " + + std::to_string(edge)); + require(!word.empty() && word.back() != '0' + spec.q_color, + "hidden word merges into the parent q boundary"); + for (const char value : word) { + require(value >= '0' && value < '0' + kColors, + "hidden word has an invalid colour"); + ++hidden_counts[static_cast(value - '0')]; + } + } + require(std::all_of(row.hidden_bottom_to_top[0].begin(), + row.hidden_bottom_to_top[0].end(), + [&spec](char value) { + return value == '0' + spec.bad[2]; + }), + "bad hidden suffix is not its forced final run"); + Debts exposed = spec.debts; + for (const int cap : caps) exposed[spec.q_color] += cap; + for (int color = 0; color < kColors; ++color) { + require(hidden_counts[static_cast(color)] == + kHeight - exposed[static_cast(color)], + "hidden inventory does not complement the parent"); + } + ++counts[row.spec_index]; + rows.push_back(std::move(row)); + } + require(rows.size() == kCheckpointLocalNo, + "local-NO ledger does not contain 14784 rows"); + for (std::size_t index = 0; index < specs.size(); ++index) { + require(counts[index] == specs[index].local_no_rows, + "per-edge local-NO ledger count drifted on edge " + + std::to_string(specs[index].edge)); + } + return rows; +} + +Words restore_layout(const ParentSpec& spec, const LedgerRow& row, + const PrefixTemplate& prefix) { + Words result; + Debts counts{}; + const auto caps = spec.caps(); + for (int column = 0; column < kColors; ++column) { + const std::string hidden_top = reversed( + row.hidden_bottom_to_top[static_cast(column)]); + const std::string& past = + prefix.words_top_to_bottom[static_cast(column)]; + require(past.size() == + static_cast(caps[static_cast(column)]), + "past prefix length drifted"); + require(!hidden_top.empty() && past.back() != hidden_top.front(), + "restored checkpoint boundary merged"); + result[static_cast(column)] = past + hidden_top; + require(result[static_cast(column)].size() == kHeight, + "restored column does not have height seven"); + for (const char value : result[static_cast(column)]) { + ++counts[static_cast(value - '0')]; + } + } + require(std::all_of(counts.begin(), counts.end(), + [](int value) { return value == kHeight; }), + "restored initial layout is not colour-balanced"); + return result; +} + +Sample make_sample(std::uint64_t restoration_index, const LedgerRow& row, + const ParentSpec& spec, const PrefixTemplate& prefix, + const Words& columns, bool solvable, std::uint32_t mask, + const std::string& path) { + Sample sample; + sample.present = true; + sample.restoration_index = restoration_index; + sample.future_index = row.future_index; + sample.edge = spec.edge; + sample.prefix_index = prefix.ordinal; + sample.reachable = prefix.reachable; + sample.solvable = solvable; + sample.columns_top_to_bottom = columns; + for (int column = 0; column < kColors; ++column) { + sample.columns_bottom_to_top[static_cast(column)] = + reversed(columns[static_cast(column)]); + } + sample.safe_mask = mask; + sample.path = path; + return sample; +} + +void write_words_json(std::ostream& output, const Words& words) { + output << '['; + for (int column = 0; column < kColors; ++column) { + if (column != 0) output << ','; + output << '"' << words[static_cast(column)] << '"'; + } + output << ']'; +} + +void write_sample_json(std::ostream& output, + const std::optional& optional) { + if (!optional) { + output << "null"; + return; + } + const Sample& sample = *optional; + output << "{\"restoration_index\":" << sample.restoration_index + << ",\"future_index\":" << sample.future_index + << ",\"bridge_edge\":" << sample.edge + << ",\"prefix_index\":" << sample.prefix_index + << ",\"parent_reachable\":" + << (sample.reachable ? "true" : "false") + << ",\"initial_status\":\"" + << (sample.solvable ? "YES" : "NO") + << "\",\"columns_top_to_bottom\":"; + write_words_json(output, sample.columns_top_to_bottom); + output << ",\"columns_bottom_to_top\":"; + write_words_json(output, sample.columns_bottom_to_top); + output << ",\"safe_source_mask\":" << sample.safe_mask + << ",\"escape_columns\":\"" << sample.path << "\"}"; +} + +RunStats run(const Options& options, const std::vector& specs, + const std::vector>& prefixes, + const std::vector& rows) { + std::filesystem::create_directories(options.output_dir); + std::ofstream result_ledger(options.output_dir / "initial-results.tsv", + std::ios::binary); + std::ofstream no_ledger(options.output_dir / "initial-no-candidates.jsonl", + std::ios::binary); + require(result_ledger && no_ledger, "cannot open restoration output ledgers"); + result_ledger + << "restoration_index\tfuture_index\tbridge_edge\tprefix_index" + "\tparent_reachable\tcolumns_top_to_bottom\tinitial_status" + "\tsafe_source_mask\tescape_columns\n"; + + RunStats stats; + stats.limit_requested = options.limit_restorations; + stats.per_edge.reserve(specs.size()); + for (const ParentSpec& spec : specs) { + EdgeStats edge; + edge.edge = spec.edge; + edge.local_no_rows = spec.local_no_rows; + edge.prefix_candidates = spec.prefix_candidates; + edge.prefix_reachable = spec.prefix_reachable; + edge.legal_histories = spec.legal_histories; + edge.balanced_expected = spec.local_no_rows * spec.prefix_candidates; + edge.reachable_expected = spec.local_no_rows * spec.prefix_reachable; + stats.per_edge.push_back(edge); + } + const std::uint64_t expected_balanced = std::accumulate( + stats.per_edge.begin(), stats.per_edge.end(), std::uint64_t{0}, + [](std::uint64_t sum, const EdgeStats& edge) { + return sum + edge.balanced_expected; + }); + const std::uint64_t expected_reachable = std::accumulate( + stats.per_edge.begin(), stats.per_edge.end(), std::uint64_t{0}, + [](std::uint64_t sum, const EdgeStats& edge) { + return sum + edge.reachable_expected; + }); + require(expected_balanced == kBalancedRestorations, + "balanced restoration universe is not 285600"); + require(expected_reachable == kReachableRestorations, + "reachable restoration universe is not 281904"); + const std::uint64_t effective_limit = options.limit_restorations == 0 + ? expected_balanced + : std::min(options.limit_restorations, expected_balanced); + + std::unordered_map cache; + const auto started = std::chrono::steady_clock::now(); + bool stop = false; + for (const LedgerRow& row : rows) { + if (stop) break; + const ParentSpec& spec = specs[row.spec_index]; + EdgeStats& edge = stats.per_edge[row.spec_index]; + for (const PrefixTemplate& prefix : prefixes[row.spec_index]) { + if (stats.restorations_checked >= effective_limit) { + stop = true; + break; + } + const std::uint64_t restoration_index = stats.restorations_checked; + const Words columns = restore_layout(spec, row, prefix); + const CanonicalLayout canonical = canonicalize(columns); + SolverResult canonical_result; + const auto found = cache.find(canonical.key); + if (found == cache.end()) { + InitialSolver solver(canonical.columns_top_to_bottom); + canonical_result = solver.solve(); + require(!canonical_result.solvable || + solver.replay(canonical_result.path), + "canonical initial YES path did not replay"); + cache.emplace(canonical.key, canonical_result); + ++stats.canonical_classes_solved; + stats.states += canonical_result.states; + stats.transitions += canonical_result.transitions; + } else { + canonical_result = found->second; + ++stats.symmetry_cache_hits; + } + const std::uint32_t mask = map_mask( + canonical_result.safe_mask, canonical.canonical_to_original); + const std::string path = map_path( + canonical_result.path, canonical.canonical_to_original); + if (canonical_result.solvable) { + InitialSolver replay_solver(columns); + require(replay_solver.replay(path), + "symmetry-translated initial YES path did not replay"); + ++stats.initial_yes; + ++stats.witnesses_replayed; + ++edge.initial_yes; + if (!stats.first_yes) { + stats.first_yes = make_sample( + restoration_index, row, spec, prefix, columns, true, + mask, path); + } + } else { + require(mask == 0 && path.empty(), + "initial NO has a winning witness"); + ++stats.initial_no; + ++edge.initial_no; + const Sample sample = make_sample( + restoration_index, row, spec, prefix, columns, false, 0, + ""); + if (!stats.first_no) stats.first_no = sample; + no_ledger << "{\"scope\":\"complete_balanced_c4_h7_layout\","; + no_ledger << "\"independently_verified\":false,\"candidate\":"; + write_sample_json(no_ledger, sample); + no_ledger << "}\n"; + } + + ++stats.restorations_checked; + ++edge.checked; + if (prefix.reachable) { + ++stats.reachable_checked; + ++edge.reachable_checked; + } else { + ++stats.unreachable_checked; + } + std::ostringstream ledger_row; + ledger_row << restoration_index << '\t' << row.future_index << '\t' + << spec.edge << '\t' << prefix.ordinal << '\t' + << (prefix.reachable ? 1 : 0) << '\t'; + for (int column = 0; column < kColors; ++column) { + if (column != 0) ledger_row << ','; + ledger_row << columns[static_cast(column)]; + } + ledger_row << '\t' << (canonical_result.solvable ? "YES" : "NO") + << '\t' << mask << '\t' << path; + const std::string ledger_text = ledger_row.str(); + result_ledger << ledger_text << '\n'; + update_hash(stats.result_hash, ledger_text); + + if (stats.restorations_checked % 50'000 == 0) { + std::cout << "progress restorations=" << stats.restorations_checked + << '/' << effective_limit + << " initial_no=" << stats.initial_no + << " classes=" << stats.canonical_classes_solved << '\n'; + } + } + } + stats.elapsed_seconds = std::chrono::duration( + std::chrono::steady_clock::now() - started).count(); + stats.universe_complete = + stats.restorations_checked == kBalancedRestorations; + require(stats.restorations_checked == effective_limit, + "restoration run stopped before its requested limit"); + require(stats.initial_yes + stats.initial_no == stats.restorations_checked, + "initial YES/NO counts do not partition restorations"); + require(stats.witnesses_replayed == stats.initial_yes, + "an initial YES witness was not replayed"); + require(stats.reachable_checked + stats.unreachable_checked == + stats.restorations_checked, + "reachable flag does not partition restorations"); + if (stats.universe_complete) { + require(stats.reachable_checked == kReachableRestorations && + stats.unreachable_checked == + kBalancedRestorations - kReachableRestorations, + "full run has the wrong reachable/unreachable split"); + for (const EdgeStats& edge : stats.per_edge) { + require(edge.checked == edge.balanced_expected && + edge.reachable_checked == edge.reachable_expected, + "full per-edge restoration coverage drifted"); + } + } + stats.self_checks_passed = true; + return stats; +} + +std::string status(const RunStats& stats) { + if (stats.initial_no != 0) return "INITIAL_NO_CANDIDATES_EXPORTED"; + if (!stats.universe_complete) return "INCOMPLETE"; + return "THREE_SOURCE_PAST_FAMILY_ELIMINATED"; +} + +void write_report(const Options& options, const std::vector& specs, + const RunStats& stats) { + std::ofstream json(options.output_dir / "report.json"); + require(static_cast(json), "cannot write report.json"); + const bool eliminated = stats.universe_complete && stats.initial_no == 0; + json << "{\n" + << " \"schema_version\": 1,\n" + << " \"experiment\": \"c4_h7_d2_three_source_past_restoration\",\n" + << " \"status\": \"" << status(stats) << "\",\n" + << " \"parameters\": {\"colors\":4,\"height\":7,\"empty\":2},\n" + << " \"input\": {\"checkpoint_report\":\"" + << options.checkpoint_report.filename().string() + << "\",\"checkpoint_status\":\"LOCAL_NO_RESIDUALS_EXPORTED\"," + "\"fixed_futures\":1106490,\"checkpoint_local_no\":14784},\n" + << " \"scope\": {\"balanced_completion_superset_only\":true," + "\"checkpoint_reachable_subset_tracked\":true," + "\"full_h7_theorem\":false},\n" + << " \"universe\": {\"parent_families\":7," + "\"checkpoint_local_no_rows\":14784," + "\"balanced_restorations\":285600," + "\"reachable_restorations\":281904," + "\"unreachable_balanced_completions\":3696},\n" + << " \"run\": {\"limit_requested\":" << stats.limit_requested + << ",\"universe_complete\":" + << (stats.universe_complete ? "true" : "false") + << ",\"restorations_checked\":" << stats.restorations_checked + << ",\"reachable_checked\":" << stats.reachable_checked + << ",\"unreachable_checked\":" << stats.unreachable_checked + << ",\"initial_yes\":" << stats.initial_yes + << ",\"initial_no\":" << stats.initial_no + << ",\"winning_paths_replayed\":" << stats.witnesses_replayed + << ",\"canonical_classes_solved\":" + << stats.canonical_classes_solved + << ",\"symmetry_cache_hits\":" << stats.symmetry_cache_hits + << ",\"states\":" << stats.states + << ",\"transitions\":" << stats.transitions + << ",\"elapsed_seconds\":" << stats.elapsed_seconds << "},\n" + << " \"claims\": {\"restoration_family_eliminated\":" + << (eliminated ? "true" : "false") + << ",\"reachable_past_family_eliminated\":" + << (eliminated ? "true" : "false") + << ",\"universal_c4_h7_solvability\":false," + "\"initial_no_candidates_found\":" + << (stats.initial_no != 0 ? "true" : "false") + << ",\"global_no_certified\":false," + "\"global_no_independently_verified\":false," + "\"independent_verification_complete\":false},\n" + << " \"ledgers\": {\"initial_results\":\"initial-results.tsv\"," + "\"initial_no_candidates\":\"initial-no-candidates.jsonl\"," + "\"result_rows_fnv1a64\":\"" + << hex_u64(stats.result_hash) << "\"},\n" + << " \"first_initial_yes\": "; + write_sample_json(json, stats.first_yes); + json << ",\n \"first_initial_no\": "; + write_sample_json(json, stats.first_no); + json << ",\n \"per_edge\": [\n"; + for (std::size_t index = 0; index < stats.per_edge.size(); ++index) { + if (index != 0) json << ",\n"; + const EdgeStats& edge = stats.per_edge[index]; + const ParentSpec& spec = specs[index]; + json << " {\"bridge_edge\":" << edge.edge + << ",\"parent_debts\":[" << spec.debts[0] << ',' + << spec.debts[1] << ',' << spec.debts[2] << ',' + << spec.debts[3] << "]" + << ",\"caps\":[" << spec.bad[1] << ',' << spec.q_caps[0] + << ',' << spec.q_caps[1] << ',' << spec.q_caps[2] << ']' + << ",\"checkpoint_local_no\":" << edge.local_no_rows + << ",\"prefix_candidates\":" << edge.prefix_candidates + << ",\"prefix_reachable\":" << edge.prefix_reachable + << ",\"legal_prefix_histories\":" << edge.legal_histories + << ",\"balanced_restorations_expected\":" + << edge.balanced_expected + << ",\"reachable_restorations_expected\":" + << edge.reachable_expected + << ",\"restorations_checked\":" << edge.checked + << ",\"reachable_checked\":" << edge.reachable_checked + << ",\"initial_yes\":" << edge.initial_yes + << ",\"initial_no\":" << edge.initial_no << '}'; + } + json << "\n ],\n \"self_checks_passed\": " + << (stats.self_checks_passed ? "true" : "false") << "\n}\n"; + + std::ofstream markdown(options.output_dir / "report.md"); + require(static_cast(markdown), "cannot write report.md"); + markdown << "# c=4, h=7 three-source zero-debt past restoration\n\n" + << "- Status: **" << status(stats) << "**\n" + << "- Balanced restoration superset checked: " + << stats.restorations_checked << " / " + << kBalancedRestorations << ".\n" + << "- Parent-reachable restorations checked: " + << stats.reachable_checked << " / " + << kReachableRestorations << ".\n" + << "- Zero-debt initial YES / NO: " << stats.initial_yes + << " / " << stats.initial_no << ".\n" + << "- Canonical symmetry classes solved: " + << stats.canonical_classes_solved << ".\n" + << "- Scope: only the 285,600 balanced completions of the 14,784 " + "three-source checkpoint-local-NO rows.\n" + << "- This report does not claim universal c4/h7 solvability.\n"; + + if (stats.first_no) { + std::ofstream candidate_json( + options.output_dir / "initial-no-candidate.json"); + require(static_cast(candidate_json), + "cannot write initial-no-candidate.json"); + candidate_json + << "{\"scope\":\"complete_balanced_c4_h7_layout\"," + "\"independently_verified\":false,\"candidate\":"; + write_sample_json(candidate_json, stats.first_no); + candidate_json << "}\n"; + + std::ofstream candidate_text( + options.output_dir / "initial-no-candidate.txt"); + require(static_cast(candidate_text), + "cannot write initial-no-candidate.txt"); + candidate_text << "# c=4 h=7 complete balanced candidate\n" + << "# Columns are written bottom-to-top.\n" + << "height=7\ncolors=4\nempty=2\n"; + for (const std::string& column : + stats.first_no->columns_bottom_to_top) { + candidate_text << "column=" << column << '\n'; + } + } +} + +void run_self_tests() { + const auto specs = expected_specs(); + std::uint64_t balanced = 0; + std::uint64_t reachable = 0; + for (const ParentSpec& spec : specs) { + const auto prefixes = enumerate_prefixes(spec); + balanced += spec.local_no_rows * prefixes.size(); + reachable += spec.local_no_rows * static_cast( + std::count_if(prefixes.begin(), prefixes.end(), + [](const PrefixTemplate& item) { + return item.reachable; + })); + } + require(balanced == kBalancedRestorations, + "self-test balanced restoration count drifted"); + require(reachable == kReachableRestorations, + "self-test reachable restoration count drifted"); + + const Words solid{{"0000000", "1111111", "2222222", "3333333"}}; + InitialSolver solid_solver(solid); + const SolverResult solid_result = solid_solver.solve(); + require(solid_result.solvable && solid_solver.replay(solid_result.path), + "solid initial fixture is not solved"); + + const Words ring{{"0000001", "1111112", "2222223", "3333330"}}; + InitialSolver ring_solver(ring); + const SolverResult ring_result = ring_solver.solve(); + require(ring_result.solvable && !ring_result.path.empty() && + ring_solver.replay(ring_result.path), + "nontrivial initial fixture is not solved"); + + Words permuted{{ring[2], ring[0], ring[3], ring[1]}}; + for (std::string& word : permuted) { + for (char& value : word) value = static_cast('0' + (value - '0' + 1) % 4); + } + require(canonicalize(ring).key == canonicalize(permuted).key, + "colour/column canonicalization is not invariant"); +} + +} // namespace + +int main(int argc, char** argv) { + try { + const Options options = parse_options(argc, argv); + if (options.self_test) run_self_tests(); + if (options.checkpoint_report.empty()) { + if (options.self_test) { + std::cout << "three-source past-restoration self-test passed\n"; + return 0; + } + throw std::runtime_error("--checkpoint-report is required"); + } + if (options.output_dir.empty()) { + throw std::runtime_error("--output-dir is required"); + } + const auto specs = expected_specs(); + std::vector> prefixes; + prefixes.reserve(specs.size()); + for (const ParentSpec& spec : specs) { + prefixes.push_back(enumerate_prefixes(spec)); + } + const std::filesystem::path ledger_path = + validate_checkpoint_report(options.checkpoint_report); + const auto rows = load_ledger(ledger_path, specs); + const RunStats stats = run(options, specs, prefixes, rows); + write_report(options, specs, stats); + std::cout << "status=" << status(stats) + << " restorations=" << stats.restorations_checked << '/' + << kBalancedRestorations + << " reachable=" << stats.reachable_checked << '/' + << kReachableRestorations + << " initial_yes=" << stats.initial_yes + << " initial_no=" << stats.initial_no + << " classes=" << stats.canonical_classes_solved << '\n'; + return 0; + } catch (const std::exception& error) { + std::cerr << "error: " << error.what() << '\n'; + return 1; + } +} diff --git a/docs/c4-h7-anchor-pair-graph.md b/docs/c4-h7-anchor-pair-graph.md new file mode 100644 index 0000000..5bd7a14 --- /dev/null +++ b/docs/c4-h7-anchor-pair-graph.md @@ -0,0 +1,399 @@ +# The charged anchor-pair graph at `c=4, h=7, k=2` + +## Scope and claim boundary + +At a zero-exhaustion border checkpoint with exactly two positive debts, the +other two colors form an **anchor pair**. There are six such pairs. This +note organizes them as the octahedral graph `J(4,2)` and proves two facts. + +1. A color which enters the anchor pair must receive a new exposed run. + Therefore the six-vertex graph becomes acyclic after it is lifted by the + four-color exposure vector. +2. In the clean two-switch rotor realized by the committed four-lock + example, a return to the original anchor pair which is also a `D2` + terminal saturates one anchor color at height seven. + +The unweighted six-vertex graph is **not** acyclic. The height-seven +four-lock layout has a legal projected two-cycle, and the cycle ends with +seven, not eight, exposed items of one color. Thus neither + +- "an anchor-pair cycle is impossible at height seven", nor +- "one projected cycle already charges an eighth item" + +is true. The correct statement is that a later entry of a color already at +exposure seven would require an eighth item. This is a well-foundedness and +saturation lemma, not a proof of universal height-seven solvability. In +particular, it does not prove that every unresolved `D2` admits the clean +switch used in Section 4. + +## 1. Exact anchor checkpoints + +For a color `c`, write + +\[ + d_c=F_c-G_c, +\] + +where `F_c` is exposed inventory and `G_c` is the sum of active host caps +currently topped by `c`. Before the first exhaustion, + +\[ + \sum_c d_c=0, + \qquad |\operatorname{Pos}(d)|\le2. \tag{1} +\] + +A source of top color `x` and cap `s` is legal exactly when + +\[ + |\operatorname{Pos}(d+s e_x)|\le2. \tag{2} +\] + +A live border event + +\[ + x_s\longrightarrow y_R, + \qquad x\ne y,quad s0` and `d_c(T)<=0`. Exhausting +events never decrease a debt coordinate, and in (3) the only way to +decrease `d_c` is for `c` to be the destination of a live event. At least +one event + +\[ + u_s\longrightarrow c_R, + \qquad R>s, +\] + +must therefore occur between `S` and `T`. It newly exposes the positive +length `R-s` run of `c`, so `F_c` increases by at least one. Exposure never +decreases later. This proves (6). \(\square\) + +For a sequence of exact checkpoints `S_0,...,S_m`, put `A_i=A(S_i)` and + +\[ + N_c=\#\{i:c\in A_{i+1}\setminus A_i\}. \tag{7} +\] + +Summing (6) over the disjoint time segments gives the vector inequality + +\[ + F_c(S_m)-F_c(S_0)\ge N_c. \tag{8} +\] + +Consequently + +\[ + \sum_{i=0}^{m-1}|A_{i+1}\setminus A_i| + \le \sum_c (h-F_c(S_0)). \tag{9} +\] + +The left side is the octahedral path length, counting a jump to the opposite +pair with cost two. The residual-inventory potential + +\[ + \Phi(F)=\sum_c(h-F_c) \tag{10} +\] + +decreases on every nonconstant pair transition. Thus the lifted graph + +\[ + (A,F)\longrightarrow(B,F') \tag{11} +\] + +is acyclic, even though its projection to the six values of `A` need not be. + +For a closed projected walk `A_m=A_0`, entries and exits balance separately +for every color. Every nonconstant closed walk charges at least two colors, +and a fixed cyclic word can be repeated at most + +\[ + \min_{c:N_c>0} + \left\lfloor\frac{h-F_c(S_0)}{N_c}\right\rfloor + \tag{12} +\] + +times along one coherent history. In particular, if `F_c=7` at height +seven, any transition with `c in B\A` would require `F_c>=8` by (6) and is +impossible. + +This last statement is the precise "eighth item" obstruction. Charges +cannot be added across counterfactual branches: all checkpoints in (8) must +belong to the same legal history and the same fixed layout. + +## 3. A projected cycle at height seven + +The committed balanced four-lock layout, with colors `(q,f,g,h)` encoded as +`(0,1,2,3)`, is written bottom to top as + +```text +2221032 +3321023 +3321003 +1111000 +``` + +The legal column sequence + +```text +0,0,1,0,2,1 +``` + +contains the following exact checkpoints. + +| prefix length | debt `(q,f,g,h)` | anchor pair | exposure `(Fq,Ff,Fg,Fh)` | +|---:|---|---|---| +| 2 | `(-2,0,1,1)` | `{q,f}` | `(4,0,1,3)` | +| 4 | `(1,-3,0,2)` | `{f,g}` | `(4,1,2,3)` | +| 6 | `(-2,-3,2,3)` | `{q,f}` | `(7,1,2,3)` | + +Thus the projected graph has the two-cycle + +\[ + \{q,f\}\longrightarrow\{f,g\} + \longrightarrow\{q,f\}. \tag{13} +\] + +The first edge charges the new anchor `g` once. The second charges the new +anchor `q` three times, stronger than the one-item lower bound in (6). The +return is not a lifted cycle because exposure has changed from +`(4,0,1,3)` to `(7,1,2,3)`. Its final checkpoint is a `3+1` `D2` terminal +with three `q_3` tops and one `f_4` top. A second traversal of the same +projected cycle would eventually have to re-enter `q` and expose an eighth +`q`, so that repetition is excluded, but the first terminal traversal is +real. + +The complete layout is nevertheless YES. One winning column sequence is + +```text +0,0,1,0,2,2,0,1,1,1,1,2,2,3 +``` + +Therefore a projected cycle neither implies NO nor can simply be deleted +from the proof. It records a bad scheduling choice in a solvable layout. + +## 4. Clean two-switch return saturation + +The same example belongs to a more rigid normal form. This is the part of +the graph idea that uses height seven sharply. + +Use four distinct colors `(x,b,y,p)`. Start at an exact checkpoint with + +\[ + d=(-A,0,X,Y), + \qquad X,Y\ge1, + \qquad A=X+Y, \tag{14} +\] + +and top multiset + +\[ + x_t,\ x_c,\ p_s,\ p_u. \tag{15} +\] + +The zero in (14) is forced: `b` is an anchor with no current host, hence +`d_b=F_b` is both nonnegative and nonpositive. Balance then gives +`A=X+Y`. + +Consider the four live events + +\[ + \begin{aligned} + p_s&\longrightarrow y_r, & X&\le sA,\\ + p_u&\longrightarrow x_w, & u&\ge t-A,\quad u