diff --git a/.github/workflows/oeis-a147983-chomp-lean-audit.yml b/.github/workflows/oeis-a147983-chomp-lean-audit.yml index c7f6ff17..96aa53f9 100644 --- a/.github/workflows/oeis-a147983-chomp-lean-audit.yml +++ b/.github/workflows/oeis-a147983-chomp-lean-audit.yml @@ -4,6 +4,7 @@ on: pull_request: branches: [main] paths: + - 'proofs/chomp-10x42/lean/**' - '.github/workflows/oeis-a147983-chomp-lean-audit.yml' workflow_dispatch: @@ -19,15 +20,21 @@ jobs: runs-on: ubuntu-latest timeout-minutes: 30 steps: - - name: Checkout immutable DTD source commit + - name: Checkout ProofPlaygrond proof sources + uses: actions/checkout@v4 + with: + path: playground + + - name: Checkout immutable canonical DTD source commit uses: actions/checkout@v4 with: repository: DomTheDeveloper/formal-conjectures - ref: 5fa4e5d2f63eefdba1b001cdce5d44c2ec8cabda + ref: 9242e34d74bea32655e840a5e8637377de1431e4 + path: formal-conjectures - - name: Confirm immutable source + - name: Confirm immutable DTD source shell: bash - run: test "$(git rev-parse HEAD)" = "5fa4e5d2f63eefdba1b001cdce5d44c2ec8cabda" + run: test "$(git -C formal-conjectures rev-parse HEAD)" = "9242e34d74bea32655e840a5e8637377de1431e4" - name: Install pinned Lean toolchain shell: bash @@ -40,32 +47,54 @@ jobs: - name: Fetch Mathlib cache shell: bash + working-directory: formal-conjectures run: | set -euo pipefail lake exe cache get + lake build FormalConjecturesUtil - - name: Compile exact Chomp module + - name: Compile exact canonical Chomp catalog module shell: bash + working-directory: formal-conjectures run: | set -euo pipefail - lake lean FormalConjectures/OEIS/147983.lean 2>&1 | tee chomp-a147983-lean.log + mkdir -p .lake/build/lib/lean/FormalConjectures/OEIS + lake env lean \ + -o .lake/build/lib/lean/FormalConjectures/OEIS/147983.olean \ + FormalConjectures/OEIS/147983.lean \ + 2>&1 | tee chomp-a147983-lean.log - - name: Audit kernel-checkable helper declarations + - name: Compile pure kernel theorem layers shell: bash + working-directory: formal-conjectures run: | set -euo pipefail - cat >> FormalConjectures/OEIS/147983.lean <<'EOF' - - #print axioms OeisA147983.child₁_is_legal_move - #print axioms OeisA147983.child₂_is_legal_move - #print axioms OeisA147983.child₃_is_legal_move - #print axioms OeisA147983.candidate_children_pairwise_distinct - #print axioms OeisA147983.three_openings_of_p_positions - EOF - lake lean FormalConjectures/OEIS/147983.lean 2>&1 | tee chomp-a147983-axioms.log - if grep -E 'sorryAx|Lean\.trustCompiler|Lean\.ofReduce|Lean\.ofReduceBool' \ - chomp-a147983-axioms.log; then - echo 'A kernel-checkable helper depends on a forbidden proof escape.' >&2 + cp ../playground/proofs/chomp-10x42/lean/KernelCertificate.lean ./ChompKernelCertificate.lean + cp ../playground/proofs/chomp-10x42/lean/KernelGameTheory.lean ./ChompKernelGameTheory.lean + cp ../playground/proofs/chomp-10x42/lean/KernelPSet.lean ./ChompKernelPSet.lean + cp ../playground/proofs/chomp-10x42/lean/MDDCertificate.lean ./ChompMDDCertificate.lean + cp ../playground/proofs/chomp-10x42/lean/ChompRank.lean ./ChompRank.lean + cp ../playground/proofs/chomp-10x42/lean/ChompPosition.lean ./ChompPosition.lean + cp ../playground/proofs/chomp-10x42/lean/ChompCatalogBridge.lean ./ChompCatalogBridge.lean + mkdir -p .lake/build/lib/lean + compile_module() { + local module="$1" + local log="$2" + lake env lean -o ".lake/build/lib/lean/${module}.olean" "${module}.lean" 2>&1 | tee "$log" + } + compile_module ChompKernelCertificate chomp-kernel-certificate.log + compile_module ChompKernelGameTheory chomp-kernel-game-theory.log + compile_module ChompKernelPSet chomp-kernel-pset.log + compile_module ChompMDDCertificate chomp-mdd-certificate.log + compile_module ChompRank chomp-rank.log + compile_module ChompPosition chomp-position.log + compile_module ChompCatalogBridge chomp-catalog-bridge.log + if grep -nE '\b(sorry|admit)\b|native_decide|unsafe|^axiom\b|Lean\.trustCompiler|Lean\.ofReduce|Lean\.ofReduceBool|sorryAx' \ + ChompKernelCertificate.lean ChompKernelGameTheory.lean ChompKernelPSet.lean \ + ChompMDDCertificate.lean ChompRank.lean ChompPosition.lean ChompCatalogBridge.lean \ + chomp-kernel-certificate.log chomp-kernel-game-theory.log chomp-kernel-pset.log \ + chomp-mdd-certificate.log chomp-rank.log chomp-position.log chomp-catalog-bridge.log; then + echo 'Forbidden placeholder or trust escape in kernel certificate development.' >&2 exit 1 fi @@ -73,8 +102,14 @@ jobs: if: always() uses: actions/upload-artifact@v4 with: - name: oeis-a147983-chomp-lean-audit + name: oeis-a147983-chomp-kernel-audit path: | - chomp-a147983-lean.log - chomp-a147983-axioms.log + formal-conjectures/chomp-a147983-lean.log + formal-conjectures/chomp-kernel-certificate.log + formal-conjectures/chomp-kernel-game-theory.log + formal-conjectures/chomp-kernel-pset.log + formal-conjectures/chomp-mdd-certificate.log + formal-conjectures/chomp-rank.log + formal-conjectures/chomp-position.log + formal-conjectures/chomp-catalog-bridge.log if-no-files-found: warn diff --git a/proofs/chomp-10x42/MDD_COMPRESSION_REPORT.md b/proofs/chomp-10x42/MDD_COMPRESSION_REPORT.md new file mode 100644 index 00000000..075dd5d8 --- /dev/null +++ b/proofs/chomp-10x42/MDD_COMPRESSION_REPORT.md @@ -0,0 +1,51 @@ +# Exact MDD compression of the Chomp 10×42 P-set + +The target-stopping exact solver enumerates all P-positions in rank order through the third +claimed child. Its database contains **107,342,138** exact P-position ranks and ends at + +```text +[42,42,42,42,42,42,42,25,25,25] +``` + +with combinatorial rank `15,820,013,305`. + +`chomp_p_mdd.cpp` unranks that sorted stream and constructs the exact reduced layered +multi-valued decision diagram over the ten row lengths. Hashes only select candidate buckets; +a node is merged only after exact transition-by-transition comparison. + +A complete run produced: + +```text +words=107342138 +depth=0 nodes=1 transitions=42 +depth=1 nodes=42 transitions=797 +depth=2 nodes=756 transitions=10166 +depth=3 nodes=9364 transitions=102147 +depth=4 nodes=90493 transitions=825905 +depth=5 nodes=678267 transitions=5403664 +depth=6 nodes=3667697 transitions=25241311 +depth=7 nodes=9994761 transitions=54615011 +depth=8 nodes=2465000 transitions=10555794 +depth=9 nodes=40 transitions=40 +total_nodes=16906422 total_transitions=96754877 +``` + +The construction took about 29 seconds and under 1 GiB RSS in the current sandbox. This is a +substantial compression relative to 107 million explicit P states and the multi-billion-state +retrograde scan, but it is still too large for a naive theorem-per-node Lean development. + +## Formal-proof consequence + +The viable route is symbolic model checking over the reduced MDD: + +1. represent the exact P predicate by a layered decision diagram; +2. verify, inside Lean, sound MDD operations for intersection, union, complement within the + bounded Ferrers domain, and preimages under each bite map; +3. certify that no P-position has a P child; +4. certify that every valid non-P position below the target rank has a move to P; +5. invoke the progressively bounded game theorem to obtain kernel proofs that the three target + children are losing. + +The MDD builder remains untrusted. The final Lean checker must verify node well-formedness and +every symbolic-operation certificate, and the final theorem must contain no `sorry`, `admit`, +`native_decide`, custom axiom, `Lean.ofReduce`, `Lean.ofReduceBool`, or compiler-trust escape. diff --git a/proofs/chomp-10x42/chomp_export_p_ranks.cpp b/proofs/chomp-10x42/chomp_export_p_ranks.cpp new file mode 100644 index 00000000..41c86cc7 --- /dev/null +++ b/proofs/chomp-10x42/chomp_export_p_ranks.cpp @@ -0,0 +1,206 @@ +// Export the exact Chomp P-positions as sorted combinatorial ranks. +// +// The output is discovery data for the Lean proof-DAG generator. It is not trusted by Lean. +// The final proof must be checked from generated proof terms. + +#include +#include +#include +#include +#include +#include +#include +#include +#include + +using std::min; +using std::vector; + +struct Bits { + vector words; + Bits() = default; + explicit Bits(uint64_t nbits) : words((nbits + 63) / 64 + 1) {} + bool get(uint64_t i) const { return (words[i >> 6] >> (i & 63)) & 1ULL; } + uint64_t get64(uint64_t i) const { + const uint64_t q = i >> 6; + const int s = static_cast(i & 63); + return s ? (words[q] >> s) | (words[q + 1] << (64 - s)) : words[q]; + } + void set(uint64_t i) { words[i >> 6] |= 1ULL << (i & 63); } + void clear() { std::memset(words.data(), 0, words.size() * sizeof(uint64_t)); } +}; + +class Solver { +public: + Solver(int rows, int max_width, const std::string& output) + : K(rows), N(max_width), C(max_width + rows + 3, vector(rows + 3)), + shadow_sets(rows - 1), x(rows), out(output, std::ios::binary) { + if (K < 2 || K > 63 || N < 1) throw std::runtime_error("unsupported dimensions"); + if (!out) throw std::runtime_error("cannot open output file"); + for (int a = 0; a < static_cast(C.size()); ++a) { + C[a][0] = 1; + for (int b = 1; b <= min(a, rows + 1); ++b) { + __uint128_t z = static_cast<__uint128_t>(C[a - 1][b - 1]) + C[a - 1][b]; + if (z > std::numeric_limits::max()) + throw std::runtime_error("rank overflow"); + C[a][b] = static_cast(z); + } + } + for (int i = 0; i < K - 1; ++i) { + const int suffix_len = K - i - 1; + shadow_sets[i] = Bits(C[N + suffix_len][suffix_len]); + } + } + + void run() { + write_header(); + for (int top = 1; top <= N; ++top) { + x[0] = top; + if (K > 2) shadow_sets[1].clear(); + dfs(1, top); + } + out.flush(); + if (!out) throw std::runtime_error("failed while writing rank database"); + std::cerr << "P=" << p_count << " prefixes=" << prefix_count + << " last_rank=" << last_rank << "\n"; + } + +private: + int K, N; + vector> C; + vector shadow_sets; + vector x; + std::ofstream out; + uint64_t p_count = 0; + uint64_t prefix_count = 0; + uint64_t last_rank = 0; + bool have_last = false; + + void write_u64(uint64_t v) { out.write(reinterpret_cast(&v), sizeof(v)); } + void write_header() { + const char magic[8] = {'C', 'H', 'P', 'R', 'A', 'N', 'K', '1'}; + out.write(magic, sizeof(magic)); + write_u64(static_cast(K)); + write_u64(static_cast(N)); + } + + uint64_t rank_suffix(int start) const { + uint64_t rank = 0; + for (int pos = start; pos < K; ++pos) { + const int j = K - pos; + rank += C[x[pos] + j - 1][j]; + } + return rank; + } + + void record_p_rank() { + const uint64_t rank = rank_suffix(0); + if (have_last && rank <= last_rank) { + std::cerr << "non-increasing P rank: " << rank << " after " << last_rank << "\n"; + std::abort(); + } + write_u64(rank); + last_rank = rank; + have_last = true; + } + + void enumerate_shadow(int move_row, int pos, int equal_block_end, int upper, int lower) { + if (pos > equal_block_end) { + shadow_sets[move_row].set(rank_suffix(move_row + 1)); + return; + } + const int old = x[pos]; + for (int v = lower; v <= upper; ++v) { + x[pos] = v; + enumerate_shadow(move_row, pos + 1, equal_block_end, v, lower); + } + x[pos] = old; + } + + void add_shadow_of_current_p() { + const vector p = x; + for (int i = 0; i < K - 1; ++i) { + const int t = x[i]; + int m = i; + while (m + 1 < K && x[m + 1] == t) ++m; + const int upper = (i == 0) ? N : x[i - 1]; + if (upper > t) enumerate_shadow(i, i + 1, m, upper, t); + x = p; + } + } + + void process_prefix() { + ++prefix_count; + const int bottom_bound = x[K - 2]; + uint64_t base[64]; + base[K - 2] = 0; + uint64_t acc = 0; + for (int pos = K - 2; pos >= 1; --pos) { + const int j = K - pos; + acc += C[x[pos] + j - 1][j]; + base[pos - 1] = acc; + } + + int chosen = -1; + if (bottom_bound < 48) { + for (int v = 0; v <= bottom_bound; ++v) { + bool has_p_option = false; + for (int i = 0; i < K - 1; ++i) { + if (shadow_sets[i].get(base[i] + static_cast(v))) { + has_p_option = true; + break; + } + } + if (!has_p_option) { + chosen = v; + break; + } + } + } else { + for (int v0 = 0; v0 <= bottom_bound; v0 += 64) { + uint64_t hit = 0; + for (int i = 0; i < K - 1; ++i) + hit |= shadow_sets[i].get64(base[i] + static_cast(v0)); + const int len = min(64, bottom_bound - v0 + 1); + const uint64_t valid = len == 64 ? ~0ULL : ((1ULL << len) - 1); + const uint64_t available = (~hit) & valid; + if (available) { + chosen = v0 + __builtin_ctzll(available); + break; + } + } + } + + if (chosen < 0) return; + x[K - 1] = chosen; + ++p_count; + record_p_rank(); + add_shadow_of_current_p(); + } + + void dfs(int pos, int bound) { + if (pos == K - 1) { + process_prefix(); + return; + } + for (int v = 0; v <= bound; ++v) { + x[pos] = v; + if (pos + 1 < K - 1) shadow_sets[pos + 1].clear(); + dfs(pos + 1, v); + } + } +}; + +int main(int argc, char** argv) { + try { + if (argc != 4) { + std::cerr << "usage: " << argv[0] << " ROWS MAX_WIDTH OUTPUT.bin\n"; + return 2; + } + Solver(std::stoi(argv[1]), std::stoi(argv[2]), argv[3]).run(); + return 0; + } catch (const std::exception& e) { + std::cerr << "error: " << e.what() << "\n"; + return 1; + } +} diff --git a/proofs/chomp-10x42/chomp_p_mdd.cpp b/proofs/chomp-10x42/chomp_p_mdd.cpp new file mode 100644 index 00000000..30c82abe --- /dev/null +++ b/proofs/chomp-10x42/chomp_p_mdd.cpp @@ -0,0 +1,248 @@ +// Build the exact reduced layered multi-valued decision diagram for the Chomp P-set. +// +// Input is the sorted combinatorial-rank stream produced by chomp_export_p_ranks.cpp. +// Hashes are used only to select candidate buckets: signatures are compared exactly before +// nodes are merged. This is a certificate-design and measurement tool, not trusted proof code. + +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include + +struct Node { + uint64_t hash; + uint32_t offset; + uint8_t length; + uint8_t padding[3]; +}; + +struct Layer { + std::vector nodes; + // Packed transition: low six bits are the symbol, remaining bits are the child id. + std::vector transitions; + // Open-addressed table containing node id + 1; zero is empty. + std::vector table; + + static uint64_t mix(uint64_t x) { + x ^= x >> 30; + x *= 0xbf58476d1ce4e5b9ULL; + x ^= x >> 27; + x *= 0x94d049bb133111ebULL; + x ^= x >> 31; + return x; + } + + void initialize() { + if (table.empty()) table.assign(16, 0); + } + + uint64_t signatureHash(const std::vector>& signature) const { + uint64_t h = 0x9e3779b97f4a7c15ULL ^ signature.size(); + for (const auto [symbol, child] : signature) { + const uint64_t x = (static_cast(child) << 6) | symbol; + h ^= mix(x + 0x517cc1b727220a95ULL + (h << 1)); + h = (h << 23) | (h >> 41); + h *= 0x94d049bb133111ebULL; + } + return mix(h); + } + + bool exactlyEqual(const Node& node, + const std::vector>& signature) const { + if (node.length != signature.size()) return false; + for (size_t i = 0; i < signature.size(); ++i) { + const uint32_t packed = transitions[node.offset + i]; + if ((packed & 63U) != signature[i].first || + (packed >> 6) != signature[i].second) { + return false; + } + } + return true; + } + + void rehash() { + std::vector next(table.size() * 2, 0); + const size_t mask = next.size() - 1; + for (uint32_t id = 0; id < nodes.size(); ++id) { + size_t slot = mix(nodes[id].hash) & mask; + while (next[slot] != 0) slot = (slot + 1) & mask; + next[slot] = id + 1; + } + table.swap(next); + } + + uint32_t intern(const std::vector>& signature) { + initialize(); + if ((nodes.size() + 1) * 10 > table.size() * 7) rehash(); + + const uint64_t hash = signatureHash(signature); + const size_t mask = table.size() - 1; + size_t slot = mix(hash) & mask; + while (table[slot] != 0) { + const uint32_t id = table[slot] - 1; + if (nodes[id].hash == hash && exactlyEqual(nodes[id], signature)) return id; + slot = (slot + 1) & mask; + } + + if (signature.size() > 255 || transitions.size() > UINT32_MAX) + throw std::runtime_error("MDD layer overflow"); + const uint32_t id = static_cast(nodes.size()); + const uint32_t offset = static_cast(transitions.size()); + for (const auto [symbol, child] : signature) { + if (child >= (1U << 26)) throw std::runtime_error("MDD child-id overflow"); + transitions.push_back((child << 6) | symbol); + } + nodes.push_back({hash, offset, static_cast(signature.size()), {0, 0, 0}}); + table[slot] = id + 1; + return id; + } + + uint64_t allocatedBytes() const { + return nodes.capacity() * sizeof(Node) + transitions.capacity() * sizeof(uint32_t) + + table.capacity() * sizeof(uint32_t); + } +}; + +struct ActiveNode { + std::vector> transitions; +}; + +int main(int argc, char** argv) { + try { + if (argc < 2) { + std::cerr << "usage: " << argv[0] << " P_RANKS.bin [WORD_LIMIT]\n"; + return 2; + } + const uint64_t limit = argc > 2 ? std::stoull(argv[2]) : UINT64_MAX; + std::ifstream input(argv[1], std::ios::binary); + if (!input) throw std::runtime_error("cannot open rank database"); + + char magic[8]; + uint64_t rows = 0; + uint64_t width = 0; + input.read(magic, 8); + input.read(reinterpret_cast(&rows), 8); + input.read(reinterpret_cast(&width), 8); + if (!input || std::string(magic, 8) != "CHPRANK1" || rows != 10) + throw std::runtime_error("invalid rank database"); + + std::vector> choose(width + rows + 3, + std::vector(rows + 3)); + for (int a = 0; a < static_cast(choose.size()); ++a) { + choose[a][0] = 1; + for (int b = 1; b <= std::min(a, rows + 1); ++b) + choose[a][b] = choose[a - 1][b - 1] + choose[a - 1][b]; + } + + std::array layers; + std::array active; + std::array edge{}; + std::array previous{}; + std::array word{}; + bool first = true; + + auto canonicalize = [&](int depth) { + const uint32_t id = layers[depth].intern(active[depth].transitions); + active[depth].transitions.clear(); + return id; + }; + + auto minimizeTo = [&](int commonPrefix) { + for (int depth = 9; depth >= commonPrefix; --depth) { + const uint32_t child = depth == 9 ? 0 : canonicalize(depth + 1); + active[depth].transitions.push_back({edge[depth], child}); + } + }; + + uint64_t rank = 0; + uint64_t words = 0; + const auto started = std::chrono::steady_clock::now(); + while (words < limit && input.read(reinterpret_cast(&rank), 8)) { + uint64_t remainder = rank; + int bound = static_cast(width); + for (int position = 0; position < 10; ++position) { + const int suffixLength = 10 - position; + int low = 0; + int high = bound; + int value = 0; + while (low <= high) { + const int middle = (low + high) / 2; + if (choose[middle + suffixLength - 1][suffixLength] <= remainder) { + value = middle; + low = middle + 1; + } else { + high = middle - 1; + } + } + word[position] = static_cast(value); + remainder -= choose[value + suffixLength - 1][suffixLength]; + bound = value; + } + if (remainder != 0) throw std::runtime_error("rank unranking failed"); + + int commonPrefix = 0; + if (!first) { + while (commonPrefix < 10 && previous[commonPrefix] == word[commonPrefix]) + ++commonPrefix; + minimizeTo(commonPrefix); + } + for (int depth = commonPrefix; depth < 10; ++depth) { + edge[depth] = word[depth]; + if (depth + 1 < 10) active[depth + 1].transitions.clear(); + } + previous = word; + first = false; + ++words; + + if (words % 10000000 == 0) { + uint64_t nodeCount = 1; + uint64_t transitionCount = 0; + uint64_t bytes = 0; + for (const Layer& layer : layers) { + nodeCount += layer.nodes.size(); + transitionCount += layer.transitions.size(); + bytes += layer.allocatedBytes(); + } + const double seconds = std::chrono::duration( + std::chrono::steady_clock::now() - started).count(); + std::cerr << "words=" << words << " seconds=" << seconds + << " nodes=" << nodeCount << " transitions=" << transitionCount + << " allocatedMiB=" << bytes / 1048576 << '\n'; + } + } + + if (!first) { + minimizeTo(0); + canonicalize(0); + } + + uint64_t nodeCount = 1; // shared accepting terminal + uint64_t transitionCount = 0; + uint64_t bytes = 0; + std::cout << "words=" << words << '\n'; + for (int depth = 0; depth < 10; ++depth) { + std::cout << "depth=" << depth << " nodes=" << layers[depth].nodes.size() + << " transitions=" << layers[depth].transitions.size() << '\n'; + nodeCount += layers[depth].nodes.size(); + transitionCount += layers[depth].transitions.size(); + bytes += layers[depth].allocatedBytes(); + } + const double seconds = std::chrono::duration( + std::chrono::steady_clock::now() - started).count(); + std::cout << "total_nodes=" << nodeCount + << " total_transitions=" << transitionCount + << " allocated_bytes=" << bytes + << " seconds=" << seconds << '\n'; + return 0; + } catch (const std::exception& error) { + std::cerr << "error: " << error.what() << '\n'; + return 1; + } +} diff --git a/proofs/chomp-10x42/chomp_proof_dag.cpp b/proofs/chomp-10x42/chomp_proof_dag.cpp new file mode 100644 index 00000000..5d1d0eab --- /dev/null +++ b/proofs/chomp-10x42/chomp_proof_dag.cpp @@ -0,0 +1,237 @@ +// Build the shared normal-play proof DAG reachable from one or more exact P-positions. +// +// The P-rank database and this extractor are untrusted discovery tools. The resulting DAG must +// be translated to Lean proof terms and checked by the kernel. + +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include + +using State = std::array; + +struct Database { + int K = 0; + int N = 0; + std::vector> C; + std::vector pRanks; + + explicit Database(const std::string& path) { + std::ifstream in(path, std::ios::binary); + if (!in) throw std::runtime_error("cannot open rank database"); + char magic[8]; + in.read(magic, 8); + if (!in || std::string(magic, 8) != "CHPRANK1") + throw std::runtime_error("bad rank database magic"); + uint64_t k = 0, n = 0; + in.read(reinterpret_cast(&k), 8); + in.read(reinterpret_cast(&n), 8); + if (!in || k < 2 || k > 63 || n > 63) throw std::runtime_error("bad dimensions"); + K = static_cast(k); + N = static_cast(n); + in.seekg(0, std::ios::end); + const uint64_t size = static_cast(in.tellg()); + if (size < 24 || (size - 24) % 8) throw std::runtime_error("bad database size"); + const uint64_t count = (size - 24) / 8; + pRanks.resize(count); + in.seekg(24, std::ios::beg); + in.read(reinterpret_cast(pRanks.data()), static_cast(count * 8)); + if (!in || !std::is_sorted(pRanks.begin(), pRanks.end())) + throw std::runtime_error("unsorted rank database"); + + C.assign(N + K + 3, std::vector(K + 3)); + for (int a = 0; a < static_cast(C.size()); ++a) { + C[a][0] = 1; + for (int b = 1; b <= std::min(a, K + 1); ++b) { + __uint128_t z = static_cast<__uint128_t>(C[a - 1][b - 1]) + C[a - 1][b]; + if (z > std::numeric_limits::max()) + throw std::runtime_error("rank overflow"); + C[a][b] = static_cast(z); + } + } + } + + uint64_t rank(const State& s) const { + uint64_t r = 0; + for (int pos = 0; pos < K; ++pos) { + const int j = K - pos; + r += C[static_cast(s[pos]) + j - 1][j]; + } + return r; + } + + bool isP(const State& s) const { + const uint64_t r = rank(s); + return std::binary_search(pRanks.begin(), pRanks.end(), r); + } +}; + +uint64_t pack(const State& s, int K) { + uint64_t z = 0; + for (int i = 0; i < K; ++i) z |= static_cast(s[i]) << (6 * i); + return z; +} + +State unpack(uint64_t z, int K) { + State s{}; + for (int i = 0; i < K; ++i) s[i] = static_cast((z >> (6 * i)) & 63); + return s; +} + +int weight(const State& s, int K) { + int w = 0; + for (int i = 0; i < K; ++i) w += s[i]; + return w; +} + +std::string show(const State& s, int K) { + std::ostringstream out; + out << '('; + for (int i = 0; i < K; ++i) { + if (i) out << ','; + out << static_cast(s[i]); + } + out << ')'; + return out.str(); +} + +std::vector children(const State& p, int K) { + std::vector out; + for (int i = 0; i < K; ++i) { + for (int t = 0; t < p[i]; ++t) { + if (i == 0 && t == 0) continue; + State q = p; + for (int j = i; j < K; ++j) q[j] = std::min(q[j], t); + out.push_back(q); + } + } + std::sort(out.begin(), out.end(), [K](const State& a, const State& b) { + return pack(a, K) < pack(b, K); + }); + out.erase(std::unique(out.begin(), out.end(), [K](const State& a, const State& b) { + return pack(a, K) == pack(b, K); + }), out.end()); + return out; +} + +State parse(const std::string& text, int K, int N) { + State s{}; + std::stringstream input(text); + std::string part; + int i = 0; + int previous = N; + while (std::getline(input, part, ',')) { + if (i >= K) throw std::runtime_error("root has too many rows"); + const int v = std::stoi(part); + if (v < 0 || v > N || v > previous) throw std::runtime_error("invalid root"); + s[i++] = static_cast(v); + previous = v; + } + if (i != K || s[0] == 0) throw std::runtime_error("root has wrong row count or no poison"); + return s; +} + +int main(int argc, char** argv) { + try { + if (argc < 4) { + std::cerr << "usage: " << argv[0] << " DB.bin NODE_LIMIT ROOT [ROOT ...]\n"; + return 2; + } + Database db(argv[1]); + const uint64_t limit = std::stoull(argv[2]); + std::vector stack; + std::unordered_set seen; + seen.reserve(std::min(limit * 2, 100000000)); + + for (int a = 3; a < argc; ++a) { + State root = parse(argv[a], db.K, db.N); + if (!db.isP(root)) throw std::runtime_error("root is not P: " + show(root, db.K)); + const uint64_t key = pack(root, db.K); + if (seen.insert(key).second) stack.push_back(key); + } + + uint64_t pNodes = 0; + uint64_t nNodes = 0; + uint64_t edges = 0; + uint64_t maxFan = 0; + uint64_t reusedReplies = 0; + uint64_t processed = 0; + + while (!stack.empty()) { + const uint64_t key = stack.back(); + stack.pop_back(); + const State s = unpack(key, db.K); + ++processed; + const auto next = children(s, db.K); + + if (db.isP(s)) { + ++pNodes; + edges += next.size(); + maxFan = std::max(maxFan, next.size()); + for (const State& q : next) { + if (db.isP(q)) + throw std::runtime_error("P node has P child: " + show(s, db.K) + + " -> " + show(q, db.K)); + const uint64_t qkey = pack(q, db.K); + if (seen.insert(qkey).second) { + if (seen.size() > limit) goto limit_hit; + stack.push_back(qkey); + } + } + } else { + ++nNodes; + const State* choice = nullptr; + int bestWeight = std::numeric_limits::max(); + for (const State& q : next) { + if (!db.isP(q)) continue; + const uint64_t qkey = pack(q, db.K); + if (seen.count(qkey)) { + choice = &q; + ++reusedReplies; + break; + } + const int qWeight = weight(q, db.K); + if (qWeight < bestWeight) { + bestWeight = qWeight; + choice = &q; + } + } + if (!choice) throw std::runtime_error("N node has no P child: " + show(s, db.K)); + ++edges; + const uint64_t qkey = pack(*choice, db.K); + if (seen.insert(qkey).second) { + if (seen.size() > limit) goto limit_hit; + stack.push_back(qkey); + } + } + + if (processed % 1000000 == 0) { + std::cerr << "processed=" << processed << " seen=" << seen.size() + << " P=" << pNodes << " N=" << nNodes + << " stack=" << stack.size() << "\n"; + } + } + + std::cout << "COMPLETE nodes=" << seen.size() << " P=" << pNodes << " N=" << nNodes + << " edges=" << edges << " maxFan=" << maxFan + << " reused=" << reusedReplies << "\n"; + return 0; + +limit_hit: + std::cout << "LIMIT nodes=" << seen.size() << " processed=" << processed + << " P=" << pNodes << " N=" << nNodes << " edges=" << edges + << " maxFan=" << maxFan << " reused=" << reusedReplies + << " stack=" << stack.size() << "\n"; + return 3; + } catch (const std::exception& e) { + std::cerr << "error: " << e.what() << "\n"; + return 1; + } +} diff --git a/proofs/chomp-10x42/lean/ChompCatalogBridge.lean b/proofs/chomp-10x42/lean/ChompCatalogBridge.lean new file mode 100644 index 00000000..2748844e --- /dev/null +++ b/proofs/chomp-10x42/lean/ChompCatalogBridge.lean @@ -0,0 +1,130 @@ +/- +Copyright 2026 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import ChompPosition +import ChompKernelGameTheory +import ChompKernelPSet + +/-! +# Bridge from kernel game outcomes to the catalog P-set definition + +The catalog defines a P-position by membership in a global complete P-set. For a progressively +bounded normal-play game, the set of valid positions having a losing outcome is exactly such a +set. Thus a finite certificate proving one child losing implies the existing catalog predicate; +the theorem statement does not need to be weakened. +-/ + +namespace OeisA147983 + +/-- The global set of valid positions with kernel-checked losing outcomes. -/ +def kernelPSet : Set (List ℕ) := + {p | IsPosition p ∧ ChompKernel.IsLosing rankedGame.Move p} + +/-- The global losing-outcome set is a complete Chomp P-set. -/ +theorem kernelPSet_isPSet : IsPSet kernelPSet := by + refine ⟨?_, ?_, ?_⟩ + · intro p hp + exact hp.1 + · intro p q hp hmove hq + rcases hp with ⟨_, ⟨hpLosing⟩⟩ + rcases hq with ⟨_, ⟨hqLosing⟩⟩ + have hqWinning : ChompKernel.Outcome rankedGame.Move q true := + hpLosing.children q hmove + exact rankedGame.outcome_exclusive q ⟨hqLosing, hqWinning⟩ + · intro p hpPosition hpNot + rcases rankedGame.outcome_total p with hpLosing | hpWinning + · exact (hpNot ⟨hpPosition, ⟨hpLosing⟩⟩).elim + · obtain ⟨q, hmove, hqLosing⟩ := hpWinning.reply + refine ⟨q, ?_, hmove⟩ + exact ⟨move_preserves_position hpPosition hmove, ⟨hqLosing⟩⟩ + +/-- Every valid position with a losing outcome satisfies the catalog's `IsPPosition`. -/ +theorem isPPosition_of_losing {p : List ℕ} + (hp : IsPosition p) (hlosing : ChompKernel.IsLosing rankedGame.Move p) : + IsPPosition p := by + exact ⟨kernelPSet, kernelPSet_isPSet, hp, hlosing⟩ + +@[category test, AMS 5] +theorem child₁_is_position : IsPosition child₁ := by + norm_num [IsPosition, IsFerrers, child₁] + +@[category test, AMS 5] +theorem child₂_is_position : IsPosition child₂ := by + norm_num [IsPosition, IsFerrers, child₂] + +@[category test, AMS 5] +theorem child₃_is_position : IsPosition child₃ := by + norm_num [IsPosition, IsFerrers, child₃] + +/-- Each claimed child belongs to the exact finite symbolic-certificate domain. -/ +theorem child₁_in_certificateDomain : CertificateDomain child₁ := by + exact ⟨child₁_is_position, by norm_num [child₁], by norm_num [child₁]⟩ + +/-- Each claimed child belongs to the exact finite symbolic-certificate domain. -/ +theorem child₂_in_certificateDomain : CertificateDomain child₂ := by + exact ⟨child₂_is_position, by norm_num [child₂], by norm_num [child₂]⟩ + +/-- Each claimed child belongs to the exact finite symbolic-certificate domain. -/ +theorem child₃_in_certificateDomain : CertificateDomain child₃ := by + exact ⟨child₃_is_position, by norm_num [child₃], by norm_num [child₃]⟩ + +/-- Three kernel losing proofs discharge the catalog theorem without any external axiom. -/ +theorem three_openings_of_losing + (h₁ : ChompKernel.IsLosing rankedGame.Move child₁) + (h₂ : ChompKernel.IsLosing rankedGame.Move child₂) + (h₃ : ChompKernel.IsLosing rankedGame.Move child₃) : + IsWinningOpening rectangle child₁ ∧ + IsWinningOpening rectangle child₂ ∧ + IsWinningOpening rectangle child₃ ∧ + child₁ ≠ child₂ ∧ child₁ ≠ child₃ ∧ child₂ ≠ child₃ := by + apply three_openings_of_p_positions + · exact isPPosition_of_losing child₁_is_position h₁ + · exact isPPosition_of_losing child₂_is_position h₂ + · exact isPPosition_of_losing child₃_is_position h₃ + +/-- Final interface for the concrete symbolic certificate. + +A predicate on ten-row positions proves the exact Chomp challenge once Lean verifies that the +finite certificate domain is partitioned by the two P-position laws and that all three displayed +children satisfy the predicate. -/ +theorem three_openings_of_local_pSet + (S : List ℕ → Prop) + (no_move : ∀ {p : List ℕ}, CertificateDomain p → S p → + ∀ q, rankedGame.Move p q → ¬S q) + (has_reply : ∀ {p : List ℕ}, CertificateDomain p → ¬S p → + ∃ q, rankedGame.Move p q ∧ S q) + (h₁ : S child₁) (h₂ : S child₂) (h₃ : S child₃) : + IsWinningOpening rectangle child₁ ∧ + IsWinningOpening rectangle child₂ ∧ + IsWinningOpening rectangle child₃ ∧ + child₁ ≠ child₂ ∧ child₁ ≠ child₃ ∧ child₂ ≠ child₃ := by + apply three_openings_of_losing + · exact ChompKernel.RankedGame.losing_of_local_pSet + (G := rankedGame) CertificateDomain S move_preserves_certificateDomain + no_move has_reply child₁_in_certificateDomain h₁ + · exact ChompKernel.RankedGame.losing_of_local_pSet + (G := rankedGame) CertificateDomain S move_preserves_certificateDomain + no_move has_reply child₂_in_certificateDomain h₂ + · exact ChompKernel.RankedGame.losing_of_local_pSet + (G := rankedGame) CertificateDomain S move_preserves_certificateDomain + no_move has_reply child₃_in_certificateDomain h₃ + +#print axioms kernelPSet_isPSet +#print axioms isPPosition_of_losing +#print axioms three_openings_of_losing +#print axioms three_openings_of_local_pSet + +end OeisA147983 diff --git a/proofs/chomp-10x42/lean/ChompPosition.lean b/proofs/chomp-10x42/lean/ChompPosition.lean new file mode 100644 index 00000000..aef45a00 --- /dev/null +++ b/proofs/chomp-10x42/lean/ChompPosition.lean @@ -0,0 +1,131 @@ +/- +Copyright 2026 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import ChompRank + +/-! +# Legal Chomp moves preserve the position invariants +-/ + +namespace OeisA147983 + +/-- Cutting every row at a fixed threshold preserves the Ferrers inequalities. -/ +theorem cutSuffix_isFerrers (t : ℕ) : ∀ {p : List ℕ}, IsFerrers p → IsFerrers (cutSuffix t p) + | [], h => by simp [IsFerrers] at h + | [x], _ => by simp [cutSuffix, IsFerrers] + | x :: y :: xs, h => by + rcases h with ⟨hyx, htail⟩ + simp only [cutSuffix, IsFerrers] + exact ⟨min_le_min hyx le_rfl, cutSuffix_isFerrers t htail⟩ + +/-- Cutting a suffix preserves the number of rows. -/ +theorem cutSuffix_length (t : ℕ) : ∀ p : List ℕ, + (cutSuffix t p).length = p.length + | [] => by simp [cutSuffix] + | x :: xs => by simp [cutSuffix, cutSuffix_length t xs] + +/-- A bite never increases the first row. -/ +theorem bite_head_le (i t : ℕ) : ∀ p : List ℕ, + (bite i t p).getD 0 0 ≤ p.getD 0 0 + | [] => by simp [bite] + | x :: xs => by + cases i <;> simp [bite, cutSuffix] + +/-- A bite preserves the number of rows. -/ +theorem bite_length (i t : ℕ) (p : List ℕ) : + (bite i t p).length = p.length := by + induction i generalizing p with + | zero => + cases p <;> simp [bite, cutSuffix_length] + | succ i ih => + cases p with + | nil => simp [bite] + | cons x xs => simp [bite, ih] + +/-- A bite preserves the Ferrers inequalities. -/ +theorem bite_isFerrers (t : ℕ) : ∀ i : ℕ, ∀ {p : List ℕ}, + IsFerrers p → IsFerrers (bite i t p) + | 0, [], h => by + simp [IsFerrers] at h + | 0, x :: xs, h => by + simpa [bite] using cutSuffix_isFerrers t h + | i + 1, [], h => by + simp [IsFerrers] at h + | i + 1, [x], _ => by + simp [bite, IsFerrers] + | i + 1, x :: y :: xs, h => by + rcases h with ⟨hyx, htail⟩ + have htailFerrers : IsFerrers (bite i t (y :: xs)) := + bite_isFerrers t i htail + have hhead : (bite i t (y :: xs)).getD 0 0 ≤ x := + le_trans (bite_head_le i t (y :: xs)) hyx + have hnonempty : bite i t (y :: xs) ≠ [] := by + cases i <;> simp [bite, cutSuffix] + cases hbite : bite i t (y :: xs) with + | nil => exact (hnonempty hbite).elim + | cons z zs => + have hz : z ≤ x := by simpa [hbite] using hhead + simp only [bite, hbite, IsFerrers] + exact ⟨hz, by simpa [hbite] using htailFerrers⟩ + +/-- If the poisoned square was present and a first-row move does not take it, the bitten +position still contains the poisoned square. -/ +theorem bite_head_pos {p : List ℕ} {i t : ℕ} + (hp : 0 < p.getD 0 0) (hpoison : i = 0 → 0 < t) : + 0 < (bite i t p).getD 0 0 := by + cases p with + | nil => simp at hp + | cons x xs => + have hx : 0 < x := by simpa using hp + cases i with + | zero => + have ht : 0 < t := hpoison rfl + simpa [bite, cutSuffix] using (lt_min hx ht) + | succ i => + simpa [bite] using hx + +/-- Every legal move from a legal Chomp position produces another legal Chomp position. -/ +theorem move_preserves_position {p q : List ℕ} + (hp : IsPosition p) (hmove : Move p q) : IsPosition q := by + rcases hp with ⟨hferrers, hpoisoned⟩ + rcases hmove with ⟨i, t, _, _, hpoison, rfl⟩ + exact ⟨bite_isFerrers t i hferrers, bite_head_pos hpoisoned hpoison⟩ + +/-- The finite symbolic-certificate universe: legal ten-row positions whose first row has width +at most 42. -/ +def CertificateDomain (p : List ℕ) : Prop := + IsPosition p ∧ p.length = 10 ∧ p.getD 0 0 ≤ 42 + +/-- The concrete 10 × 42 certificate domain is closed under legal Chomp moves. -/ +theorem move_preserves_certificateDomain {p q : List ℕ} + (hp : CertificateDomain p) (hmove : Move p q) : CertificateDomain q := by + rcases hp with ⟨hpPosition, hpLength, hpHead⟩ + rcases hmove with ⟨i, t, hi, ht, hpoison, rfl⟩ + refine ⟨move_preserves_position hpPosition ⟨i, t, hi, ht, hpoison, rfl⟩, ?_, ?_⟩ + · calc + (bite i t p).length = p.length := bite_length i t p + _ = 10 := hpLength + · exact (bite_head_le i t p).trans hpHead + +#print axioms cutSuffix_isFerrers +#print axioms cutSuffix_length +#print axioms bite_length +#print axioms bite_isFerrers +#print axioms bite_head_pos +#print axioms move_preserves_position +#print axioms move_preserves_certificateDomain + +end OeisA147983 diff --git a/proofs/chomp-10x42/lean/ChompRank.lean b/proofs/chomp-10x42/lean/ChompRank.lean new file mode 100644 index 00000000..db810ac1 --- /dev/null +++ b/proofs/chomp-10x42/lean/ChompRank.lean @@ -0,0 +1,74 @@ +/- +Copyright 2026 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import FormalConjectures.OEIS.«147983» +import ChompKernelCertificate + +/-! +# Chomp is progressively bounded + +Every legal bite strictly decreases the total number of remaining squares. This supplies the +natural-number rank used by the kernel certificate theorem. +-/ + +namespace OeisA147983 + +/-- Cutting a suffix never increases its total row length. -/ +theorem cutSuffix_sum_le (t : ℕ) : ∀ p : List ℕ, (cutSuffix t p).sum ≤ p.sum + | [] => by simp [cutSuffix] + | x :: xs => by + simpa [cutSuffix] using + Nat.add_le_add (min_le_left x t) (cutSuffix_sum_le t xs) + +/-- A legal bite strictly decreases the total number of remaining squares. -/ +theorem bite_sum_lt {p : List ℕ} {i t : ℕ} + (hi : i < p.length) (ht : t < p.getD i 0) : + (bite i t p).sum < p.sum := by + induction i generalizing p with + | zero => + cases p with + | nil => simp at hi + | cons x xs => + have htx : t < x := by simpa using ht + have htail := cutSuffix_sum_le t xs + simp only [bite, cutSuffix, List.sum_cons] + rw [min_eq_right (Nat.le_of_lt htx)] + omega + | succ i ih => + cases p with + | nil => simp at hi + | cons x xs => + have hi' : i < xs.length := by simpa using hi + have ht' : t < xs.getD i 0 := by simpa using ht + have hrec := ih (p := xs) hi' ht' + simpa only [bite, List.sum_cons] using Nat.add_lt_add_left hrec x + +/-- Every move in the catalog Chomp relation strictly decreases area. -/ +theorem move_sum_lt {p q : List ℕ} (h : Move p q) : q.sum < p.sum := by + rcases h with ⟨i, t, hi, ht, _, rfl⟩ + exact bite_sum_lt hi ht + +/-- The catalog Chomp relation as a progressively bounded ranked game. -/ +def rankedGame : ChompKernel.RankedGame (List ℕ) where + Move := Move + rank := List.sum + decreases := move_sum_lt + +#print axioms cutSuffix_sum_le +#print axioms bite_sum_lt +#print axioms move_sum_lt + +end OeisA147983 diff --git a/proofs/chomp-10x42/lean/KernelCertificate.lean b/proofs/chomp-10x42/lean/KernelCertificate.lean new file mode 100644 index 00000000..adef4049 --- /dev/null +++ b/proofs/chomp-10x42/lean/KernelCertificate.lean @@ -0,0 +1,135 @@ +/- +Copyright 2026 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import FormalConjecturesUtil + +/-! +# Kernel-checked finite game certificates + +The certificate producer is untrusted. A certificate contains finitely many nodes, interprets +each node as an actual game position, and proves every edge it uses is a real move. At a +losing-labelled node it must additionally prove that every real legal child is represented. +Lean reconstructs the normal-play outcome proof by strong induction on a decreasing rank. +-/ + +namespace ChompKernel + +/-- A finite proof that a position is losing (`false`) or winning (`true`). + +A losing proof contains a winning proof for every legal child. A winning proof contains one +legal move to a position with a losing proof. -/ +inductive Outcome {P : Type} (Move : P → P → Prop) : P → Bool → Prop + | losing {p : P} (children : ∀ q, Move p q → Outcome Move q true) : Outcome Move p false + | winning {p q : P} (move : Move p q) (child : Outcome Move q false) : Outcome Move p true + +/-- A position has a kernel-checked losing proof. -/ +def IsLosing {P : Type} (Move : P → P → Prop) (p : P) : Prop := + Nonempty (Outcome Move p false) + +/-- A position has a kernel-checked winning proof. -/ +def IsWinning {P : Type} (Move : P → P → Prop) (p : P) : Prop := + Nonempty (Outcome Move p true) + +/-- A progressively bounded game: every move strictly decreases a natural-number rank. -/ +structure RankedGame (P : Type) where + Move : P → P → Prop + rank : P → ℕ + decreases : ∀ {p q : P}, Move p q → rank q < rank p + +namespace RankedGame + +variable {P : Type} {G : RankedGame P} {n : ℕ} + +/-- A finite, interpreted game certificate. + +At losing nodes, `losing_complete` proves that all actual legal children occur in `children`. +At winning nodes only one legal losing reply is required, so irrelevant alternatives need not be +stored. -/ +structure Certificate (G : RankedGame P) (n : ℕ) where + pos : Fin n → P + label : Fin n → Bool + children : Fin n → Finset (Fin n) + reply : Fin n → Option (Fin n) + children_sound : ∀ {i j : Fin n}, j ∈ children i → G.Move (pos i) (pos j) + losing_complete : ∀ (i : Fin n), label i = false → ∀ (q : P), G.Move (pos i) q → + ∃ j, j ∈ children i ∧ pos j = q + +namespace Certificate + +/-- Local outcome-label validity. + +* Every represented child of a losing-labelled node is labelled winning. +* Every winning-labelled node names a represented child labelled losing. +-/ +def ValidAt (C : Certificate G n) (i : Fin n) : Prop := + match C.label i with + | false => ∀ j, j ∈ C.children i → C.label j = true + | true => ∃ j, C.reply i = some j ∧ j ∈ C.children i ∧ C.label j = false + +/-- A valid finite interpreted certificate yields genuine outcome proofs for the actual game. + +An arbitrary real move from a losing node is brought into the finite certificate through +`losing_complete`. A winning node needs only its one certified reply. -/ +theorem outcome_of_valid (C : Certificate G n) (hvalid : ∀ i, C.ValidAt i) (i : Fin n) : + Outcome G.Move (C.pos i) (C.label i) := by + have all : ∀ k : ℕ, ∀ i : Fin n, G.rank (C.pos i) = k → + Outcome G.Move (C.pos i) (C.label i) := by + intro k + induction k using Nat.strong_induction_on with + | h k ih => + intro i hrank + cases hi : C.label i with + | false => + have hv : ∀ j, j ∈ C.children i → C.label j = true := by + simpa [ValidAt, hi] using hvalid i + exact Outcome.losing (fun q hq ↦ by + obtain ⟨j, hj, hpos⟩ := C.losing_complete i hi q hq + subst q + have hlt : G.rank (C.pos j) < k := by + simpa [← hrank] using G.decreases (C.children_sound hj) + have hout := ih _ hlt j rfl + simpa [hv j hj] using hout) + | true => + have hv : ∃ j, C.reply i = some j ∧ j ∈ C.children i ∧ C.label j = false := by + simpa [ValidAt, hi] using hvalid i + obtain ⟨j, _, hj, hlabel⟩ := hv + exact Outcome.winning (C.children_sound hj) (by + have hlt : G.rank (C.pos j) < k := by + simpa [← hrank] using G.decreases (C.children_sound hj) + have hout := ih _ hlt j rfl + simpa [hlabel] using hout) + exact all _ i rfl + +/-- A losing-labelled root of a valid certificate has a kernel-checked losing proof. -/ +theorem losing_of_valid (C : Certificate G n) (hvalid : ∀ i, C.ValidAt i) {i : Fin n} + (hi : C.label i = false) : IsLosing G.Move (C.pos i) := by + refine ⟨?_⟩ + simpa [hi] using C.outcome_of_valid hvalid i + +/-- A winning-labelled root of a valid certificate has a kernel-checked winning proof. -/ +theorem winning_of_valid (C : Certificate G n) (hvalid : ∀ i, C.ValidAt i) {i : Fin n} + (hi : C.label i = true) : IsWinning G.Move (C.pos i) := by + refine ⟨?_⟩ + simpa [hi] using C.outcome_of_valid hvalid i + +end Certificate +end RankedGame + +#print axioms RankedGame.Certificate.outcome_of_valid +#print axioms RankedGame.Certificate.losing_of_valid +#print axioms RankedGame.Certificate.winning_of_valid + +end ChompKernel diff --git a/proofs/chomp-10x42/lean/KernelGameTheory.lean b/proofs/chomp-10x42/lean/KernelGameTheory.lean new file mode 100644 index 00000000..93b22e1f --- /dev/null +++ b/proofs/chomp-10x42/lean/KernelGameTheory.lean @@ -0,0 +1,103 @@ +/- +Copyright 2026 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import ChompKernelCertificate + +/-! +# Determinacy of progressively bounded normal-play games + +No finite-branching assumption is needed: classical excluded middle selects whether a position +has a losing child, and the natural rank makes the recursive outcome proof well founded. +-/ + +namespace ChompKernel + +namespace Outcome + +variable {P : Type} {Move : P → P → Prop} {p : P} + +/-- A losing proof supplies a winning proof for every child. -/ +theorem children (h : Outcome Move p false) : ∀ q, Move p q → Outcome Move q true := by + cases h with + | losing children => exact children + +/-- A winning proof supplies one legal losing reply. -/ +theorem reply (h : Outcome Move p true) : ∃ q, Move p q ∧ Outcome Move q false := by + cases h with + | winning move child => exact ⟨_, move, child⟩ + +end Outcome + +namespace RankedGame + +variable {P : Type} (G : RankedGame P) + +/-- Every position in a progressively bounded normal-play game is losing or winning. -/ +theorem outcome_total (p : P) : Outcome G.Move p false ∨ Outcome G.Move p true := by + have all : ∀ k : ℕ, ∀ p : P, G.rank p = k → + Outcome G.Move p false ∨ Outcome G.Move p true := by + intro k + induction k using Nat.strong_induction_on with + | h k ih => + intro p hrank + by_cases hasLosingChild : ∃ q, G.Move p q ∧ Outcome G.Move q false + · obtain ⟨q, hmove, hq⟩ := hasLosingChild + exact Or.inr (Outcome.winning hmove hq) + · apply Or.inl + exact Outcome.losing (fun q hmove ↦ by + have hlt : G.rank q < k := by + simpa [← hrank] using G.decreases hmove + rcases ih _ hlt q rfl with hq | hq + · exact (hasLosingChild ⟨q, hmove, hq⟩).elim + · exact hq) + exact all _ p rfl + +/-- A position cannot be both losing and winning. -/ +theorem outcome_exclusive (p : P) : + ¬(Outcome G.Move p false ∧ Outcome G.Move p true) := by + have all : ∀ k : ℕ, ∀ p : P, G.rank p = k → + ¬(Outcome G.Move p false ∧ Outcome G.Move p true) := by + intro k + induction k using Nat.strong_induction_on with + | h k ih => + intro p hrank hboth + rcases hboth with ⟨hlosing, hwinning⟩ + obtain ⟨q, hmove, hqLosing⟩ := hwinning.reply + have hqWinning := hlosing.children q hmove + have hlt : G.rank q < k := by + simpa [← hrank] using G.decreases hmove + exact ih _ hlt q rfl ⟨hqLosing, hqWinning⟩ + exact all _ p rfl + +/-- A losing proof rules out every winning proof of the same position. -/ +theorem not_winning_of_losing {p : P} (h : Outcome G.Move p false) : + ¬Outcome G.Move p true := by + intro hw + exact G.outcome_exclusive p ⟨h, hw⟩ + +/-- A winning proof rules out every losing proof of the same position. -/ +theorem not_losing_of_winning {p : P} (h : Outcome G.Move p true) : + ¬Outcome G.Move p false := by + intro hl + exact G.outcome_exclusive p ⟨hl, h⟩ + +#print axioms outcome_total +#print axioms outcome_exclusive +#print axioms not_winning_of_losing +#print axioms not_losing_of_winning + +end RankedGame +end ChompKernel diff --git a/proofs/chomp-10x42/lean/KernelPSet.lean b/proofs/chomp-10x42/lean/KernelPSet.lean new file mode 100644 index 00000000..3cb8faae --- /dev/null +++ b/proofs/chomp-10x42/lean/KernelPSet.lean @@ -0,0 +1,139 @@ +/- +Copyright 2026 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import ChompKernelCertificate + +/-! +# Certified P-sets give genuine normal-play outcome proofs + +For a progressively bounded game, a predicate is the losing-position predicate when + +* no position satisfying it can move to another position satisfying it; and +* every position not satisfying it has a move to a position satisfying it. + +The local form additionally restricts those obligations to a move-closed domain. This is the +form needed by the concrete Chomp certificate: only the finite descendant domain of the three +10 × 42 children must be represented by the symbolic decision diagram. +-/ + +namespace ChompKernel +namespace RankedGame + +variable {P : Type} {G : RankedGame P} + +/-- A predicate satisfying the two global P-position conditions produces actual losing and +winning proof objects for every ranked game position. -/ +theorem outcomes_of_pSet + (S : P → Prop) + (no_move : ∀ {p : P}, S p → ∀ q, G.Move p q → ¬S q) + (has_reply : ∀ {p : P}, ¬S p → ∃ q, G.Move p q ∧ S q) : + ∀ p : P, (S p → Outcome G.Move p false) ∧ (¬S p → Outcome G.Move p true) := by + intro p + have all : ∀ k : ℕ, ∀ p : P, G.rank p = k → + (S p → Outcome G.Move p false) ∧ (¬S p → Outcome G.Move p true) := by + intro k + induction k using Nat.strong_induction_on with + | h k ih => + intro p hrank + constructor + · intro hp + exact Outcome.losing (fun q hmove ↦ by + have hnq : ¬S q := no_move hp q hmove + have hlt : G.rank q < k := by + simpa [← hrank] using G.decreases hmove + exact (ih _ hlt q rfl).2 hnq) + · intro hnp + obtain ⟨q, hmove, hq⟩ := has_reply hnp + have hlt : G.rank q < k := by + simpa [← hrank] using G.decreases hmove + exact Outcome.winning hmove ((ih _ hlt q rfl).1 hq) + exact all _ p rfl + +/-- Membership in a certified global P-set gives a kernel-checked losing proof. -/ +theorem losing_of_pSet + (S : P → Prop) + (no_move : ∀ {p : P}, S p → ∀ q, G.Move p q → ¬S q) + (has_reply : ∀ {p : P}, ¬S p → ∃ q, G.Move p q ∧ S q) + {p : P} (hp : S p) : IsLosing G.Move p := by + exact ⟨(outcomes_of_pSet S no_move has_reply p).1 hp⟩ + +/-- Nonmembership in a certified global P-set gives a kernel-checked winning proof. -/ +theorem winning_of_not_pSet + (S : P → Prop) + (no_move : ∀ {p : P}, S p → ∀ q, G.Move p q → ¬S q) + (has_reply : ∀ {p : P}, ¬S p → ∃ q, G.Move p q ∧ S q) + {p : P} (hp : ¬S p) : IsWinning G.Move p := by + exact ⟨(outcomes_of_pSet S no_move has_reply p).2 hp⟩ + +/-- A P-set certificate restricted to a move-closed domain still reconstructs genuine outcomes +for every position in that domain. -/ +theorem outcomes_of_local_pSet + (D S : P → Prop) + (closed : ∀ {p q : P}, D p → G.Move p q → D q) + (no_move : ∀ {p : P}, D p → S p → ∀ q, G.Move p q → ¬S q) + (has_reply : ∀ {p : P}, D p → ¬S p → ∃ q, G.Move p q ∧ S q) : + ∀ p : P, D p → + (S p → Outcome G.Move p false) ∧ (¬S p → Outcome G.Move p true) := by + intro p hpD + have all : ∀ k : ℕ, ∀ p : P, G.rank p = k → D p → + (S p → Outcome G.Move p false) ∧ (¬S p → Outcome G.Move p true) := by + intro k + induction k using Nat.strong_induction_on with + | h k ih => + intro p hrank hpD + constructor + · intro hp + exact Outcome.losing (fun q hmove ↦ by + have hqD : D q := closed hpD hmove + have hnq : ¬S q := no_move hpD hp q hmove + have hlt : G.rank q < k := by + simpa [← hrank] using G.decreases hmove + exact (ih _ hlt q rfl hqD).2 hnq) + · intro hnp + obtain ⟨q, hmove, hq⟩ := has_reply hpD hnp + have hqD : D q := closed hpD hmove + have hlt : G.rank q < k := by + simpa [← hrank] using G.decreases hmove + exact Outcome.winning hmove ((ih _ hlt q rfl hqD).1 hq) + exact all _ p rfl hpD + +/-- Membership in a locally certified P-set gives a kernel-checked losing proof. -/ +theorem losing_of_local_pSet + (D S : P → Prop) + (closed : ∀ {p q : P}, D p → G.Move p q → D q) + (no_move : ∀ {p : P}, D p → S p → ∀ q, G.Move p q → ¬S q) + (has_reply : ∀ {p : P}, D p → ¬S p → ∃ q, G.Move p q ∧ S q) + {p : P} (hpD : D p) (hp : S p) : IsLosing G.Move p := by + exact ⟨(outcomes_of_local_pSet D S closed no_move has_reply p hpD).1 hp⟩ + +/-- Nonmembership in a locally certified P-set gives a kernel-checked winning proof. -/ +theorem winning_of_not_local_pSet + (D S : P → Prop) + (closed : ∀ {p q : P}, D p → G.Move p q → D q) + (no_move : ∀ {p : P}, D p → S p → ∀ q, G.Move p q → ¬S q) + (has_reply : ∀ {p : P}, D p → ¬S p → ∃ q, G.Move p q ∧ S q) + {p : P} (hpD : D p) (hp : ¬S p) : IsWinning G.Move p := by + exact ⟨(outcomes_of_local_pSet D S closed no_move has_reply p hpD).2 hp⟩ + +#print axioms outcomes_of_pSet +#print axioms losing_of_pSet +#print axioms winning_of_not_pSet +#print axioms outcomes_of_local_pSet +#print axioms losing_of_local_pSet +#print axioms winning_of_not_local_pSet + +end RankedGame +end ChompKernel diff --git a/proofs/chomp-10x42/lean/MDDCertificate.lean b/proofs/chomp-10x42/lean/MDDCertificate.lean new file mode 100644 index 00000000..e79d6e99 --- /dev/null +++ b/proofs/chomp-10x42/lean/MDDCertificate.lean @@ -0,0 +1,139 @@ +/- +Copyright 2026 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import FormalConjecturesUtil + +/-! +# Kernel certificates for layered decision-diagram languages + +The concrete Chomp P-set is represented externally by a reduced layered multi-valued decision +diagram. This file supplies the small trusted theorem layer: local simulation certificates imply +language inclusion, and local product-closure certificates imply language disjointness. + +Concrete node tables and local certificates remain untrusted data until these hypotheses are +proved in Lean. +-/ + +namespace ChompKernel +namespace MDD + +/-- A deterministic finite-state acceptor. Layering is not needed for semantic correctness; +the concrete MDD checker separately proves that its node table is layered and well formed. -/ +structure Automaton (σ : Type) (n : ℕ) where + step : Fin n → σ → Option (Fin n) + accept : Fin n → Bool + +namespace Automaton + +variable {σ : Type} {n m : ℕ} + +/-- Evaluate a word from a selected automaton state. -/ +def acceptsFrom (A : Automaton σ n) (i : Fin n) : List σ → Bool + | [] => A.accept i + | a :: word => + match A.step i a with + | none => false + | some j => A.acceptsFrom j word + +/-- A local forward simulation between deterministic acceptors. -/ +structure InclusionCertificate (A : Automaton σ n) (B : Automaton σ m) where + Rel : Fin n → Fin m → Prop + accept_mono : ∀ {i j}, Rel i j → A.accept i = true → B.accept j = true + step_sim : ∀ {i j i'} (a : σ), Rel i j → A.step i a = some i' → + ∃ j', B.step j a = some j' ∧ Rel i' j' + +namespace InclusionCertificate + +variable {A : Automaton σ n} {B : Automaton σ m} + +/-- Related states accept an included language. -/ +theorem accepts_mono (C : InclusionCertificate A B) {i : Fin n} {j : Fin m} + (hrel : C.Rel i j) (word : List σ) : + A.acceptsFrom i word = true → B.acceptsFrom j word = true := by + induction word generalizing i j with + | nil => + simpa [acceptsFrom] using C.accept_mono hrel + | cons a word ih => + intro haccept + cases hi : A.step i a with + | none => + simp [acceptsFrom, hi] at haccept + | some i' => + obtain ⟨j', hj, hnext⟩ := C.step_sim a hrel hi + have htail : A.acceptsFrom i' word = true := by + simpa [acceptsFrom, hi] using haccept + have := ih hnext htail + simpa [acceptsFrom, hj] using this + +end InclusionCertificate + +/-- A local synchronized-product certificate proving that two languages are disjoint. -/ +structure DisjointnessCertificate (A : Automaton σ n) (B : Automaton σ m) where + Rel : Fin n → Fin m → Prop + terminal_disjoint : ∀ {i j}, Rel i j → ¬(A.accept i = true ∧ B.accept j = true) + step_closed : ∀ {i j i' j'} (a : σ), Rel i j → + A.step i a = some i' → B.step j a = some j' → Rel i' j' + +namespace DisjointnessCertificate + +variable {A : Automaton σ n} {B : Automaton σ m} + +/-- Related product states cannot both accept the same word. -/ +theorem not_both_accept (C : DisjointnessCertificate A B) {i : Fin n} {j : Fin m} + (hrel : C.Rel i j) (word : List σ) : + ¬(A.acceptsFrom i word = true ∧ B.acceptsFrom j word = true) := by + induction word generalizing i j with + | nil => + simpa [acceptsFrom] using C.terminal_disjoint hrel + | cons a word ih => + intro hboth + rcases hboth with ⟨ha, hb⟩ + cases hi : A.step i a with + | none => + simp [acceptsFrom, hi] at ha + | some i' => + cases hj : B.step j a with + | none => + simp [acceptsFrom, hj] at hb + | some j' => + have hnext := C.step_closed a hrel hi hj + have ha' : A.acceptsFrom i' word = true := by + simpa [acceptsFrom, hi] using ha + have hb' : B.acceptsFrom j' word = true := by + simpa [acceptsFrom, hj] using hb + exact ih hnext ⟨ha', hb'⟩ + +end DisjointnessCertificate + +/-- Two opposite inclusion certificates prove language equality at related roots. -/ +theorem language_eq_of_inclusions + {A : Automaton σ n} {B : Automaton σ m} + (AB : InclusionCertificate A B) (BA : InclusionCertificate B A) + {i : Fin n} {j : Fin m} (hAB : AB.Rel i j) (hBA : BA.Rel j i) : + ∀ word, A.acceptsFrom i word = B.acceptsFrom j word := by + intro word + apply Bool.eq_iff_iff.mpr + constructor + · exact AB.accepts_mono hAB word + · exact BA.accepts_mono hBA word + +#print axioms InclusionCertificate.accepts_mono +#print axioms DisjointnessCertificate.not_both_accept +#print axioms language_eq_of_inclusions + +end Automaton +end MDD +end ChompKernel diff --git a/proofs/chomp-10x42/run_kernel_feasibility.sh b/proofs/chomp-10x42/run_kernel_feasibility.sh new file mode 100644 index 00000000..c6c0e33d --- /dev/null +++ b/proofs/chomp-10x42/run_kernel_feasibility.sh @@ -0,0 +1,44 @@ +#!/usr/bin/env bash +set -euo pipefail + +# This is a measurement run, not the final proof check. The two-million-node cap determines +# whether direct theorem generation is plausible before a full certificate is serialized. +g++ -std=c++17 -O3 -march=native -DNDEBUG -Wall -Wextra -Wpedantic \ + chomp_export_p_ranks.cpp -o chomp_export_p_ranks +g++ -std=c++17 -O3 -march=native -DNDEBUG -Wall -Wextra -Wpedantic \ + chomp_proof_dag.cpp -o chomp_proof_dag + +./chomp_export_p_ranks 4 10 p4x10.bin 2> p4x10-export.log +./chomp_proof_dag p4x10.bin 100000 10,8,8,7 | tee p4x10-dag.log +grep -F 'P=75 prefixes=285 last_rank=967' p4x10-export.log +grep -F 'COMPLETE nodes=470 P=58 N=412 edges=1306 maxFan=32' p4x10-dag.log + +/usr/bin/time -v ./chomp_export_p_ranks 10 42 p10x42.bin \ + > p10x42-export.out 2> p10x42-export.log +test "$(stat -c%s p10x42.bin)" -gt 800000000 +grep -E '^P=[0-9]+ prefixes=3042312350 last_rank=' p10x42-export.log + +set +e +/usr/bin/time -v ./chomp_proof_dag p10x42.bin 2000000 \ + 42,42,42,42,35,35,35,35,35,35 \ + 42,42,42,42,42,42,29,29,29,29 \ + 42,42,42,42,42,42,42,25,25,25 \ + > p10x42-dag.out 2> p10x42-dag.log +status=$? +set -e +if [[ $status -ne 0 && $status -ne 3 ]]; then + cat p10x42-dag.log >&2 + exit "$status" +fi +grep -E '^(COMPLETE|LIMIT) nodes=' p10x42-dag.out + +{ + echo '# Chomp 10x42 kernel-certificate feasibility' + echo + echo '## Full P database' + tail -n 20 p10x42-export.log + echo + echo '## Shared proof DAG' + cat p10x42-dag.out + tail -n 30 p10x42-dag.log +} | tee certificate-feasibility.md