diff --git a/.github/workflows/c4-h7-tq-exhaust-siblings.yml b/.github/workflows/c4-h7-tq-exhaust-siblings.yml new file mode 100644 index 0000000..fafefad --- /dev/null +++ b/.github/workflows/c4-h7-tq-exhaust-siblings.yml @@ -0,0 +1,149 @@ +name: Census first-exhaustion Tq sibling forks +run-name: Audit the c4 k2 h7 first-exhaustion Tq next-run universe + +on: + push: + branches: [codex/c4-h7-tq-exhaust-siblings] + workflow_dispatch: + +permissions: + contents: read + +concurrency: + group: c4-h7-tq-exhaust-siblings-${{ github.ref }} + cancel-in-progress: true + +jobs: + build-and-audit: + 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 focused census program + run: >- + cmake --build build + --target water-c4-h7-tq-exhaust-siblings + --parallel 2 + - name: Run its focused C++ test + run: >- + ctest --test-dir build --output-on-failure + --no-tests=error + -R '^water-c4-h7-tq-exhaust-siblings-smoke$' + - name: Run the built-in structural self-test + run: | + mkdir -p out/build-audit + set -o pipefail + build/water-c4-h7-tq-exhaust-siblings --self-test 2>&1 \ + | tee out/build-audit/self-test.log + - name: Independently rebuild the census and run a bounded differential + run: | + set -o pipefail + python tests/check_c4_h7_tq_exhaust_siblings.py \ + --program build/water-c4-h7-tq-exhaust-siblings \ + --limit 257 \ + --json out/build-audit/independent-audit.json 2>&1 \ + | tee out/build-audit/independent.log + - name: Preserve a bounded artifact for strict validation + run: >- + build/water-c4-h7-tq-exhaust-siblings + --limit 257 + --output-dir out/build-audit/bounded + - name: Strictly reject claims beyond the bounded run + run: >- + python scripts/validate_c4_h7_tq_exhaust_siblings_report.py + --report out/build-audit/bounded/report.json + --output-dir out/build-audit/bounded + --audit out/build-audit/independent-audit.json + --status-file out/build-audit/bounded/status.txt + - name: Confirm the bounded status + run: test "$(tr -d '\r\n' < out/build-audit/bounded/status.txt)" = INCOMPLETE + - name: Configure the Clang sanitizer smoke build + run: >- + cmake -S . -B build-sanitize + -DCMAKE_BUILD_TYPE=Debug + -DCMAKE_CXX_COMPILER=clang++ + -DWSC_WARNINGS_AS_ERRORS=ON + -DCMAKE_CXX_FLAGS='-fsanitize=address,undefined -fno-omit-frame-pointer' + -DCMAKE_EXE_LINKER_FLAGS='-fsanitize=address,undefined' + - name: Build and run the sanitizer smoke test + env: + ASAN_OPTIONS: detect_leaks=1:halt_on_error=1 + UBSAN_OPTIONS: halt_on_error=1:print_stacktrace=1 + run: | + cmake --build build-sanitize \ + --target water-c4-h7-tq-exhaust-siblings --parallel 2 + build-sanitize/water-c4-h7-tq-exhaust-siblings --self-test + - uses: actions/upload-artifact@v6 + if: always() + with: + name: c4-h7-tq-exhaust-build-audit-${{ github.run_id }} + path: out/build-audit/ + if-no-files-found: error + retention-days: 30 + + next-run-census: + runs-on: ubuntu-latest + timeout-minutes: 30 + steps: + - uses: actions/checkout@v5 + - uses: actions/setup-python@v5 + with: + python-version: "3.12" + - name: Configure and build the Release census program + run: | + cmake -S . -B build \ + -DCMAKE_BUILD_TYPE=Release \ + -DWSC_WARNINGS_AS_ERRORS=ON + cmake --build build \ + --target water-c4-h7-tq-exhaust-siblings --parallel 2 + - name: Enumerate all 1,256,148 next-run decorations + run: | + mkdir -p out/census + set -o pipefail + build/water-c4-h7-tq-exhaust-siblings \ + --output-dir out/census 2>&1 | tee out/census/run.log + - name: Independently audit the complete report and replay its samples + run: | + set -o pipefail + python tests/check_c4_h7_tq_exhaust_siblings.py \ + --report out/census/report.json \ + --json out/census/independent-audit.json 2>&1 \ + | tee out/census/independent.log + - name: Strictly validate status and claim boundaries + run: >- + python scripts/validate_c4_h7_tq_exhaust_siblings_report.py + --report out/census/report.json + --output-dir out/census + --audit out/census/independent-audit.json + --status-file out/census/status.txt + - name: Require the exact complete-census status + run: test "$(tr -d '\r\n' < out/census/status.txt)" = NEXT_RUN_CENSUS_COMPLETE + - name: Record the intentionally limited conclusion + run: | + cat >> "$GITHUB_STEP_SUMMARY" <<'EOF' + > This job completely enumerates the 1,256,148 committed next-run decorations only. It does not enumerate the 6,131,033,832 residual words, eliminate the entry family, or prove all c4/k2/h7 layouts solvable. + EOF + cat out/census/summary.md >> "$GITHUB_STEP_SUMMARY" + - name: Create and verify the SHA-256 manifest + if: always() + run: | + mkdir -p out/census + find out/census -type f ! -name SHA256SUMS -print0 \ + | sort -z \ + | xargs -0 -r sha256sum > out/census/SHA256SUMS + sha256sum --check out/census/SHA256SUMS + - uses: actions/upload-artifact@v6 + if: always() + with: + name: c4-h7-tq-exhaust-next-run-census-${{ github.run_id }} + path: out/census/ + if-no-files-found: error + retention-days: 30 diff --git a/CMakeLists.txt b/CMakeLists.txt index a0820a8..8068aa7 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -102,6 +102,19 @@ else() endif() endif() +add_executable(water-c4-h7-tq-exhaust-siblings apps/c4_h7_tq_exhaust_siblings.cpp) +if(MSVC) + target_compile_options(water-c4-h7-tq-exhaust-siblings PRIVATE /W4) + if(WSC_WARNINGS_AS_ERRORS) + target_compile_options(water-c4-h7-tq-exhaust-siblings PRIVATE /WX) + endif() +else() + target_compile_options(water-c4-h7-tq-exhaust-siblings PRIVATE -Wall -Wextra -Wpedantic) + if(WSC_WARNINGS_AS_ERRORS) + target_compile_options(water-c4-h7-tq-exhaust-siblings PRIVATE -Werror) + endif() +endif() + include(CTest) if(BUILD_TESTING) add_executable(water-sort-tests tests/test_main.cpp) @@ -114,6 +127,11 @@ if(BUILD_TESTING) --self-test --limit 64 --output-dir ${CMAKE_CURRENT_BINARY_DIR}/test-c4-h7-tq-sibling-forks-output) + add_test(NAME water-c4-h7-tq-exhaust-siblings-smoke + COMMAND water-c4-h7-tq-exhaust-siblings + --self-test + --limit 64 + --output-dir ${CMAKE_CURRENT_BINARY_DIR}/test-c4-h7-tq-exhaust-siblings-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_exhaust_siblings.cpp b/apps/c4_h7_tq_exhaust_siblings.cpp new file mode 100644 index 0000000..e5d5c7c --- /dev/null +++ b/apps/c4_h7_tq_exhaust_siblings.cpp @@ -0,0 +1,1337 @@ +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include + +namespace { + +constexpr int kHeight = 7; +constexpr int kColors = 4; +constexpr int kEmpty = 2; + +constexpr std::uint64_t kExpectedTqTerminals = 71; +constexpr std::uint64_t kExpectedLabeledCandidates = 624; +constexpr std::uint64_t kExpectedCanonicalParents = 418; +constexpr std::uint64_t kExpectedCanonicalEdges = 429; +constexpr std::uint64_t kExpectedUniqueParents = 6; +constexpr std::uint64_t kExpectedSiblingParents = 412; +constexpr std::uint64_t kExpectedUniqueEdges = 6; +constexpr std::uint64_t kExpectedSiblingEdges = 423; +constexpr std::uint64_t kExpectedLegalSiblingCards = 18177; +constexpr std::uint64_t kExpectedLegalSiblingJoint = 1220361; +constexpr std::uint64_t kExpectedAllQJoint = 1256148; +constexpr std::uint64_t kExpectedFeasible = 403685; +constexpr std::uint64_t kExpectedNonnegative = 406528; +constexpr std::uint64_t kExpectedResidualWords = 6131033832ULL; +constexpr std::uint64_t kExpectedTwoExhaustion = 70633; +constexpr std::uint64_t kExpectedTwoExhaustionWords = 8629839; +constexpr std::uint64_t kExpectedLiveHandoff = 254899; +constexpr std::uint64_t kExpectedLiveHandoffWords = 3235811235ULL; +constexpr std::uint64_t kExpectedObstruction = 78153; +constexpr std::uint64_t kExpectedObstructionWords = 2886592758ULL; +constexpr std::uint64_t kExpectedDirectCertified = 101922; +constexpr std::uint64_t kExpectedDirectCertifiedWords = 13128393; +constexpr std::uint64_t kExpectedHandoffNGe3 = 11226; +constexpr std::uint64_t kExpectedHandoffNGe3Words = 10591970; +constexpr std::uint64_t kExpectedHandoffNLe2 = 223321; +constexpr std::uint64_t kExpectedHandoffNLe2Words = 3223219144ULL; +constexpr std::uint64_t kExpectedD2Reduction = 67206; +constexpr std::uint64_t kExpectedD2ReductionWords = 2883858705ULL; +constexpr std::uint64_t kExpectedTqCornerOnly = 10; +constexpr std::uint64_t kExpectedTqCornerOnlyWords = 235620; + +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; +using Caps = std::array, kColors>; + +struct Source { + int color = 0; + int cap = 0; +}; + +struct ExhaustAction { + int old_color = 0; + int old_cap = 0; + int final_color = 0; + + bool operator<(const ExhaustAction& other) const { + return std::tie(old_color, old_cap, final_color) < + std::tie(other.old_color, other.old_cap, other.final_color); + } +}; + +struct Card { + int color = 0; + int endpoint = 0; +}; + +struct Edge { + std::size_t ordinal = 0; + State parent; + State terminal; + ExhaustAction bad; + Debts terminal_debts{}; // Labeled in the parent's color coordinates. + int q_color = -1; + std::array q_caps{}; + int legal_source_count = 0; + bool old_bad_equals_q = false; + std::uint64_t raw_expected = 0; +}; + +struct ClassStats { + std::uint64_t decorations = 0; + std::uint64_t residual_words = 0; +}; + +struct Sample { + std::string id; + std::size_t edge = 0; + std::array cards{}; + std::array free_tail_lengths{}; + Counts residual_after_forced{}; + std::uint64_t completion_count = 0; + std::string classification; + // Column order is bad, q0, q1, q2. Each word is bottom-to-top. + std::array, 4> hidden_words; +}; + +struct DecorationKey { + std::size_t edge = 0; + std::array cards{}; +}; + +struct EdgeStats { + std::uint64_t raw_checked = 0; + std::uint64_t nonnegative = 0; + std::uint64_t feasible = 0; + std::uint64_t infeasible = 0; + std::uint64_t residual_words = 0; + ClassStats two_exhaustion; + ClassStats live_handoff; + ClassStats obstruction; + std::uint64_t handoff_n_ge_3 = 0; + std::uint64_t handoff_n_ge_3_words = 0; + std::uint64_t handoff_n_le_2 = 0; + std::uint64_t handoff_n_le_2_words = 0; + std::uint64_t immediate_tq_corner = 0; + std::uint64_t immediate_tq_corner_words = 0; + ClassStats direct_certified; + ClassStats n_ge_3_certified; + ClassStats n_le_2_certified; + ClassStats d2_reduction; + ClassStats tq_corner_only; + std::optional sample; +}; + +struct Bridge { + std::vector edges; + std::uint64_t terminal_count = 0; + std::uint64_t labeled_candidates = 0; + std::uint64_t canonical_parent_count = 0; + std::uint64_t canonical_edge_count = 0; + std::uint64_t unique_parent_count = 0; + std::uint64_t sibling_parent_count = 0; + std::uint64_t unique_edge_count = 0; + std::uint64_t sibling_edge_count = 0; + std::map parent_legal_distribution; + std::map edge_legal_distribution; + bool action_unique = true; + bool all_edges_replay = true; + bool all_final_colors_isolated = true; +}; + +struct RunStats { + bool self_checks_passed = false; + bool next_run_universe_complete = false; + std::uint64_t limit_requested = 0; + std::uint64_t legal_sibling_cards = 0; + std::uint64_t legal_sibling_joint = 0; + std::uint64_t all_q_joint = 0; + std::uint64_t raw_checked = 0; + std::uint64_t nonnegative = 0; + std::uint64_t feasible = 0; + std::uint64_t infeasible = 0; + std::uint64_t residual_words = 0; + ClassStats two_exhaustion; + ClassStats live_handoff; + ClassStats obstruction; + std::uint64_t handoff_n_ge_3 = 0; + std::uint64_t handoff_n_ge_3_words = 0; + std::uint64_t handoff_n_le_2 = 0; + std::uint64_t handoff_n_le_2_words = 0; + std::uint64_t immediate_tq_corner = 0; + std::uint64_t immediate_tq_corner_words = 0; + std::uint64_t immediate_tq_corner_card_count = 0; + std::uint64_t immediate_tq_corner_edge_count = 0; + std::uint64_t immediate_tq_corner_parent_count = 0; + std::map immediate_tq_corner_m_distribution; + ClassStats direct_certified; + ClassStats n_ge_3_certified; + ClassStats n_le_2_certified; + ClassStats d2_reduction; + ClassStats tq_corner_only; + std::vector per_edge; + std::vector samples; + std::vector checked_prefix; + double elapsed_seconds = 0.0; +}; + +void require(bool condition, const std::string& message) { + if (!condition) throw std::runtime_error("self-check failed: " + message); +} + +void usage() { + std::cerr << "Usage: water-c4-h7-tq-exhaust-siblings " + "[--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, Caps caps) { + State result; + for (int color = 0; color < kColors; ++color) { + std::sort(caps[color].begin(), caps[color].end()); + result[static_cast(color)] = {debts[color], caps[color]}; + } + std::sort(result.begin(), result.end()); + return result; +} + +Debts state_debts(const State& state) { + Debts result{}; + for (int color = 0; color < kColors; ++color) result[color] = state[color].debt; + return result; +} + +Caps state_caps(const State& state) { + Caps result; + for (int color = 0; color < kColors; ++color) result[color] = state[color].caps; + return result; +} + +Counts exposed_counts(const State& state) { + Counts result{}; + for (int color = 0; color < kColors; ++color) { + result[color] = state[color].debt; + for (const int cap : state[color].caps) result[color] += cap; + } + return result; +} + +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 Counts exposed = exposed_counts(state); + Counts remaining{}; + for (int color = 0; color < kColors; ++color) { + if (exposed[color] < multiplicity[color] || exposed[color] > kHeight) return false; + remaining[color] = kHeight - exposed[color]; + } + for (int color = 0; color < kColors; ++color) { + int allowed = 0; + for (int other = 0; other < kColors; ++other) { + if (other != color) allowed += remaining[other]; + } + if (multiplicity[color] > allowed) return false; + } + return true; +} + +bool source_is_legal(const Debts& debts, int z, int color, int cap) { + Debts adjusted = debts; + adjusted[color] += cap; + return positive_count(adjusted) <= kEmpty + z; +} + +bool source_is_legal(const State& state, int z, int color, int cap) { + return source_is_legal(state_debts(state), z, color, cap); +} + +std::vector sources(const State& state) { + std::vector result; + for (int color = 0; color < kColors; ++color) { + for (const int cap : state[color].caps) result.push_back({color, cap}); + } + return result; +} + +std::vector legal_sources(const State& state, int z) { + std::vector result; + for (const Source source : sources(state)) { + if (source_is_legal(state, z, source.color, source.cap)) result.push_back(source); + } + return result; +} + +bool is_tq_terminal(const State& state) { + if (!algebraically_consistent(state, 1) || !legal_sources(state, 1).empty()) return false; + int positive = 0; + int nonpositive = 0; + int topped_nonpositive = 0; + int topped_positive = 0; + for (const Bucket& bucket : state) { + if (bucket.debt > 0) { + ++positive; + topped_positive += !bucket.caps.empty(); + } else { + ++nonpositive; + topped_nonpositive += !bucket.caps.empty(); + } + } + return positive == 3 && nonpositive == 1 && topped_nonpositive == 1 && + topped_positive == 0; +} + +std::vector enumerate_tq_terminals() { + std::set terminals; + for (int energy = 0; energy <= 2; ++energy) { + for (int c0 = 1; c0 < kHeight; ++c0) { + for (int c1 = c0; c1 < kHeight; ++c1) { + for (int c2 = c1; c2 < kHeight; ++c2) { + if (c0 <= energy || c0 + c1 + c2 - energy > kHeight) continue; + for (int p0 = 1; p0 <= kHeight; ++p0) { + for (int p1 = p0; p1 <= kHeight; ++p1) { + for (int p2 = p1; p2 <= kHeight; ++p2) { + if (p0 + p1 + p2 - energy != kHeight) continue; + Debts debts{{-energy, p0, p1, p2}}; + Caps caps; + caps[0] = {c0, c1, c2}; + State state = canonical_state(debts, caps); + if (is_tq_terminal(state)) terminals.insert(std::move(state)); + } + } + } + } + } + } + } + return {terminals.begin(), terminals.end()}; +} + +std::optional apply_exhausting_action(const State& state, int z, + const ExhaustAction& action) { + if (action.old_color < 0 || action.old_color >= kColors || + action.final_color < 0 || action.final_color >= kColors || + action.old_color == action.final_color || action.old_cap < 1 || + action.old_cap >= kHeight || + !source_is_legal(state, z, action.old_color, action.old_cap)) { + return std::nullopt; + } + Debts debts = state_debts(state); + Caps caps = state_caps(state); + auto& old_caps = caps[action.old_color]; + const auto found = std::find(old_caps.begin(), old_caps.end(), action.old_cap); + if (found == old_caps.end()) return std::nullopt; + old_caps.erase(found); + debts[action.old_color] += action.old_cap; + debts[action.final_color] += kHeight - action.old_cap; + State successor = canonical_state(debts, caps); + if (!algebraically_consistent(successor, z + 1)) return std::nullopt; + return successor; +} + +std::vector exhausting_actions_to(const State& parent, + const State& terminal) { + std::set actions; + for (int old_color = 0; old_color < kColors; ++old_color) { + std::set unique_caps(parent[old_color].caps.begin(), + parent[old_color].caps.end()); + for (const int old_cap : unique_caps) { + for (int final_color = 0; final_color < kColors; ++final_color) { + ExhaustAction action{old_color, old_cap, final_color}; + const auto successor = apply_exhausting_action(parent, 0, action); + if (successor && *successor == terminal) actions.insert(action); + } + } + } + return {actions.begin(), actions.end()}; +} + +bool final_color_is_isolated(const State& parent, const ExhaustAction& action) { + Debts debts = state_debts(parent); + Caps caps = state_caps(parent); + auto& old_caps = caps[action.old_color]; + const auto found = std::find(old_caps.begin(), old_caps.end(), action.old_cap); + if (found == old_caps.end()) return false; + old_caps.erase(found); + debts[action.old_color] += action.old_cap; + debts[action.final_color] += kHeight - action.old_cap; + return debts[action.final_color] == kHeight - action.old_cap && + caps[action.final_color].empty(); +} + +std::vector reverse_exhausting_candidates(const State& terminal) { + std::vector candidates; + for (int old_cap = 1; old_cap < kHeight; ++old_cap) { + for (int old_color = 0; old_color < kColors; ++old_color) { + for (int final_color = 0; final_color < kColors; ++final_color) { + if (old_color == final_color) continue; + Debts debts = state_debts(terminal); + Caps caps = state_caps(terminal); + debts[old_color] -= old_cap; + debts[final_color] -= kHeight - old_cap; + caps[old_color].push_back(old_cap); + Debts test = debts; + test[old_color] += old_cap; + if (positive_count(test) > kEmpty) continue; + State parent = canonical_state(debts, caps); + if (algebraically_consistent(parent, 0)) candidates.push_back(std::move(parent)); + } + } + } + std::sort(candidates.begin(), candidates.end()); + return candidates; +} + +Bridge build_bridge() { + Bridge bridge; + const auto terminals = enumerate_tq_terminals(); + bridge.terminal_count = terminals.size(); + std::vector> labeled; + std::set> pairs; + for (const State& terminal : terminals) { + for (const State& parent : reverse_exhausting_candidates(terminal)) { + labeled.emplace_back(parent, terminal); + pairs.emplace(parent, terminal); + } + } + bridge.labeled_candidates = labeled.size(); + bridge.canonical_edge_count = pairs.size(); + std::set parents; + std::set unique_parents; + std::set sibling_parents; + for (const auto& pair : pairs) { + parents.insert(pair.first); + const auto legal = legal_sources(pair.first, 0); + if (legal.size() == 1) unique_parents.insert(pair.first); + else sibling_parents.insert(pair.first); + } + bridge.canonical_parent_count = parents.size(); + bridge.unique_parent_count = unique_parents.size(); + bridge.sibling_parent_count = sibling_parents.size(); + for (const State& parent : parents) { + const int count = static_cast(legal_sources(parent, 0).size()); + if (count >= 2) ++bridge.parent_legal_distribution[count]; + } + + for (const auto& pair : pairs) { + const State& parent = pair.first; + const State& terminal = pair.second; + const auto legal = legal_sources(parent, 0); + const auto actions = exhausting_actions_to(parent, terminal); + bridge.action_unique = bridge.action_unique && actions.size() == 1; + if (actions.empty()) { + bridge.all_edges_replay = false; + continue; + } + const ExhaustAction bad = actions.front(); + bridge.all_edges_replay = bridge.all_edges_replay && + apply_exhausting_action(parent, 0, bad) == std::optional(terminal); + bridge.all_final_colors_isolated = bridge.all_final_colors_isolated && + final_color_is_isolated(parent, bad); + if (legal.size() == 1) { + ++bridge.unique_edge_count; + continue; + } + ++bridge.edge_legal_distribution[static_cast(legal.size())]; + ++bridge.sibling_edge_count; + + Debts labeled_terminal = state_debts(parent); + Caps remaining_caps = state_caps(parent); + auto& bad_caps = remaining_caps[bad.old_color]; + const auto found = std::find(bad_caps.begin(), bad_caps.end(), bad.old_cap); + require(found != bad_caps.end(), "bridge bad source is absent"); + bad_caps.erase(found); + labeled_terminal[bad.old_color] += bad.old_cap; + labeled_terminal[bad.final_color] += kHeight - bad.old_cap; + require(canonical_state(labeled_terminal, remaining_caps) == terminal, + "labeled bridge replay does not canonicalize to terminal"); + + int q_color = -1; + for (int color = 0; color < kColors; ++color) { + if (remaining_caps[color].size() == 3) { + require(q_color == -1, "bridge has more than one three-column color"); + q_color = color; + } else { + require(remaining_caps[color].empty(), + "bridge remainder is not an all-q triple"); + } + } + require(q_color >= 0, "bridge has no q color"); + std::sort(remaining_caps[q_color].begin(), remaining_caps[q_color].end()); + Edge edge; + edge.ordinal = bridge.edges.size(); + edge.parent = parent; + edge.terminal = terminal; + edge.bad = bad; + edge.terminal_debts = labeled_terminal; + edge.q_color = q_color; + std::copy(remaining_caps[q_color].begin(), remaining_caps[q_color].end(), + edge.q_caps.begin()); + edge.legal_source_count = static_cast(legal.size()); + edge.old_bad_equals_q = bad.old_color == q_color; + edge.raw_expected = 1; + for (const int cap : edge.q_caps) { + edge.raw_expected *= static_cast((kColors - 1) * (kHeight - cap)); + } + bridge.edges.push_back(std::move(edge)); + } + return bridge; +} + +std::vector cards_for(int q_color, int cap) { + std::vector cards; + for (int color = 0; color < kColors; ++color) { + if (color == q_color) continue; + for (int endpoint = cap + 1; endpoint <= kHeight; ++endpoint) { + cards.push_back({color, endpoint}); + } + } + return cards; +} + +std::uint64_t multinomial(const Counts& counts) { + static constexpr std::array factorial{{ + 1ULL, 1ULL, 2ULL, 6ULL, 24ULL, 120ULL, 720ULL, 5040ULL, + 40320ULL, 362880ULL, 3628800ULL, 39916800ULL, 479001600ULL, + 6227020800ULL, 87178291200ULL, 1307674368000ULL, + 20922789888000ULL, 355687428096000ULL, 6402373705728000ULL, + 121645100408832000ULL, 2432902008176640000ULL}}; + int total = 0; + for (const int count : counts) { + if (count < 0) return 0; + total += count; + } + require(total >= 0 && total <= 20, "multinomial total exceeds exact table"); + std::uint64_t value = factorial[static_cast(total)]; + for (const int count : counts) value /= factorial[static_cast(count)]; + return value; +} + +struct CompletionInfo { + std::uint64_t count = 0; + std::optional, 3>> free_tails; +}; + +CompletionInfo count_completions(const Counts& residual, + const std::array& tail_lengths, + const std::array& cards, + bool want_sample) { + CompletionInfo result; + int total_positions = 0; + int distinguished = 0; + for (int i = 0; i < 3; ++i) { + if (tail_lengths[i] < 0) return result; + total_positions += tail_lengths[i]; + distinguished += tail_lengths[i] > 0; + } + int residual_total = 0; + for (const int count : residual) { + if (count < 0) return result; + residual_total += count; + } + if (residual_total != total_positions) return result; + + Counts remaining = residual; + std::array chosen{{-1, -1, -1}}; + const auto recurse = [&](const auto& self, int column) -> void { + while (column < 3 && tail_lengths[column] == 0) ++column; + if (column == 3) { + const std::uint64_t ways = multinomial(remaining); + result.count += ways; + if (want_sample && ways > 0 && !result.free_tails) { + std::array, 3> tails; + Counts pool = remaining; + for (int i = 0; i < 3; ++i) { + tails[i].assign(static_cast(tail_lengths[i]), -1); + if (tail_lengths[i] > 0) tails[i].back() = chosen[i]; + } + for (int i = 0; i < 3; ++i) { + const int free_slots = tail_lengths[i] - (tail_lengths[i] > 0 ? 1 : 0); + for (int slot = 0; slot < free_slots; ++slot) { + int color = 0; + while (color < kColors && pool[color] == 0) ++color; + require(color < kColors, "sample pool ran out of colors"); + tails[i][static_cast(slot)] = color; + --pool[color]; + } + } + require(std::all_of(pool.begin(), pool.end(), [](int x) { return x == 0; }), + "sample pool was not exhausted"); + result.free_tails = std::move(tails); + } + return; + } + for (int color = 0; color < kColors; ++color) { + if (color == cards[column].color || remaining[color] == 0) continue; + --remaining[color]; + chosen[column] = color; + self(self, column + 1); + ++remaining[color]; + chosen[column] = -1; + } + }; + recurse(recurse, 0); + (void)distinguished; + return result; +} + +bool bad_source_legal_after_live(const Edge& edge, int q_cap, const Card& card) { + Debts debts = state_debts(edge.parent); + debts[edge.q_color] += q_cap; + debts[card.color] -= q_cap; + return source_is_legal(debts, 0, edge.bad.old_color, edge.bad.old_cap); +} + +bool bad_source_legal_after_sibling_exhaust(const Edge& edge, int q_cap, + const Card& card) { + Debts debts = state_debts(edge.parent); + debts[edge.q_color] += q_cap; + debts[card.color] += kHeight - q_cap; + return source_is_legal(debts, 1, edge.bad.old_color, edge.bad.old_cap); +} + +bool q_source_is_legal(const Edge& edge, int cap) { + return source_is_legal(edge.parent, 0, edge.q_color, cap); +} + +bool immediate_tq_after_sibling_exhaust(const Edge& edge, int slot, + const Card& card) { + if (card.endpoint != kHeight) return false; + Debts debts = state_debts(edge.parent); + Caps caps = state_caps(edge.parent); + auto& q_caps = caps[edge.q_color]; + const auto found = std::find(q_caps.begin(), q_caps.end(), edge.q_caps[slot]); + require(found != q_caps.end(), "q slot is absent during direct replay"); + q_caps.erase(found); + debts[edge.q_color] += edge.q_caps[slot]; + debts[card.color] += kHeight - edge.q_caps[slot]; + return is_tq_terminal(canonical_state(debts, caps)); +} + +std::string state_json(const State& state) { + std::ostringstream out; + out << '['; + for (int i = 0; i < kColors; ++i) { + if (i) out << ','; + out << "{\"debt\":" << state[i].debt << ",\"caps\":["; + for (std::size_t j = 0; j < state[i].caps.size(); ++j) { + if (j) out << ','; + out << state[i].caps[j]; + } + out << "]}"; + } + out << ']'; + return out.str(); +} + +template +std::string array_json(const std::array& values) { + std::ostringstream out; + out << '['; + for (std::size_t i = 0; i < N; ++i) { + if (i) out << ','; + out << values[i]; + } + out << ']'; + return out.str(); +} + +std::string vector_json(const std::vector& values) { + std::ostringstream out; + out << '['; + for (std::size_t i = 0; i < values.size(); ++i) { + if (i) out << ','; + out << values[i]; + } + out << ']'; + return out.str(); +} + +void add_class(ClassStats& target, std::uint64_t completions) { + ++target.decorations; + target.residual_words += completions; +} + +bool is_exact_live_tq_corner(const Edge& edge, int slot, + const std::array& cards, int n_value) { + if (n_value != 0 || cards[slot].endpoint != 3) return false; + for (int other = 0; other < 3; ++other) { + if (other == slot) continue; + if (edge.q_caps[other] != 1 || cards[other].color != cards[slot].color || + cards[other].endpoint != 3) { + return false; + } + } + return true; +} + +std::string refined_classification(bool direct_certified, bool n_ge_3, + bool n_le_2_noncorner, bool nonhandoff, + bool corner) { + if (direct_certified) return "direct_exhaustion_certified_yes"; + if (n_ge_3) return "live_handoff_n_ge_3_certified_yes"; + if (n_le_2_noncorner) return "live_handoff_n_le_2_certified_yes"; + if (nonhandoff) return "live_nonhandoff_d2_reduction"; + if (corner) return "tq_low_energy_corner_only"; + return "unclassified"; +} + +void record_sample(const Edge& edge, const std::array& cards, + const std::array& tails, const Counts& residual, + const CompletionInfo& completion, const std::string& classification, + RunStats& stats, EdgeStats& edge_stats) { + require(completion.free_tails.has_value(), "feasible sample has no concrete tails"); + Sample sample; + sample.edge = edge.ordinal; + sample.id = "edge-" + std::to_string(edge.ordinal) + "-sample"; + sample.cards = cards; + sample.free_tail_lengths = tails; + sample.residual_after_forced = residual; + sample.completion_count = completion.count; + sample.classification = classification; + sample.hidden_words[0].assign( + static_cast(kHeight - edge.bad.old_cap), edge.bad.final_color); + for (int slot = 0; slot < 3; ++slot) { + sample.hidden_words[slot + 1] = (*completion.free_tails)[slot]; + const int forced = cards[slot].endpoint - edge.q_caps[slot]; + sample.hidden_words[slot + 1].insert( + sample.hidden_words[slot + 1].end(), static_cast(forced), + cards[slot].color); + require(sample.hidden_words[slot + 1].size() == + static_cast(kHeight - edge.q_caps[slot]), + "sample q word has the wrong length"); + } + Counts used{}; + for (const auto& word : sample.hidden_words) { + for (const int color : word) ++used[color]; + } + const Counts exposed = exposed_counts(edge.parent); + for (int color = 0; color < kColors; ++color) { + require(used[color] == kHeight - exposed[color], + "sample does not realize the parent color balance"); + } + edge_stats.sample = stats.samples.size(); + stats.samples.push_back(std::move(sample)); +} + +RunStats run_census(const Bridge& bridge, std::uint64_t limit) { + const auto started = std::chrono::steady_clock::now(); + RunStats stats; + stats.limit_requested = limit; + stats.per_edge.resize(bridge.edges.size()); + + std::set direct_corner_parents; + std::set direct_corner_edges; + for (const Edge& edge : bridge.edges) { + std::uint64_t legal_joint = 1; + int legal_q_slots = 0; + for (int slot = 0; slot < 3; ++slot) { + const auto cards = cards_for(edge.q_color, edge.q_caps[slot]); + if (q_source_is_legal(edge, edge.q_caps[slot])) { + ++legal_q_slots; + stats.legal_sibling_cards += cards.size(); + legal_joint *= cards.size(); + } + } + require(legal_q_slots >= 1, "sibling edge has no legal q sibling"); + stats.legal_sibling_joint += legal_joint; + stats.all_q_joint += edge.raw_expected; + + std::set> unique_direct_cards; + for (int slot = 0; slot < 3; ++slot) { + const int cap = edge.q_caps[slot]; + if (!q_source_is_legal(edge, cap)) continue; + for (int color = 0; color < kColors; ++color) { + if (color == edge.q_color) continue; + const Card card{color, kHeight}; + if (!immediate_tq_after_sibling_exhaust(edge, slot, card)) continue; + if (kHeight - edge.bad.old_cap + kHeight - cap > kHeight) continue; + unique_direct_cards.emplace(cap, color); + } + } + for (const auto& card_key : unique_direct_cards) { + ++stats.immediate_tq_corner_card_count; + direct_corner_edges.insert(edge.ordinal); + direct_corner_parents.insert(edge.parent); + const int energy = -edge.terminal_debts[edge.q_color]; + const int m_value = edge.bad.old_cap + energy - card_key.first; + require(m_value == 0 || m_value == 1, + "jointly feasible immediate Tq card is not low-energy"); + std::vector other_caps(edge.q_caps.begin(), edge.q_caps.end()); + const auto found = std::find(other_caps.begin(), other_caps.end(), card_key.first); + require(found != other_caps.end(), "direct corner cap is absent"); + other_caps.erase(found); + require(std::min({edge.bad.old_cap, other_caps[0], other_caps[1]}) > m_value, + "direct Tq corner violates its cap inequality"); + ++stats.immediate_tq_corner_m_distribution[m_value]; + } + } + stats.immediate_tq_corner_edge_count = direct_corner_edges.size(); + stats.immediate_tq_corner_parent_count = direct_corner_parents.size(); + + bool stop = false; + for (const Edge& edge : bridge.edges) { + EdgeStats& edge_stats = stats.per_edge[edge.ordinal]; + const auto cards0 = cards_for(edge.q_color, edge.q_caps[0]); + const auto cards1 = cards_for(edge.q_color, edge.q_caps[1]); + const auto cards2 = cards_for(edge.q_color, edge.q_caps[2]); + for (const Card& card0 : cards0) { + for (const Card& card1 : cards1) { + for (const Card& card2 : cards2) { + if (limit != 0 && stats.raw_checked >= limit) { + stop = true; + break; + } + const std::array cards{{card0, card1, card2}}; + ++stats.raw_checked; + ++edge_stats.raw_checked; + if (limit != 0) stats.checked_prefix.push_back({edge.ordinal, cards}); + + Counts residual{}; + const Counts exposed = exposed_counts(edge.parent); + for (int color = 0; color < kColors; ++color) { + residual[color] = kHeight - exposed[color]; + } + residual[edge.bad.final_color] -= kHeight - edge.bad.old_cap; + std::array tails{}; + for (int slot = 0; slot < 3; ++slot) { + residual[cards[slot].color] -= + cards[slot].endpoint - edge.q_caps[slot]; + tails[slot] = kHeight - cards[slot].endpoint; + } + int residual_total = 0; + int tail_total = 0; + bool nonnegative = true; + for (const int value : residual) { + nonnegative = nonnegative && value >= 0; + residual_total += value; + } + for (const int length : tails) tail_total += length; + nonnegative = nonnegative && residual_total == tail_total; + if (nonnegative) { + ++stats.nonnegative; + ++edge_stats.nonnegative; + } + + CompletionInfo completion = count_completions( + residual, tails, cards, !edge_stats.sample.has_value()); + if (completion.count == 0) { + ++stats.infeasible; + ++edge_stats.infeasible; + continue; + } + ++stats.feasible; + ++edge_stats.feasible; + stats.residual_words += completion.count; + edge_stats.residual_words += completion.count; + + bool two_exhaustion = false; + bool live_handoff = false; + bool direct_certified = false; + bool n_ge_3 = false; + bool n_le_2_noncorner = false; + bool nonhandoff = false; + bool corner = false; + bool direct_corner_present = false; + for (int slot = 0; slot < 3; ++slot) { + if (!q_source_is_legal(edge, edge.q_caps[slot])) continue; + const Card& card = cards[slot]; + if (card.endpoint == kHeight) { + const bool immediate_tq = + immediate_tq_after_sibling_exhaust(edge, slot, card); + direct_corner_present = direct_corner_present || immediate_tq; + corner = corner || immediate_tq; + direct_certified = direct_certified || !immediate_tq; + two_exhaustion = two_exhaustion || + bad_source_legal_after_sibling_exhaust( + edge, edge.q_caps[slot], card); + continue; + } + const bool persists = bad_source_legal_after_live( + edge, edge.q_caps[slot], card); + if (!persists) { + nonhandoff = true; + continue; + } + live_handoff = true; + const int n_value = + edge.q_caps[slot] - edge.terminal_debts[card.color]; + require(n_value >= 0, "live handoff has negative N"); + if (n_value >= 3) { + n_ge_3 = true; + } else if (is_exact_live_tq_corner(edge, slot, cards, n_value)) { + corner = true; + } else { + n_le_2_noncorner = true; + } + } + + std::string legacy_class; + if (two_exhaustion) { + legacy_class = "two_exhaustion"; + add_class(stats.two_exhaustion, completion.count); + add_class(edge_stats.two_exhaustion, completion.count); + } else if (live_handoff) { + legacy_class = "live_bad_persistent"; + add_class(stats.live_handoff, completion.count); + add_class(edge_stats.live_handoff, completion.count); + } else { + legacy_class = "obstruction"; + add_class(stats.obstruction, completion.count); + add_class(edge_stats.obstruction, completion.count); + } + if (n_ge_3) { + ++stats.handoff_n_ge_3; + stats.handoff_n_ge_3_words += completion.count; + ++edge_stats.handoff_n_ge_3; + edge_stats.handoff_n_ge_3_words += completion.count; + } + if (live_handoff && !n_ge_3) { + ++stats.handoff_n_le_2; + stats.handoff_n_le_2_words += completion.count; + ++edge_stats.handoff_n_le_2; + edge_stats.handoff_n_le_2_words += completion.count; + } + if (direct_corner_present) { + ++stats.immediate_tq_corner; + stats.immediate_tq_corner_words += completion.count; + ++edge_stats.immediate_tq_corner; + edge_stats.immediate_tq_corner_words += completion.count; + } + + const std::string refined = refined_classification( + direct_certified, n_ge_3, n_le_2_noncorner, nonhandoff, corner); + if (refined == "direct_exhaustion_certified_yes") { + add_class(stats.direct_certified, completion.count); + add_class(edge_stats.direct_certified, completion.count); + } else if (refined == "live_handoff_n_ge_3_certified_yes") { + add_class(stats.n_ge_3_certified, completion.count); + add_class(edge_stats.n_ge_3_certified, completion.count); + } else if (refined == "live_handoff_n_le_2_certified_yes") { + add_class(stats.n_le_2_certified, completion.count); + add_class(edge_stats.n_le_2_certified, completion.count); + } else if (refined == "live_nonhandoff_d2_reduction") { + add_class(stats.d2_reduction, completion.count); + add_class(edge_stats.d2_reduction, completion.count); + } else if (refined == "tq_low_energy_corner_only") { + add_class(stats.tq_corner_only, completion.count); + add_class(edge_stats.tq_corner_only, completion.count); + } else { + require(false, "feasible decoration was not classified"); + } + if (!edge_stats.sample) { + record_sample(edge, cards, tails, residual, completion, legacy_class, + stats, edge_stats); + } + } + if (stop) break; + } + if (stop) break; + } + if (stop) break; + } + stats.next_run_universe_complete = stats.raw_checked == stats.all_q_joint; + stats.self_checks_passed = true; + stats.elapsed_seconds = std::chrono::duration( + std::chrono::steady_clock::now() - started).count(); + return stats; +} + +std::string distribution_json(const std::map& distribution) { + std::ostringstream out; + out << '{'; + bool first = true; + for (const auto& item : distribution) { + if (!first) out << ','; + first = false; + out << '\"' << item.first << "\":" << item.second; + } + out << '}'; + return out.str(); +} + +std::string class_json(const ClassStats& stats) { + std::ostringstream out; + out << "{\"decorations\":" << stats.decorations + << ",\"residual_words\":" << stats.residual_words << '}'; + return out.str(); +} + +std::string cards_json(const std::array& cards) { + std::ostringstream out; + out << '['; + for (int slot = 0; slot < 3; ++slot) { + if (slot) out << ','; + out << '[' << cards[slot].color << ',' << cards[slot].endpoint << ']'; + } + out << ']'; + return out.str(); +} + +std::string render_json(const Bridge& bridge, const RunStats& stats) { + const bool complete = stats.next_run_universe_complete; + std::ostringstream out; + out << "{\n" + << " \"schema_version\": 1,\n" + << " \"model\": {\"colors\":4,\"height\":7,\"empty_columns\":2},\n" + << " \"coverage_scope\": \"first_exhaustion_tq_sibling_next_run_forks\",\n" + << " \"status\": \"" << (complete ? "NEXT_RUN_CENSUS_COMPLETE" : "INCOMPLETE") << "\",\n" + << " \"verified\": " << (complete ? "true" : "false") << ",\n" + << " \"self_checks_passed\": " << (stats.self_checks_passed ? "true" : "false") << ",\n" + << " \"limit_requested\": " << stats.limit_requested << ",\n" + << " \"limit_unit\": \"raw_all_q_next_run_decorations\",\n" + << " \"ordering\": {\"edges\":\"lexicographic (parent,terminal) canonical states\"," + "\"q_slots\":\"nondecreasing cap, physical multiplicity retained\"," + "\"cards\":\"slot0 outer; slot2 inner; color-major then endpoint-major\"},\n" + << " \"bridge\": {\n" + << " \"terminal_count\": " << bridge.terminal_count << ",\n" + << " \"labeled_candidates\": " << bridge.labeled_candidates << ",\n" + << " \"canonical_parents\": " << bridge.canonical_parent_count << ",\n" + << " \"canonical_edges\": " << bridge.canonical_edge_count << ",\n" + << " \"unique_source_parents\": " << bridge.unique_parent_count << ",\n" + << " \"sibling_parents\": " << bridge.sibling_parent_count << ",\n" + << " \"unique_source_edges\": " << bridge.unique_edge_count << ",\n" + << " \"sibling_edges\": " << bridge.sibling_edge_count << ",\n" + << " \"parent_legal_source_distribution\": " + << distribution_json(bridge.parent_legal_distribution) << ",\n" + << " \"edge_legal_source_distribution\": " + << distribution_json(bridge.edge_legal_distribution) << ",\n" + << " \"action_unique\": " << (bridge.action_unique ? "true" : "false") << ",\n" + << " \"all_edges_replay\": " << (bridge.all_edges_replay ? "true" : "false") << ",\n" + << " \"all_final_colors_isolated\": " + << (bridge.all_final_colors_isolated ? "true" : "false") << "\n },\n" + << " \"raw\": {\"legal_sibling_cards\":" << stats.legal_sibling_cards + << ",\"legal_sibling_joint_decorations\":" << stats.legal_sibling_joint + << ",\"all_q_joint_decorations\":" << stats.all_q_joint + << ",\"checked\":" << stats.raw_checked << "},\n" + << " \"census\": {\n" + << " \"nonnegative_decorations\": " << stats.nonnegative << ",\n" + << " \"feasible_decorations\": " << stats.feasible << ",\n" + << " \"infeasible_decorations\": " << stats.infeasible << ",\n" + << " \"residual_words\": " << stats.residual_words << ",\n" + << " \"legacy\": {\"two_exhaustion\":" << class_json(stats.two_exhaustion) + << ",\"live_bad_persistent\":" << class_json(stats.live_handoff) + << ",\"obstruction\":" << class_json(stats.obstruction) << "},\n" + << " \"refined\": {" + << "\"direct_certified\":" << class_json(stats.direct_certified) << ',' + << "\"n_ge_3_certified\":" << class_json(stats.n_ge_3_certified) << ',' + << "\"n_le_2_certified\":" << class_json(stats.n_le_2_certified) << ',' + << "\"d2_reduction\":" << class_json(stats.d2_reduction) << ',' + << "\"tq_corner_only\":" << class_json(stats.tq_corner_only) << "},\n" + << " \"property_counts\": {" + << "\"handoff_n_ge_3_present\":" << stats.handoff_n_ge_3 << ',' + << "\"handoff_n_ge_3_present_words\":" << stats.handoff_n_ge_3_words << ',' + << "\"handoff_n_le_2_present_after_n_ge_3_precedence\":" << stats.handoff_n_le_2 << ',' + << "\"handoff_n_le_2_present_words\":" << stats.handoff_n_le_2_words << ',' + << "\"direct_immediate_tq_corner_present\":" << stats.immediate_tq_corner << ',' + << "\"direct_immediate_tq_corner_present_words\":" << stats.immediate_tq_corner_words << "},\n" + << " \"direct_tq_corner_structure\": {" + << "\"cards\":" << stats.immediate_tq_corner_card_count << ',' + << "\"edges\":" << stats.immediate_tq_corner_edge_count << ',' + << "\"parents\":" << stats.immediate_tq_corner_parent_count << ',' + << "\"m_distribution\":" << distribution_json(stats.immediate_tq_corner_m_distribution) + << "}\n },\n" + << " \"next_run_universe_complete\": " << (complete ? "true" : "false") << ",\n" + << " \"full_residual_word_coverage\": false,\n" + << " \"entry_family_eliminated\": false,\n" + << " \"full_layout_coverage\": false,\n" + << " \"per_edge\": [\n"; + for (std::size_t index = 0; index < bridge.edges.size(); ++index) { + const Edge& edge = bridge.edges[index]; + const EdgeStats& row = stats.per_edge[index]; + out << " {\"edge_id\":\"exhaust-sibling-e" << index << "\"," + << "\"parent\":" << state_json(edge.parent) << ',' + << "\"terminal\":" << state_json(edge.terminal) << ',' + << "\"bad_action\":[" << edge.bad.old_color << ',' << edge.bad.old_cap + << ',' << edge.bad.final_color << "]," + << "\"q_color\":" << edge.q_color << ',' + << "\"q_caps\":" << array_json(edge.q_caps) << ',' + << "\"old_bad_equals_q\":" << (edge.old_bad_equals_q ? "true" : "false") << ',' + << "\"legal_source_count\":" << edge.legal_source_count << ',' + << "\"raw_expected\":" << edge.raw_expected << ',' + << "\"raw_checked\":" << row.raw_checked << ',' + << "\"nonnegative\":" << row.nonnegative << ',' + << "\"feasible\":" << row.feasible << ',' + << "\"infeasible\":" << row.infeasible << ',' + << "\"residual_words\":" << row.residual_words << ',' + << "\"legacy\":{\"two_exhaustion\":" << class_json(row.two_exhaustion) + << ",\"live_bad_persistent\":" << class_json(row.live_handoff) + << ",\"obstruction\":" << class_json(row.obstruction) << "}," + << "\"refined\":{" + << "\"direct_certified\":" << class_json(row.direct_certified) << ',' + << "\"n_ge_3_certified\":" << class_json(row.n_ge_3_certified) << ',' + << "\"n_le_2_certified\":" << class_json(row.n_le_2_certified) << ',' + << "\"d2_reduction\":" << class_json(row.d2_reduction) << ',' + << "\"tq_corner_only\":" << class_json(row.tq_corner_only) << "}," + << "\"sample_id\":"; + if (row.sample) out << '\"' << stats.samples[*row.sample].id << '\"'; + else out << "null"; + out << '}' << (index + 1 == bridge.edges.size() ? "\n" : ",\n"); + } + out << " ],\n \"replay_samples\": [\n"; + for (std::size_t index = 0; index < stats.samples.size(); ++index) { + const Sample& sample = stats.samples[index]; + const Edge& edge = bridge.edges[sample.edge]; + out << " {\"sample_id\":\"" << sample.id << "\"," + << "\"edge_id\":\"exhaust-sibling-e" << sample.edge << "\"," + << "\"feasible\":true," + << "\"classification\":\"" << sample.classification << "\"," + << "\"bad_action\":[" << edge.bad.old_color << ',' << edge.bad.old_cap + << ',' << edge.bad.final_color << "]," + << "\"q_color\":" << edge.q_color << ',' + << "\"q_caps\":" << array_json(edge.q_caps) << ',' + << "\"cards\":" << cards_json(sample.cards) << ',' + << "\"free_tail_lengths\":" << array_json(sample.free_tail_lengths) << ',' + << "\"residual_after_forced\":" << array_json(sample.residual_after_forced) << ',' + << "\"completion_count\":" << sample.completion_count << ',' + << "\"hidden_words_bottom_to_top\":["; + for (int column = 0; column < 4; ++column) { + if (column) out << ','; + out << vector_json(sample.hidden_words[column]); + } + out << "]}" << (index + 1 == stats.samples.size() ? "\n" : ",\n"); + } + out << " ],\n \"hall_regression\": {" + << "\"residual_counts\":[0,5,0,0]," + << "\"tail_lengths\":[3,2,0]," + << "\"forbidden_colors\":[1,2,null]," + << "\"nonnegative\":true,\"feasible\":false},\n" + << " \"checked_prefix\": ["; + for (std::size_t index = 0; index < stats.checked_prefix.size(); ++index) { + if (index) out << ','; + out << "{\"edge_id\":\"exhaust-sibling-e" << stats.checked_prefix[index].edge + << "\",\"cards\":" << cards_json(stats.checked_prefix[index].cards) << '}'; + } + out << "],\n \"elapsed_seconds\": " << stats.elapsed_seconds << "\n}\n"; + return out.str(); +} + +std::string render_markdown(const Bridge& bridge, const RunStats& stats) { + std::ostringstream out; + out << "# c=4, h=7 first-exhaustion Tq sibling next-run census\n\n" + << "- Status: **" << (stats.next_run_universe_complete + ? "NEXT_RUN_CENSUS_COMPLETE" : "INCOMPLETE") << "**.\n" + << "- Scope: committed next runs only; this is not full residual-word or layout coverage.\n" + << "- Tq terminals / canonical bridge parents / edges: " << bridge.terminal_count + << " / " << bridge.canonical_parent_count << " / " << bridge.canonical_edge_count << ".\n" + << "- Sibling parents / edges: " << bridge.sibling_parent_count << " / " + << bridge.sibling_edge_count << ".\n" + << "- Raw all-q decorations checked: " << stats.raw_checked << " / " + << stats.all_q_joint << ".\n" + << "- Nonnegative / Hall-feasible decorations: " << stats.nonnegative << " / " + << stats.feasible << ".\n" + << "- Represented labeled residual words: " << stats.residual_words << ".\n\n" + << "## Legacy first-layer classification\n\n" + << "| Class | Decorations | Residual words |\n|---|---:|---:|\n" + << "| two exhaustions | " << stats.two_exhaustion.decorations << " | " + << stats.two_exhaustion.residual_words << " |\n" + << "| live bad handoff | " << stats.live_handoff.decorations << " | " + << stats.live_handoff.residual_words << " |\n" + << "| obstruction | " << stats.obstruction.decorations << " | " + << stats.obstruction.residual_words << " |\n\n" + << "The refined labels in `report.json` are mathematical reconnaissance. " + "D2/Tq labels are reductions, not global NO certificates.\n"; + return out.str(); +} + +void write_outputs(const Options& options, const Bridge& bridge, const RunStats& stats) { + if (options.output_dir.empty()) return; + std::filesystem::create_directories(options.output_dir); + { + std::ofstream file(options.output_dir / "report.json"); + if (!file) throw std::runtime_error("cannot write report.json"); + file << render_json(bridge, stats); + } + { + std::ofstream file(options.output_dir / "summary.md"); + if (!file) throw std::runtime_error("cannot write summary.md"); + file << render_markdown(bridge, stats); + } +} + +void verify_structural_counts(const Bridge& bridge, const RunStats& stats) { + require(stats.legal_sibling_cards == kExpectedLegalSiblingCards, + "legal sibling card count mismatch"); + require(stats.legal_sibling_joint == kExpectedLegalSiblingJoint, + "legal-sibling joint count mismatch"); + require(stats.all_q_joint == kExpectedAllQJoint, + "all-q joint count mismatch"); + require(bridge.parent_legal_distribution == + std::map{{2, 1}, {3, 12}, {4, 399}}, + "parent legal-source distribution mismatch"); + require(bridge.edge_legal_distribution == + std::map{{2, 2}, {3, 14}, {4, 407}}, + "edge legal-source distribution mismatch"); + require(stats.immediate_tq_corner_card_count == 12, + "jointly feasible direct Tq card count mismatch"); + require(stats.immediate_tq_corner_edge_count == 12, + "jointly feasible direct Tq edge count mismatch"); + require(stats.immediate_tq_corner_parent_count == 10, + "jointly feasible direct Tq parent count mismatch"); + require(stats.immediate_tq_corner_m_distribution == + std::map{{0, 8}, {1, 4}}, + "direct Tq M distribution mismatch"); + + const Counts hall_counts{{0, 5, 0, 0}}; + const std::array hall_tails{{3, 2, 0}}; + const std::array hall_cards{{Card{1, 4}, Card{2, 5}, Card{0, 7}}}; + require(count_completions(hall_counts, hall_tails, hall_cards, false).count == 0, + "Hall regression unexpectedly has a completion"); +} + +void verify_full_counts(const RunStats& stats) { + if (!stats.next_run_universe_complete) return; + require(stats.raw_checked == kExpectedAllQJoint, "full raw count mismatch"); + require(stats.nonnegative == kExpectedNonnegative, "nonnegative count mismatch"); + require(stats.feasible == kExpectedFeasible, "feasible count mismatch"); + require(stats.infeasible == kExpectedAllQJoint - kExpectedFeasible, + "infeasible count mismatch"); + require(stats.residual_words == kExpectedResidualWords, "residual-word weight mismatch"); + require(stats.two_exhaustion.decorations == kExpectedTwoExhaustion && + stats.two_exhaustion.residual_words == kExpectedTwoExhaustionWords, + "two-exhaustion class mismatch"); + require(stats.live_handoff.decorations == kExpectedLiveHandoff && + stats.live_handoff.residual_words == kExpectedLiveHandoffWords, + "live-handoff class mismatch"); + require(stats.obstruction.decorations == kExpectedObstruction && + stats.obstruction.residual_words == kExpectedObstructionWords, + "obstruction class mismatch"); + require(stats.direct_certified.decorations == kExpectedDirectCertified && + stats.direct_certified.residual_words == kExpectedDirectCertifiedWords, + "refined direct-certified class mismatch"); + require(stats.n_ge_3_certified.decorations == kExpectedHandoffNGe3 && + stats.n_ge_3_certified.residual_words == kExpectedHandoffNGe3Words, + "refined N>=3 class mismatch"); + require(stats.n_le_2_certified.decorations == kExpectedHandoffNLe2 && + stats.n_le_2_certified.residual_words == kExpectedHandoffNLe2Words, + "refined N<=2 class mismatch"); + require(stats.d2_reduction.decorations == kExpectedD2Reduction && + stats.d2_reduction.residual_words == kExpectedD2ReductionWords, + "refined D2-reduction class mismatch"); + require(stats.tq_corner_only.decorations == kExpectedTqCornerOnly && + stats.tq_corner_only.residual_words == kExpectedTqCornerOnlyWords, + "refined Tq-corner class mismatch"); + require(stats.samples.size() == kExpectedSiblingEdges, + "full census does not have one sample per edge"); +} + +} // namespace + +int main(int argc, char** argv) { + try { + const Options options = parse_options(argc, argv); + const Bridge bridge = build_bridge(); + require(bridge.terminal_count == kExpectedTqTerminals, "Tq terminal count mismatch"); + require(bridge.labeled_candidates == kExpectedLabeledCandidates, + "labeled candidate count mismatch"); + require(bridge.canonical_parent_count == kExpectedCanonicalParents, + "canonical parent count mismatch"); + require(bridge.canonical_edge_count == kExpectedCanonicalEdges, + "canonical edge count mismatch"); + require(bridge.unique_parent_count == kExpectedUniqueParents, + "unique parent count mismatch"); + require(bridge.sibling_parent_count == kExpectedSiblingParents, + "sibling parent count mismatch"); + require(bridge.unique_edge_count == kExpectedUniqueEdges, + "unique edge count mismatch"); + require(bridge.sibling_edge_count == kExpectedSiblingEdges, + "sibling edge count mismatch"); + require(bridge.action_unique && bridge.all_edges_replay && + bridge.all_final_colors_isolated, + "bridge replay checks failed"); + + std::uint64_t effective_limit = options.limit; + if (options.self_test && effective_limit == 0) effective_limit = 64; + // A limit covering the whole finite universe is an ordinary full run. + // Normalizing it to zero avoids retaining every decoration in the + // bounded-run checked-prefix audit trail. + if (effective_limit >= kExpectedAllQJoint) effective_limit = 0; + RunStats stats = run_census(bridge, effective_limit); + verify_structural_counts(bridge, stats); + verify_full_counts(stats); + write_outputs(options, bridge, stats); + std::cout << "status=" + << (stats.next_run_universe_complete + ? "NEXT_RUN_CENSUS_COMPLETE" : "INCOMPLETE") + << " raw=" << stats.raw_checked << '/' << stats.all_q_joint + << " feasible=" << stats.feasible + << " residual_words=" << stats.residual_words << '\n'; + return 0; + } catch (const std::exception& error) { + std::cerr << "error: " << error.what() << '\n'; + return 1; + } +} diff --git a/docs/c4-h7-tq-exhaust-sibling-checker-design.md b/docs/c4-h7-tq-exhaust-sibling-checker-design.md new file mode 100644 index 0000000..f7fa4df --- /dev/null +++ b/docs/c4-h7-tq-exhaust-sibling-checker-design.md @@ -0,0 +1,237 @@ +# First-exhaustion Tq sibling checker: implementation design + +## Claim boundary + +This checker concerns only the `z=0 -> z=1` exhausting entrances into a +`Tq` terminal that have another legal source at the parent. The already +verified numerical bridge has: + +- 71 canonical `Tq` terminals; +- 624 labeled reverse candidates; +- 418 canonical parent states and 429 canonical parent-terminal edges; +- 6 unique-source parents; and +- 412 sibling parents carried by 423 canonical edges. + +A census of committed next runs is not a census of complete residual words. +Accordingly, completing the proposed first implementation must not by itself +claim that the 412-parent entry family is eliminated, and says nothing about +all balanced height-seven layouts. + +## Two exact edge types + +For an exhausting edge let the bad source be `a_s`, its isolated final color +be `b`, and let the other three current sources have the common `Tq` top +color `q`. The source test of the bad edge is + +```text +d(P) + s e_a = d(D) - (7-s) e_b. +``` + +It has exactly the two non-`q`, non-`b` positive coordinates. The 423 +sibling edges split into two useful, independently checkable types: + +- `a != q`: 270 edges. Here `a` is one of those two positive colors in + `D`; sibling legality forces `d_a(P) <= 0`, while `d_b(P) = 0`. All three + `q` columns are legal, so the parent has four legal physical sources. +- `a == q`: 153 edges. All four current tops are `q`; there are 137 edges + with four legal sources, 14 with three, and 2 with two. + +The corresponding sibling-parent state distribution is one state with two +legal sources, twelve with three, and 399 with four. State and edge +distributions must be reported separately. + +## The smallest sound decoration + +The bad column has no undecided future: its entire hidden prefix is +`b^(7-s)`. A decoration must commit the actual next run of **all three** +remaining `q` columns, including a currently illegal column. Recording only +the currently legal siblings is enough to discuss the first move, but is not +enough to replay a continuation on one fixed layout. + +For a `q` column of current cap `r`, a card `(x,u)` has + +```text +x != q, r < u <= 7. +``` + +It forces `x^(u-r)` at the top of that column's hidden prefix. If `u < 7`, +the next lower cell must differ from `x`, so that `u` is the exact endpoint +rather than merely a lower bound. + +The raw, pre-balance sizes are: + +| object | count | +|---|---:| +| individual cards of currently legal siblings | 18,177 | +| joint cards of currently legal siblings | 1,220,361 | +| joint cards of all three fixed `q` columns | 1,256,148 | + +The last count is the preferred production universe. + +## Exact color-feasibility without residual-word expansion + +After subtracting the fixed bad tail and the three forced card runs from +`7-F_c(P)`, let `m_i=7-u_i` be the uncommitted length of `q` column `i`. +For each `m_i>0`, reserve its top uncommitted cell and forbid the card color +there. There are at most three such distinguished cells. Enumerate their +allowed colors (at most `3^3=27` assignments); all remaining cells are +unrestricted labeled positions. If their remaining color multiplicities +are `n_c`, that assignment contributes + +```text +N! / product_c(n_c!) +``` + +complete residual words, where `N=sum_c n_c`. This gives both an exact +existence test and an exact residual-word weight for every one-layer +decoration, without enumerating the words themselves. + +A read-only prototype, not yet an independently certified project constant, +gave: + +| prototype quantity | count | +|---|---:| +| color-feasible all-`q` decorations | 403,685 | +| edge-summed complete residual words represented | 6,131,033,832 | +| smallest / largest per-edge residual count | 924 / 344,323,980 | + +The 6.13-billion figure is why the same-z app's explicit residual loop should +not be copied into this checker. + +## First-layer classifications + +For each currently legal sibling card, replay its exact live or exhausting +debt update and retest the bad source with the correct host threshold: + +- `two_exhaustion`: the sibling exhausts and the bad source is then legal at + `z=1`; the two fixed events reach `z=2`. +- `live_bad_persistent`: the sibling moves live and the bad source remains + legal at `z=0`. Taking it next reaches a nonterminal `z=1` checkpoint, not + the goal. This is only a handoff, not an elimination proof. +- `obstruction`: no currently legal sibling has either property. + +With precedence `two_exhaustion > live_bad_persistent > obstruction`, the +same provisional prototype produced: + +| class | feasible decorations | represented residual words | +|---|---:|---:| +| two-exhaustion | 70,633 | 8,629,839 | +| live handoff | 254,899 | 3,235,811,235 | +| obstruction | 78,153 | 2,886,592,758 | + +These figures are reconnaissance only until a separate checker derives them. +In particular, the large obstruction class prevents a first-layer +persistence census from supporting `ENTRY_FAMILY_ELIMINATED`. + +## Minimal production interface + +The first executable should have one fixed scope rather than a mode whose +meaning can drift: + +```text +water-c4-h7-tq-exhaust-siblings + --output-dir DIR + [--limit N] + [--self-test] +``` + +`--limit` counts raw all-three-`q` decorations in deterministic +edge/card order. A bare `--self-test` may run structural assertions and a +small bounded prefix without writing output. + +The first report should use: + +```text +coverage_scope = "first_exhaustion_tq_sibling_next_run_forks" +limit_unit = "raw_all_q_next_run_decorations" +``` + +and contain at least: + +- the 71/624/418/429/6/412/423 bridge census; +- parent and edge legal-source distributions; +- action uniqueness and isolated-final-color checks; +- 18,177 / 1,220,361 / 1,256,148 raw counts; +- feasible/infeasible decoration counts and residual-word weights; +- the three first-layer classifications, split by `a==q` and `a!=q`; +- per-edge counts plus replayable samples; and +- explicit coverage flags. + +Required flags are: + +```text +next_run_universe_complete +full_residual_word_coverage = false +entry_family_eliminated = false +full_layout_coverage = false +``` + +Suggested statuses are: + +- `NEXT_RUN_CENSUS_COMPLETE`: the bounded mathematical object above is fully + checked; +- `REDUCTION_CERTIFIED`: reserved for a later theorem whose targets and + dependencies are explicitly named; +- `ENTRY_FAMILY_ELIMINATED`: reserved for a genuine universal fixed-future + argument; +- `INCOMPLETE`: any limited run. + +`verified=true` means only that the declared `coverage_scope` is complete. +The strict validator must reject `ENTRY_FAMILY_ELIMINATED` while +`full_residual_word_coverage=false` unless the report names and verifies a +separate universal strategy certificate. + +## Minimal code reuse + +Do not copy the complete same-z application. Once the bridge mathematics is +stable, move only these family-neutral pieces into an app-internal header: + +- `Bucket`, `State`, canonicalization, consistency, and source legality; +- fixed-run card generation and color-count keys; and +- the fixed-chain checkpoint recursion used for bounded differential samples. + +Keep terminal/edge enumeration, classification, report writing, and all +expected constants family-specific. The same-z executable and its +independent report checker must remain regression-identical after the +extraction. + +## Independent checker + +`tests/check_c4_h7_tq_exhaust_siblings.py` must not import either production +app or `scripts/c4_h7_macro_recon.py`. It should independently: + +1. reconstruct the 71 terminals and the 624/418/429 bridge; +2. replay all 429 actions and the isolated-final-color identity; +3. reproduce the unique/sibling split and both legal-source distributions; +4. enumerate all-three-`q` cards in a different loop order; +5. test feasibility with a small max-flow or explicit distinguished-cell + assignment, rather than production's implementation; +6. replay all report samples with an independent debt recursion; and +7. run bounded production differentials and schema-negative tests. + +The artifact validator should additionally enforce status/coverage +compatibility and reject missing per-edge coverage. + +## GitHub Actions shape + +Use two jobs initially: + +1. `build-and-audit`: GCC Release build, focused CTest, bare self-test, + bounded production/independent differential, and sanitizer or Clang smoke. +2. `next-run-census`: complete 1,256,148-decoration census, independent report + validation, deterministic hashes, and artifact upload. + +Do not add a job that loops over the 6.13-billion residual words. Add a +separate proof job only after the anchor/all-`q` case split has a stable +universal strategy or a proof-producing symbolic encoding. The workflow +must fail if a next-run-only report claims entry-family elimination. + +## Mathematical next decision + +The 270 `a!=q` edges have two nonpositive anchors (`a` and the isolated +color `b`) and all three `q` siblings legal. Advancing columns through the +two-anchor corridor can end at a two-anchor, all-top state, which has the +shape of the unresolved `D2` family. The 153 `a==q` edges form a separate +all-`q` cap-inequality case. The next proof step should therefore decide +whether the bridge is reduced to a named `D2` subfamily or eliminated +directly; the checker should not silently treat that reduction as a win. diff --git a/docs/c4-h7-tq-exhaust-sibling-reduction.md b/docs/c4-h7-tq-exhaust-sibling-reduction.md new file mode 100644 index 0000000..0466aac --- /dev/null +++ b/docs/c4-h7-tq-exhaust-sibling-reduction.md @@ -0,0 +1,699 @@ +# The first-exhaustion `Tq` sibling reduction at `c=4, h=7, k=2` + +## Scope and status + +This note studies the `z=0` parents whose **first exhausting event** enters a +`Tq` terminal at `z=1`, and only the subfamily in which the parent has a +legal source other than the exhausting source. + +The result is a reduction, not an elimination theorem. It proves several +large branches safe and isolates the branches that still require a `D2` +argument or a unique-source `Tq` argument. In particular, this note does +**not** prove that every first-exhaustion `Tq` parent is checkpoint-YES and +does **not** prove universal solvability at height 7. + +The canonical census has + +```text +418 first-exhaustion Tq parents / 429 parent-terminal edges, + 6 unique-source parents / 6 edges, +412 sibling parents / 423 edges. +``` + +Inside the sibling family, 270 parents and 270 edges have bad-source top +different from the terminal top color, while 142 parents and 153 edges have +the same bad-source and terminal top color. Eleven of the latter parents +have two canonical terminal children. + +All calculations below are for one fixed future (the actual remaining run +chains). A macro transition is not silently treated as a jointly realizable +decoration: whenever two proposed branches reserve items of the same color, +the common color budget is imposed explicitly. + +## 1. Border equations and two input lemmas + +For a border state let + +\[ +d_c=F_c-G_c, +\] + +where `F_c` is the exposed amount of color `c` and `G_c` is the active host +capacity currently topped by `c`. A source of top color `x` and current cap +`r` is legal exactly when + +\[ + \#\{c:d_c+r[c=x]>0\}\le 2+z. \tag{1} +\] + +A live event `x_r -> y_R`, with `x != y` and `r=3`, the state is checkpoint-YES. +2. **Same-level `Tq` sibling-entry lemma.** A live `z=1` entrance into a + `Tq` terminal is checkpoint-YES if its parent has a legal sibling source. + Equivalently, in the notation of that lemma, the still-unresolved entrance + is precisely the unique-source case `p_x>r`; the sibling case is + `p_x<=r`. + +The second fact is proved in `docs/c4-h7-tq-sibling-lemma.md` by the anchor +corridor and all-anchor rotor. + +## 2. Normal form of a first-exhaustion bridge + +Let `D` be the `Tq` child. Its three active columns have common top color +`q`, with caps `r_1,r_2,r_3`, and + +\[ +d_q(D)=-E,\qquad d_c(D)=p_c>0\quad(c\ne q), + \tag{4} +\] + +where + +\[ +0\le E\le2,\qquad r_i>E. \tag{5} +\] + +Let the bad first-exhausting edge be + +\[ +a_s\xrightarrow{\text{final }f^{\,7-s}}D, +\qquad a\ne f. \tag{6} +\] + +Writing its parent as `P`, inversion of (3) gives + +\[ +d(P)=d(D)-s e_a-(7-s)e_f. \tag{7} +\] + +Testing the bad source at `P` gives + +\[ +d(P)+s e_a=d(D)-(7-s)e_f. \tag{8} +\] + +The right side initially has the three positive non-`q` coordinates of +`D`. Bad-source legality at `z=0` forces the subtraction to remove one of +them, so `f` is a positive-debt color. Moreover, `P` has no `f`-top source: +its active tops are the three `q` tops and `a`, and `a!=f`. Consequently +`G_f(P)=0`, while `F_f(P)=d_f(P)>=0`. Equation (8) also gives +`d_f(P)<=0`. Hence equality is forced: + +\[ +p_f=7-s,\qquad d_f(P)=F_f(P)=0. \tag{9} +\] + +Thus the bad-source test has exactly two positive coordinates: the two +positive colors other than `f`. + +### 2.1 The case `a != q` + +Let `b` be the fourth color, so the colors are `q,f,a,b`, and define + +\[ +A=s-p_a. \tag{10} +\] + +Since the debts of `D` sum to 7, (9) gives + +\[ +p_a+p_b=s+E,\qquad p_b=A+E. \tag{11} +\] + +In the order `(q,f,a,b)`, the parent therefore has the particularly rigid +form + +\[ +d(P)=(-E,0,-A,A+E). \tag{12} +\] + +Testing any terminal `q` column of cap `r_i` makes `q` positive, because +`r_i>E`, while `b` is positive already. It is legal exactly when `a` is +nonpositive, that is, + +\[ +A\ge0\quad\Longleftrightarrow\quad p_a\le s. \tag{13} +\] + +If (13) holds, **all three** `q` columns are legal. If it fails, none is +legal. The census has 270 sibling parents of the first kind. The six +unique-source bridge parents are exactly the second kind; numerically they +have `E=2` and `A=-1`. + +Notice also that `E=0` implies `A>=1`, because `p_b=A+E>0`. + +### 2.2 The case `a=q` + +Let the two positive colors other than `f` be `g,h`, and put + +\[ +Q=s+E=p_g+p_h. \tag{14} +\] + +Then, in the order `(q,f,g,h)`, + +\[ +d(P)=(-Q,0,p_g,p_h). \tag{15} +\] + +A terminal `q` column of cap `r` is a legal sibling exactly when + +\[ +r\le Q. \tag{16} +\] + +Unlike (13), legality need not hold for all three terminal columns. At the +parent level the 142 states in this case split into 129 with four legal +physical sources, 12 with three, and one with two. + +## 3. A strengthened height-7 all-anchor fact + +At `z=1`, suppose all three active tops have color `x` and `d_x=-M`. If +`M>=3`, a source of cap at most `M` must exist. Indeed, otherwise + +\[ +F_x=\sum_i r_i-M + \ge3(M+1)-M=2M+3>7, \tag{17} +\] + +contradicting the seven available `x` items. Selecting such a source and +following the anchor corridor either exhausts it or returns to `x` with +strictly larger energy. This is also an immediate consequence of Debt +Recovery, but (17) is useful for the low-energy boundary: an all-`x` state +with `M=2` can be terminal only when all three caps are exactly 3. + +## 4. A sibling whose next event exhausts + +Let a legal terminal `q` sibling of cap `r` exhaust first, with final color +`x`. Let `u,v` be the other two terminal `q` caps. After this event the +three surviving caps are the bad cap `s` and `u,v`. + +### 4.1 If `a != q`, every exhausting sibling branch is safe + +The parent has the two permanent anchors `a` and `f` from (12). The +exhausting update can add its final run to at most one of those colors, so at +least one survives as a nonpositive coordinate at `z=1`. + +If `x!=a`, use `a` as the surviving anchor. The bad source already has top +`a`. Bring the other two active columns to `a`, unless one exhausts first. +At the resulting all-`a` checkpoint the energy is at least + +\[ +M_a\ge A+u+v\ge A+2(E+1)\ge3. \tag{18} +\] + +The last inequality uses `A>=1` when `E=0` and is stronger when `E>=1`. + +If `x=a`, then `f` survives. Bring all three active columns to `f`; the +energy is at least + +\[ +M_f\ge s+u+v\ge1+2(E+1)\ge3. \tag{19} +\] + +An intermediate exhaustion is already the goal `z=2`; otherwise Debt +Recovery applies to (18) or (19). Thus all 270 `a!=q` sibling edges are +safe whenever the chosen sibling's next event is exhausting, independently +of its final color. + +### 4.2 If `a=q` and the final color is not `f`, the branch is safe + +Here `f` remains a zero-debt anchor. All three survivors still have top +`q`. Bring them to `f`, unless one exhausts first. The resulting energy is +at least + +\[ +M_f\ge s+u+v\ge3, \tag{20} +\] + +so this branch is checkpoint-YES. + +### 4.3 If `a=q` and the sibling also exhausts to `f` + +This is the only low-energy direct-exhaustion branch. Put + +\[ +M=Q-r=s+E-r. \tag{21} +\] + +After the sibling exhausts, all three surviving tops are `q`, and + +\[ +d_q=-M,\qquad d_f=7-r>0,\qquad d_g,d_h>0. \tag{22} +\] + +Thus the resulting state is immediately `Tq` precisely when + +\[ +\min\{s,u,v\}>M. \tag{23} +\] + +If `M>=3`, Debt Recovery proves YES. For `M<=2`, condition (23) is the +exact immediate-terminal test. + +There is an additional fixed-decoration constraint. The bad edge already +reserves `7-s` hidden items of color `f`, and this alternative exhausting +sibling would reserve another `7-r`. Equation (9) says that all seven `f` +items are hidden at `P`. The two tails coexist in one fixed future exactly +when + +\[ +(7-s)+(7-r)\le7 +\quad\Longleftrightarrow\quad +r\ge7-s. \tag{24} +\] + +This is not implied by checking the alternative successor macro state in +isolation. + +Under (24), an immediate terminal with `M=2` is impossible. If it existed, +then `s,u,v>=3`. Since the `q`-exposed count in `D` gives + +\[ +r+u+v-E\le7 \tag{25} +\] + +and `r=s+E-2`, we would have `s+u+v<=9`. Hence +`s=u=v=3` and `r=E+1`. But (24) would require `r>=4`, contradicting +`E<=2`. + +Consequently the jointly realizable direct terminals are exactly + +\[ +\begin{array}{ll} +M=0, &\text{or}\\ +M=1\text{ and }\min\{s,u,v\}\ge2, +\end{array} \tag{26} +\] + +together with (21) and (24). + +If `M<=2` but (23) fails, the branch is safe. The only nontrivial case is +`M=1`, where a surviving cap 1 can be selected. A return to `q` with old +cap at least 3 raises the energy to at least 3. A return with old cap 2 +raises it to 2. Were that new all-`q` state terminal, (17) at equality +would force all three caps to be 3. The selected cap 1 cannot be the bad +cap, since `s=1` and `M=1` would give `r=E`, contrary to `r>E`. Hence +`E=0`; the two unchanged caps being 3 would force `s=3,r=2`, contradicting +the joint budget `r>=7-s=4`. Thus another legal source remains and the next +return raises the energy to at least 3. + +Here is the implicit low-energy dichotomy used in that paragraph. If some +color other than `q` is nonpositive, use it as a fresh anchor; bringing all +three columns to it contributes at least three units of energy. Otherwise +the other three debts are positive, so nonterminality of the all-`q` state +forces a current `q` cap at most `M`. This is the source used for the return +argument above. + +#### Why the macro count is 41/79 but the decoration count is 12 + +With the stored canonical bad-edge witness, an isolated macro replay finds +41 `a=q` edges and 79 physical sibling-source cards whose exhaustion to `f` +would by itself produce `Tq`. Of those 79 cards, 67 violate (24): they +cannot coexist with the bad tail that defines the bridge. They are not +removed by choosing another strategy; they are absent from the joint fixed +decoration universe. + +After (24), 12 physical cards remain, on 12 canonical edges and 10 canonical +parents. Eight have `M=0` and four have `M=1`. These are precisely the +low-energy direct-terminal corner (26). If all color-symmetric labeled bad +actions are retained instead of the report's one stored witness, the same +corner has 17 labeled action identities; the canonical-witness count used +here is 12. + +For completeness, after reserving both `f` tails the two untouched `q` +columns have residual color counts + +\[ +\begin{aligned} +R_q&=7-r-u-v+E,\\ +R_f&=s+r-7,\\ +R_g&=7-p_g,\\ +R_h&=7-p_h. +\end{aligned} \tag{27} +\] + +They sum to `14-u-v`. The first is nonnegative by (25), the second exactly +by (24), and + +\[ +R_g+R_h=14-(s+E)\ge6. \tag{28} +\] + +Thus the two residual words can both start with a non-`q` color. In this +normal form, (24) is the exact extra decoration-level obstruction, rather +than merely a necessary color count. + +## 5. A sibling whose next event is live + +Let the live event be + +\[ +q_r\longrightarrow x_R,\qquad r0`. If `x=f`, the two other positive +coordinates of `D` remain positive, so (30) has three positive coordinates +and the bad source is illegal at `z=0`. + +If `x` is one of the two positive colors different from `f`, say its +terminal debt is `p_x`, then (30) has at most two positive coordinates +exactly when + +\[ +r\ge p_x. \tag{31} +\] + +Therefore the live-to-bad handoff is legal exactly under (31), with +`x!=f`. + +After taking the bad exhaustion, live and exhausting debt updates commute, +and the `z=1` state is + +\[ +C=D+r e_q-r e_x. \tag{32} +\] + +It has active tops `x_R,q_u,q_v` and debts + +\[ +d_x(C)=-(r-p_x)=-N,\qquad +d_q(C)=r-E>0, \tag{33} +\] + +while the other two non-`x` debts are positive. Hence + +\[ +N=r-p_x. \tag{34} +\] + +If `N>=3`, Debt Recovery immediately proves checkpoint-YES. + +### 5.2 The exact low-energy handoff corner + +For `N<=2`, use `x` as an anchor and advance the two `q` columns to `x` or +to exhaustion. If their old caps at first entry into `x` are `c_1,c_2`, +the all-`x` energy is + +\[ +M=N+c_1+c_2\ge N+2(E+1). \tag{35} +\] + +Debt Recovery handles `M>=3`. Equality below 3 is possible only when + +\[ +E=0,\qquad N=0,\qquad c_1=c_2=1. \tag{36} +\] + +Thus `r=p_x`, the two remaining terminal `q` caps are both 1, and their +entries into `x` are direct. At energy 2, an all-`x` terminal would have to +have caps exactly `(3,3,3)` by (17). Consequently the full corner is + +\[ +\begin{gathered} +E=0,\quad r=p_x,\quad u=v=1,\\ +q_r\to x_3,\quad q_1\to x_3,\quad q_1\to x_3. + \tag{37} +\end{gathered} +\] + +The last entrance in (37) is a **unique-source** same-level `Tq` entrance. +Immediately before it, `d_x=-1`; testing either existing `x_3` source makes +all four coordinates positive, whereas the final `q_1` source is legal. +Therefore the same-level sibling lemma does not eliminate (37). If the +all-`x` state is not terminal, a cap at most 2 remains legal and one more +anchor cycle raises the energy to at least 3. + +The color accounting in (37) is tight rather than spurious: `F_x(P)=p_x=r`, +and the three displayed `x` runs consume + +\[ +(3-r)+2+2=7-r +\] + +hidden `x` items, exactly the remaining supply. + +## 6. Live events without a bad-source handoff + +### 6.1 Persistence when `a != q` + +At a parent of form (12), an untouched `q_u` sibling remains legal after +any live event (29). Before the event its source test already has positive +`q` and `b` coordinates. The change `+r e_q-r e_x` cannot introduce a new +positive coordinate at `q`, and the subtraction cannot introduce one +anywhere. Thus all untouched `q` siblings persist. + +The colors `a` and `f` remain nonpositive anchors. A moved column whose top +is neither can be followed until it exhausts or first reaches `a` or `f`. +Process the three `q` siblings in this way. If one exhausts during this +first sweep, one of `a,f` survives at `z=1`. Bringing the two other sibling +columns to `a` gives the lower bound (18), or bringing all three survivors +to `f` gives (19); hence that branch is safe. + +If no sibling exhausts, all four active tops lie in `{a,f}`. + +### 6.2 The two-anchor reduction + +Consider a `z=0` state with + +\[ +d_\alpha=-A\le0,\qquad d_\beta=-B\le0, \tag{38} +\] + +and all active tops in `{alpha,beta}`. If the other two debts are positive, +an `alpha` source of cap `c` is legal exactly when `c<=A`, and a `beta` +source is legal exactly when `c<=B`. + +If those two debts are not both positive, there is at most one positive +coordinate. Then the still-reserved bad source is legal. In this bridge +application its old and final colors are exactly the two original anchors. +Exhaust it immediately; the third nonpositive coordinate is untouched and +survives at `z=1`. + +It remains to iterate only in the region where the two non-anchor debts are +positive. Choose a legal anchor source. If it is the reserved bad source, +its next event exhausts and gives the first outcome below. Otherwise its +live departure leaves its old anchor nonpositive. If it enters a +non-anchor color, the other anchor is also unchanged, so the same column can +be followed until it exhausts or first returns to `{alpha,beta}`. At an +all-anchor checkpoint the total anchor energy never decreases; it increases +strictly whenever the excursion has a non-anchor intermediate run. Every +event strictly advances a fixed finite run chain. + +It follows that this procedure has only two possible `z=0` outcomes: + +1. a first exhaustion is reached; or +2. an all-anchor state has no legal source. + +The second outcome is exactly a `D2` terminal. In exact coordinates it has + +\[ +d=(-A,-B,X,Y),\qquad A+B=X+Y,qquad X,Y>0, \tag{39} +\] + +all tops in the two anchor colors, and + +\[ +\begin{array}{ll} +c>A &\text{for every `alpha`-top cap }c,\\ +c>B &\text{for every `beta`-top cap }c. +\end{array} \tag{40} +\] + +The host multiplicities are `3+1` or `2+2`. For a putative `4+0` terminal, +the unused anchor has no host and hence cannot have negative debt, so its +energy is zero. The occupied anchor energy is then `X+Y>=2`. Four caps +strictly above that energy would give +`F>=4(A+1)-A=3A+4>=10`, contradicting `F<=7`. + +This is a genuine residual family, not an artifact of the inequalities. For +example, the normal-form parent + +\[ +d_P=(0,0,-1,1),qquad +\text{tops }q_1,q_1,q_1,a_6 \tag{41} +\] + +can have its three `q` runs enter `a_3,f_3,f_3`. The resulting state has + +\[ +d=(3,1,-2,-2),\qquad +\text{anchor caps }(6,3)\text{ and }(3,3), \tag{42} +\] + +and every source test has three positive coordinates. The macro state is +physically consistent. It also respects the reserved bad tail in the +displayed instance: the bad tail uses one `f`, and the two `q_1->f_3` runs +use four more. + +For the **first** `a!=q` sweep, a terminal can only have multiplicity `2+2`. +Indeed, suppose `m` of the three siblings first enter `a`. The anchor +energies are + +\[ +A'=A+\sum_{i\to a}c_i,qquad +B'=\sum_{j\to f}c_j, \tag{43} +\] + +where every entry cap is greater than `E`. + +- If `m=0`, the three `f` sources give `B'>=3`; if all their caps exceeded + `B'`, then `F_f>=2B'+3>7`. +- If `m=2`, then `A'>=3` (using `A>=1` when `E=0`); the three `a` sources + similarly give `F_a>7`. +- If `m=3`, the four-`a` bound is even stronger. + +Thus `m=1`. With one sibling entering `a` at old cap `c_a` and two entering +`f` at old caps `c_1,c_2`, the exact first-sweep `D2` conditions are + +\[ +\begin{gathered} +A'=A+c_a,\qquad B'=c_1+c_2,\\ +d_q>0,qquad d_b>0,\\ +s>A',\quad R_a>A',\quad R_{f,1}>B',\quad R_{f,2}>B'. + \tag{44} +\end{gathered} +\] + +The first inequality also says `c_a0, \tag{47} +\] + +with one `f_R` source and the three remaining `q` sources. The `f_R` source +is illegal because `R>r`. A remaining `q` cap `c` is legal exactly when +`c<=Q-r`. The bad cap is never such a source, since + +\[ +s-(Q-r)=r-E>0. \tag{48} +\] + +Therefore (47) is an immediate `D2` terminal of multiplicity `3+1` +precisely when the two other terminal caps satisfy + +\[ +u>Q-r,qquad v>Q-r. \tag{49} +\] + +At decoration level the new live `f` run and the reserved bad tail coexist +only when + +\[ +R-r\le s. \tag{50} +\] + +If (49) fails, a legal `q` source remains and the same two-anchor reduction +continues. It may still terminate at a later `D2`; no lemma in this note +eliminates that terminal. + +## 7. What happens after a first exhaustion from a two-anchor path + +Every legal exhaustion produced by the two-anchor procedure reaches a `z=1` +state with at least one nonpositive coordinate. Indeed, immediately before +the final run is exposed, the source-test vector in (1) has at most two +positive coordinates. The final run increases only its own color +coordinate, so the successor has at most three positive coordinates. This +argument does not require the old anchor itself to remain nonpositive. + +Using that coordinate as an anchor, advance every non-anchor-top source to +the anchor or to exhaustion. If the resulting all-anchor energy is at least +3, Debt Recovery finishes. If a second coordinate is nonpositive, use it as +a new anchor: bringing the three active columns to it, unless one exhausts, +creates energy at least 3. We may therefore assume that the other three +debts are positive. In that case a nonterminal all-anchor state of energy +`M` has a source cap at most `M`; otherwise all four source-test coordinates +would be positive. For `M=2`, one departure and return raises the energy to +at least 3. For `M=1`, the first return raises it to at least 2 and, if the +state is still nonterminal, one more return raises it to at least 3. Thus at +energy at most 2 the only possible failures are: + +1. the first exhausting event itself has produced an all-top-equal `Tq` + terminal; or +2. the anchor corridor enters a `Tq` terminal through a same-level + **unique-source** edge, characterized by `p_x>r`. + +A same-level sibling entrance is removed by the existing sibling-entry +lemma. A nonterminal all-anchor state of energy 2 gains energy at the next +return; an energy-1 state can require two returns, and the only terminal +created on the first return is exactly the same-level `Tq` case just listed. + +Thus a live non-handoff branch is rigorously reduced to `D2` before the first +exhaustion, plus direct or unique-source low-energy `Tq` after it. This note +does not identify those residual cases with YES. + +## 8. Reduction ledger + +| Branch | Strict conclusion | Input used | +|---|---|---| +| `a!=q`, sibling next event exhausts | YES | surviving anchor, energy bounds (18)-(19), Debt Recovery | +| `a=q`, sibling exhausts to `x!=f` | YES | zero `f` anchor, (20), Debt Recovery | +| `a=q`, sibling exhausts to `f`, `M>=3` | YES | Debt Recovery | +| same branch, `M<=2`, not immediately terminal | YES | low-energy anchor rotor plus joint budget (24) | +| same branch, joint immediate terminal | unresolved 12-card corner (26) | exact fixed-decoration count | +| live sibling, bad handoff, `N>=3` | YES | exact handoff (31), Debt Recovery | +| live handoff, `N<=2` | YES except the unique corner (37) | anchor corridor and same-level entrance test | +| live branch without handoff | reduces to `D2`, then possible low-energy unique `Tq` after exhaustion | two-anchor reduction and sibling-entry lemma | + +The unresolved objects are therefore explicit: + +- jointly realizable `D2` terminals satisfying (39)-(40), including the + first-sweep `2+2` conditions (44)-(45) and the `a=q` `3+1` condition + (47)-(50); +- the 12-card direct-exhaustion `Tq` corner (26); +- the unique-source same-level `Tq` corner (37), and any later unique-source + `Tq` entrance described in Section 7. + +Eliminating those objects needs an additional argument or an exact fixed-word +classification. Nothing in this note promotes the reduction to a proof of +the whole first-exhaustion bridge family, still less to a proof for all +height-7 layouts. diff --git a/scripts/validate_c4_h7_tq_exhaust_siblings_report.py b/scripts/validate_c4_h7_tq_exhaust_siblings_report.py new file mode 100644 index 0000000..6cc7f15 --- /dev/null +++ b/scripts/validate_c4_h7_tq_exhaust_siblings_report.py @@ -0,0 +1,317 @@ +#!/usr/bin/env python3 +"""Strict claim-boundary validator for the first-exhaustion Tq census.""" + +from __future__ import annotations + +import argparse +import json +from pathlib import Path +from typing import NoReturn + + +SCOPE = "first_exhaustion_tq_sibling_next_run_forks" +LIMIT_UNIT = "raw_all_q_next_run_decorations" +EXPECTED = { + "terminal_count": 71, + "labeled_candidates": 624, + "canonical_parents": 418, + "canonical_edges": 429, + "unique_source_parents": 6, + "sibling_parents": 412, + "unique_source_edges": 6, + "sibling_edges": 423, +} +EXPECTED_PARENT_DISTRIBUTION = {"2": 1, "3": 12, "4": 399} +EXPECTED_EDGE_DISTRIBUTION = {"2": 2, "3": 14, "4": 407} +EXPECTED_RAW = { + "legal_sibling_cards": 18_177, + "legal_sibling_joint_decorations": 1_220_361, + "all_q_joint_decorations": 1_256_148, +} +EXPECTED_NONNEGATIVE = 406_528 +EXPECTED_FEASIBLE = 403_685 +EXPECTED_RESIDUAL_WORDS = 6_131_033_832 +EXPECTED_CLASS_COUNTS = { + "two_exhaustion": 70_633, + "live_bad_persistent": 254_899, + "obstruction": 78_153, +} +EXPECTED_CLASS_WEIGHTS = { + "two_exhaustion": 8_629_839, + "live_bad_persistent": 3_235_811_235, + "obstruction": 2_886_592_758, +} +EXPECTED_REFINED_COUNTS = { + "direct_certified": 101_922, + "n_ge_3_certified": 11_226, + "n_le_2_certified": 223_321, + "d2_reduction": 67_206, + "tq_corner_only": 10, +} +EXPECTED_REFINED_WEIGHTS = { + "direct_certified": 13_128_393, + "n_ge_3_certified": 10_591_970, + "n_le_2_certified": 3_223_219_144, + "d2_reduction": 2_883_858_705, + "tq_corner_only": 235_620, +} + + +def fail(message: str) -> NoReturn: + raise SystemExit(message) + + +def require(condition: bool, message: str) -> None: + if not condition: + fail(message) + + +def obj(value: object, label: str) -> dict[str, object]: + require(isinstance(value, dict), f"{label} must be an object") + return value + + +def array(value: object, label: str) -> list[object]: + require(isinstance(value, list), f"{label} must be an array") + return value + + +def integer(value: object, label: str, minimum: int = 0) -> int: + require( + isinstance(value, int) and not isinstance(value, bool), + f"{label} must be an integer", + ) + require(value >= minimum, f"{label} must be at least {minimum}") + return value + + +def distribution(value: object, label: str) -> dict[str, int]: + result = obj(value, label) + require( + all(isinstance(key, str) and isinstance(count, int) for key, count in result.items()), + f"{label} must map string keys to integer counts", + ) + return {key: int(count) for key, count in result.items()} + + +def class_pair( + value: object, + label: str, + names: set[str] | None = None, +) -> tuple[dict[str, int], dict[str, int]]: + """Accept the canonical nested class schema and reject ambiguous shapes.""" + + classes = obj(value, label) + expected_names = set(EXPECTED_CLASS_COUNTS) if names is None else names + require(set(classes) == expected_names, f"{label} has wrong class keys") + counts: dict[str, int] = {} + weights: dict[str, int] = {} + for name, raw in classes.items(): + entry = obj(raw, f"{label}.{name}") + require(set(entry) >= {"decorations", "residual_words"}, f"{label}.{name} lacks counts") + counts[name] = integer(entry["decorations"], f"{label}.{name}.decorations") + weights[name] = integer(entry["residual_words"], f"{label}.{name}.residual_words") + return counts, weights + + +def read_json(path: Path, label: str) -> dict[str, object]: + require(path.is_file(), f"missing {label}: {path}") + try: + value = json.loads(path.read_text(encoding="utf-8")) + except (OSError, UnicodeError, json.JSONDecodeError) as error: + fail(f"cannot parse {label} {path}: {error}") + return obj(value, label) + + +def validate( + report_path: Path, + output_dir: Path, + audit_path: Path | None, +) -> str: + report = read_json(report_path, "production report") + require((output_dir / "summary.md").is_file(), "missing summary.md") + require(report.get("schema_version") == 1, "unsupported schema_version") + require(report.get("coverage_scope") == SCOPE, "wrong coverage_scope") + require(report.get("limit_unit") == LIMIT_UNIT, "wrong limit_unit") + require(report.get("self_checks_passed") is True, "production self-checks failed") + require(report.get("status") in {"NEXT_RUN_CENSUS_COMPLETE", "INCOMPLETE"}, "unsupported status") + for key in ( + "verified", + "next_run_universe_complete", + "full_residual_word_coverage", + "entry_family_eliminated", + "full_layout_coverage", + ): + require(isinstance(report.get(key), bool), f"{key} must be Boolean") + require(report["full_residual_word_coverage"] is False, "next-run census cannot claim residual-word coverage") + require(report["entry_family_eliminated"] is False, "next-run census cannot claim entry-family elimination") + require(report["full_layout_coverage"] is False, "next-run census cannot claim full-layout coverage") + + model = obj(report.get("model"), "model") + require( + model == {"colors": 4, "height": 7, "empty_columns": 2}, + f"wrong model dimensions: {model}", + ) + bridge = obj(report.get("bridge"), "bridge") + for key, expected in EXPECTED.items(): + require(bridge.get(key) == expected, f"bridge.{key} must be {expected}") + require( + distribution(bridge.get("parent_legal_source_distribution"), "bridge.parent_legal_source_distribution") + == EXPECTED_PARENT_DISTRIBUTION, + "parent legal-source distribution mismatch", + ) + require( + distribution(bridge.get("edge_legal_source_distribution"), "bridge.edge_legal_source_distribution") + == EXPECTED_EDGE_DISTRIBUTION, + "edge legal-source distribution mismatch", + ) + for key in ("action_unique", "all_edges_replay", "all_final_colors_isolated"): + require(bridge.get(key) is True, f"bridge.{key} must be true") + + raw = obj(report.get("raw"), "raw") + for key, expected in EXPECTED_RAW.items(): + require(raw.get(key) == expected, f"raw.{key} must be {expected}") + checked = integer(raw.get("checked"), "raw.checked") + require(checked <= EXPECTED_RAW["all_q_joint_decorations"], "raw.checked exceeds universe") + + census = obj(report.get("census"), "census") + nonnegative = integer(census.get("nonnegative_decorations"), "census.nonnegative_decorations") + feasible = integer(census.get("feasible_decorations"), "census.feasible_decorations") + infeasible = integer(census.get("infeasible_decorations"), "census.infeasible_decorations") + residual_words = integer(census.get("residual_words"), "census.residual_words") + require(feasible + infeasible == checked, "feasible/infeasible counts do not partition checked decorations") + require(feasible <= nonnegative <= checked, "nonnegative/Hall-feasible counts are inconsistent") + legacy_counts, legacy_weights = class_pair(census.get("legacy"), "census.legacy") + require(sum(legacy_counts.values()) == feasible, "legacy classes do not partition Hall-feasible decorations") + require(sum(legacy_weights.values()) == residual_words, "legacy weights do not partition residual words") + refined_counts, refined_weights = class_pair( + census.get("refined"), "census.refined", set(EXPECTED_REFINED_COUNTS) + ) + require(sum(refined_counts.values()) == feasible, "refined classes do not partition Hall-feasible decorations") + require(sum(refined_weights.values()) == residual_words, "refined weights do not partition residual words") + + rows = array(report.get("per_edge"), "per_edge") + require(len(rows) == EXPECTED["sibling_edges"], "per_edge must contain all 423 sibling edges") + seen_ids: set[str] = set() + row_raw_expected = row_checked = row_feasible = row_infeasible = row_words = 0 + row_class_counts: dict[str, int] = {name: 0 for name in EXPECTED_CLASS_COUNTS} + row_class_weights: dict[str, int] = {name: 0 for name in EXPECTED_CLASS_COUNTS} + row_refined_counts: dict[str, int] = {name: 0 for name in EXPECTED_REFINED_COUNTS} + row_refined_weights: dict[str, int] = {name: 0 for name in EXPECTED_REFINED_COUNTS} + for index, raw_row in enumerate(rows): + row = obj(raw_row, f"per_edge[{index}]") + edge_id = row.get("edge_id") + require(isinstance(edge_id, str) and edge_id, f"per_edge[{index}].edge_id invalid") + require(edge_id not in seen_ids, f"duplicate edge_id {edge_id}") + seen_ids.add(edge_id) + expected = integer(row.get("raw_expected"), f"{edge_id}.raw_expected") + edge_checked = integer(row.get("raw_checked"), f"{edge_id}.raw_checked") + edge_feasible = integer(row.get("feasible"), f"{edge_id}.feasible") + edge_infeasible = integer(row.get("infeasible"), f"{edge_id}.infeasible") + edge_words = integer(row.get("residual_words"), f"{edge_id}.residual_words") + require(edge_checked <= expected, f"{edge_id} checked more than its universe") + require(edge_feasible + edge_infeasible == edge_checked, f"{edge_id} classifications do not sum") + counts, weights = class_pair(row.get("legacy"), f"{edge_id}.legacy") + refined_edge_counts, refined_edge_weights = class_pair( + row.get("refined"), f"{edge_id}.refined", set(EXPECTED_REFINED_COUNTS) + ) + require(sum(counts.values()) == edge_feasible, f"{edge_id} legacy classes do not sum") + require(sum(weights.values()) == edge_words, f"{edge_id} legacy weights do not sum") + require(sum(refined_edge_counts.values()) == edge_feasible, f"{edge_id} refined classes do not sum") + require(sum(refined_edge_weights.values()) == edge_words, f"{edge_id} refined weights do not sum") + row_raw_expected += expected + row_checked += edge_checked + row_feasible += edge_feasible + row_infeasible += edge_infeasible + row_words += edge_words + for name in row_class_counts: + row_class_counts[name] += counts[name] + row_class_weights[name] += weights[name] + for name in row_refined_counts: + row_refined_counts[name] += refined_edge_counts[name] + row_refined_weights[name] += refined_edge_weights[name] + require(row_raw_expected == EXPECTED_RAW["all_q_joint_decorations"], "per-edge raw universes do not sum") + require(row_checked == checked, "per-edge checked counts disagree with raw.checked") + require(row_feasible == feasible and row_infeasible == infeasible, "per-edge feasibility totals disagree") + require(row_words == residual_words, "per-edge residual weights disagree") + require(row_class_counts == legacy_counts, "per-edge legacy counts disagree") + require(row_class_weights == legacy_weights, "per-edge legacy weights disagree") + require(row_refined_counts == refined_counts, "per-edge refined counts disagree") + require(row_refined_weights == refined_weights, "per-edge refined weights disagree") + + samples = array(report.get("replay_samples"), "replay_samples") + sample_ids: set[str] = set() + for index, raw_sample in enumerate(samples): + sample = obj(raw_sample, f"replay_samples[{index}]") + sample_id = sample.get("sample_id") + require(isinstance(sample_id, str) and sample_id, "sample_id must be nonempty") + require(sample_id not in sample_ids, f"duplicate sample_id {sample_id}") + sample_ids.add(sample_id) + for raw_row in rows: + row = obj(raw_row, "per_edge row") + sample_id = row.get("sample_id") + require(sample_id is None or sample_id in sample_ids, f"unknown sample_id {sample_id!r}") + + complete = checked == EXPECTED_RAW["all_q_joint_decorations"] + status = str(report["status"]) + if status == "NEXT_RUN_CENSUS_COMPLETE": + require(complete, "complete status has unchecked decorations") + require(report["verified"] is True, "complete status requires verified=true") + require(report["next_run_universe_complete"] is True, "complete status requires complete-universe flag") + require(nonnegative == EXPECTED_NONNEGATIVE, "full nonnegative count mismatch") + require(feasible == EXPECTED_FEASIBLE, "full Hall-feasible count mismatch") + require(residual_words == EXPECTED_RESIDUAL_WORDS, "full residual-word weight mismatch") + require(legacy_counts == EXPECTED_CLASS_COUNTS, "full legacy class counts mismatch") + require(legacy_weights == EXPECTED_CLASS_WEIGHTS, "full legacy class weights mismatch") + require(refined_counts == EXPECTED_REFINED_COUNTS, "full refined class counts mismatch") + require(refined_weights == EXPECTED_REFINED_WEIGHTS, "full refined class weights mismatch") + else: + require(not complete, "a complete census may not use INCOMPLETE") + require(report["verified"] is False, "INCOMPLETE must set verified=false") + require(report["next_run_universe_complete"] is False, "INCOMPLETE may not claim complete universe") + + if audit_path is not None: + audit = read_json(audit_path, "independent audit") + scalar_map = { + "terminal_count": bridge["terminal_count"], + "labeled_reverse_candidates": bridge["labeled_candidates"], + "canonical_parent_count": bridge["canonical_parents"], + "canonical_edge_count": bridge["canonical_edges"], + "unique_source_parent_count": bridge["unique_source_parents"], + "sibling_parent_count": bridge["sibling_parents"], + "sibling_edge_count": bridge["sibling_edges"], + "raw_individual_legal_sibling_cards": raw["legal_sibling_cards"], + "raw_joint_legal_sibling_decorations": raw["legal_sibling_joint_decorations"], + "raw_all_q_next_run_decorations": raw["all_q_joint_decorations"], + } + for key, value in scalar_map.items(): + require(audit.get(key) == value, f"independent audit disagrees on {key}") + if complete: + require(audit.get("nonnegative_decorations") == nonnegative, "audit nonnegative mismatch") + require(audit.get("hall_feasible_decorations") == feasible, "audit feasible mismatch") + require(audit.get("residual_word_weight") == residual_words, "audit residual weight mismatch") + require(audit.get("classification_counts") == legacy_counts, "audit class-count mismatch") + require(audit.get("classification_weights") == legacy_weights, "audit class-weight mismatch") + require(audit.get("refined_classification_counts") == refined_counts, "audit refined-count mismatch") + require(audit.get("refined_classification_weights") == refined_weights, "audit refined-weight mismatch") + + require(not (output_dir / "no-instance.txt").exists(), "next-run census must not publish a global-NO witness") + return status + + +def main() -> None: + parser = argparse.ArgumentParser(description=__doc__) + 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: + args.status_file.parent.mkdir(parents=True, exist_ok=True) + args.status_file.write_text(status + "\n", encoding="utf-8") + print(f"strict first-exhaustion Tq report validation passed: status={status}") + + +if __name__ == "__main__": + main() diff --git a/tests/check_c4_h7_tq_exhaust_siblings.py b/tests/check_c4_h7_tq_exhaust_siblings.py new file mode 100644 index 0000000..e21b135 --- /dev/null +++ b/tests/check_c4_h7_tq_exhaust_siblings.py @@ -0,0 +1,1292 @@ +#!/usr/bin/env python3 +"""Independent audit for the c=4, k=2, h=7 first-exhaustion Tq forks. + +The checker deliberately does not import the production executable or the +macro-reconnaissance script. It reconstructs the numerical border model, +replays every exhausting entrance in the *parent's* labelled coordinates, +enumerates the committed next run of all three surviving q columns, and +counts compatible complete residual words without expanding those words. + +``--program`` runs a bounded production differential. ``--report`` checks +an existing production report, including every replayable sample. +""" + +from __future__ import annotations + +import argparse +import copy +import itertools +import json +import math +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, NoReturn, Sequence + + +HEIGHT = 7 +COLORS = 4 +EMPTY_COLUMNS = 2 +SCOPE = "first_exhaustion_tq_sibling_next_run_forks" + +EXPECTED_TERMINALS = 71 +EXPECTED_LABELED_CANDIDATES = 624 +EXPECTED_PARENTS = 418 +EXPECTED_EDGES = 429 +EXPECTED_UNIQUE_PARENTS = 6 +EXPECTED_SIBLING_PARENTS = 412 +EXPECTED_SIBLING_EDGES = 423 +EXPECTED_A_NOT_Q_EDGES = 270 +EXPECTED_A_EQ_Q_EDGES = 153 +EXPECTED_RAW_INDIVIDUAL = 18_177 +EXPECTED_RAW_LEGAL_JOINT = 1_220_361 +EXPECTED_RAW_ALL_Q = 1_256_148 +EXPECTED_NONNEGATIVE = 406_528 +EXPECTED_HALL_FEASIBLE = 403_685 +EXPECTED_RESIDUAL_WEIGHT = 6_131_033_832 +EXPECTED_CLASS_COUNTS = { + "two_exhaustion": 70_633, + "live_bad_persistent": 254_899, + "obstruction": 78_153, +} +EXPECTED_CLASS_WEIGHTS = { + "two_exhaustion": 8_629_839, + "live_bad_persistent": 3_235_811_235, + "obstruction": 2_886_592_758, +} +EXPECTED_REFINED_COUNTS = { + "direct_certified": 101_922, + "n_ge_3_certified": 11_226, + "n_le_2_certified": 223_321, + "d2_reduction": 67_206, + "tq_corner_only": 10, +} +EXPECTED_REFINED_WEIGHTS = { + "direct_certified": 13_128_393, + "n_ge_3_certified": 10_591_970, + "n_le_2_certified": 3_223_219_144, + "d2_reduction": 2_883_858_705, + "tq_corner_only": 235_620, +} + +Bucket = tuple[int, tuple[int, ...]] +State = tuple[Bucket, Bucket, Bucket, Bucket] +ExhaustingAction = tuple[int, int, int] # old color, old cap, final color +Card = tuple[int, int] # next color, cumulative endpoint + + +def require(condition: bool, message: str) -> None: + if not condition: + raise AssertionError(message) + + +def fail(message: str) -> NoReturn: + raise AssertionError(message) + + +def canonical_state( + debts: Sequence[int], columns: Iterable[tuple[int, int]] +) -> State: + caps_by_color: list[list[int]] = [[] for _ in range(COLORS)] + for color, cap in columns: + caps_by_color[color].append(cap) + result = tuple( + sorted( + (int(debts[color]), tuple(sorted(caps_by_color[color]))) + for color in range(COLORS) + ) + ) + require(len(result) == COLORS, "canonical state lost a color") + return result # 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: + 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) + multiplicity = tuple(len(caps) for _, caps in state) + if any( + not multiplicity[color] <= exposed[color] <= HEIGHT + for color in range(COLORS) + ): + return False + remaining = tuple(HEIGHT - count for count in exposed) + return all( + multiplicity[color] + <= sum(remaining[other] for other in range(COLORS) if other != color) + for color in range(COLORS) + ) + + +def source_is_legal( + debts_or_state: Sequence[int] | State, + exhausted: int, + color: int, + cap: int, +) -> bool: + if len(debts_or_state) == COLORS and isinstance(debts_or_state[0], tuple): + debts = [bucket[0] for bucket in debts_or_state] # type: ignore[index] + else: + debts = [int(value) for value in debts_or_state] # type: ignore[arg-type] + debts[color] += cap + return sum(value > 0 for value in debts) <= 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( + (color, cap) + for color, cap in physical_sources(state) + if source_is_legal(state, exhausted, color, cap) + ) + + +def enumerate_tq_terminals() -> tuple[State, ...]: + terminals: set[State] = set() + for magnitude in range(3): + for caps in itertools.combinations_with_replacement(range(1, HEIGHT), 3): + if min(caps) <= magnitude or sum(caps) - magnitude > HEIGHT: + continue + for positive in itertools.combinations_with_replacement( + range(1, HEIGHT + 1), 3 + ): + if sum(positive) - magnitude != HEIGHT: + continue + state = tuple( + sorted(((-magnitude, caps), *((value, ()) for value in positive))) + ) + 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 apply_exhausting_canonical( + parent: State, exhausted: int, action: ExhaustingAction +) -> State | None: + old_color, old_cap, final_color = action + if old_color == final_color or not 1 <= old_cap < HEIGHT: + return None + if not 0 <= old_color < COLORS or not 0 <= final_color < COLORS: + return None + if old_cap not in parent[old_color][1]: + return None + if not source_is_legal(parent, exhausted, old_color, old_cap): + return None + debts = [debt for debt, _ in parent] + caps = [list(bucket_caps) for _, bucket_caps in parent] + caps[old_color].remove(old_cap) + debts[old_color] += old_cap + debts[final_color] += HEIGHT - old_cap + successor = canonical_state( + debts, + ((color, cap) for color in range(COLORS) for cap in caps[color]), + ) + return successor if state_is_consistent(successor, exhausted + 1) else None + + +def exhausting_actions_to(parent: State, terminal: State) -> tuple[ExhaustingAction, ...]: + actions: list[ExhaustingAction] = [] + for old_color, (_, caps) in enumerate(parent): + for old_cap in sorted(set(caps)): + if not source_is_legal(parent, 0, old_color, old_cap): + continue + for final_color in range(COLORS): + action = old_color, old_cap, final_color + if apply_exhausting_canonical(parent, 0, action) == terminal: + actions.append(action) + return tuple(actions) + + +def reverse_bridge( + terminals: Sequence[State], +) -> tuple[int, tuple[tuple[State, State], ...]]: + labeled: list[tuple[State, State]] = [] + for terminal in terminals: + for old_cap in range(1, HEIGHT): + for old_color in range(COLORS): + for final_color in range(COLORS): + if old_color == final_color: + continue + debts = [debt for debt, _ in terminal] + caps = [list(bucket_caps) for _, bucket_caps in terminal] + debts[old_color] -= old_cap + debts[final_color] -= HEIGHT - old_cap + caps[old_color].append(old_cap) + if not source_is_legal(debts, 0, old_color, old_cap): + continue + parent = canonical_state( + debts, + ((color, cap) for color in range(COLORS) for cap in caps[color]), + ) + if state_is_consistent(parent, 0): + labeled.append((parent, terminal)) + return len(labeled), tuple(sorted(set(labeled))) + + +@dataclass(frozen=True) +class Edge: + edge_id: str + parent: State + terminal: State + action: ExhaustingAction + q_color: int + q_caps: tuple[int, int, int] + legal_q_indices: tuple[int, ...] + + @property + def a_equals_q(self) -> bool: + return self.action[0] == self.q_color + + +def build_sibling_edges( + pairs: Sequence[tuple[State, State]], +) -> tuple[Edge, ...]: + raw: list[tuple[State, State, ExhaustingAction, int, tuple[int, ...]]] = [] + for parent, terminal in pairs: + if len(legal_sources(parent, 0)) < 2: + continue + actions = exhausting_actions_to(parent, terminal) + require(len(actions) == 1, "bridge edge does not have one canonical action") + action = actions[0] + old_color, old_cap, final_color = action + + # Keep this derivation in the parent's coordinates. Canonicalizing + # the terminal may permute color indices, so its q-bucket index is not + # a sound coordinate for replaying the bad action. + caps_after = [list(caps) for _, caps in parent] + caps_after[old_color].remove(old_cap) + q_candidates = [color for color, caps in enumerate(caps_after) if len(caps) == 3] + require(len(q_candidates) == 1, "cannot identify the three surviving q columns") + q_color = q_candidates[0] + q_caps = tuple(sorted(caps_after[q_color])) + require(len(q_caps) == 3, "wrong surviving q multiplicity") + legal_q_indices = tuple( + index + for index, cap in enumerate(q_caps) + if source_is_legal(parent, 0, q_color, cap) + ) + require(legal_q_indices, "sibling parent has no legal q sibling") + + # Isolated-final-color identity, checked before canonicalization. + replay_debts = [debt for debt, _ in parent] + replay_caps = [list(caps) for _, caps in parent] + replay_caps[old_color].remove(old_cap) + replay_debts[old_color] += old_cap + replay_debts[final_color] += HEIGHT - old_cap + require( + replay_debts[final_color] == HEIGHT - old_cap + and not replay_caps[final_color], + "final color is not isolated in parent coordinates", + ) + raw.append((parent, terminal, action, q_color, q_caps + legal_q_indices)) + + edges: list[Edge] = [] + for ordinal, (parent, terminal, action, q_color, packed) in enumerate(raw): + q_caps = packed[:3] + legal_indices = packed[3:] + edges.append( + Edge( + f"edge-{ordinal:03d}", + parent, + terminal, + action, + q_color, + q_caps, # type: ignore[arg-type] + legal_indices, + ) + ) + return tuple(edges) + + +def cards(q_color: int, cap: int) -> tuple[Card, ...]: + # Color-major order is deliberately different from production's expected + # endpoint-major order; report matching uses semantic keys, not ordinals. + return tuple( + (color, endpoint) + for color in range(COLORS) + if color != q_color + for endpoint in range(cap + 1, HEIGHT + 1) + ) + + +@lru_cache(maxsize=None) +def residual_count( + remaining: tuple[int, int, int, int], forbidden: tuple[int, ...] +) -> int: + """Count fillings by explicitly assigning the at-most-three boundary cells.""" + + if any(value < 0 for value in remaining): + return 0 + total = 0 + for chosen in itertools.product(range(COLORS), repeat=len(forbidden)): + if any(color == blocked for color, blocked in zip(chosen, forbidden)): + continue + counts = list(remaining) + for color in chosen: + counts[color] -= 1 + if any(value < 0 for value in counts): + continue + unrestricted = sum(counts) + ways = math.factorial(unrestricted) + for value in counts: + ways //= math.factorial(value) + total += ways + return total + + +def decoration_balance( + edge: Edge, chosen_cards: tuple[Card, Card, Card] +) -> tuple[tuple[int, int, int, int], tuple[int, ...], int]: + old_color, old_cap, final_color = edge.action + del old_color + remaining = [HEIGHT - count for count in exposed_counts(edge.parent)] + remaining[final_color] -= HEIGHT - old_cap + forbidden: list[int] = [] + for cap, (color, endpoint) in zip(edge.q_caps, chosen_cards): + remaining[color] -= endpoint - cap + if endpoint < HEIGHT: + forbidden.append(color) + key = tuple(remaining) # type: ignore[assignment] + weight = residual_count(key, tuple(forbidden)) + return key, tuple(forbidden), weight + + +def replay_sibling_in_parent_coordinates( + edge: Edge, q_index: int, card: Card +) -> tuple[list[int], int]: + """Apply a sibling event without allowing canonicalization to relabel a/b/q.""" + + cap = edge.q_caps[q_index] + next_color, endpoint = card + debts = [debt for debt, _ in edge.parent] + debts[edge.q_color] += cap + if endpoint == HEIGHT: + debts[next_color] += HEIGHT - cap + exhausted = 1 + else: + debts[next_color] -= cap + exhausted = 0 + return debts, exhausted + + +def classify_decoration(edge: Edge, chosen: tuple[Card, Card, Card]) -> str: + old_color, old_cap, _ = edge.action + has_live_handoff = False + for index in edge.legal_q_indices: + debts, exhausted = replay_sibling_in_parent_coordinates(edge, index, chosen[index]) + if not source_is_legal(debts, exhausted, old_color, old_cap): + continue + if exhausted == 1: + return "two_exhaustion" + has_live_handoff = True + return "live_bad_persistent" if has_live_handoff else "obstruction" + + +def terminal_debts_in_parent_coordinates(edge: Edge) -> list[int]: + debts = [debt for debt, _ in edge.parent] + old_color, old_cap, final_color = edge.action + debts[old_color] += old_cap + debts[final_color] += HEIGHT - old_cap + return debts + + +def is_tq_terminal(state: State) -> bool: + if not state_is_consistent(state, 1) or legal_sources(state, 1): + return False + positive = [index for index, (debt, _) in enumerate(state) if debt > 0] + nonpositive = [index for index, (debt, _) in enumerate(state) if debt <= 0] + topped = [index for index, (_, caps) in enumerate(state) if caps] + return len(positive) == 3 and len(nonpositive) == 1 and topped == nonpositive + + +def immediate_tq_after_sibling_exhaust(edge: Edge, slot: int, card: Card) -> bool: + if card[1] != HEIGHT: + return False + cap = edge.q_caps[slot] + debts = [debt for debt, _ in edge.parent] + caps = [list(values) for _, values in edge.parent] + caps[edge.q_color].remove(cap) + debts[edge.q_color] += cap + debts[card[0]] += HEIGHT - cap + successor = canonical_state( + debts, + ((color, value) for color in range(COLORS) for value in caps[color]), + ) + return is_tq_terminal(successor) + + +def is_unique_tq_handoff_corner( + edge: Edge, + slot: int, + chosen: tuple[Card, Card, Card], +) -> bool: + """Check equation (37) of the reduction note on one fixed decoration.""" + + color, endpoint = chosen[slot] + cap = edge.q_caps[slot] + if endpoint >= HEIGHT: + return False + terminal_debts = terminal_debts_in_parent_coordinates(edge) + energy = -terminal_debts[edge.q_color] + p_x = terminal_debts[color] + other_slots = [index for index in range(3) if index != slot] + return ( + energy == 0 + and cap == p_x + and endpoint == 3 + and all(edge.q_caps[index] == 1 for index in other_slots) + and all(chosen[index] == (color, 3) for index in other_slots) + ) + + +def refined_classify_decoration( + edge: Edge, + chosen: tuple[Card, Card, Card], +) -> str: + """Apply the proof ledger's strategy precedence to one fixed decoration.""" + + has_n_ge_3 = False + has_n_le_2 = False + has_d2_reduction = False + has_tq_corner = False + terminal_debts = terminal_debts_in_parent_coordinates(edge) + for slot in edge.legal_q_indices: + card = chosen[slot] + cap = edge.q_caps[slot] + if card[1] == HEIGHT: + if immediate_tq_after_sibling_exhaust(edge, slot, card): + # A feasible joint decoration already enforces the shared-f + # budget (24), so every such terminal is the low-energy corner. + has_tq_corner = True + else: + return "direct_certified" + continue + + debts_after_live, _ = replay_sibling_in_parent_coordinates(edge, slot, card) + if source_is_legal( + debts_after_live, 0, edge.action[0], edge.action[1] + ): + successor_debts = terminal_debts.copy() + successor_debts[edge.q_color] += cap + successor_debts[card[0]] -= cap + energy = -min(successor_debts) + if energy >= 3: + has_n_ge_3 = True + elif is_unique_tq_handoff_corner(edge, slot, chosen): + has_tq_corner = True + else: + has_n_le_2 = True + else: + has_d2_reduction = True + + if has_n_ge_3: + return "n_ge_3_certified" + if has_n_le_2: + return "n_le_2_certified" + if has_d2_reduction: + return "d2_reduction" + require(has_tq_corner, "refined proof ledger found no applicable branch") + return "tq_corner_only" + + +def direct_corner_card_census(edges: Sequence[Edge]) -> dict[str, object]: + cards_count = 0 + edge_keys: set[tuple[State, State, ExhaustingAction]] = set() + parents: set[State] = set() + energy_distribution: Counter[int] = Counter() + for edge in edges: + for slot in edge.legal_q_indices: + cap = edge.q_caps[slot] + for card in cards(edge.q_color, cap): + if not immediate_tq_after_sibling_exhaust(edge, slot, card): + continue + # Exact joint fixed-decoration budget (24). + if cap < HEIGHT - edge.action[1]: + continue + cards_count += 1 + edge_keys.add((edge.parent, edge.terminal, edge.action)) + parents.add(edge.parent) + terminal_debts = terminal_debts_in_parent_coordinates(edge) + q_energy = -terminal_debts[edge.q_color] + energy_distribution[edge.action[1] + q_energy - cap] += 1 + return { + "physical_cards": cards_count, + "canonical_edges": len(edge_keys), + "canonical_parents": len(parents), + "m_distribution": {str(key): value for key, value in sorted(energy_distribution.items())}, + } + + +def state_json(state: State) -> list[dict[str, object]]: + return [ + {"debt": debt, "caps": list(caps), "exposed": debt + sum(caps)} + for debt, caps in state + ] + + +def edge_key_from_json(row: dict[str, object]) -> tuple[State, State, ExhaustingAction]: + def parse_state(value: object) -> State: + require(isinstance(value, list) and len(value) == COLORS, "invalid state JSON") + result: list[Bucket] = [] + for bucket in value: + require(isinstance(bucket, dict), "state bucket must be an object") + debt = bucket.get("debt") + caps = bucket.get("caps") + require(isinstance(debt, int), "state debt must be an integer") + require(isinstance(caps, list) and all(isinstance(x, int) for x in caps), "invalid caps") + result.append((debt, tuple(caps))) + return tuple(result) # type: ignore[return-value] + + action = row.get("bad_action", row.get("action")) + require( + isinstance(action, list) + and len(action) == 3 + and all(isinstance(value, int) for value in action), + "invalid bad action", + ) + return ( + parse_state(row.get("parent")), + parse_state(row.get("terminal")), + tuple(action), # type: ignore[arg-type] + ) + + +def known_hall_counterexample_check() -> None: + """Replay a concrete bridge decoration that is nonnegative but Hall-impossible.""" + + parent: State = ( + (-8, (3, 3, 3, 6)), + (0, ()), + (1, ()), + (7, ()), + ) + terminal: State = ( + (-2, (3, 3, 3)), + (1, ()), + (1, ()), + (7, ()), + ) + edge = Edge( + "hall-regression", + parent, + terminal, + (0, 6, 1), + 0, + (3, 3, 3), + (0, 1, 2), + ) + chosen: tuple[Card, Card, Card] = ((1, 4), (2, 5), (2, 7)) + require( + apply_exhausting_canonical(parent, 0, edge.action) == terminal, + "Hall regression is not a valid first-exhaustion edge", + ) + remaining, forbidden, weight = decoration_balance(edge, chosen) + require(remaining == (0, 5, 0, 0), "Hall regression residual vector drifted") + require(forbidden == (1, 2), "Hall regression boundary constraints drifted") + require(all(value >= 0 for value in remaining), "Hall fixture is not nonnegative") + require(weight == 0, "known in-universe Hall obstruction was accepted") + + +def independent_census() -> dict[str, object]: + known_hall_counterexample_check() + terminals = enumerate_tq_terminals() + labeled_count, pairs = reverse_bridge(terminals) + parents = {parent for parent, _ in pairs} + unique_parents = {parent for parent in parents if len(legal_sources(parent, 0)) == 1} + sibling_parents = parents - unique_parents + edges = build_sibling_edges(pairs) + + require(len(terminals) == EXPECTED_TERMINALS, "Tq terminal count mismatch") + require(labeled_count == EXPECTED_LABELED_CANDIDATES, "labeled bridge count mismatch") + require(len(parents) == EXPECTED_PARENTS, "canonical bridge parent count mismatch") + require(len(pairs) == EXPECTED_EDGES, "canonical bridge edge count mismatch") + require(len(unique_parents) == EXPECTED_UNIQUE_PARENTS, "unique-source parent count mismatch") + require(len(sibling_parents) == EXPECTED_SIBLING_PARENTS, "sibling-parent count mismatch") + require(len(edges) == EXPECTED_SIBLING_EDGES, "sibling-edge count mismatch") + + parent_distribution = Counter(len(legal_sources(parent, 0)) for parent in sibling_parents) + edge_distribution = Counter(len(legal_sources(edge.parent, 0)) for edge in edges) + require(parent_distribution == {2: 1, 3: 12, 4: 399}, "parent legal-source distribution mismatch") + require(edge_distribution == {2: 2, 3: 14, 4: 407}, "edge legal-source distribution mismatch") + require(sum(not edge.a_equals_q for edge in edges) == EXPECTED_A_NOT_Q_EDGES, "a!=q edge split mismatch") + require(sum(edge.a_equals_q for edge in edges) == EXPECTED_A_EQ_Q_EDGES, "a==q edge split mismatch") + + raw_individual = 0 + raw_legal_joint = 0 + raw_all_q = 0 + nonnegative = 0 + feasible = 0 + residual_weight = 0 + class_counts: Counter[str] = Counter() + class_weights: Counter[str] = Counter() + refined_counts: Counter[str] = Counter() + refined_weights: Counter[str] = Counter() + type_counts: dict[str, Counter[str]] = { + "a_equals_q": Counter(), + "a_not_q": Counter(), + } + type_weights: dict[str, Counter[str]] = { + "a_equals_q": Counter(), + "a_not_q": Counter(), + } + per_edge: list[dict[str, object]] = [] + + for edge in edges: + card_sets = tuple(cards(edge.q_color, cap) for cap in edge.q_caps) + raw_individual += sum(len(card_sets[index]) for index in edge.legal_q_indices) + joint = math.prod(len(card_sets[index]) for index in edge.legal_q_indices) + raw_legal_joint += joint + edge_raw = math.prod(map(len, card_sets)) + raw_all_q += edge_raw + row_counts: Counter[str] = Counter() + row_weights: Counter[str] = Counter() + row_refined_counts: Counter[str] = Counter() + row_refined_weights: Counter[str] = Counter() + row_nonnegative = 0 + row_feasible = 0 + row_weight = 0 + samples: dict[str, dict[str, object]] = {} + + # Iterate the last column fastest, unlike a natural nested production + # loop over endpoints, to make accidental shared ordering less likely. + for chosen in itertools.product(*card_sets): + chosen = tuple(chosen) # type: ignore[assignment] + remaining, forbidden, weight = decoration_balance(edge, chosen) # type: ignore[arg-type] + if all(value >= 0 for value in remaining): + nonnegative += 1 + row_nonnegative += 1 + if weight == 0: + continue + feasible += 1 + row_feasible += 1 + residual_weight += weight + row_weight += weight + classification = classify_decoration(edge, chosen) # type: ignore[arg-type] + refined = refined_classify_decoration(edge, chosen) # type: ignore[arg-type] + class_counts[classification] += 1 + class_weights[classification] += weight + refined_counts[refined] += 1 + refined_weights[refined] += weight + row_counts[classification] += 1 + row_weights[classification] += weight + row_refined_counts[refined] += 1 + row_refined_weights[refined] += weight + edge_type = "a_equals_q" if edge.a_equals_q else "a_not_q" + type_counts[edge_type][classification] += 1 + type_weights[edge_type][classification] += weight + if classification not in samples: + samples[classification] = { + "cards": [list(card) for card in chosen], + "remaining_color_counts": list(remaining), + "boundary_forbidden_colors": list(forbidden), + "residual_word_weight": weight, + } + + per_edge.append( + { + "edge_id": edge.edge_id, + "parent": state_json(edge.parent), + "terminal": state_json(edge.terminal), + "bad_action": list(edge.action), + "q_color": edge.q_color, + "q_caps": list(edge.q_caps), + "legal_q_indices": list(edge.legal_q_indices), + "a_equals_q": edge.a_equals_q, + "legal_source_count": len(legal_sources(edge.parent, 0)), + "raw_all_q_decorations": edge_raw, + "nonnegative_decorations": row_nonnegative, + "hall_feasible_decorations": row_feasible, + "residual_word_weight": row_weight, + "classification_counts": dict(row_counts), + "classification_weights": dict(row_weights), + "refined_classification_counts": dict(row_refined_counts), + "refined_classification_weights": dict(row_refined_weights), + "samples": samples, + } + ) + + require(raw_individual == EXPECTED_RAW_INDIVIDUAL, "raw individual-card count mismatch") + require(raw_legal_joint == EXPECTED_RAW_LEGAL_JOINT, "raw legal-joint count mismatch") + require(raw_all_q == EXPECTED_RAW_ALL_Q, "raw all-q count mismatch") + require(nonnegative == EXPECTED_NONNEGATIVE, "nonnegative decoration count mismatch") + require(feasible == EXPECTED_HALL_FEASIBLE, "Hall-feasible decoration count mismatch") + require(residual_weight == EXPECTED_RESIDUAL_WEIGHT, "residual-word weight mismatch") + require(dict(class_counts) == EXPECTED_CLASS_COUNTS, f"classification counts mismatch: {class_counts}") + require(dict(class_weights) == EXPECTED_CLASS_WEIGHTS, f"classification weights mismatch: {class_weights}") + require(dict(refined_counts) == EXPECTED_REFINED_COUNTS, f"refined counts mismatch: {refined_counts}") + require(dict(refined_weights) == EXPECTED_REFINED_WEIGHTS, f"refined weights mismatch: {refined_weights}") + require(sum(class_counts.values()) == feasible, "classification counts do not partition feasible decorations") + require(sum(class_weights.values()) == residual_weight, "classification weights do not partition residual words") + require(sum(refined_counts.values()) == feasible, "refined counts do not partition feasible decorations") + require(sum(refined_weights.values()) == residual_weight, "refined weights do not partition residual words") + + corner_cards = direct_corner_card_census(edges) + require( + corner_cards + == { + "physical_cards": 12, + "canonical_edges": 12, + "canonical_parents": 10, + "m_distribution": {"0": 8, "1": 4}, + }, + f"direct Tq-corner card census mismatch: {corner_cards}", + ) + + return { + "schema_version": 1, + "coverage_scope": SCOPE, + "terminal_count": len(terminals), + "labeled_reverse_candidates": labeled_count, + "canonical_parent_count": len(parents), + "canonical_edge_count": len(pairs), + "unique_source_parent_count": len(unique_parents), + "sibling_parent_count": len(sibling_parents), + "sibling_edge_count": len(edges), + "a_not_q_edge_count": sum(not edge.a_equals_q for edge in edges), + "a_equals_q_edge_count": sum(edge.a_equals_q for edge in edges), + "parent_legal_source_distribution": {str(k): v for k, v in sorted(parent_distribution.items())}, + "edge_legal_source_distribution": {str(k): v for k, v in sorted(edge_distribution.items())}, + "raw_individual_legal_sibling_cards": raw_individual, + "raw_joint_legal_sibling_decorations": raw_legal_joint, + "raw_all_q_next_run_decorations": raw_all_q, + "nonnegative_decorations": nonnegative, + "hall_feasible_decorations": feasible, + "residual_word_weight": residual_weight, + "classification_counts": dict(class_counts), + "classification_weights": dict(class_weights), + "refined_classification_counts": dict(refined_counts), + "refined_classification_weights": dict(refined_weights), + "classification_counts_by_edge_type": { + key: dict(value) for key, value in type_counts.items() + }, + "classification_weights_by_edge_type": { + key: dict(value) for key, value in type_weights.items() + }, + "known_hall_counterexample_checked": True, + "direct_tq_corner_card_census": corner_cards, + "per_edge": per_edge, + } + + +def partition_stats( + value: object, + label: str, + names: Iterable[str], +) -> tuple[dict[str, int], dict[str, int]]: + require(isinstance(value, dict), f"{label} must be an object") + required_names = set(names) + require(set(value) == required_names, f"{label} has wrong class keys") + counts: dict[str, int] = {} + weights: dict[str, int] = {} + for name, raw in value.items(): + require(isinstance(raw, dict), f"{label}.{name} must be an object") + require(isinstance(raw.get("decorations"), int), f"{label}.{name}.decorations invalid") + require(isinstance(raw.get("residual_words"), int), f"{label}.{name}.residual_words invalid") + counts[name] = int(raw["decorations"]) + weights[name] = int(raw["residual_words"]) + return counts, weights + + +def class_stats(value: object, label: str) -> tuple[dict[str, int], dict[str, int]]: + return partition_stats(value, label, EXPECTED_CLASS_COUNTS) + + +def refined_stats(value: object, label: str) -> tuple[dict[str, int], dict[str, int]]: + return partition_stats(value, label, EXPECTED_REFINED_COUNTS) + + +def independent_edges() -> tuple[Edge, ...]: + _, pairs = reverse_bridge(enumerate_tq_terminals()) + return build_sibling_edges(pairs) + + +def prefix_census(limit: int) -> dict[str, object]: + """Independently rescan exactly the documented edge/card prefix.""" + + edges = independent_edges() + rows: dict[tuple[State, State, ExhaustingAction], dict[str, object]] = {} + for edge in edges: + rows[(edge.parent, edge.terminal, edge.action)] = { + "raw_checked": 0, + "nonnegative": 0, + "feasible": 0, + "infeasible": 0, + "residual_words": 0, + "counts": Counter(), + "weights": Counter(), + "refined_counts": Counter(), + "refined_weights": Counter(), + } + checked = nonnegative = feasible = residual_words = 0 + counts: Counter[str] = Counter() + weights: Counter[str] = Counter() + refined_counts: Counter[str] = Counter() + refined_weights: Counter[str] = Counter() + prefix_keys: list[ + tuple[tuple[State, State, ExhaustingAction], tuple[Card, Card, Card]] + ] = [] + stop = False + for edge in edges: + row = rows[(edge.parent, edge.terminal, edge.action)] + card_sets = tuple(cards(edge.q_color, cap) for cap in edge.q_caps) + for chosen in itertools.product(*card_sets): + if checked >= limit: + stop = True + break + checked += 1 + prefix_keys.append( + ((edge.parent, edge.terminal, edge.action), tuple(chosen)) # type: ignore[arg-type] + ) + row["raw_checked"] = int(row["raw_checked"]) + 1 + remaining, _, weight = decoration_balance(edge, chosen) # type: ignore[arg-type] + if all(value >= 0 for value in remaining): + nonnegative += 1 + row["nonnegative"] = int(row["nonnegative"]) + 1 + if weight == 0: + row["infeasible"] = int(row["infeasible"]) + 1 + continue + feasible += 1 + residual_words += weight + row["feasible"] = int(row["feasible"]) + 1 + row["residual_words"] = int(row["residual_words"]) + weight + classification = classify_decoration(edge, chosen) # type: ignore[arg-type] + refined = refined_classify_decoration(edge, chosen) # type: ignore[arg-type] + counts[classification] += 1 + weights[classification] += weight + refined_counts[refined] += 1 + refined_weights[refined] += weight + row_counts: Counter[str] = row["counts"] # type: ignore[assignment] + row_weights: Counter[str] = row["weights"] # type: ignore[assignment] + row_refined_counts: Counter[str] = row["refined_counts"] # type: ignore[assignment] + row_refined_weights: Counter[str] = row["refined_weights"] # type: ignore[assignment] + row_counts[classification] += 1 + row_weights[classification] += weight + row_refined_counts[refined] += 1 + row_refined_weights[refined] += weight + if stop: + break + return { + "checked": checked, + "nonnegative": nonnegative, + "feasible": feasible, + "infeasible": checked - feasible, + "residual_words": residual_words, + "counts": dict(counts), + "weights": dict(weights), + "refined_counts": dict(refined_counts), + "refined_weights": dict(refined_weights), + "rows": rows, + "prefix_keys": prefix_keys, + } + + +def parse_hidden_word(value: object, label: str) -> list[int]: + if isinstance(value, str): + require(all(symbol in "0123" for symbol in value), f"{label} contains a bad color") + return [int(symbol) for symbol in value] + require( + isinstance(value, list) + and all(isinstance(symbol, int) and 0 <= symbol < COLORS for symbol in value), + f"{label} must be a color word", + ) + return list(value) + + +def validate_sample(edge: Edge, sample: dict[str, object]) -> None: + cards_json = sample.get("cards") + require( + isinstance(cards_json, list) + and len(cards_json) == 3 + and all( + isinstance(card, list) + and len(card) == 2 + and all(isinstance(value, int) for value in card) + for card in cards_json + ), + "sample has invalid cards", + ) + chosen = tuple(tuple(card) for card in cards_json) + for cap, card in zip(edge.q_caps, chosen): + require(card in cards(edge.q_color, cap), "sample card is outside the edge universe") + remaining, _, weight = decoration_balance(edge, chosen) # type: ignore[arg-type] + require(weight > 0, "sample decoration is Hall-infeasible") + classification = classify_decoration(edge, chosen) # type: ignore[arg-type] + require(sample.get("classification") == classification, "sample classification does not replay") + require(sample.get("completion_count") == weight, "sample completion count mismatch") + if "free_tail_lengths" in sample: + require( + sample["free_tail_lengths"] + == [HEIGHT - endpoint for _, endpoint in chosen], + "sample free-tail lengths mismatch", + ) + if "residual_after_forced" in sample: + require(sample["residual_after_forced"] == list(remaining), "sample residual vector mismatch") + + words_json = sample.get("hidden_words_bottom_to_top") + require(isinstance(words_json, list) and len(words_json) == 4, "sample must contain four hidden words") + words = [parse_hidden_word(word, f"sample word {index}") for index, word in enumerate(words_json)] + old_color, old_cap, final_color = edge.action + del old_color + require(words[0] == [final_color] * (HEIGHT - old_cap), "sample bad tail is not the fixed exhausting run") + for index, (cap, card, word) in enumerate(zip(edge.q_caps, chosen, words[1:])): + color, endpoint = card + forced = endpoint - cap + free = HEIGHT - endpoint + require(len(word) == HEIGHT - cap, f"sample q{index} has wrong hidden length") + require(word[free:] == [color] * forced, f"sample q{index} does not realize its card") + if free: + require(word[free - 1] != color, f"sample q{index} card endpoint is not exact") + hidden_counts = Counter(symbol for word in words for symbol in word) + required = [HEIGHT - count for count in exposed_counts(edge.parent)] + require([hidden_counts[color] for color in range(COLORS)] == required, "sample is not color-balanced") + + +def audit_edge_objects(audit: dict[str, object]) -> dict[tuple[State, State, ExhaustingAction], Edge]: + result: dict[tuple[State, State, ExhaustingAction], Edge] = {} + for raw in audit["per_edge"]: # type: ignore[index] + require(isinstance(raw, dict), "independent per-edge row is invalid") + key = edge_key_from_json(raw) + result[key] = Edge( + str(raw["edge_id"]), key[0], key[1], key[2], int(raw["q_color"]), + tuple(raw["q_caps"]), tuple(raw["legal_q_indices"]), # type: ignore[arg-type] + ) + return result + + +def enforce_claim_boundary(report: dict[str, object]) -> None: + require(report.get("full_residual_word_coverage") is False, "next-run report may not claim residual-word coverage") + require(report.get("entry_family_eliminated") is False, "next-run report may not claim entry elimination") + require(report.get("full_layout_coverage") is False, "next-run report may not claim full-layout coverage") + + +def validate_report( + report: dict[str, object], + audit: dict[str, object], + *, + bounded_limit: int | None = None, +) -> None: + require(report.get("schema_version") == 1, "unsupported report schema") + require(report.get("coverage_scope") == SCOPE, "wrong coverage scope") + require(report.get("limit_unit") == "raw_all_q_next_run_decorations", "wrong limit unit") + require(report.get("self_checks_passed") is True, "production self-checks failed") + enforce_claim_boundary(report) + + bridge = report.get("bridge") + raw = report.get("raw") + census = report.get("census") + require(isinstance(bridge, dict) and isinstance(raw, dict) and isinstance(census, dict), "missing nested census objects") + bridge_expected = { + "terminal_count": audit["terminal_count"], + "labeled_candidates": audit["labeled_reverse_candidates"], + "canonical_parents": audit["canonical_parent_count"], + "canonical_edges": audit["canonical_edge_count"], + "unique_source_parents": audit["unique_source_parent_count"], + "sibling_parents": audit["sibling_parent_count"], + "unique_source_edges": EXPECTED_EDGES - EXPECTED_SIBLING_EDGES, + "sibling_edges": audit["sibling_edge_count"], + "parent_legal_source_distribution": audit["parent_legal_source_distribution"], + "edge_legal_source_distribution": audit["edge_legal_source_distribution"], + } + for key, value in bridge_expected.items(): + require(bridge.get(key) == value, f"production bridge.{key} disagrees with audit") + for key in ("action_unique", "all_edges_replay", "all_final_colors_isolated"): + require(bridge.get(key) is True, f"bridge.{key} is not true") + raw_expected = { + "legal_sibling_cards": audit["raw_individual_legal_sibling_cards"], + "legal_sibling_joint_decorations": audit["raw_joint_legal_sibling_decorations"], + "all_q_joint_decorations": audit["raw_all_q_next_run_decorations"], + } + for key, value in raw_expected.items(): + require(raw.get(key) == value, f"production raw.{key} disagrees with audit") + + if bounded_limit is None: + expected_dynamic: dict[str, object] = { + "checked": EXPECTED_RAW_ALL_Q, + "nonnegative": audit["nonnegative_decorations"], + "feasible": audit["hall_feasible_decorations"], + "infeasible": EXPECTED_RAW_ALL_Q - EXPECTED_HALL_FEASIBLE, + "residual_words": audit["residual_word_weight"], + "counts": audit["classification_counts"], + "weights": audit["classification_weights"], + "refined_counts": audit["refined_classification_counts"], + "refined_weights": audit["refined_classification_weights"], + } + expected_rows = { + edge_key_from_json(row): { + "raw_checked": row["raw_all_q_decorations"], + "nonnegative": row["nonnegative_decorations"], + "feasible": row["hall_feasible_decorations"], + "infeasible": row["raw_all_q_decorations"] - row["hall_feasible_decorations"], + "residual_words": row["residual_word_weight"], + "counts": Counter(row["classification_counts"]), + "weights": Counter(row["classification_weights"]), + "refined_counts": Counter(row["refined_classification_counts"]), + "refined_weights": Counter(row["refined_classification_weights"]), + } + for row in audit["per_edge"] # type: ignore[index] + } + else: + prefix = prefix_census(min(bounded_limit, EXPECTED_RAW_ALL_Q)) + expected_dynamic = prefix + expected_rows = prefix["rows"] # type: ignore[assignment] + + require(raw.get("checked") == expected_dynamic["checked"], "bounded/full checked count mismatch") + require(census.get("nonnegative_decorations") == expected_dynamic["nonnegative"], "nonnegative prefix mismatch") + require(census.get("feasible_decorations") == expected_dynamic["feasible"], "feasible prefix mismatch") + require(census.get("infeasible_decorations") == expected_dynamic["infeasible"], "infeasible prefix mismatch") + require(census.get("residual_words") == expected_dynamic["residual_words"], "residual-weight prefix mismatch") + actual_counts, actual_weights = class_stats(census.get("legacy"), "census.legacy") + expected_counts = {name: int(expected_dynamic["counts"].get(name, 0)) for name in EXPECTED_CLASS_COUNTS} # type: ignore[union-attr] + expected_weights = {name: int(expected_dynamic["weights"].get(name, 0)) for name in EXPECTED_CLASS_COUNTS} # type: ignore[union-attr] + require(actual_counts == expected_counts, "legacy classification prefix mismatch") + require(actual_weights == expected_weights, "legacy classification-weight prefix mismatch") + actual_refined_counts, actual_refined_weights = refined_stats(census.get("refined"), "census.refined") + expected_refined_counts = { + name: int(expected_dynamic["refined_counts"].get(name, 0)) + for name in EXPECTED_REFINED_COUNTS + } # type: ignore[union-attr] + expected_refined_weights = { + name: int(expected_dynamic["refined_weights"].get(name, 0)) + for name in EXPECTED_REFINED_COUNTS + } # type: ignore[union-attr] + require(actual_refined_counts == expected_refined_counts, "refined classification prefix mismatch") + require(actual_refined_weights == expected_refined_weights, "refined weight prefix mismatch") + if "direct_tq_corner_card_census" in audit: + independent_corner = audit["direct_tq_corner_card_census"] + require(isinstance(independent_corner, dict), "independent corner census is invalid") + require( + census.get("direct_tq_corner_structure") + == { + "cards": independent_corner["physical_cards"], + "edges": independent_corner["canonical_edges"], + "parents": independent_corner["canonical_parents"], + "m_distribution": independent_corner["m_distribution"], + }, + "direct Tq-corner structure disagrees with independent audit", + ) + hall = report.get("hall_regression") + require( + hall + == { + "residual_counts": [0, 5, 0, 0], + "tail_lengths": [3, 2, 0], + "forbidden_colors": [1, 2, None], + "nonnegative": True, + "feasible": False, + }, + "Hall regression fixture drifted or was accepted", + ) + + rows = report.get("per_edge") + require(isinstance(rows, list) and len(rows) == EXPECTED_SIBLING_EDGES, "per_edge must cover 423 edges") + edges = audit_edge_objects(audit) + actual_keys: set[tuple[State, State, ExhaustingAction]] = set() + rows_by_id: dict[str, tuple[State, State, ExhaustingAction]] = {} + sample_refs: dict[str, tuple[State, State, ExhaustingAction]] = {} + audit_rows = {edge_key_from_json(row): row for row in audit["per_edge"]} # type: ignore[index] + for raw_row in rows: + require(isinstance(raw_row, dict), "per_edge row must be an object") + key = edge_key_from_json(raw_row) + require(key in edges and key not in actual_keys, "unknown or duplicate per_edge row") + actual_keys.add(key) + expected_static = audit_rows[key] + require(raw_row.get("q_color") == expected_static["q_color"], "per-edge q_color mismatch") + require(raw_row.get("q_caps") == expected_static["q_caps"], "per-edge q_caps mismatch") + require(raw_row.get("old_bad_equals_q") == expected_static["a_equals_q"], "per-edge a==q flag mismatch") + require(raw_row.get("legal_source_count") == expected_static["legal_source_count"], "per-edge legal count mismatch") + require(raw_row.get("raw_expected") == expected_static["raw_all_q_decorations"], "per-edge raw universe mismatch") + expected = expected_rows[key] + for field in ("raw_checked", "nonnegative", "feasible", "infeasible", "residual_words"): + if field == "nonnegative" and field not in raw_row: + continue + require(raw_row.get(field) == expected[field], f"per-edge {field} prefix mismatch") + counts, weights = class_stats(raw_row.get("legacy"), "per-edge legacy") + require(counts == {name: int(expected["counts"].get(name, 0)) for name in EXPECTED_CLASS_COUNTS}, "per-edge class counts mismatch") # type: ignore[union-attr] + require(weights == {name: int(expected["weights"].get(name, 0)) for name in EXPECTED_CLASS_COUNTS}, "per-edge class weights mismatch") # type: ignore[union-attr] + row_refined_counts, row_refined_weights = refined_stats( + raw_row.get("refined"), "per-edge refined" + ) + require( + row_refined_counts + == { + name: int(expected["refined_counts"].get(name, 0)) + for name in EXPECTED_REFINED_COUNTS + }, + "per-edge refined counts mismatch", + ) # type: ignore[union-attr] + require( + row_refined_weights + == { + name: int(expected["refined_weights"].get(name, 0)) + for name in EXPECTED_REFINED_COUNTS + }, + "per-edge refined weights mismatch", + ) # type: ignore[union-attr] + edge_id = raw_row.get("edge_id") + require(isinstance(edge_id, str) and edge_id not in rows_by_id, "bad or duplicate edge_id") + rows_by_id[edge_id] = key + sample_id = raw_row.get("sample_id") + if sample_id is not None: + require(isinstance(sample_id, str) and sample_id not in sample_refs, "bad or duplicate sample reference") + sample_refs[sample_id] = key + require(actual_keys == set(edges), "per_edge coverage is incomplete") + + checked_prefix = report.get("checked_prefix") + require(isinstance(checked_prefix, list), "checked_prefix must be an array") + if bounded_limit is None: + require(not checked_prefix, "an unbounded report should not serialize a redundant full prefix") + else: + expected_prefix = expected_dynamic["prefix_keys"] + require(len(checked_prefix) == len(expected_prefix), "checked_prefix length mismatch") # type: ignore[arg-type] + for index, (actual, expected) in enumerate(zip(checked_prefix, expected_prefix)): # type: ignore[arg-type] + require(isinstance(actual, dict), f"checked_prefix[{index}] must be an object") + edge_id = actual.get("edge_id") + cards_json = actual.get("cards") + require(isinstance(edge_id, str) and edge_id in rows_by_id, "checked prefix names an unknown edge") + require(rows_by_id[edge_id] == expected[0], f"checked_prefix[{index}] edge mismatch") + require( + isinstance(cards_json, list) + and tuple(tuple(card) for card in cards_json) == expected[1], + f"checked_prefix[{index}] card mismatch", + ) + + samples = report.get("replay_samples") + require(isinstance(samples, list), "replay_samples must be an array") + seen_samples: set[str] = set() + for raw_sample in samples: + require(isinstance(raw_sample, dict), "sample must be an object") + sample_id = raw_sample.get("sample_id") + edge_id = raw_sample.get("edge_id") + require(isinstance(sample_id, str) and sample_id not in seen_samples, "bad or duplicate sample_id") + require(isinstance(edge_id, str) and edge_id in rows_by_id, "sample names an unknown edge") + key = rows_by_id[edge_id] + require(sample_refs.get(sample_id) == key, "sample is not referenced by its edge") + require(raw_sample.get("bad_action") == list(key[2]), "sample bad action mismatch") + require(raw_sample.get("q_color") == edges[key].q_color, "sample q color mismatch") + require(raw_sample.get("q_caps") == list(edges[key].q_caps), "sample q caps mismatch") + validate_sample(edges[key], raw_sample) + seen_samples.add(sample_id) + require(seen_samples == set(sample_refs), "sample references and sample array disagree") + + if bounded_limit is None: + require(report.get("status") == "NEXT_RUN_CENSUS_COMPLETE", "full report has wrong status") + require(report.get("verified") is True, "full report must be verified") + require(report.get("next_run_universe_complete") is True, "full report lacks universe-complete flag") + else: + require(report.get("status") == "INCOMPLETE", "bounded report has wrong status") + require(report.get("verified") is False, "bounded report may not be verified") + require(report.get("next_run_universe_complete") is False, "bounded report claims a complete universe") + + +def read_report(path: Path) -> dict[str, object]: + require(path.is_file(), f"missing production report: {path}") + value = json.loads(path.read_text(encoding="utf-8")) + require(isinstance(value, dict), "report root must be an object") + return value + + +def run_program(program: Path, audit: dict[str, object], limit: int) -> None: + with tempfile.TemporaryDirectory(prefix="c4-h7-tq-exhaust-audit-") as raw_dir: + output_dir = Path(raw_dir) + subprocess.run( + [str(program), "--output-dir", str(output_dir), "--limit", str(limit)], + check=True, + ) + report = read_report(output_dir / "report.json") + bounded = limit if report.get("status") == "INCOMPLETE" else None + validate_report(report, audit, bounded_limit=bounded) + require((output_dir / "summary.md").is_file(), "production did not write summary.md") + + +def schema_negative_tests(audit: dict[str, object]) -> None: + # Target each forbidden overclaim independently. Full schema mutation is + # additionally exercised by the artifact validator in CI. + for key in ("full_residual_word_coverage", "entry_family_eliminated", "full_layout_coverage"): + skeleton = { + "full_residual_word_coverage": False, + "entry_family_eliminated": False, + "full_layout_coverage": False, + } + skeleton[key] = True + try: + enforce_claim_boundary(skeleton) + except AssertionError: + pass + else: + fail(f"claim-boundary checker accepted {key}=true") + require(len(audit["per_edge"]) == EXPECTED_SIBLING_EDGES, "negative per-edge fixture has wrong base") # type: ignore[arg-type] + + +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 report.json") + parser.add_argument( + "--audit", + type=Path, + help="reuse a previously generated independent census (bounded development only)", + ) + parser.add_argument("--limit", type=int, default=257, help="bounded differential size") + parser.add_argument("--json", type=Path, dest="json_path", help="write the independent census") + 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") + if args.audit: + audit = read_report(args.audit) + require( + (args.program is None) != (args.report is None), + "--audit reuse requires exactly one bounded --program or --report check", + ) + else: + audit = independent_census() + schema_negative_tests(audit) + if args.program: + require(args.program.is_file(), f"program not found: {args.program}") + run_program(args.program.resolve(), audit, args.limit) + if args.report: + production_report = read_report(args.report) + bounded = args.limit if production_report.get("status") == "INCOMPLETE" else None + validate_report(production_report, audit, bounded_limit=bounded) + output = json.dumps(audit, 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(output, encoding="utf-8") + else: + print( + "PASS: " + f"Tq={audit['terminal_count']}, bridge={audit['labeled_reverse_candidates']}/" + f"{audit['canonical_parent_count']}/{audit['canonical_edge_count']}, " + f"sibling={audit['sibling_parent_count']}/{audit['sibling_edge_count']}, " + f"decorations={audit['raw_all_q_next_run_decorations']}, " + f"feasible={audit['hall_feasible_decorations']}, " + f"residual-weight={audit['residual_word_weight']}" + ) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main())