From e0ffd1d9281e4c031ed7eec1aca121830d8ae3db Mon Sep 17 00:00:00 2001 From: lieoric <129092606+lieoric@users.noreply.github.com> Date: Tue, 11 Aug 2026 05:02:17 +1000 Subject: [PATCH] Prove the c4 h7 Tq sibling-entry lemma --- .github/workflows/c4-h7-tq-sibling-forks.yml | 135 ++ CMakeLists.txt | 19 + apps/c4_h7_tq_sibling_forks.cpp | 1062 ++++++++++++ docs/c4-h7-tq-sibling-lemma.md | 275 ++++ .../validate_c4_h7_tq_sibling_forks_report.py | 241 +++ tests/check_c4_h7_tq_sibling_forks.py | 1442 +++++++++++++++++ 6 files changed, 3174 insertions(+) create mode 100644 .github/workflows/c4-h7-tq-sibling-forks.yml create mode 100644 apps/c4_h7_tq_sibling_forks.cpp create mode 100644 docs/c4-h7-tq-sibling-lemma.md create mode 100644 scripts/validate_c4_h7_tq_sibling_forks_report.py create mode 100644 tests/check_c4_h7_tq_sibling_forks.py diff --git a/.github/workflows/c4-h7-tq-sibling-forks.yml b/.github/workflows/c4-h7-tq-sibling-forks.yml new file mode 100644 index 0000000..b6856bf --- /dev/null +++ b/.github/workflows/c4-h7-tq-sibling-forks.yml @@ -0,0 +1,135 @@ +name: Check the c4 k2 h7 Tq sibling forks +run-name: Complete same-z Tq sibling-fork check + +on: + push: + branches: [codex/c4-h7-tq-sibling-forks] + workflow_dispatch: + +permissions: + contents: read + +concurrency: + group: c4-h7-tq-sibling-forks-${{ github.ref }} + cancel-in-progress: true + +jobs: + check: + runs-on: ubuntu-latest + timeout-minutes: 30 + steps: + - uses: actions/checkout@v5 + - uses: actions/setup-python@v5 + with: + python-version: "3.12" + - name: Configure the Release build + run: >- + cmake -S . -B build + -DCMAKE_BUILD_TYPE=Release + -DWSC_WARNINGS_AS_ERRORS=ON + - name: Build the targeted checker and independent oracles + run: >- + cmake --build build + --target water-c4-h7-tq-sibling-forks water-oracle water-verify + --parallel 2 + - name: Run the focused C++ unit test + run: >- + ctest --test-dir build --output-on-failure + --no-tests=error + -R '^water-c4-h7-tq-sibling-forks-smoke$' + - name: Run the program self-test + run: | + mkdir -p out + set -o pipefail + build/water-c4-h7-tq-sibling-forks --self-test 2>&1 | tee out/self-test.log + - name: Run the independent checker against the program + run: | + set -o pipefail + python tests/check_c4_h7_tq_sibling_forks.py \ + --program build/water-c4-h7-tq-sibling-forks \ + --json out/independent-audit.json 2>&1 \ + | tee out/checker-program.log + - name: Exercise the bounded incomplete path + run: | + set -o pipefail + build/water-c4-h7-tq-sibling-forks \ + --limit 32 \ + --output-dir out/limited 2>&1 | tee out/limited.log + python scripts/validate_c4_h7_tq_sibling_forks_report.py \ + --report out/limited/report.json \ + --output-dir out/limited \ + --audit out/independent-audit.json \ + --status-file out/limited/status.txt + test "$(tr -d '\r\n' < out/limited/status.txt)" = "INCOMPLETE" + - name: Check every same-z Tq sibling fork + run: | + set -o pipefail + build/water-c4-h7-tq-sibling-forks \ + --output-dir out 2>&1 | tee out/run.log + - name: Independently audit checkpoint decisions and replay escapes + run: | + set -o pipefail + python tests/check_c4_h7_tq_sibling_forks.py \ + --report out/report.json \ + --json out/independent-report-audit.json 2>&1 \ + | tee out/checker-report.log + - name: Strictly validate the result schema and artifacts + run: >- + python scripts/validate_c4_h7_tq_sibling_forks_report.py + --report out/report.json + --output-dir out + --audit out/independent-report-audit.json + --status-file out/status.txt + - name: Record the exact claim boundary + run: | + status=$(tr -d '\r\n' < out/status.txt) + if test "$status" = "ENTRY_FAMILY_ELIMINATED"; then + echo '> Every residual word at the targeted entry checkpoints is YES, so this entry family is eliminated. This is not a claim that every c4/k2/h7 layout is YES.' >> "$GITHUB_STEP_SUMMARY" + elif test "$status" = "RESIDUALS_EXPORTED"; then + echo '> The residual-word universe is completely classified, but local-NO residuals still require prefix completion. This is not a global NO.' >> "$GITHUB_STEP_SUMMARY" + elif test "$status" = "INCOMPLETE"; then + echo '> This run is incomplete and makes no YES/NO claim.' >> "$GITHUB_STEP_SUMMARY" + fi + - name: Independently certify any reported global NO + run: | + status=$(tr -d '\r\n' < out/status.txt) + if test "$status" = "GLOBAL_NO_FOUND"; then + set -o pipefail + build/water-oracle \ + --input out/no-instance.txt \ + --count 1 \ + --certificate out/no-instance.wscert 2>&1 | tee out/oracle.log + grep -q '^border_sequences=0 ' out/oracle.log + grep -qx 'UNSOLVABLE' out/oracle.log + test -s out/no-instance.wscert + build/water-verify \ + --input out/no-instance.txt \ + --certificate out/no-instance.wscert 2>&1 | tee out/verifier.log + grep -qx 'VALID NO CERTIFICATE' out/verifier.log + fi + - name: Create and verify the SHA-256 manifest + 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 + - name: Add the result to the run summary + if: always() + run: | + if test -f out/report.md; then + cat out/report.md >> "$GITHUB_STEP_SUMMARY" + fi + if test -f out/SHA256SUMS; then + echo '```text' >> "$GITHUB_STEP_SUMMARY" + cat out/SHA256SUMS >> "$GITHUB_STEP_SUMMARY" + echo '```' >> "$GITHUB_STEP_SUMMARY" + fi + - uses: actions/upload-artifact@v6 + if: always() + with: + name: c4-h7-tq-sibling-forks-${{ github.run_id }} + path: out/ + if-no-files-found: error + retention-days: 30 diff --git a/CMakeLists.txt b/CMakeLists.txt index 3e7ff4f..a0820a8 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -88,6 +88,20 @@ else() endif() endif() +add_executable(water-c4-h7-tq-sibling-forks apps/c4_h7_tq_sibling_forks.cpp) +target_link_libraries(water-c4-h7-tq-sibling-forks PRIVATE water_sort) +if(MSVC) + target_compile_options(water-c4-h7-tq-sibling-forks PRIVATE /W4) + if(WSC_WARNINGS_AS_ERRORS) + target_compile_options(water-c4-h7-tq-sibling-forks PRIVATE /WX) + endif() +else() + target_compile_options(water-c4-h7-tq-sibling-forks PRIVATE -Wall -Wextra -Wpedantic) + if(WSC_WARNINGS_AS_ERRORS) + target_compile_options(water-c4-h7-tq-sibling-forks PRIVATE -Werror) + endif() +endif() + include(CTest) if(BUILD_TESTING) add_executable(water-sort-tests tests/test_main.cpp) @@ -95,6 +109,11 @@ if(BUILD_TESTING) target_compile_definitions(water-sort-tests PRIVATE WSC_SOURCE_DIR="${CMAKE_CURRENT_SOURCE_DIR}") add_test(NAME water-sort-tests COMMAND water-sort-tests) + add_test(NAME water-c4-h7-tq-sibling-forks-smoke + COMMAND water-c4-h7-tq-sibling-forks + --self-test + --limit 64 + --output-dir ${CMAKE_CURRENT_BINARY_DIR}/test-c4-h7-tq-sibling-forks-output) 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_tq_sibling_forks.cpp b/apps/c4_h7_tq_sibling_forks.cpp new file mode 100644 index 0000000..530daae --- /dev/null +++ b/apps/c4_h7_tq_sibling_forks.cpp @@ -0,0 +1,1062 @@ +#include "water_sort/border_oracle.hpp" +#include "water_sort/instance.hpp" + +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include + +namespace { + +using water_sort::Color; +using water_sort::Instance; + +constexpr int kHeight = 7; +constexpr int kColors = 4; +constexpr int kEmpty = 2; +constexpr std::uint64_t kExpectedResidualWords = 10073448; + +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; +using Debts = std::array; +using Counts = std::array; + +struct Source { + int color = 0; + int cap = 0; +}; + +struct Action { + int old_color = 0; + int old_cap = 0; + int new_color = 0; + int new_cap = 0; + + bool operator<(const Action& other) const { + return std::tie(old_color, old_cap, new_color, new_cap) < + std::tie(other.old_color, other.old_cap, + other.new_color, other.new_cap); + } +}; + +struct Card { + int color = 0; + int cap = 0; // cap==7 is the exhausting final run. +}; + +struct CandidateWord { + std::vector word; // bottom to top, below the checkpoint border. + Counts counts{}; +}; + +struct Edge { + std::size_t ordinal = 0; + State parent; + State terminal; + Action bad; + Debts parent_debts{}; + Debts terminal_debts{}; // in the parent's labeled coordinates. + std::array columns{}; // bad, sibling 0, sibling 1. + Counts remaining{}; + std::uint64_t raw_single = 0; + std::uint64_t raw_simultaneous = 0; +}; + +struct Decoration { + std::size_t edge = 0; + std::array cards{}; // bad card, sibling cards. + std::uint64_t completions = 0; + bool direct_exhaustion = false; + std::uint32_t persistent_bad_sources = 0; +}; + +struct Sample { + bool present = false; + bool solvable = false; + std::array words; + std::string removal_columns; + std::uint32_t safe_mask = 0; +}; + +struct EdgeStats { + std::uint64_t feasible_decorations = 0; + std::uint64_t residual_words_expected = 0; + std::uint64_t residual_words_checked = 0; + std::uint64_t checkpoint_yes = 0; + std::uint64_t local_no = 0; + std::uint64_t states_evaluated = 0; + std::uint64_t transitions_tested = 0; + std::array safe_source_counts{}; + std::uint64_t both_siblings_safe = 0; + Sample sample; +}; + +struct RunStats { + bool self_checks_passed = false; + bool next_run_census_complete = false; + bool residual_word_universe_complete = false; + std::uint64_t raw_single = 0; + std::uint64_t raw_simultaneous = 0; + std::uint64_t feasible_decorations = 0; + std::uint64_t infeasible_decorations = 0; + std::uint64_t direct_exhaustion_decorations = 0; + std::uint64_t bad_source_persistent_decorations = 0; + std::uint64_t obstruction_decorations = 0; + std::uint64_t residual_words_expected = 0; + std::uint64_t residual_words_checked = 0; + std::uint64_t checkpoint_yes = 0; + std::uint64_t local_no = 0; + std::uint64_t states_evaluated = 0; + std::uint64_t transitions_tested = 0; + std::array safe_source_counts{}; + std::uint64_t both_siblings_safe = 0; + double elapsed_seconds = 0.0; + std::vector edges; + std::optional> first_local_no; +}; + +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-tq-sibling-forks " + "[--output-dir DIR] [--limit N] [--self-test]\n"; +} + +Options parse_options(int argc, char** argv) { + Options options; + for (int i = 1; i < argc; ++i) { + const std::string argument = argv[i]; + if (argument == "--output-dir" && i + 1 < argc) { + options.output_dir = argv[++i]; + } else if (argument == "--limit" && i + 1 < argc) { + options.limit = std::stoull(argv[++i]); + } 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; +} + +State canonical_state(const Debts& debts, + const std::array, kColors>& caps) { + State result; + for (int color = 0; color < kColors; ++color) { + result[static_cast(color)] = {debts[color], caps[color]}; + std::sort(result[static_cast(color)].caps.begin(), + result[static_cast(color)].caps.end()); + } + 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; +} + +std::array, kColors> state_caps(const State& state) { + std::array, kColors> 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; +} + +int positive_count(const Debts& debts) { + return static_cast(std::count_if( + debts.begin(), debts.end(), [](int value) { return value > 0; })); +} + +bool algebraically_consistent(const State& state, int z) { + 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 - z || debt_sum != z * kHeight) return false; + const auto 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 available = 0; + for (int other = 0; other < kColors; ++other) { + if (other != color) available += remaining[other]; + } + if (multiplicity[color] > available) return false; + } + return true; +} + +bool source_legal(const State& state, int z, int color, int cap) { + auto debts = state_debts(state); + debts[color] += cap; + return positive_count(debts) <= kEmpty + z; +} + +std::vector physical_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 z) { + auto result = physical_sources(state); + result.erase(std::remove_if(result.begin(), result.end(), [&](const Source& source) { + return !source_legal(state, z, source.color, source.cap); + }), + result.end()); + return result; +} + +std::optional apply_live(const State& state, int z, const Action& action) { + if (action.old_color == action.new_color || action.old_cap < 1 || + action.old_cap >= action.new_cap || action.new_cap >= kHeight) { + return std::nullopt; + } + auto debts = state_debts(state); + auto caps = state_caps(state); + auto found = std::find(caps[action.old_color].begin(), + caps[action.old_color].end(), action.old_cap); + if (found == caps[action.old_color].end() || + !source_legal(state, z, action.old_color, action.old_cap)) { + return std::nullopt; + } + caps[action.old_color].erase(found); + caps[action.new_color].push_back(action.new_cap); + debts[action.old_color] += action.old_cap; + debts[action.new_color] -= action.old_cap; + auto successor = canonical_state(debts, caps); + if (!algebraically_consistent(successor, z)) return std::nullopt; + return successor; +} + +std::vector live_actions_to(const State& parent, const State& terminal) { + std::vector result; + for (int old_color = 0; old_color < kColors; ++old_color) { + std::set old_caps(parent[old_color].caps.begin(), parent[old_color].caps.end()); + for (const int old_cap : old_caps) { + for (int new_color = 0; new_color < kColors; ++new_color) { + if (new_color == old_color) continue; + for (int new_cap = old_cap + 1; new_cap < kHeight; ++new_cap) { + const Action action{old_color, old_cap, new_color, new_cap}; + const auto successor = apply_live(parent, 1, action); + if (successor && *successor == terminal) result.push_back(action); + } + } + } + } + std::sort(result.begin(), result.end()); + return result; +} + +bool tq_terminal(const State& state) { + if (!algebraically_consistent(state, 1) || !legal_sources(state, 1).empty()) return false; + int nonpositive = -1; + int positives = 0; + for (int color = 0; color < kColors; ++color) { + if (state[color].debt > 0) ++positives; + else { + if (nonpositive != -1) return false; + nonpositive = color; + } + } + if (positives != 3 || nonpositive < 0) return false; + for (int color = 0; color < kColors; ++color) { + if (color == nonpositive) { + if (state[color].caps.size() != 3) return false; + } else if (!state[color].caps.empty()) { + return false; + } + } + return true; +} + +std::vector enumerate_tq_terminals() { + std::set states; + for (int e = 0; e <= 2; ++e) { + for (int a = 1; a < kHeight; ++a) { + for (int b = a; b < kHeight; ++b) { + for (int c = b; c < kHeight; ++c) { + if (a <= e || a + b + c - e > kHeight) continue; + for (int x = 1; x <= kHeight; ++x) { + for (int y = x; y <= kHeight; ++y) { + for (int z = y; z <= kHeight; ++z) { + if (x + y + z - e != kHeight) continue; + State state{{{-e, {a, b, c}}, {x, {}}, {y, {}}, {z, {}}}}; + std::sort(state.begin(), state.end()); + if (tq_terminal(state)) states.insert(std::move(state)); + } + } + } + } + } + } + } + return {states.begin(), states.end()}; +} + +std::vector reverse_parents(const State& terminal) { + std::set parents; + for (int new_color = 0; new_color < kColors; ++new_color) { + std::set new_caps(terminal[new_color].caps.begin(), terminal[new_color].caps.end()); + for (const int new_cap : new_caps) { + for (int old_color = 0; old_color < kColors; ++old_color) { + if (old_color == new_color) continue; + for (int old_cap = 1; old_cap < new_cap; ++old_cap) { + auto debts = state_debts(terminal); + auto caps = state_caps(terminal); + auto found = std::find(caps[new_color].begin(), + caps[new_color].end(), new_cap); + caps[new_color].erase(found); + caps[old_color].push_back(old_cap); + debts[old_color] -= old_cap; + debts[new_color] += old_cap; + auto test = debts; + test[old_color] += old_cap; + if (positive_count(test) > 3) continue; + auto parent = canonical_state(debts, caps); + if (algebraically_consistent(parent, 1)) parents.insert(std::move(parent)); + } + } + } + } + return {parents.begin(), parents.end()}; +} + +std::vector enumerate_edges() { + const auto terminals = enumerate_tq_terminals(); + require(terminals.size() == 71, "Tq terminal count is not 71"); + + std::set> all_pairs; + std::set all_parents; + for (const auto& terminal : terminals) { + for (const auto& parent : reverse_parents(terminal)) { + all_parents.insert(parent); + all_pairs.emplace(parent, terminal); + } + } + require(all_parents.size() == 80, "Tq reverse parent count is not 80"); + require(all_pairs.size() == 116, "Tq reverse edge count is not 116"); + + std::vector result; + std::set sibling_parents; + for (const auto& pair : all_pairs) { + const auto& parent = pair.first; + const auto& terminal = pair.second; + const auto legal = legal_sources(parent, 1); + if (legal.size() < 2) continue; + const auto actions = live_actions_to(parent, terminal); + require(!actions.empty(), "reverse edge has no replay action"); + const auto bad = actions.front(); + + auto sources = physical_sources(parent); + auto selected = std::find_if(sources.begin(), sources.end(), [&](const Source& source) { + return source.color == bad.old_color && source.cap == bad.old_cap; + }); + require(selected != sources.end(), "bad physical source missing"); + Source bad_source = *selected; + sources.erase(selected); + require(sources.size() == 2, "z=1 parent does not have three sources"); + require(legal.size() == 3, "Tq sibling parent does not have three legal sources"); + require(sources[0].color == bad.new_color && sources[1].color == bad.new_color, + "Tq siblings are not both q sources"); + + Edge edge; + edge.parent = parent; + edge.terminal = terminal; + edge.bad = bad; + edge.parent_debts = state_debts(parent); + edge.terminal_debts = edge.parent_debts; + edge.terminal_debts[bad.old_color] += bad.old_cap; + edge.terminal_debts[bad.new_color] -= bad.old_cap; + edge.columns = {bad_source, sources[0], sources[1]}; + const auto exposed = exposed_counts(parent); + for (int color = 0; color < kColors; ++color) { + edge.remaining[color] = kHeight - exposed[color]; + } + const auto cards0 = 3ULL * static_cast(kHeight - sources[0].cap); + const auto cards1 = 3ULL * static_cast(kHeight - sources[1].cap); + edge.raw_single = cards0 + cards1; + edge.raw_simultaneous = cards0 * cards1; + result.push_back(std::move(edge)); + sibling_parents.insert(parent); + } + require(sibling_parents.size() == 23, "Tq sibling parent count is not 23"); + require(result.size() == 32, "Tq sibling bad edge count is not 32"); + std::sort(result.begin(), result.end(), [](const Edge& left, const Edge& right) { + return std::tie(left.parent, left.terminal, left.bad) < + std::tie(right.parent, right.terminal, right.bad); + }); + for (std::size_t i = 0; i < result.size(); ++i) result[i].ordinal = i; + return result; +} + +std::vector cards_for(const Source& source) { + std::vector result; + for (int color = 0; color < kColors; ++color) { + if (color == source.color) continue; + for (int cap = source.cap + 1; cap <= kHeight; ++cap) { + result.push_back({color, cap}); + } + } + return result; +} + +std::string word_string(const std::vector& word) { + std::string result; + for (const auto color : word) result.push_back(water_sort::color_to_char(color)); + return result; +} + +std::vector candidate_words(int old_cap, const Card& card) { + const int length = kHeight - old_cap; + const int forced = card.cap - old_cap; + const int free = length - forced; + require(length > 0 && forced > 0 && free >= 0, "invalid candidate-word card"); + CandidateWord current; + current.word.assign(static_cast(length), 0); + for (int position = free; position < length; ++position) { + current.word[static_cast(position)] = + static_cast(card.color); + } + std::vector result; + std::function visit = [&](int position) { + if (position == free) { + if (free > 0 && current.word[static_cast(free - 1)] == card.color) { + return; + } + current.counts.fill(0); + for (const auto color : current.word) ++current.counts[color]; + result.push_back(current); + return; + } + for (int color = 0; color < kColors; ++color) { + current.word[static_cast(position)] = static_cast(color); + visit(position + 1); + } + }; + visit(0); + return result; +} + +std::uint32_t pack_counts(const Counts& counts) { + std::uint32_t result = 0; + for (int color = 0; color < kColors; ++color) { + result |= static_cast(counts[color]) << (4 * color); + } + return result; +} + +Counts subtract_counts(const Counts& total, const Counts& left, const Counts& middle, + bool& valid) { + Counts result{}; + valid = true; + for (int color = 0; color < kColors; ++color) { + result[color] = total[color] - left[color] - middle[color]; + if (result[color] < 0) valid = false; + } + return result; +} + +bool bad_source_persists(const Edge& edge, const Source& sibling, const Card& card) { + if (card.cap == kHeight) return false; + auto debts = edge.parent_debts; + debts[sibling.color] += sibling.cap; + debts[card.color] -= sibling.cap; + debts[edge.bad.old_color] += edge.bad.old_cap; + return positive_count(debts) <= 3; +} + +struct WordCacheKey { + int old_cap = 0; + int color = 0; + int cap = 0; + bool operator<(const WordCacheKey& other) const { + return std::tie(old_cap, color, cap) < + std::tie(other.old_cap, other.color, other.cap); + } +}; + +using WordCache = std::map>; + +const std::vector& words_for(WordCache& cache, int old_cap, + const Card& card) { + const WordCacheKey key{old_cap, card.color, card.cap}; + auto found = cache.find(key); + if (found == cache.end()) { + found = cache.emplace(key, candidate_words(old_cap, card)).first; + } + return found->second; +} + +std::uint64_t completion_count(const Edge& edge, const std::array& cards, + WordCache& cache) { + const auto& first = words_for(cache, edge.columns[0].cap, cards[0]); + const auto& second = words_for(cache, edge.columns[1].cap, cards[1]); + const auto& third = words_for(cache, edge.columns[2].cap, cards[2]); + std::unordered_map third_counts; + for (const auto& word : third) ++third_counts[pack_counts(word.counts)]; + std::uint64_t total = 0; + for (const auto& left : first) { + for (const auto& middle : second) { + bool valid = false; + const auto needed = subtract_counts(edge.remaining, left.counts, + middle.counts, valid); + if (!valid) continue; + const auto found = third_counts.find(pack_counts(needed)); + if (found != third_counts.end()) total += found->second; + } + } + return total; +} + +std::vector enumerate_decorations(const std::vector& edges, + WordCache& cache, RunStats& stats) { + std::vector result; + for (const auto& edge : edges) { + stats.raw_single += edge.raw_single; + stats.raw_simultaneous += edge.raw_simultaneous; + const Card bad{edge.bad.new_color, edge.bad.new_cap}; + const auto left_cards = cards_for(edge.columns[1]); + const auto right_cards = cards_for(edge.columns[2]); + for (const auto& left : left_cards) { + for (const auto& right : right_cards) { + Decoration decoration; + decoration.edge = edge.ordinal; + decoration.cards = {bad, left, right}; + decoration.direct_exhaustion = + left.cap == kHeight || right.cap == kHeight; + decoration.persistent_bad_sources = + static_cast(bad_source_persists( + edge, edge.columns[1], left)) + + static_cast(bad_source_persists( + edge, edge.columns[2], right)); + decoration.completions = completion_count(edge, decoration.cards, cache); + if (decoration.completions == 0) { + ++stats.infeasible_decorations; + continue; + } + ++stats.feasible_decorations; + stats.residual_words_expected += decoration.completions; + if (decoration.direct_exhaustion) ++stats.direct_exhaustion_decorations; + if (decoration.persistent_bad_sources != 0) { + ++stats.bad_source_persistent_decorations; + } else if (!decoration.direct_exhaustion) { + ++stats.obstruction_decorations; + } + result.push_back(std::move(decoration)); + } + } + } + stats.next_run_census_complete = true; + require(stats.raw_single == 840, "raw single-card count is not 840"); + require(stats.raw_simultaneous == 5526, "raw simultaneous count is not 5526"); + require(stats.feasible_decorations == 2958, "feasible decoration count is not 2958"); + require(stats.residual_words_expected == kExpectedResidualWords, + "residual-word count is not 10073448"); + return result; +} + +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 Edge& edge, + const std::array& words) + : initial_debts_(edge.parent_debts), columns_(edge.columns) { + std::uint32_t multiplier = 1; + for (std::size_t column = 0; column < 3; ++column) { + build_events(column, words[column]->word); + 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 < 3; ++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 < 3; ++column) { + if (!safe_from(state, column)) continue; + result.path.push_back(static_cast('0' + column)); + state += multipliers_[column]; + advanced = true; + break; + } + if (!advanced) throw std::runtime_error("winning state has no safe source"); + } + } + result.states = states_; + result.transitions = transitions_; + return result; + } + +private: + struct Event { + int old_color = 0; + int old_cap = 0; + int next_color = 0; + int next_cap = 0; + }; + + Debts initial_debts_{}; + std::array columns_{}; + std::array, 3> events_; + std::array, 3> 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 = columns_[column].color; + int old_cap = columns_[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, "future run repeats current top"); + 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 end in exhaustion"); + 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 auto& 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 < 3; ++column) { + ranks[column] = (state / multipliers_[column]) % + (events_[column].size() + 1); + } + return ranks; + } + + bool goal(std::uint32_t state) const { + const auto ranks = decode(state); + for (std::size_t column = 0; column < ranks.size(); ++column) { + if (ranks[column] == events_[column].size()) return true; + } + return false; + } + + bool legal(std::uint32_t state, std::size_t column) const { + const auto ranks = decode(state); + int exhausted = 0; + Debts debts = initial_debts_; + for (std::size_t other = 0; other < 3; ++other) { + if (ranks[other] == events_[other].size()) ++exhausted; + for (int color = 0; color < kColors; ++color) { + debts[color] += deltas_[other][ranks[other]][color]; + } + } + if (ranks[column] == events_[column].size()) return false; + const auto& event = events_[column][ranks[column]]; + debts[event.old_color] += event.old_cap; + return positive_count(debts) <= kEmpty + 1 + exhausted; + } + + 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; + auto& memo = memo_[state]; + if (memo >= 0) return memo != 0; + ++states_; + for (std::size_t column = 0; column < 3; ++column) { + if (safe_from(state, column)) { + memo = 1; + return true; + } + } + memo = 0; + return false; + } +}; + +template +bool for_each_completion(const Edge& edge, const Decoration& decoration, + WordCache& cache, Callback&& callback) { + const auto& first = words_for(cache, edge.columns[0].cap, decoration.cards[0]); + const auto& second = words_for(cache, edge.columns[1].cap, decoration.cards[1]); + const auto& third = words_for(cache, edge.columns[2].cap, decoration.cards[2]); + std::unordered_map> third_by_counts; + for (const auto& word : third) third_by_counts[pack_counts(word.counts)].push_back(&word); + for (const auto& left : first) { + for (const auto& middle : second) { + bool valid = false; + const auto needed = subtract_counts(edge.remaining, left.counts, + middle.counts, valid); + if (!valid) continue; + const auto found = third_by_counts.find(pack_counts(needed)); + if (found == third_by_counts.end()) continue; + for (const auto* right : found->second) { + const std::array words{&left, &middle, right}; + if (!callback(words)) return false; + } + } + } + return true; +} + +RunStats run(const Options& options, const std::vector& edges, + const std::vector& decorations, WordCache& cache, + RunStats stats) { + stats.edges.resize(edges.size()); + for (const auto& decoration : decorations) { + auto& edge_stats = stats.edges[decoration.edge]; + ++edge_stats.feasible_decorations; + edge_stats.residual_words_expected += decoration.completions; + } + + const auto 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 auto& decoration : decorations) { + const auto& edge = edges[decoration.edge]; + auto& edge_stats = stats.edges[decoration.edge]; + const bool complete = for_each_completion( + edge, decoration, cache, + [&](const std::array& words) { + if (stats.residual_words_checked >= effective_limit) return false; + FixedFutureSolver solver(edge, words); + const auto result = solver.solve(); + ++stats.residual_words_checked; + ++edge_stats.residual_words_checked; + stats.states_evaluated += result.states; + stats.transitions_tested += result.transitions; + edge_stats.states_evaluated += result.states; + edge_stats.transitions_tested += result.transitions; + if (result.solvable) { + ++stats.checkpoint_yes; + ++edge_stats.checkpoint_yes; + } else { + ++stats.local_no; + ++edge_stats.local_no; + } + for (std::size_t column = 0; column < 3; ++column) { + if ((result.safe_mask & (1U << column)) != 0) { + ++edge_stats.safe_source_counts[column]; + ++stats.safe_source_counts[column]; + } + } + if ((result.safe_mask & 0x6U) == 0x6U) { + ++edge_stats.both_siblings_safe; + ++stats.both_siblings_safe; + } + Sample sample; + sample.present = true; + sample.solvable = result.solvable; + sample.safe_mask = result.safe_mask; + sample.removal_columns = result.path; + for (std::size_t column = 0; column < 3; ++column) { + sample.words[column] = word_string(words[column]->word); + } + if (!edge_stats.sample.present) edge_stats.sample = sample; + if (!result.solvable && !stats.first_local_no) { + stats.first_local_no = std::make_pair(decoration.edge, sample); + } + return true; + }); + if (!complete && stats.residual_words_checked >= effective_limit) { + stop = true; + break; + } + } + static_cast(stop); + stats.elapsed_seconds = std::chrono::duration( + std::chrono::steady_clock::now() - started).count(); + stats.residual_word_universe_complete = + stats.residual_words_checked == stats.residual_words_expected; + stats.self_checks_passed = true; + require(stats.checkpoint_yes + stats.local_no == stats.residual_words_checked, + "checkpoint classification does not sum to checked words"); + require(stats.safe_source_counts[0] == 0, + "a terminal-entering bad source was unexpectedly safe"); + require(stats.safe_source_counts[1] == stats.residual_words_checked && + stats.safe_source_counts[2] == stats.residual_words_checked && + stats.both_siblings_safe == stats.residual_words_checked, + "both q siblings are not safe in every checked fixed future"); + return stats; +} + +std::string status(const RunStats& stats) { + if (!stats.residual_word_universe_complete) return "INCOMPLETE"; + if (stats.local_no != 0) return "RESIDUALS_EXPORTED"; + return "ENTRY_FAMILY_ELIMINATED"; +} + +std::string json_state(const State& state) { + std::ostringstream output; + output << '['; + for (std::size_t color = 0; color < state.size(); ++color) { + if (color != 0) output << ','; + output << "{\"debt\":" << state[color].debt << ",\"caps\":["; + for (std::size_t i = 0; i < state[color].caps.size(); ++i) { + if (i != 0) output << ','; + output << state[color].caps[i]; + } + output << "]}"; + } + output << ']'; + return output.str(); +} + +void write_sample(std::ostream& output, const Sample& sample) { + if (!sample.present) { + output << "null"; + return; + } + output << "{\"solvable\":" << (sample.solvable ? "true" : "false") + << ",\"hidden_words_bottom_to_top\":["; + for (std::size_t i = 0; i < sample.words.size(); ++i) { + if (i != 0) output << ','; + output << '"' << sample.words[i] << '"'; + } + output << "],\"safe_source_mask\":" << sample.safe_mask + << ",\"escape_columns\":\"" << sample.removal_columns << "\"}"; +} + +void write_report(const Options& options, const std::vector& edges, + const RunStats& stats) { + if (options.output_dir.empty()) return; + std::filesystem::create_directories(options.output_dir); + const auto report_path = options.output_dir / "report.json"; + std::ofstream json(report_path); + if (!json) throw std::runtime_error("cannot write " + report_path.string()); + const bool verified = stats.self_checks_passed && + stats.next_run_census_complete && + stats.residual_word_universe_complete; + json << "{\n" + << " \"schema_version\": 1,\n" + << " \"coverage_scope\": \"same_z_tq_sibling_entry_family\",\n" + << " \"status\": \"" << status(stats) << "\",\n" + << " \"self_checks_passed\": " + << (stats.self_checks_passed ? "true" : "false") << ",\n" + << " \"verified\": " << (verified ? "true" : "false") << ",\n" + << " \"universe_complete\": " + << (stats.residual_word_universe_complete ? "true" : "false") << ",\n" + << " \"next_run_census_complete\": " + << (stats.next_run_census_complete ? "true" : "false") << ",\n" + << " \"residual_word_universe_complete\": " + << (stats.residual_word_universe_complete ? "true" : "false") << ",\n" + << " \"full_residual_word_coverage\": " + << (stats.residual_word_universe_complete ? "true" : "false") << ",\n" + << " \"full_layout_coverage\": false,\n" + << " \"terminal_count\": 71,\n" + << " \"sibling_parent_count\": 23,\n" + << " \"bad_edge_count\": 32,\n" + << " \"raw_single_next_run_outcomes\": " << stats.raw_single << ",\n" + << " \"raw_simultaneous_decorations\": " << stats.raw_simultaneous << ",\n" + << " \"feasible_decorations\": " << stats.feasible_decorations << ",\n" + << " \"infeasible_decorations\": " << stats.infeasible_decorations << ",\n" + << " \"direct_exhaustion_decorations\": " + << stats.direct_exhaustion_decorations << ",\n" + << " \"bad_source_persistent_decorations\": " + << stats.bad_source_persistent_decorations << ",\n" + << " \"obstruction_decorations\": " << stats.obstruction_decorations << ",\n" + << " \"residual_words_expected\": " << stats.residual_words_expected << ",\n" + << " \"fixed_future_completions\": " << stats.residual_words_expected << ",\n" + << " \"residual_words_checked\": " << stats.residual_words_checked << ",\n" + << " \"checked_completions\": " << stats.residual_words_checked << ",\n" + << " \"checkpoint_yes_count\": " << stats.checkpoint_yes << ",\n" + << " \"yes_count\": " << stats.checkpoint_yes << ",\n" + << " \"local_no_count\": " << stats.local_no << ",\n" + << " \"no_count\": " << stats.local_no << ",\n" + << " \"global_no_count\": 0,\n" + << " \"safe_source_counts\": [" << stats.safe_source_counts[0] << ',' + << stats.safe_source_counts[1] << ',' << stats.safe_source_counts[2] << "],\n" + << " \"both_siblings_safe_count\": " << stats.both_siblings_safe << ",\n" + << " \"edge_summed_residual_words\": true,\n" + << " \"states_evaluated\": " << stats.states_evaluated << ",\n" + << " \"transitions_tested\": " << stats.transitions_tested << ",\n" + << " \"elapsed_seconds\": " << stats.elapsed_seconds << ",\n" + << " \"per_edge\": [\n"; + for (std::size_t i = 0; i < edges.size(); ++i) { + if (i != 0) json << ",\n"; + const auto& edge = edges[i]; + const auto& row = stats.edges[i]; + json << " {\"edge_id\":\"tq-sibling-e" << i << "\"," + << "\"parent\":" << json_state(edge.parent) << ',' + << "\"terminal\":" << json_state(edge.terminal) << ',' + << "\"bad_action\":[" << edge.bad.old_color << ',' << edge.bad.old_cap + << ',' << edge.bad.new_color << ',' << edge.bad.new_cap << "]," + << "\"columns\":[[" << edge.columns[0].color << ',' << edge.columns[0].cap + << "],[" << edge.columns[1].color << ',' << edge.columns[1].cap + << "],[" << edge.columns[2].color << ',' << edge.columns[2].cap << "]]," + << "\"raw_single_next_run_outcomes\":" << edge.raw_single << ',' + << "\"raw_simultaneous_decorations\":" << edge.raw_simultaneous << ',' + << "\"feasible_decorations\":" << row.feasible_decorations << ',' + << "\"residual_words_expected\":" << row.residual_words_expected << ',' + << "\"residual_words_checked\":" << row.residual_words_checked << ',' + << "\"checkpoint_yes_count\":" << row.checkpoint_yes << ',' + << "\"local_no_count\":" << row.local_no << ',' + << "\"safe_source_counts\":[" << row.safe_source_counts[0] << ',' + << row.safe_source_counts[1] << ',' << row.safe_source_counts[2] << "]," + << "\"both_siblings_safe_count\":" << row.both_siblings_safe << ',' + << "\"sample\":"; + write_sample(json, row.sample); + json << '}'; + } + json << "\n ]"; + if (stats.first_local_no) { + json << ",\n \"first_local_no\": {\"edge_index\":" + << stats.first_local_no->first << ",\"residual\":"; + write_sample(json, stats.first_local_no->second); + json << '}'; + } + json << "\n}\n"; + + std::ofstream markdown(options.output_dir / "report.md"); + if (!markdown) throw std::runtime_error("cannot write report.md"); + markdown << "# c=4, h=7, k=2 same-z Tq sibling-fork census\n\n" + << "- Scope: checkpoint residual words for the 23 same-z Tq sibling parents.\n" + << "- Status: **" << status(stats) << "**\n" + << "- Terminals / sibling parents / bad edges: 71 / 23 / 32.\n" + << "- Raw single cards / simultaneous decorations: " << stats.raw_single + << " / " << stats.raw_simultaneous << ".\n" + << "- Color-feasible decorations: " << stats.feasible_decorations << ".\n" + << "- Complete residual words checked: " << stats.residual_words_checked + << " / " << stats.residual_words_expected << ".\n" + << "- Checkpoint YES / local NO: " << stats.checkpoint_yes << " / " + << stats.local_no << ".\n" + << "- Full initial-layout coverage: no (not needed when every checkpoint is YES).\n"; +} + +} // namespace + +int main(int argc, char** argv) { + try { + auto options = parse_options(argc, argv); + const auto edges = enumerate_edges(); + WordCache cache; + RunStats structural; + const auto decorations = enumerate_decorations(edges, cache, structural); + structural.self_checks_passed = true; + + // A bare self-test deliberately checks a small exact prefix. Supplying + // --output-dir and --limit exercises the normal report path instead. + if (options.self_test && options.output_dir.empty() && options.limit == 0) { + options.limit = 64; + } + const auto stats = run(options, edges, decorations, cache, structural); + write_report(options, edges, stats); + std::cout << "status=" << status(stats) + << " terminals=71 parents=23 edges=32" + << " raw_single=" << stats.raw_single + << " raw_simultaneous=" << stats.raw_simultaneous + << " feasible=" << stats.feasible_decorations + << " residual=" << stats.residual_words_checked << '/' + << stats.residual_words_expected + << " yes=" << stats.checkpoint_yes + << " local_no=" << stats.local_no << '\n'; + return 0; + } catch (const std::exception& error) { + std::cerr << "error: " << error.what() << '\n'; + return 1; + } +} diff --git a/docs/c4-h7-tq-sibling-lemma.md b/docs/c4-h7-tq-sibling-lemma.md new file mode 100644 index 0000000..b6011f2 --- /dev/null +++ b/docs/c4-h7-tq-sibling-lemma.md @@ -0,0 +1,275 @@ +# The same-level Tq sibling-entry lemma at c=4, h=7, k=2 + +## Scope + +This note eliminates the **same-`z` live entrances into `Tq` that have a +legal sibling source**. In the canonical numerical census this is the family +of 23 parents and 32 parent-terminal edges. The argument applies to every +balanced fixed future represented by those edges; it does not depend on an +enumeration of the residual words. + +This is only a local lemma. It does not eliminate the unique-source +same-`z` entrances, the first-exhaustion entrances, the `D2` terminal family, +or all height-7 layouts. In particular, it is not by itself a proof of +universal solvability at height 7. + +## Border model + +Work after one original column has already been exhausted, so `z=1` and three +original columns remain active. For each color `c`, let + +\[ +d_c=F_c-G_c, +\] + +where `F_c` is the exposed amount of color `c` and `G_c` is the capacity +currently hosted by active columns whose top color is `c`. A live source of +top color `x` and cumulative cap `r` is legal exactly when + +\[ +\#\{c:d_c+r[c=x]>0\}\le k+z=3. \tag{1} +\] + +If its next run has color `y` and ends at a live cap `R`, where +`x != y` and `r0\quad(c\ne q), \tag{3} +\] + +and let the three current caps be `t,u,v`. Terminal blockedness gives + +\[ +t,u,v>E. \tag{4} +\] + +Suppose that `P` enters `D` by the same-level live event + +\[ +a_s\longrightarrow q_t,\qquad a\ne q. \tag{5} +\] + +The standard entrance sandwich is + +\[ +1\le s\le E0. +\] + +Inverting (2) gives + +\[ +d(P)=d(D)-s e_a+s e_q, +\] + +and hence + +\[ +d_a(P)=p-s,\qquad d_q(P)=s-E. \tag{7} +\] + +Assume that `P` belongs to the sibling family, so at least one of the two +`q`-top columns is legal. Test, for example, the column of cap `u`. In its +source-test vector, the `q` coordinate is + +\[ +s-E+u>0 +\] + +by (4), and the two non-`q`, non-`a` coordinates are the unchanged positive +coordinates of `D`. There are already three positive coordinates. By (1), +the remaining `a` coordinate must be nonpositive. Therefore + +\[ +p-s\le0,\qquad\text{or equivalently}\qquad p\le s. \tag{8} +\] + +The same sign calculation then proves that the other `q`-top column is legal +as well. Thus a sibling parent actually has **both** `q` siblings available. + +Equation (8) is the source of the anchor used below; it is not an additional +enumerated property of the 23 parents. + +## Anchor-corridor lemma + +**Lemma 1 (anchor corridor).** At `z=1`, suppose `d_a<=0`. Any active source +whose current top color is not `a` is legal. Moreover, that same fixed column +may be advanced until it either exhausts or first acquires top color `a`, and +`d_a` stays nonpositive throughout. + +**Proof.** Testing a source of top color different from `a` leaves the +`a` coordinate unchanged and nonpositive. Among four coordinates there can +therefore be at most three positive ones, so (1) holds. A live event whose +new color is not `a` leaves `d_a` unchanged by (2); the first event whose new +color is `a` subtracts its old cap from `d_a`. Hence every intermediate +source is legal and the anchor never becomes positive. An endpoint 7 is +already the goal. \(\square\) + +## Bringing both siblings to the anchor + +At `P`, equation (8) says that `a` is a nonpositive anchor. Start with +**either** of the two `q` siblings. It is legal by the preceding calculation. +Apply Lemma 1 to that column until it exhausts or first reaches top color `a`. +If it exhausts, the proof is finished. Otherwise, `d_a` has only decreased, +so Lemma 1 applies to the other `q` sibling as well. Advance that second +column to exhaustion or to its first `a`. + +It remains to consider the case in which both siblings reach live `a` +boundaries. Together with the untouched source in (5), all three active tops +are now `a`. Let `c_1,c_2` be the caps immediately before the two sibling +columns enter `a`. Caps strictly increase along a fixed column, so + +\[ +c_1\ge u,\qquad c_2\ge v. \tag{9} +\] + +Starting from `d_a(P)=p-s`, the two first entries into `a` subtract `c_1` and +`c_2`. No earlier event on either corridor changes `d_a`. At the resulting +all-`a` checkpoint `A`, + +\[ +d_a(A)=p-s-c_1-c_2. +\] + +Define its `a`-energy by `M=-d_a(A)`. Equations (4), (6), (8), and (9) give + +\[ +M=s+c_1+c_2-p + \ge c_1+c_2 + \ge u+v + \ge4. \tag{10} +\] + +The lower bound 4 is the height-7 leverage: a same-level entrance has +`E>=1`, while both terminal sibling caps are integers strictly larger than +`E`. + +## The all-anchor rotor + +**Lemma 2 (high-energy all-anchor rotor).** In a balanced height-7 state at +`z=1`, suppose all three active tops are `a` and + +\[ +d_a=-M,\qquad M\ge4. +\] + +Then the fixed chains have a legal path to `z=2`. + +**Proof.** Let the three current caps be `r_1,r_2,r_3`. Since all three tops +are `a`, the debt definition gives + +\[ +F_a=r_1+r_2+r_3-M. \tag{11} +\] + +There are exactly seven items of color `a`, hence `F_a<=7`. If every cap were +strictly larger than `M`, integrality and (11) would imply + +\[ +F_a\ge3(M+1)-M=2M+3\ge11, +\] + +a contradiction. Therefore some current cap `r` satisfies `r<=M`. That +`a`-source is legal because its adjusted `a` debt is `-M+r<=0`. + +Take this source. If its next event exhausts the column, `z=2` is reached. +Otherwise it leaves `a`; immediately after that live event the anchor debt is + +\[ +d_a=-M+r\le0. +\] + +Apply Lemma 1 to the same column until it exhausts or first returns to `a`. +If it returns, let `w` be its cap immediately before the return event. The +cap has strictly advanced, so `w>r`. Departure from `a` added `r` to `d_a`, +the intermediate non-`a` events did not touch `d_a`, and return to `a` +subtracts `w`. The new all-`a` energy is therefore + +\[ +M'=M+w-r>M. \tag{12} +\] + +It is still at least 4, so the argument repeats. Every repetition strictly +advances at least one fixed column cap. The three chains have only finitely +many boundaries, and no cap ever decreases. Consequently the construction +cannot return to an all-`a` checkpoint forever; one of its corridor events +must eventually have endpoint 7. \(\square\) + +## Main conclusion + +**Theorem (same-level `Tq` sibling-entry elimination).** Every balanced +fixed future realizing a same-`z` live entrance (5) into `Tq` with a legal +sibling source is checkpoint-YES: from `P`, a second original column can be +exhausted. In fact, the next event of **either** `q` sibling is a safe first +move. + +**Proof.** Equation (8) supplies the anchor. Starting from either sibling, +the two applications of Lemma 1 either reach `z=2` directly or reach the +all-`a` checkpoint whose energy satisfies (10). Lemma 2 finishes the latter +case. The construction uses only the actual successive runs in the fixed +chains, so it applies independently to every choice of residual words. +\(\square\) + +## Audit of the shorter persistence formula + +There is also a correct one-event persistence observation. If the sibling of +cap `u` moves live from `q` to `x`, testing the untouched sibling of cap `v` +uses + +\[ +d(P)+(u+v)e_q-u e_x. \tag{13} +\] + +The informal statement that the subtraction in (13) cannot create a positive +coordinate needs one explicit premise: adding `u` must not make `q` newly +positive relative to the original test of the `v` sibling. Here that premise +holds because + +\[ +d_q(P)+v=s-E+v>0 +\] + +by (4) and (7). Thus the additional `u e_q` does not change the sign of `q`, +and `-u e_x` can only remove a positive coordinate. If the sibling event has +endpoint 7, it reaches the goal and no persistence claim is needed. + +The persistence formula is therefore sound on this family, but it alone only +justifies the commuting first layer. The anchor-corridor and all-anchor rotor +arguments are what prove eventual exhaustion for arbitrary fixed suffixes. + +## Role of the exhaustive machine run + +The independent census identifies 23 canonical sibling parents, 32 bad +edges, and 10,073,448 labeled balanced residual fixed futures. An exhaustive +checkpoint DP over those futures is useful as an independent implementation +check: it can catch an incorrect transition, scope mismatch, or transcription +error in this note. + +It is not a logical premise of the theorem. The proof above quantifies over +an arbitrary balanced fixed future and supplies a legal terminating strategy +directly. Therefore the machine run should be reported as corroborating +full-universe verification, not as 10,073,448 unrelated searches on which the +lemma depends. diff --git a/scripts/validate_c4_h7_tq_sibling_forks_report.py b/scripts/validate_c4_h7_tq_sibling_forks_report.py new file mode 100644 index 0000000..d2bb36c --- /dev/null +++ b/scripts/validate_c4_h7_tq_sibling_forks_report.py @@ -0,0 +1,241 @@ +#!/usr/bin/env python3 +"""Strict artifact-level validation for the c4/k2/h7 Tq sibling-fork run. + +This checker deliberately does not reproduce the independent mathematical +census. Its job is to prevent a partial or local obstruction from being +reported as a complete Water Sort result and to validate the shape of any +full-instance witness before the independent oracle is invoked. +""" + +from __future__ import annotations + +import argparse +import json +import re +from pathlib import Path +from typing import NoReturn + + +EXPECTED_TERMINALS = 71 +EXPECTED_SIBLING_PARENTS = 23 +EXPECTED_BAD_EDGES = 32 +EXPECTED_RAW_SINGLE_OUTCOMES = 840 +EXPECTED_RAW_SIMULTANEOUS_DECORATIONS = 5_526 +EXPECTED_RESIDUAL_WORDS = 10_073_448 +EXPECTED_SCOPE = "same_z_tq_sibling_entry_family" +ALLOWED_STATUSES = { + "ENTRY_FAMILY_ELIMINATED", + "RESIDUALS_EXPORTED", + "GLOBAL_NO_FOUND", + "INCOMPLETE", +} + + +def fail(message: str) -> NoReturn: + raise SystemExit(message) + + +def require(condition: bool, message: str) -> None: + if not condition: + fail(message) + + +def integer(report: dict[str, object], key: str, *, minimum: int = 0) -> int: + value = report.get(key) + require( + isinstance(value, int) and not isinstance(value, bool), + f"{key} must be an integer, got {value!r}", + ) + require(value >= minimum, f"{key} must be at least {minimum}, got {value}") + return value + + +def parse_complete_instance(path: Path) -> None: + """Check that a claimed global NO witness is a complete balanced instance.""" + + require(path.is_file(), f"NO_FOUND is missing the full instance {path}") + fields: dict[str, int] = {} + columns: list[str] = [] + for raw_line in path.read_text(encoding="utf-8").splitlines(): + line = raw_line.strip() + if not line or line.startswith("#"): + continue + if line.startswith("column="): + columns.append(line.removeprefix("column=")) + continue + match = re.fullmatch(r"(height|colors|empty)=(\d+)", line) + require(match is not None, f"unrecognized instance line: {raw_line!r}") + key, value = match.groups() + require(key not in fields, f"duplicate instance field: {key}") + fields[key] = int(value) + + require( + fields == {"height": 7, "colors": 4, "empty": 2}, + f"NO witness has wrong dimensions: {fields}", + ) + require(len(columns) == 4, f"NO witness must contain four columns, got {len(columns)}") + counts = [0, 0, 0, 0] + for index, column in enumerate(columns): + require(len(column) == 7, f"column {index} has length {len(column)}, expected 7") + require(re.fullmatch(r"[0-3]{7}", column) is not None, f"invalid column {index}: {column!r}") + for symbol in column: + counts[int(symbol)] += 1 + require(counts == [7, 7, 7, 7], f"NO witness is not balanced: color counts {counts}") + + +def validate(report_path: Path, output_dir: Path, audit_path: Path | None) -> str: + require(report_path.is_file(), f"missing JSON report: {report_path}") + markdown_path = output_dir / "report.md" + require(markdown_path.is_file(), f"missing Markdown report: {markdown_path}") + + try: + report = json.loads(report_path.read_text(encoding="utf-8")) + except (OSError, UnicodeError, json.JSONDecodeError) as error: + fail(f"cannot parse {report_path}: {error}") + require(isinstance(report, dict), "the top-level report must be a JSON object") + require(report.get("schema_version") == 1, "unsupported or missing schema_version") + require(report.get("self_checks_passed") is True, "production self-checks did not pass") + + if audit_path is not None: + require(audit_path.is_file(), f"missing independent census: {audit_path}") + try: + audit = json.loads(audit_path.read_text(encoding="utf-8")) + except (OSError, UnicodeError, json.JSONDecodeError) as error: + fail(f"cannot parse {audit_path}: {error}") + require(isinstance(audit, dict), "the independent census must be a JSON object") + for key in ( + "terminal_count", + "sibling_parent_count", + "bad_edge_count", + "raw_single_next_run_outcomes", + "raw_simultaneous_decorations", + "feasible_decorations", + "fixed_future_completions", + ): + require( + report.get(key) == audit.get(key), + f"production {key}={report.get(key)!r} disagrees with independent audit " + f"{audit.get(key)!r}", + ) + + status = report.get("status") + require(status in ALLOWED_STATUSES, f"unsupported report status: {status!r}") + require( + report.get("coverage_scope") == EXPECTED_SCOPE, + f"coverage_scope must be {EXPECTED_SCOPE!r}", + ) + require(isinstance(report.get("verified"), bool), "verified must be Boolean") + require( + isinstance(report.get("universe_complete"), bool), + "universe_complete must be Boolean", + ) + for key in ("next_run_census_complete", "residual_word_universe_complete"): + require(isinstance(report.get(key), bool), f"{key} must be Boolean") + + fixed_census = { + "terminal_count": EXPECTED_TERMINALS, + "sibling_parent_count": EXPECTED_SIBLING_PARENTS, + "bad_edge_count": EXPECTED_BAD_EDGES, + "raw_single_next_run_outcomes": EXPECTED_RAW_SINGLE_OUTCOMES, + "raw_simultaneous_decorations": EXPECTED_RAW_SIMULTANEOUS_DECORATIONS, + } + actual_census = {key: report.get(key) for key in fixed_census} + require( + actual_census == fixed_census, + f"fixed sibling-fork census mismatch: expected {fixed_census}, got {actual_census}", + ) + + feasible = integer(report, "feasible_decorations") + fixed_futures = integer(report, "fixed_future_completions") + residual_expected = integer(report, "residual_words_expected") + residual_checked = integer(report, "residual_words_checked") + checkpoint_yes = integer(report, "checkpoint_yes_count") + local_no = integer(report, "local_no_count") + global_no = integer(report, "global_no_count") + require(feasible <= EXPECTED_RAW_SIMULTANEOUS_DECORATIONS, "feasible census exceeds raw decorations") + require( + fixed_futures == 0 or feasible > 0, + "fixed-future completions cannot exist without a feasible decoration", + ) + require( + residual_checked <= residual_expected, + f"residual_words_checked={residual_checked} exceeds expected={residual_expected}", + ) + require( + checkpoint_yes + local_no == residual_checked, + "checkpoint classifications do not sum to checked residual words", + ) + require( + residual_expected == fixed_futures == EXPECTED_RESIDUAL_WORDS, + "residual-word universe must match the independently derived 10,073,448 words", + ) + + verified = report["verified"] + complete = report["universe_complete"] + next_run_complete = report["next_run_census_complete"] + residual_complete = report["residual_word_universe_complete"] + if status == "ENTRY_FAMILY_ELIMINATED": + require(verified is True, "ENTRY_FAMILY_ELIMINATED requires verified=true") + require(complete is True, "elimination requires universe_complete=true") + require(next_run_complete is True, "elimination requires a complete next-run census") + require( + residual_complete is True, + "entry elimination is forbidden without complete residual-word coverage", + ) + require(residual_expected > 0, "elimination cannot use an empty residual census") + require(residual_checked == residual_expected, "elimination has unchecked residual words") + require(checkpoint_yes == residual_expected and local_no == 0, "elimination contains a local NO") + require(global_no == 0, "eliminated entry family cannot also report a global NO") + require( + not (output_dir / "no-instance.txt").exists(), + "eliminated entry family unexpectedly contains a global NO witness", + ) + elif status == "RESIDUALS_EXPORTED": + require(verified is True, "RESIDUALS_EXPORTED requires verified=true") + require(complete is True, "residual export requires universe_complete=true for its local universe") + require(next_run_complete is True, "residual export requires the next-run census") + require(residual_complete is True, "residual export must cover every residual word") + require(residual_checked == residual_expected, "residual export has unchecked words") + require(local_no >= 1, "RESIDUALS_EXPORTED has no local-NO residual") + require(global_no == 0, "local residual export cannot report a global NO") + require( + not (output_dir / "no-instance.txt").exists(), + "local residual export must not publish an artifact named as a global NO witness", + ) + elif status == "GLOBAL_NO_FOUND": + require(verified is True, "GLOBAL_NO_FOUND requires verified=true") + require(global_no >= 1, "GLOBAL_NO_FOUND has no globally classified NO instance") + parse_complete_instance(output_dir / "no-instance.txt") + else: + require(verified is False, "INCOMPLETE must set verified=false") + require(complete is False, "INCOMPLETE must set universe_complete=false") + require( + residual_complete is False or residual_checked < residual_expected, + "INCOMPLETE contradicts complete residual-word coverage", + ) + require(global_no == 0, "a globally verified NO must use GLOBAL_NO_FOUND") + require( + not (output_dir / "no-instance.txt").exists(), + "INCOMPLETE must not publish an artifact named as a global NO witness", + ) + + return str(status) + + +def main() -> None: + parser = argparse.ArgumentParser() + parser.add_argument("--report", type=Path, required=True) + parser.add_argument("--output-dir", type=Path, required=True) + parser.add_argument("--audit", type=Path) + parser.add_argument("--status-file", type=Path) + args = parser.parse_args() + + status = validate(args.report, args.output_dir, args.audit) + if args.status_file is not None: + args.status_file.parent.mkdir(parents=True, exist_ok=True) + args.status_file.write_text(status + "\n", encoding="utf-8") + print(f"strict sibling-fork report validation passed: status={status}") + + +if __name__ == "__main__": + main() diff --git a/tests/check_c4_h7_tq_sibling_forks.py b/tests/check_c4_h7_tq_sibling_forks.py new file mode 100644 index 0000000..861344b --- /dev/null +++ b/tests/check_c4_h7_tq_sibling_forks.py @@ -0,0 +1,1442 @@ +#!/usr/bin/env python3 +"""Independent audit for the c=4, k=2, h=7 Tq sibling-fork census. + +This file deliberately does not import the production enumerator or the +earlier macro-reconnaissance script. It rebuilds the numerical border model +from the Ito source test, enumerates the same-z entrances to Tq, commits the +next run of both sibling sources simultaneously, and counts color-balanced +fixed futures by a separate dynamic program. + +With ``--program`` the checker also runs a bounded production job, validates +its JSON report, and independently replays every concrete witness emitted by +that report. +""" + +from __future__ import annotations + +import argparse +import copy +import hashlib +import itertools +import json +import subprocess +import tempfile +from collections import Counter +from dataclasses import dataclass +from functools import lru_cache +from pathlib import Path +from typing import Iterable, Iterator, Sequence + + +HEIGHT = 7 +COLORS = 4 +EMPTY_COLUMNS = 2 + +EXPECTED_TERMINALS = 71 +EXPECTED_LIVE_PARENTS = 80 +EXPECTED_LIVE_EDGES = 116 +EXPECTED_SIBLING_PARENTS = 23 +EXPECTED_BAD_EDGES = 32 +EXPECTED_RAW_SINGLE_OUTCOMES = 840 +EXPECTED_RAW_DECORATIONS = 5_526 +EXPECTED_FEASIBLE_DECORATIONS = 2_958 +EXPECTED_FIXED_FUTURES = 10_073_448 +EXPECTED_MIN_EDGE_FUTURES = 924 +EXPECTED_MAX_EDGE_FUTURES = 3_963_960 +EXPECTED_CHECKPOINT_SAMPLES = 3 * EXPECTED_BAD_EDGES + +Bucket = tuple[int, tuple[int, ...]] +State = tuple[Bucket, Bucket, Bucket, Bucket] +Action = tuple[int, int, int, int] # old color/cap, new color/cap +Card = tuple[int, int] # next color, cumulative endpoint +Run = tuple[int, int] +LiveColumn = tuple[int, int, tuple[Run, ...]] + + +def require(condition: bool, message: str) -> None: + if not condition: + raise AssertionError(message) + + +def canonical_state( + debts: Sequence[int], columns: Iterable[tuple[int, int]] +) -> State: + """Quotient labeled colors and active columns by sorting their buckets.""" + + caps_by_color: list[list[int]] = [[] for _ in range(COLORS)] + for color, cap in columns: + caps_by_color[color].append(cap) + buckets = tuple( + sorted( + (int(debts[color]), tuple(sorted(caps_by_color[color]))) + for color in range(COLORS) + ) + ) + require(len(buckets) == COLORS, "canonical state lost a color") + return buckets # type: ignore[return-value] + + +def exposed_counts(state: State) -> tuple[int, int, int, int]: + return tuple(debt + sum(caps) for debt, caps in state) # type: ignore[return-value] + + +def state_is_consistent(state: State, exhausted: int) -> bool: + """Check all bounded numerical and hidden-suffix realization conditions.""" + + if tuple(sorted(state)) != state: + return False + if sum(len(caps) for _, caps in state) != COLORS - exhausted: + return False + if sum(debt for debt, _ in state) != exhausted * HEIGHT: + return False + if any(cap < 1 or cap >= HEIGHT for _, caps in state for cap in caps): + return False + + exposed = exposed_counts(state) + top_multiplicity = tuple(len(caps) for _, caps in state) + if any( + not top_multiplicity[color] <= exposed[color] <= HEIGHT + for color in range(COLORS) + ): + return False + + # Each active column has a nonempty suffix whose first item is different + # from its current top. This is a forbidden-diagonal token assignment. + # With four colors the singleton Hall inequalities below are sufficient: + # any set containing two different forbidden colors can use all colors. + remaining = tuple(HEIGHT - count for count in exposed) + return all( + top_multiplicity[color] + <= sum(remaining[other] for other in range(COLORS) if other != color) + for color in range(COLORS) + ) + + +def source_is_legal(state: State, exhausted: int, color: int, cap: int) -> bool: + adjusted = [debt for debt, _ in state] + adjusted[color] += cap + return sum(value > 0 for value in adjusted) <= EMPTY_COLUMNS + exhausted + + +def physical_sources(state: State) -> Iterator[tuple[int, int]]: + for color, (_, caps) in enumerate(state): + for cap in caps: + yield color, cap + + +def legal_sources(state: State, exhausted: int) -> tuple[tuple[int, int], ...]: + return tuple( + source + for source in physical_sources(state) + if source_is_legal(state, exhausted, source[0], source[1]) + ) + + +def apply_live_action(state: State, action: Action) -> State | None: + """Apply one nonexhausting border event at z=1 and recanonicalize.""" + + old_color, old_cap, new_color, new_cap = action + if old_color == new_color or not (1 <= old_cap < new_cap < HEIGHT): + return None + if old_color not in range(COLORS) or new_color not in range(COLORS): + return None + if old_cap not in state[old_color][1]: + return None + if not source_is_legal(state, 1, old_color, old_cap): + return None + + debts = [debt for debt, _ in state] + caps_by_color = [list(caps) for _, caps in state] + caps_by_color[old_color].remove(old_cap) + caps_by_color[new_color].append(new_cap) + debts[old_color] += old_cap + debts[new_color] -= old_cap + successor = canonical_state( + debts, + ( + (color, cap) + for color, caps in enumerate(caps_by_color) + for cap in caps + ), + ) + return successor if state_is_consistent(successor, 1) else None + + +def actions_to(parent: State, terminal: State) -> tuple[Action, ...]: + actions: list[Action] = [] + for old_color, (_, caps) in enumerate(parent): + for old_cap in sorted(set(caps)): + if not source_is_legal(parent, 1, old_color, old_cap): + continue + for new_color in range(COLORS): + if new_color == old_color: + continue + for new_cap in range(old_cap + 1, HEIGHT): + action = old_color, old_cap, new_color, new_cap + if apply_live_action(parent, action) == terminal: + actions.append(action) + return tuple(actions) + + +def enumerate_tq_terminals() -> tuple[State, ...]: + """Enumerate Tq directly from its debt and all-q-top definition.""" + + terminals: set[State] = set() + for magnitude in range(3): + for caps in itertools.combinations_with_replacement(range(1, HEIGHT), 3): + if min(caps) <= magnitude: + continue + if sum(caps) - magnitude > HEIGHT: + continue + for positives in itertools.combinations_with_replacement( + range(1, HEIGHT + 1), 3 + ): + if sum(positives) - magnitude != HEIGHT: + continue + state = tuple( + sorted( + ((-magnitude, caps),) + + tuple((debt, ()) for debt in positives) + ) + ) + state = state # retain a narrow inferred tuple type + if not state_is_consistent(state, 1): # type: ignore[arg-type] + continue + if legal_sources(state, 1): # type: ignore[arg-type] + continue + terminals.add(state) # type: ignore[arg-type] + return tuple(sorted(terminals)) + + +def reverse_live_pairs(terminals: Sequence[State]) -> tuple[tuple[State, State], ...]: + """Invert every possible live edge and retain those that replay forward.""" + + pairs: set[tuple[State, State]] = set() + for terminal in terminals: + q_color = next( + color for color, (_, caps) in enumerate(terminal) if len(caps) == 3 + ) + for new_cap in sorted(set(terminal[q_color][1])): + for old_color in range(COLORS): + if old_color == q_color: + continue + for old_cap in range(1, new_cap): + debts = [debt for debt, _ in terminal] + caps_by_color = [list(caps) for _, caps in terminal] + caps_by_color[q_color].remove(new_cap) + caps_by_color[old_color].append(old_cap) + debts[old_color] -= old_cap + debts[q_color] += old_cap + parent = canonical_state( + debts, + ( + (color, cap) + for color, caps in enumerate(caps_by_color) + for cap in caps + ), + ) + if not state_is_consistent(parent, 1): + continue + if actions_to(parent, terminal): + pairs.add((parent, terminal)) + return tuple(sorted(pairs)) + + +@dataclass(frozen=True) +class BadEdge: + parent: State + terminal: State + action: Action + sibling_caps: tuple[int, int] + + def key(self) -> tuple[State, State, Action]: + return self.parent, self.terminal, self.action + + +def sibling_bad_edges( + pairs: Sequence[tuple[State, State]], +) -> tuple[BadEdge, ...]: + result: list[BadEdge] = [] + for parent, terminal in pairs: + legal = legal_sources(parent, 1) + if len(legal) < 2: + continue + actions = actions_to(parent, terminal) + require(len(actions) == 1, "sibling edge has ambiguous canonical action") + action = actions[0] + q_color = action[2] + require( + tuple(cap for color, cap in legal if color == q_color) + == parent[q_color][1], + "the two q siblings are not exactly the q-top columns", + ) + require(len(parent[q_color][1]) == 2, "sibling parent does not have two q columns") + require(len(legal) == 3, "sibling parent does not have exactly three legal sources") + result.append(BadEdge(parent, terminal, action, parent[q_color][1])) + return tuple(sorted(result, key=BadEdge.key)) + + +def next_cards(q_color: int, cap: int) -> tuple[Card, ...]: + return tuple( + (color, endpoint) + for color in range(COLORS) + if color != q_color + for endpoint in range(cap + 1, HEIGHT + 1) + ) + + +def remaining_tail_word_count( + edge: BadEdge, cards: tuple[Card, Card] +) -> int: + """Count labeled hidden tails realizing one simultaneous decoration. + + The bad edge commits its old source's q run. Each card commits the next + run of one labeled q sibling. If a committed run is nonfinal, the first + cell below it must have a different color; all later tail cells are free. + """ + + old_color, old_cap, q_color, q_endpoint = edge.action + del old_color + exposed = exposed_counts(edge.parent) + remaining = [HEIGHT - count for count in exposed] + + remaining[q_color] -= q_endpoint - old_cap + tails: list[tuple[int, int]] = [(HEIGHT - q_endpoint, q_color)] + for cap, (next_color, endpoint) in zip(edge.sibling_caps, cards): + require(next_color != q_color, "q sibling was decorated with another q run") + require(cap < endpoint <= HEIGHT, "next-run endpoint is out of range") + remaining[next_color] -= endpoint - cap + tails.append((HEIGHT - endpoint, next_color)) + if any(count < 0 for count in remaining): + return 0 + + forbidden_by_position: list[int | None] = [] + for length, preceding_color in tails: + if length == 0: + continue + forbidden_by_position.append(preceding_color) + forbidden_by_position.extend([None] * (length - 1)) + if len(forbidden_by_position) != sum(remaining): + return 0 + + @lru_cache(maxsize=None) + def count_words(position: int, counts: tuple[int, int, int, int]) -> int: + if position == len(forbidden_by_position): + return int(not any(counts)) + forbidden = forbidden_by_position[position] + total = 0 + for color, count in enumerate(counts): + if count == 0 or color == forbidden: + continue + child = list(counts) + child[color] -= 1 + total += count_words(position + 1, tuple(child)) # type: ignore[arg-type] + return total + + return count_words(0, tuple(remaining)) # type: ignore[arg-type] + + +def tail_problem( + edge: BadEdge, cards: tuple[Card, Card] +) -> tuple[tuple[int, int, int, int], tuple[tuple[int, int], ...]] | None: + """Return residual color counts and (length, forbidden-first-color) tails.""" + + _, old_cap, q_color, q_endpoint = edge.action + remaining = [HEIGHT - count for count in exposed_counts(edge.parent)] + remaining[q_color] -= q_endpoint - old_cap + tails: list[tuple[int, int]] = [(HEIGHT - q_endpoint, q_color)] + for cap, (next_color, endpoint) in zip(edge.sibling_caps, cards): + remaining[next_color] -= endpoint - cap + tails.append((HEIGHT - endpoint, next_color)) + if any(count < 0 for count in remaining): + return None + if sum(length for length, _ in tails) != sum(remaining): + return None + return tuple(remaining), tuple(tails) # type: ignore[return-value] + + +def one_tail_completion( + edge: BadEdge, cards: tuple[Card, Card], *, reverse: bool = False +) -> tuple[tuple[int, ...], tuple[int, ...], tuple[int, ...]] | None: + """Find the lexicographically first (or last) labeled residual words.""" + + problem = tail_problem(edge, cards) + if problem is None: + return None + remaining, tails = problem + forbidden: list[int | None] = [] + for length, preceding in tails: + if length: + forbidden.append(preceding) + forbidden.extend([None] * (length - 1)) + + color_order = tuple(reversed(range(COLORS))) if reverse else tuple(range(COLORS)) + + @lru_cache(maxsize=None) + def suffix( + position: int, counts: tuple[int, int, int, int] + ) -> tuple[int, ...] | None: + if position == len(forbidden): + return () if not any(counts) else None + for color in color_order: + if counts[color] == 0 or color == forbidden[position]: + continue + child = list(counts) + child[color] -= 1 + continuation = suffix(position + 1, tuple(child)) # type: ignore[arg-type] + if continuation is not None: + return (color,) + continuation + return None + + word = suffix(0, remaining) + if word is None: + return None + output: list[tuple[int, ...]] = [] + cursor = 0 + for length, _ in tails: + output.append(word[cursor : cursor + length]) + cursor += length + require(cursor == len(word), "tail completion split lost cells") + return tuple(output) # type: ignore[return-value] + + +def tail_completions( + edge: BadEdge, cards: tuple[Card, Card] +) -> Iterator[tuple[tuple[int, ...], tuple[int, ...], tuple[int, ...]]]: + """Yield every labeled residual tuple in lexicographic cell order.""" + + problem = tail_problem(edge, cards) + if problem is None: + return + remaining, tails = problem + forbidden: list[int | None] = [] + for length, preceding in tails: + if length: + forbidden.append(preceding) + forbidden.extend([None] * (length - 1)) + + cells = [-1] * len(forbidden) + + def visit( + position: int, counts: tuple[int, int, int, int] + ) -> Iterator[tuple[int, ...]]: + if position == len(forbidden): + if not any(counts): + yield tuple(cells) + return + for color in range(COLORS): + if counts[color] == 0 or color == forbidden[position]: + continue + child = list(counts) + child[color] -= 1 + cells[position] = color + yield from visit(position + 1, tuple(child)) # type: ignore[arg-type] + + for word in visit(0, remaining): + output: list[tuple[int, ...]] = [] + cursor = 0 + for length, _ in tails: + output.append(word[cursor : cursor + length]) + cursor += length + yield tuple(output) # type: ignore[misc] + + +def color_runs(word: Iterable[int]) -> tuple[Run, ...]: + runs: list[Run] = [] + for color in word: + if runs and runs[-1][0] == color: + runs[-1] = color, runs[-1][1] + 1 + else: + runs.append((color, 1)) + return tuple(runs) + + +def residual_checkpoint( + edge: BadEdge, + cards: tuple[Card, Card], + tails: tuple[tuple[int, ...], tuple[int, ...], tuple[int, ...]], +) -> tuple[tuple[int, int, int, int], tuple[LiveColumn, LiveColumn, LiveColumn]]: + """Build the exact three live fixed chains at the sibling parent.""" + + old_color, old_cap, q_color, q_endpoint = edge.action + hidden_words: list[tuple[int, ...]] = [ + (q_color,) * (q_endpoint - old_cap) + tails[0] + ] + for cap, (next_color, endpoint), tail in zip( + edge.sibling_caps, cards, tails[1:] + ): + hidden_words.append((next_color,) * (endpoint - cap) + tail) + require( + all(len(word) == HEIGHT - cap for word, cap in zip(hidden_words, (old_cap,) + edge.sibling_caps)), + "residual hidden word has the wrong length", + ) + columns: tuple[LiveColumn, LiveColumn, LiveColumn] = ( + (old_color, old_cap, color_runs(hidden_words[0])), + (q_color, edge.sibling_caps[0], color_runs(hidden_words[1])), + (q_color, edge.sibling_caps[1], color_runs(hidden_words[2])), + ) + require(all(column[2] for column in columns), "active residual column has no future run") + return tuple(debt for debt, _ in edge.parent), columns # type: ignore[return-value] + + +@lru_cache(maxsize=None) +def checkpoint_is_winning( + debts: tuple[int, int, int, int], + columns: tuple[LiveColumn | None, LiveColumn | None, LiveColumn | None], +) -> bool: + """Independent exact fixed-chain recursion from z=1 to one more exhaustion.""" + + if any(column is None for column in columns): + return True + for source, column in enumerate(columns): + require(column is not None, "non-goal checkpoint unexpectedly lost a column") + top, cap, future = column + if not source_is_legal_from_debts(debts, 1, top, cap): + continue + require(future, "live checkpoint column has no future border") + next_color, run_length = future[0] + require(next_color != top, "fixed chain contains adjacent equal runs") + child_debts = list(debts) + child_debts[top] += cap + child_columns = list(columns) + if len(future) == 1: + require(cap + run_length == HEIGHT, "final run does not reach the bottom") + child_debts[next_color] += run_length + child_columns[source] = None + else: + require(cap + run_length < HEIGHT, "nonfinal run exhausts its column") + child_debts[next_color] -= cap + child_columns[source] = (next_color, cap + run_length, future[1:]) + if checkpoint_is_winning( + tuple(child_debts), tuple(child_columns) # type: ignore[arg-type] + ): + return True + return False + + +def source_is_legal_from_debts( + debts: tuple[int, int, int, int], exhausted: int, color: int, cap: int +) -> bool: + adjusted = list(debts) + adjusted[color] += cap + return sum(value > 0 for value in adjusted) <= EMPTY_COLUMNS + exhausted + + +def checkpoint_escape( + debts: tuple[int, int, int, int], + columns: tuple[LiveColumn | None, LiveColumn | None, LiveColumn | None], +) -> tuple[int, ...] | None: + """Extract and independently replay one winning local source sequence.""" + + if any(column is None for column in columns): + return () + for source, column in enumerate(columns): + require(column is not None, "unexpected absent column") + top, cap, future = column + if not source_is_legal_from_debts(debts, 1, top, cap): + continue + next_color, run_length = future[0] + child_debts = list(debts) + child_debts[top] += cap + child_columns = list(columns) + if len(future) == 1: + child_debts[next_color] += run_length + child_columns[source] = None + else: + child_debts[next_color] -= cap + child_columns[source] = (next_color, cap + run_length, future[1:]) + child = tuple(child_columns) + if not checkpoint_is_winning(tuple(child_debts), child): # type: ignore[arg-type] + continue + suffix = checkpoint_escape(tuple(child_debts), child) # type: ignore[arg-type] + require(suffix is not None, "winning child has no extracted escape") + return (source,) + suffix + return None + + +def checkpoint_step( + debts: tuple[int, int, int, int], + columns: tuple[LiveColumn | None, LiveColumn | None, LiveColumn | None], + source: int, +) -> tuple[ + tuple[int, int, int, int], + tuple[LiveColumn | None, LiveColumn | None, LiveColumn | None], +] | None: + if source not in range(3) or columns[source] is None: + return None + column = columns[source] + require(column is not None, "selected checkpoint source vanished") + top, cap, future = column + if not source_is_legal_from_debts(debts, 1, top, cap): + return None + next_color, run_length = future[0] + child_debts = list(debts) + child_debts[top] += cap + child_columns = list(columns) + if len(future) == 1: + require(cap + run_length == HEIGHT, "sample final run misses the bottom") + child_debts[next_color] += run_length + child_columns[source] = None + else: + require(cap + run_length < HEIGHT, "sample nonfinal run exhausts") + child_debts[next_color] -= cap + child_columns[source] = (next_color, cap + run_length, future[1:]) + return tuple(child_debts), tuple(child_columns) # type: ignore[return-value] + + +def checkpoint_safe_mask( + debts: tuple[int, int, int, int], + columns: tuple[LiveColumn | None, LiveColumn | None, LiveColumn | None], +) -> int: + mask = 0 + for source in range(3): + child = checkpoint_step(debts, columns, source) + if child is not None and checkpoint_is_winning(*child): + mask |= 1 << source + return mask + + +def replay_abstract_sample(edge: BadEdge, value: object) -> bool: + """Replay one production residual-word witness from its sibling checkpoint.""" + + if value is None: + return False + require(isinstance(value, dict), "per-edge sample is neither object nor null") + words_value = value.get("hidden_words_bottom_to_top") + require( + isinstance(words_value, list) + and len(words_value) == 3 + and all(isinstance(word, str) for word in words_value), + "sample has no three hidden words", + ) + current = ( + (edge.action[0], edge.action[1]), + (edge.action[2], edge.sibling_caps[0]), + (edge.action[2], edge.sibling_caps[1]), + ) + words: list[tuple[int, ...]] = [] + for raw, (_, cap) in zip(words_value, current): + require(len(raw) == HEIGHT - cap, "sample hidden word has wrong length") + require(all(character in "0123" for character in raw), "sample has a bad color") + words.append(tuple(int(character) for character in raw)) + counts = Counter(color for word in words for color in word) + expected_remaining = Counter( + { + color: HEIGHT - exposed_counts(edge.parent)[color] + for color in range(COLORS) + } + ) + require(counts == expected_remaining, "sample residual words violate color balance") + + live: list[LiveColumn] = [] + for (top, cap), word in zip(current, words): + top_to_bottom = tuple(reversed(word)) + require(top_to_bottom and top_to_bottom[0] != top, "sample repeats checkpoint top") + live.append((top, cap, color_runs(top_to_bottom))) + bad_future = live[0][2] + require( + bad_future[0] + == (edge.action[2], edge.action[3] - edge.action[1]), + "sample bad column does not realize the stored bad edge", + ) + debts = tuple(debt for debt, _ in edge.parent) + columns = tuple(live) + independent_solvable = checkpoint_is_winning(debts, columns) # type: ignore[arg-type] + require(value.get("solvable") is independent_solvable, "sample solvability disagrees with DP") + safe_mask = checkpoint_safe_mask(debts, columns) # type: ignore[arg-type] + require(value.get("safe_source_mask") == safe_mask, "sample safe mask disagrees with DP") + require((safe_mask & 0x6) == 0x6, "a q sibling is not independently safe") + + escape_value = value.get("escape_columns") + require(isinstance(escape_value, str), "sample has no escape_columns string") + require(all(character in "012" for character in escape_value), "bad local escape source") + if not independent_solvable: + require(escape_value == "", "losing sample carries a claimed escape") + return True + state_debts = debts + state_columns = columns # type: ignore[assignment] + for step, character in enumerate(escape_value): + child = checkpoint_step(state_debts, state_columns, int(character)) + require(child is not None, f"sample escape is illegal at step {step}") + state_debts, state_columns = child + require(any(column is None for column in state_columns), "sample escape misses z=2") + return True + + +def audit_checkpoint_samples(edges: Sequence[BadEdge]) -> dict[str, int]: + """Classify first/middle/last fixed futures for every one of the 32 edges.""" + + samples = 0 + yes = 0 + no = 0 + for edge in edges: + q_color = edge.action[2] + feasible_cards = [ + cards + for cards in itertools.product( + next_cards(q_color, edge.sibling_caps[0]), + next_cards(q_color, edge.sibling_caps[1]), + ) + if remaining_tail_word_count(edge, cards) > 0 # type: ignore[arg-type] + ] + require(feasible_cards, "edge has no feasible simultaneous decoration") + selections = ( + (feasible_cards[0], False), + (feasible_cards[len(feasible_cards) // 2], False), + (feasible_cards[-1], True), + ) + for cards, reverse in selections: + tails = one_tail_completion(edge, cards, reverse=reverse) # type: ignore[arg-type] + require(tails is not None, "feasible decoration has no concrete residual word") + debts, columns = residual_checkpoint(edge, cards, tails) # type: ignore[arg-type] + winning = checkpoint_is_winning(debts, columns) + escape = checkpoint_escape(debts, columns) + require((escape is not None) == winning, "escape extraction disagrees with DP") + samples += 1 + yes += int(winning) + no += int(not winning) + require(samples == EXPECTED_CHECKPOINT_SAMPLES, "checkpoint sample coverage is not 3 per edge") + require(yes == EXPECTED_CHECKPOINT_SAMPLES and no == 0, "a fixed checkpoint sample is NO") + return {"checkpoint_samples": samples, "checkpoint_sample_yes": yes, "checkpoint_sample_no": no} + + +def bounded_checkpoint_audit(edges: Sequence[BadEdge], limit: int) -> dict[str, object]: + """Classify an independently ordered bounded prefix of all residual words.""" + + require(limit > 0, "bounded checkpoint audit needs a positive limit") + checked = 0 + yes = 0 + no = 0 + digest = hashlib.sha256() + for edge_ordinal, edge in enumerate(edges): + q_color = edge.action[2] + for cards in itertools.product( + next_cards(q_color, edge.sibling_caps[0]), + next_cards(q_color, edge.sibling_caps[1]), + ): + for tails in tail_completions(edge, cards): # type: ignore[arg-type] + debts, columns = residual_checkpoint(edge, cards, tails) # type: ignore[arg-type] + winning = checkpoint_is_winning(debts, columns) + escape = checkpoint_escape(debts, columns) + require((escape is not None) == winning, "bounded DP extraction mismatch") + record = { + "edge": edge_ordinal, + "cards": cards, + "tails": tails, + "winning": winning, + "escape": escape, + } + digest.update( + json.dumps(record, separators=(",", ":"), sort_keys=True).encode("ascii") + ) + checked += 1 + yes += int(winning) + no += int(not winning) + if checked == limit: + return { + "checked": checked, + "yes": yes, + "no": no, + "sha256": digest.hexdigest(), + } + require(False, f"bounded audit requested {limit} beyond the residual universe") + raise AssertionError("unreachable") + + +def replay_persistence_formula(edge: BadEdge, sibling: int, card: Card) -> None: + """Prove by direct source-test evaluation that the other q sibling persists.""" + + q_color = edge.action[2] + cap = edge.sibling_caps[sibling] + other_cap = edge.sibling_caps[1 - sibling] + next_color, endpoint = card + if endpoint == HEIGHT: + return # a second original column is exhausted: the frontier is reached + + # After q_cap -> next_color, testing the untouched q source gives + # d + (cap + other_cap)e_q - cap e_next. The subtraction cannot create a + # positive coordinate. We still evaluate the exact formula, rather than + # accepting the informal monotonicity argument alone. + adjusted = [debt for debt, _ in edge.parent] + adjusted[q_color] += cap + other_cap + adjusted[next_color] -= cap + require( + sum(value > 0 for value in adjusted) <= EMPTY_COLUMNS + 1, + "the untouched q sibling did not persist", + ) + + +def bad_source_persists(edge: BadEdge, sibling: int, card: Card) -> bool: + """Classify the finer, nonautomatic persistence of the original bad source.""" + + old_color, old_cap, q_color, _ = edge.action + cap = edge.sibling_caps[sibling] + next_color, endpoint = card + if endpoint == HEIGHT: + return False + adjusted = [debt for debt, _ in edge.parent] + adjusted[q_color] += cap + adjusted[next_color] -= cap + adjusted[old_color] += old_cap + observed = sum(value > 0 for value in adjusted) <= EMPTY_COLUMNS + 1 + + # In the (uncanonicalized) terminal coordinates the three non-q debts are + # positive. The sibling move makes q positive and subtracts ``cap`` from + # exactly one of those three. Hence the bad source persists precisely + # when that selected terminal-positive debt is no larger than ``cap``. + selected_terminal_debt = edge.parent[next_color][0] + if next_color == old_color: + selected_terminal_debt += old_cap + predicted = selected_terminal_debt <= cap + require(observed == predicted, "bad-source persistence formula disagrees with replay") + return observed + + +def state_to_json(state: State) -> list[dict[str, object]]: + return [ + {"debt": debt, "caps": list(caps), "exposed": debt + sum(caps)} + for debt, caps in state + ] + + +def edge_to_public_row(edge: BadEdge, ordinal: int) -> dict[str, object]: + q_color = edge.action[2] + raw_single = sum(len(next_cards(q_color, cap)) for cap in edge.sibling_caps) + raw_decorations = 1 + for cap in edge.sibling_caps: + raw_decorations *= len(next_cards(q_color, cap)) + + feasible = 0 + completions = 0 + persistent_source_cards = 0 + nonpersistent_source_cards = 0 + both_bad_persistent = 0 + direct_exhaustion = 0 + bad_source_persistent_decorations = 0 + obstruction_decorations = 0 + for cards in itertools.product( + next_cards(q_color, edge.sibling_caps[0]), + next_cards(q_color, edge.sibling_caps[1]), + ): + typed_cards = cards # narrow type for static readers + for sibling, card in enumerate(typed_cards): + replay_persistence_formula(edge, sibling, card) + word_count = remaining_tail_word_count(edge, typed_cards) # type: ignore[arg-type] + if word_count == 0: + continue + feasible += 1 + completions += word_count + bad_flags = tuple( + bad_source_persists(edge, sibling, card) + for sibling, card in enumerate(typed_cards) + ) + persistent_source_cards += sum(bad_flags) + nonpersistent_source_cards += len(bad_flags) - sum(bad_flags) + both_bad_persistent += int(all(bad_flags)) + direct = any(card[1] == HEIGHT for card in typed_cards) + persistent = any(bad_flags) + direct_exhaustion += int(direct) + bad_source_persistent_decorations += int(persistent) + obstruction_decorations += int(not direct and not persistent) + + return { + "id": f"edge-{ordinal:02d}", + "parent": state_to_json(edge.parent), + "terminal": state_to_json(edge.terminal), + "bad_action": list(edge.action), + "sibling_caps": list(edge.sibling_caps), + "raw_single_next_run_outcomes": raw_single, + "raw_simultaneous_decorations": raw_decorations, + "feasible_decorations": feasible, + "fixed_future_completions": completions, + "persistent_bad_source_cards": persistent_source_cards, + "nonpersistent_bad_source_cards": nonpersistent_source_cards, + "both_bad_sources_persistent_decorations": both_bad_persistent, + "direct_exhaustion_decorations": direct_exhaustion, + "bad_source_persistent_decorations": bad_source_persistent_decorations, + "obstruction_decorations": obstruction_decorations, + } + + +def independent_census() -> dict[str, object]: + terminals = enumerate_tq_terminals() + require(len(terminals) == EXPECTED_TERMINALS, "Tq terminal count is not 71") + pairs = reverse_live_pairs(terminals) + require(len(pairs) == EXPECTED_LIVE_EDGES, "same-z live edge count is not 116") + require( + len({parent for parent, _ in pairs}) == EXPECTED_LIVE_PARENTS, + "same-z live parent count is not 80", + ) + edges = sibling_bad_edges(pairs) + require(len(edges) == EXPECTED_BAD_EDGES, "sibling bad-edge count is not 32") + require( + len({edge.parent for edge in edges}) == EXPECTED_SIBLING_PARENTS, + "sibling parent count is not 23", + ) + require( + all(apply_live_action(edge.parent, edge.action) == edge.terminal for edge in edges), + "a bad-edge witness failed forward replay", + ) + + rows = [edge_to_public_row(edge, ordinal) for ordinal, edge in enumerate(edges)] + raw_single = sum(int(row["raw_single_next_run_outcomes"]) for row in rows) + raw_decorations = sum(int(row["raw_simultaneous_decorations"]) for row in rows) + feasible = sum(int(row["feasible_decorations"]) for row in rows) + completions = sum(int(row["fixed_future_completions"]) for row in rows) + direct_exhaustion = sum(int(row["direct_exhaustion_decorations"]) for row in rows) + persistent = sum(int(row["bad_source_persistent_decorations"]) for row in rows) + obstruction = sum(int(row["obstruction_decorations"]) for row in rows) + require(raw_single == EXPECTED_RAW_SINGLE_OUTCOMES, "raw single-card count is not 840") + require(raw_decorations == EXPECTED_RAW_DECORATIONS, "raw decoration count is not 5526") + require(feasible == EXPECTED_FEASIBLE_DECORATIONS, "feasible count is not 2958") + require(completions == EXPECTED_FIXED_FUTURES, "fixed-future count is not 10073448") + per_edge_futures = [int(row["fixed_future_completions"]) for row in rows] + require(all(count > 0 for count in per_edge_futures), "a bad edge has no fixed future") + require( + min(per_edge_futures) == EXPECTED_MIN_EDGE_FUTURES, + "minimum per-edge fixed-future count is not 924", + ) + require( + max(per_edge_futures) == EXPECTED_MAX_EDGE_FUTURES, + "maximum per-edge fixed-future count is not 3963960", + ) + sample_audit = audit_checkpoint_samples(edges) + + return { + "schema_version": 1, + "terminal_count": len(terminals), + "same_z_live_parent_count": len({parent for parent, _ in pairs}), + "same_z_live_edge_count": len(pairs), + "sibling_parent_count": len({edge.parent for edge in edges}), + "bad_edge_count": len(edges), + "raw_single_next_run_outcomes": raw_single, + "raw_simultaneous_decorations": raw_decorations, + "feasible_decorations": feasible, + "fixed_future_completions": completions, + "direct_exhaustion_decorations": direct_exhaustion, + "bad_source_persistent_decorations": persistent, + "obstruction_decorations": obstruction, + **sample_audit, + "per_edge": rows, + "_edges": edges, + } + + +def parse_state(value: object) -> State: + require(isinstance(value, list) and len(value) == COLORS, f"bad state: {value!r}") + buckets: list[Bucket] = [] + for bucket in value: + if isinstance(bucket, dict): + debt = bucket.get("debt") + caps = bucket.get("caps") + else: + require( + isinstance(bucket, list) and len(bucket) >= 2, + f"bad bucket: {bucket!r}", + ) + debt, caps = bucket[0], bucket[1] + require(isinstance(debt, int), f"bad debt in {bucket!r}") + require( + isinstance(caps, list) and all(isinstance(cap, int) for cap in caps), + f"bad caps in {bucket!r}", + ) + buckets.append((debt, tuple(caps))) + state = tuple(buckets) + require(tuple(sorted(state)) == state, "reported state is not canonical") + return state # type: ignore[return-value] + + +def normalized_report_edge(row: dict[str, object]) -> tuple[State, State, Action]: + parent = parse_state(row.get("parent")) + terminal = parse_state(row.get("terminal")) + action_value = row.get("bad_action", row.get("action")) + require( + isinstance(action_value, list) + and len(action_value) == 4 + and all(isinstance(item, int) for item in action_value), + "edge has no four-integer bad action", + ) + action = tuple(action_value) + require(apply_live_action(parent, action) == terminal, "reported bad edge does not replay") + return parent, terminal, action # type: ignore[return-value] + + +def validate_report( + report: dict[str, object], + census: dict[str, object], + expected_bound: int | None = None, +) -> None: + require(report.get("schema_version") == 1, "unsupported production schema") + for key in ( + "terminal_count", + "sibling_parent_count", + "bad_edge_count", + "raw_single_next_run_outcomes", + "raw_simultaneous_decorations", + "feasible_decorations", + "fixed_future_completions", + "direct_exhaustion_decorations", + "bad_source_persistent_decorations", + "obstruction_decorations", + ): + require(report.get(key) == census[key], f"report field {key} disagrees with audit") + + require(report.get("self_checks_passed") is True, "production self-checks did not pass") + for key in ("next_run_census_complete", "residual_word_universe_complete"): + require(isinstance(report.get(key), bool), f"{key} is not Boolean") + require(report.get("next_run_census_complete") is True, "next-run census is incomplete") + residual_expected = report.get("residual_words_expected") + require( + residual_expected == EXPECTED_FIXED_FUTURES, + "residual_words_expected disagrees with the independent tail DP", + ) + checked = report.get("residual_words_checked") + require(isinstance(checked, int) and checked > 0, "bad residual_words_checked") + yes = report.get("checkpoint_yes_count") + no = report.get("local_no_count") + global_no = report.get("global_no_count") + require( + isinstance(yes, int) and isinstance(no, int) and isinstance(global_no, int), + "missing checkpoint classification counts", + ) + require(yes + no == checked, "checkpoint classifications do not sum to checked residuals") + require( + report.get("both_siblings_safe_count") == checked, + "not every checked residual reports both q siblings safe", + ) + + status = report.get("status") + allowed = { + "ENTRY_FAMILY_ELIMINATED", + "RESIDUALS_EXPORTED", + "GLOBAL_NO_FOUND", + "INCOMPLETE", + } + require(status in allowed, f"bad status {status!r}") + if status == "INCOMPLETE": + if expected_bound is not None: + require( + checked == min(expected_bound, EXPECTED_FIXED_FUTURES), + "bounded job missed its requested limit", + ) + require(report.get("verified") is False, "incomplete report claims verification") + require(report.get("universe_complete") is False, "incomplete report claims completeness") + require(global_no == 0, "incomplete report claims a global NO") + elif status == "ENTRY_FAMILY_ELIMINATED": + require(checked == EXPECTED_FIXED_FUTURES, "elimination missed residual words") + require(yes == checked and no == 0, "elimination contains a local NO") + require(global_no == 0, "elimination also claims a global NO") + require(report.get("verified") is True, "elimination is not verified") + require(report.get("universe_complete") is True, "elimination lacks completeness") + require( + report.get("residual_word_universe_complete") is True, + "elimination lacks a complete residual-word universe", + ) + elif status == "RESIDUALS_EXPORTED": + require(checked == EXPECTED_FIXED_FUTURES, "residual export missed words") + require(no >= 1, "residual export has no local NO") + require(global_no == 0, "residual export incorrectly claims a global NO") + require(report.get("verified") is True, "residual export is not verified") + require(report.get("universe_complete") is True, "residual export lacks completeness") + require( + report.get("residual_word_universe_complete") is True, + "residual export is not exhaustive", + ) + else: + require(global_no >= 1, "GLOBAL_NO_FOUND has no global classification") + require(report.get("verified") is True, "global NO is not verified") + + rows_value = report.get("per_edge") + require(isinstance(rows_value, list), "production report has no per_edge array") + rows: list[dict[str, object]] = rows_value # type: ignore[assignment] + require(len(rows) == EXPECTED_BAD_EDGES, "production per_edge length is not 32") + expected_rows: list[dict[str, object]] = census["per_edge"] # type: ignore[assignment] + expected_by_key = { + ( + parse_state(row["parent"]), + parse_state(row["terminal"]), + tuple(row["bad_action"]), + ): row + for row in expected_rows + } + seen: set[tuple[State, State, Action]] = set() + abstract_samples = 0 + summed_both_siblings_safe = 0 + for row in rows: + key = normalized_report_edge(row) + require(key in expected_by_key, "production report contains an unknown bad edge") + require(key not in seen, "production report duplicates a bad edge") + seen.add(key) + expected = expected_by_key[key] + for field, expected_field in ( + ("raw_single_next_run_outcomes", "raw_single_next_run_outcomes"), + ("raw_simultaneous_decorations", "raw_simultaneous_decorations"), + ("feasible_decorations", "feasible_decorations"), + ("residual_words_expected", "fixed_future_completions"), + ): + require(row.get(field) == expected[expected_field], f"per-edge {field} mismatch") + columns = row.get("columns") + action = expected["bad_action"] + sibling_caps = expected["sibling_caps"] + expected_columns = [ + [action[0], action[1]], + [action[2], sibling_caps[0]], + [action[2], sibling_caps[1]], + ] + require(columns == expected_columns, "per-edge active columns mismatch") + both = row.get("both_siblings_safe_count") + row_checked = row.get("residual_words_checked") + require(isinstance(both, int) and isinstance(row_checked, int), "bad per-edge checked counts") + require(both == row_checked, "not every checked residual has both q siblings safe") + summed_both_siblings_safe += both + expected_edge = BadEdge(key[0], key[1], key[2], tuple(sibling_caps)) # type: ignore[arg-type] + abstract_samples += int(replay_abstract_sample(expected_edge, row.get("sample"))) + require(len(seen) == EXPECTED_BAD_EDGES, "production edge cover is incomplete") + require(summed_both_siblings_safe == checked, "both-sibling-safe total misses residuals") + if status != "INCOMPLETE": + require(abstract_samples == EXPECTED_BAD_EDGES, "complete report lacks one sample per edge") + + replay_all_witnesses(report) + + +def parse_columns(value: object) -> tuple[tuple[int, ...], ...]: + if isinstance(value, str): + value = value.split("|") + require(isinstance(value, list) and len(value) == COLORS, f"bad columns: {value!r}") + columns = [] + for raw in value: + require(isinstance(raw, str) and len(raw) == HEIGHT, f"bad column {raw!r}") + require(all(character in "0123" for character in raw), f"bad color in {raw!r}") + columns.append(tuple(int(character) for character in raw)) + counts = Counter(color for column in columns for color in column) + require(counts == Counter({0: 7, 1: 7, 2: 7, 3: 7}), f"unbalanced witness {counts}") + return tuple(columns) + + +def column_borders(column: Sequence[int]) -> tuple[int, ...]: + return (0,) + tuple( + position + for position in range(1, HEIGHT) + if column[position - 1] != column[position] + ) + + +def removal_is_legal( + columns: Sequence[Sequence[int]], ranks: Sequence[int], source: int +) -> bool: + borders = [column_borders(column) for column in columns] + if source not in range(COLORS) or ranks[source] == 0: + return False + exposed = [0] * COLORS + hosted = [0] * COLORS + exhausted = 0 + for column, rank in enumerate(ranks): + if rank == 0: + exhausted += 1 + border = borders[column][rank] + for position in range(border, HEIGHT): + exposed[columns[column][position]] += 1 + if rank: + hosted[columns[column][border]] += HEIGHT - border + + border = borders[source][ranks[source]] + top = columns[source][border] + cap = HEIGHT - border + adjusted = [exposed[color] - hosted[color] for color in range(COLORS)] + adjusted[top] += cap + return sum(value > 0 for value in adjusted) <= EMPTY_COLUMNS + exhausted + + +def parse_moves(value: object) -> tuple[int, ...]: + if isinstance(value, str): + require(all(character in "0123" for character in value), f"bad move string {value!r}") + return tuple(int(character) for character in value) + require( + isinstance(value, list) and all(isinstance(move, int) for move in value), + f"bad move sequence {value!r}", + ) + return tuple(value) + + +def replay_removals( + columns: Sequence[Sequence[int]], ranks: Sequence[int], moves: Sequence[int] +) -> tuple[int, ...]: + borders = [column_borders(column) for column in columns] + current = list(ranks) + require( + len(current) == COLORS + and all(0 <= current[i] < len(borders[i]) for i in range(COLORS)), + f"bad checkpoint ranks {ranks!r}", + ) + for step, source in enumerate(moves): + require(removal_is_legal(columns, current, source), f"illegal witness step {step}") + current[source] -= 1 + return tuple(current) + + +def replay_witness(value: dict[str, object]) -> None: + columns_value = value.get("columns", value.get("layout")) + require(columns_value is not None, "witness has no columns") + columns = parse_columns(columns_value) + borders = [column_borders(column) for column in columns] + initial_ranks = tuple(len(items) - 1 for items in borders) + + checkpoint_value = value.get("checkpoint_ranks") + prefix_value = value.get("prefix_removal_columns", value.get("prefix_removals")) + if checkpoint_value is None: + checkpoint = initial_ranks + else: + require( + isinstance(checkpoint_value, list) + and len(checkpoint_value) == COLORS + and all(isinstance(rank, int) for rank in checkpoint_value), + "bad checkpoint_ranks", + ) + checkpoint = tuple(checkpoint_value) + if prefix_value is not None: + reached = replay_removals(columns, initial_ranks, parse_moves(prefix_value)) + require(reached == checkpoint, "prefix witness does not reach checkpoint") + + move_value = next( + ( + value[key] + for key in ( + "removal_columns", + "removal_sequence", + "escape_removal_columns", + "escape_removals", + ) + if key in value + ), + None, + ) + require(move_value is not None, "witness has no removal sequence") + final_ranks = replay_removals(columns, checkpoint, parse_moves(move_value)) + target = value.get("target_exhausted_columns") + if isinstance(target, int): + require(sum(rank == 0 for rank in final_ranks) >= target, "witness misses target") + else: + require( + all(rank == 0 for rank in final_ranks) + or sum(rank == 0 for rank in final_ranks) >= 2, + "witness reaches neither state zero nor the two-column frontier", + ) + + +def replay_all_witnesses(report: dict[str, object]) -> None: + """Find and replay every nested object that declares concrete columns.""" + + found = 0 + concrete_layouts = 0 + + def visit(value: object) -> None: + nonlocal found, concrete_layouts + if isinstance(value, dict): + layout_value = value.get("columns", value.get("layout")) + has_columns = ( + isinstance(layout_value, str) + and len(layout_value.split("|")) == COLORS + ) or ( + isinstance(layout_value, list) + and len(layout_value) == COLORS + and all(isinstance(column, str) for column in layout_value) + ) + has_moves = any( + key in value + for key in ( + "removal_columns", + "removal_sequence", + "escape_removal_columns", + "escape_removals", + ) + ) + if has_columns: + parse_columns(layout_value) + concrete_layouts += 1 + if has_columns and has_moves: + replay_witness(value) + found += 1 + for child in value.values(): + visit(child) + elif isinstance(value, list): + for child in value: + visit(child) + + visit(report) + declared = report.get("witness_count") + if isinstance(declared, int): + require(found == declared, f"replayed {found} witnesses, report declares {declared}") + if report.get("status") == "GLOBAL_NO_FOUND": + # A NO certificate has no winning removal sequence to replay. The + # workflow separately invokes the independent oracle/verifier; here we + # still require its complete balanced 4x7 instance to be embedded. + require(concrete_layouts >= 1, "GLOBAL_NO_FOUND report has no complete layout") + + +def run_program(program: Path, census: dict[str, object], limit: int) -> None: + edges: tuple[BadEdge, ...] = census["_edges"] # type: ignore[assignment] + bounded = bounded_checkpoint_audit(edges, min(limit, EXPECTED_FIXED_FUTURES)) + with tempfile.TemporaryDirectory(prefix="c4-h7-tq-sibling-audit-") as temporary: + output = Path(temporary) / "out" + command = [ + str(program), + "--output-dir", + str(output), + "--limit", + str(limit), + "--self-test", + ] + completed = subprocess.run(command, text=True, capture_output=True, check=False) + require( + completed.returncode == 0, + "production program failed:\n" + + completed.stdout + + ("\n" if completed.stdout and completed.stderr else "") + + completed.stderr, + ) + report_path = output / "report.json" + require(report_path.is_file(), "production program did not write report.json") + report = json.loads(report_path.read_text(encoding="utf-8")) + require(isinstance(report, dict), "production report root is not an object") + validate_report(report, census, limit) + require( + report.get("residual_words_checked") == bounded["checked"], + "production and independent bounded jobs checked different totals", + ) + require( + report.get("checkpoint_yes_count") == bounded["yes"] + and report.get("local_no_count") == bounded["no"], + "production bounded classifications disagree with independent DP", + ) + if "bounded_prefix_sha256" in report: + require( + report["bounded_prefix_sha256"] == bounded["sha256"], + "bounded residual prefix checksum mismatch", + ) + + +def read_and_validate_report( + report_path: Path, census: dict[str, object], expected_bound: int | None = None +) -> None: + require(report_path.is_file(), f"report not found: {report_path}") + report = json.loads(report_path.read_text(encoding="utf-8")) + require(isinstance(report, dict), "production report root is not an object") + validate_report(report, census, expected_bound) + + +def schema_negative_tests(census: dict[str, object]) -> None: + """Small mutation checks ensure core census fields are not accepted blindly.""" + + census_rows: list[dict[str, object]] = census["per_edge"] # type: ignore[assignment] + production_rows: list[dict[str, object]] = [] + for index, row in enumerate(census_rows): + action = row["bad_action"] + sibling_caps = row["sibling_caps"] + checked = int(index == 0) + production_rows.append( + { + "edge_id": f"tq-sibling-e{index}", + "parent": copy.deepcopy(row["parent"]), + "terminal": copy.deepcopy(row["terminal"]), + "bad_action": list(action), + "columns": [ + [action[0], action[1]], + [action[2], sibling_caps[0]], + [action[2], sibling_caps[1]], + ], + "raw_single_next_run_outcomes": row["raw_single_next_run_outcomes"], + "raw_simultaneous_decorations": row["raw_simultaneous_decorations"], + "feasible_decorations": row["feasible_decorations"], + "residual_words_expected": row["fixed_future_completions"], + "residual_words_checked": checked, + "checkpoint_yes_count": checked, + "local_no_count": 0, + "safe_source_counts": [checked, checked, checked], + "both_siblings_safe_count": checked, + "sample": None, + } + ) + + skeleton = { + "schema_version": 1, + "verified": False, + "status": "INCOMPLETE", + "universe_complete": False, + "self_checks_passed": True, + "next_run_census_complete": True, + "residual_word_universe_complete": False, + "terminal_count": census["terminal_count"], + "sibling_parent_count": census["sibling_parent_count"], + "bad_edge_count": census["bad_edge_count"], + "raw_single_next_run_outcomes": census["raw_single_next_run_outcomes"], + "raw_simultaneous_decorations": census["raw_simultaneous_decorations"], + "feasible_decorations": census["feasible_decorations"], + "fixed_future_completions": census["fixed_future_completions"], + "direct_exhaustion_decorations": census["direct_exhaustion_decorations"], + "bad_source_persistent_decorations": census["bad_source_persistent_decorations"], + "obstruction_decorations": census["obstruction_decorations"], + "residual_words_expected": census["fixed_future_completions"], + "residual_words_checked": 1, + "checkpoint_yes_count": 1, + "local_no_count": 0, + "global_no_count": 0, + "both_siblings_safe_count": 1, + "per_edge": production_rows, + } + validate_report(skeleton, census, 1) + for field in ( + "terminal_count", + "sibling_parent_count", + "bad_edge_count", + "raw_simultaneous_decorations", + "feasible_decorations", + "fixed_future_completions", + ): + mutant = copy.deepcopy(skeleton) + mutant[field] = int(mutant[field]) + 1 + try: + validate_report(mutant, census, 1) + except AssertionError: + pass + else: + raise AssertionError(f"validator accepted a corrupted {field}") + + +def parse_args(argv: Sequence[str] | None = None) -> argparse.Namespace: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--program", type=Path, help="bounded production executable") + parser.add_argument("--report", type=Path, help="validate an existing production report") + parser.add_argument("--limit", type=int, default=64, help="production differential bound") + parser.add_argument("--json", type=Path, dest="json_path", help="write audit summary") + return parser.parse_args(argv) + + +def main(argv: Sequence[str] | None = None) -> int: + args = parse_args(argv) + require(args.limit > 0, "--limit must be positive") + census = independent_census() + schema_negative_tests(census) + if args.program: + require(args.program.is_file(), f"program not found: {args.program}") + run_program(args.program.resolve(), census, args.limit) + if args.report: + read_and_validate_report(args.report, census) + + public = {key: value for key, value in census.items() if not key.startswith("_")} + text = json.dumps(public, indent=2, sort_keys=True) + "\n" + if args.json_path: + args.json_path.parent.mkdir(parents=True, exist_ok=True) + args.json_path.write_text(text, encoding="utf-8") + else: + print( + "PASS: " + f"Tq={census['terminal_count']}, sibling parents={census['sibling_parent_count']}, " + f"bad edges={census['bad_edge_count']}, decorations={census['raw_simultaneous_decorations']}, " + f"feasible={census['feasible_decorations']}, futures={census['fixed_future_completions']}, " + f"checkpoint samples={census['checkpoint_sample_yes']}/{census['checkpoint_samples']} YES" + ) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main())