Develop pure-kernel proof of Chomp 10×42

.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,41 +47,69 @@ 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
 
       - name: Upload Lean transcripts
         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

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.

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 <algorithm>
+#include <cstdint>
+#include <cstring>
+#include <fstream>
+#include <iostream>
+#include <limits>
+#include <stdexcept>
+#include <string>
+#include <vector>
+
+using std::min;
+using std::vector;
+
+struct Bits {
+    vector<uint64_t> 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<int>(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<uint64_t>(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<int>(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<uint64_t>::max())
+                    throw std::runtime_error("rank overflow");
+                C[a][b] = static_cast<uint64_t>(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<vector<uint64_t>> C;
+    vector<Bits> shadow_sets;
+    vector<int> 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<const char*>(&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<uint64_t>(K));
+        write_u64(static_cast<uint64_t>(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<int> 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<uint64_t>(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<uint64_t>(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;
+    }
+}