From 4ac1673231be765e3fc84b4fb49aaf26444d2413 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 01:33:54 -0700 Subject: [PATCH 01/37] Add generic kernel-checked game certificate theorem --- .../chomp-10x42/lean/KernelCertificate.lean | 104 ++++++++++++++++++ 1 file changed, 104 insertions(+) create mode 100644 proofs/chomp-10x42/lean/KernelCertificate.lean diff --git a/proofs/chomp-10x42/lean/KernelCertificate.lean b/proofs/chomp-10x42/lean/KernelCertificate.lean new file mode 100644 index 00000000..38124d95 --- /dev/null +++ b/proofs/chomp-10x42/lean/KernelCertificate.lean @@ -0,0 +1,104 @@ +import FormalConjectures.Util.ProblemImports + +/-! +# Kernel-checked finite game certificates + +This module defines proof objects for finite normal-play games and a generic theorem turning a +valid ranked certificate into an actual inductive outcome proof. The certificate producer is +untrusted: only the proof of `Certificate.ValidAt` is used. +-/ + +namespace ChompKernel + +/-- A finite proof that a state 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 state with a losing proof. Because this is an inductive type, every accepted +proof object is finite. -/ +inductive Outcome {S : Type} (Move : S → S → Prop) : S → Bool → Prop + | losing {s : S} (children : ∀ t, Move s t → Outcome Move t true) : Outcome Move s false + | winning {s t : S} (move : Move s t) (child : Outcome Move t false) : Outcome Move s true + +/-- A state has a kernel-checked losing proof. -/ +def IsLosing {S : Type} (Move : S → S → Prop) (s : S) : Prop := + Nonempty (Outcome Move s false) + +/-- A state has a kernel-checked winning proof. -/ +def IsWinning {S : Type} (Move : S → S → Prop) (s : S) : Prop := + Nonempty (Outcome Move s true) + +/-- A finite game presented by its children and a strictly decreasing natural-number rank. -/ +structure RankedGame (S : Type) [DecidableEq S] where + moves : S → Finset S + rank : S → ℕ + decreases : ∀ {s t : S}, t ∈ moves s → rank t < rank s + +namespace RankedGame + +variable {S : Type} [DecidableEq S] + +/-- The move relation represented by a ranked finite game. -/ +def Move (G : RankedGame S) (s t : S) : Prop := t ∈ G.moves s + +/-- An untrusted outcome labelling together with one proposed reply at winning states. -/ +structure Certificate (G : RankedGame S) where + label : S → Bool + reply : S → Option S + +namespace Certificate + +variable {G : RankedGame S} + +/-- Local certificate validity. + +* A losing-labelled node must have every legal child labelled winning. +* A winning-labelled node must name one legal losing-labelled reply. +-/ +def ValidAt (C : Certificate G) (s : S) : Prop := + match C.label s with + | false => ∀ t, t ∈ G.moves s → C.label t = true + | true => ∃ t, C.reply s = some t ∧ t ∈ G.moves s ∧ C.label t = false + +/-- A total valid ranked certificate yields genuine inductive outcome proofs. + +For the generated Chomp certificate, the total functions are implemented by a finite ranked +array plus an unreachable default. Closure of every losing node and the recorded reply at every +winning node ensure that the default is never used below a certified root. +-/ +theorem outcome_of_valid (C : Certificate G) (hvalid : ∀ s, C.ValidAt s) (s : S) : + Outcome G.Move s (C.label s) := by + refine (measure_wf G.rank).induction s ?_ + intro s ih + cases hs : C.label s with + | false => + have hv : ∀ t, t ∈ G.moves s → C.label t = true := by + simpa [ValidAt, hs] using hvalid s + rw [hs] + exact Outcome.losing (fun t hm => by + have ht := ih t (G.decreases hm) + simpa [hv t hm] using ht) + | true => + have hv : ∃ t, C.reply s = some t ∧ t ∈ G.moves s ∧ C.label t = false := by + simpa [ValidAt, hs] using hvalid s + obtain ⟨t, _, hm, htlabel⟩ := hv + rw [hs] + exact Outcome.winning hm (by + have ht := ih t (G.decreases hm) + simpa [htlabel] using ht) + +/-- A losing-labelled root of a valid certificate has a kernel-checked losing proof. -/ +theorem losing_of_valid (C : Certificate G) (hvalid : ∀ s, C.ValidAt s) {s : S} + (hs : C.label s = false) : IsLosing G.Move s := by + refine ⟨?_⟩ + simpa [hs] using C.outcome_of_valid hvalid s + +/-- A winning-labelled root of a valid certificate has a kernel-checked winning proof. -/ +theorem winning_of_valid (C : Certificate G) (hvalid : ∀ s, C.ValidAt s) {s : S} + (hs : C.label s = true) : IsWinning G.Move s := by + refine ⟨?_⟩ + simpa [hs] using C.outcome_of_valid hvalid s + +end Certificate +end RankedGame + +end ChompKernel From 84e0cda15256b6835755336dae028767e8cb1814 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 01:34:21 -0700 Subject: [PATCH 02/37] Audit generic Chomp kernel certificate theorem --- .../oeis-a147983-chomp-lean-audit.yml | 41 ++++++++++--------- 1 file changed, 22 insertions(+), 19 deletions(-) diff --git a/.github/workflows/oeis-a147983-chomp-lean-audit.yml b/.github/workflows/oeis-a147983-chomp-lean-audit.yml index c7f6ff17..376ce907 100644 --- a/.github/workflows/oeis-a147983-chomp-lean-audit.yml +++ b/.github/workflows/oeis-a147983-chomp-lean-audit.yml @@ -5,6 +5,7 @@ on: branches: [main] paths: - '.github/workflows/oeis-a147983-chomp-lean-audit.yml' + - 'proofs/chomp-10x42/lean/**' workflow_dispatch: permissions: @@ -19,15 +20,21 @@ jobs: runs-on: ubuntu-latest timeout-minutes: 30 steps: + - name: Checkout ProofPlaygrond proof sources + uses: actions/checkout@v4 + with: + path: playground + - name: Checkout immutable DTD source commit uses: actions/checkout@v4 with: repository: DomTheDeveloper/formal-conjectures ref: 5fa4e5d2f63eefdba1b001cdce5d44c2ec8cabda + 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)" = "5fa4e5d2f63eefdba1b001cdce5d44c2ec8cabda" - name: Install pinned Lean toolchain shell: bash @@ -40,32 +47,28 @@ jobs: - name: Fetch Mathlib cache shell: bash + working-directory: formal-conjectures run: | set -euo pipefail lake exe cache get - - name: Compile exact Chomp module + - name: Compile exact 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 - - name: Audit kernel-checkable helper declarations + - name: Compile kernel certificate theorem 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 + lake lean ChompKernelCertificate.lean 2>&1 | tee chomp-kernel-certificate.log + if grep -nE '\b(sorry|admit)\b|native_decide|unsafe|^axiom\b|Lean\.trustCompiler|Lean\.ofReduce|Lean\.ofReduceBool' \ + ChompKernelCertificate.lean chomp-kernel-certificate.log; then + echo 'Forbidden placeholder or trust escape in kernel certificate development.' >&2 exit 1 fi @@ -73,8 +76,8 @@ 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 if-no-files-found: warn From ce8e0eedf52cd97800becccc6a8c715d110a3c3f Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 01:35:56 -0700 Subject: [PATCH 03/37] Audit axioms of generic certificate theorem --- proofs/chomp-10x42/lean/KernelCertificate.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/proofs/chomp-10x42/lean/KernelCertificate.lean b/proofs/chomp-10x42/lean/KernelCertificate.lean index 38124d95..ce67e135 100644 --- a/proofs/chomp-10x42/lean/KernelCertificate.lean +++ b/proofs/chomp-10x42/lean/KernelCertificate.lean @@ -101,4 +101,8 @@ theorem winning_of_valid (C : Certificate G) (hvalid : ∀ s, C.ValidAt s) {s : 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 From 8cf79cf3bf24c3ee750bcdaf3328fdfe513a52fc Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 01:37:53 -0700 Subject: [PATCH 04/37] Add exact losing-position rank exporter --- proofs/chomp-10x42/chomp_export_p_ranks.cpp | 206 ++++++++++++++++++++ 1 file changed, 206 insertions(+) create mode 100644 proofs/chomp-10x42/chomp_export_p_ranks.cpp 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; + } +} From 3795f9c0ca53fdfdda41f71bf9d8c81d66b049fc Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 01:38:18 -0700 Subject: [PATCH 05/37] Add shared proof-DAG extractor and feasibility meter --- proofs/chomp-10x42/chomp_proof_dag.cpp | 237 +++++++++++++++++++++++++ 1 file changed, 237 insertions(+) create mode 100644 proofs/chomp-10x42/chomp_proof_dag.cpp 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; + } +} From c3525420af4b431a59d7ef08df397f9e7e30c1c7 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 01:39:01 -0700 Subject: [PATCH 06/37] Measure Chomp kernel proof-DAG feasibility --- .github/workflows/chomp-10x42-audit.yml | 94 ++++++++++++++----------- 1 file changed, 52 insertions(+), 42 deletions(-) diff --git a/.github/workflows/chomp-10x42-audit.yml b/.github/workflows/chomp-10x42-audit.yml index 1aeb31ba..f7db81ea 100644 --- a/.github/workflows/chomp-10x42-audit.yml +++ b/.github/workflows/chomp-10x42-audit.yml @@ -1,4 +1,4 @@ -name: Chomp 10x42 exact audit +name: Chomp 10x42 kernel certificate feasibility on: pull_request: @@ -12,75 +12,85 @@ permissions: contents: read concurrency: - group: chomp-10x42-${{ github.event.pull_request.number || github.ref }} + group: chomp-10x42-kernel-${{ github.event.pull_request.number || github.ref }} cancel-in-progress: true jobs: - exact-audit: + certificate-feasibility: runs-on: ubuntu-latest - timeout-minutes: 30 + timeout-minutes: 90 defaults: run: working-directory: proofs/chomp-10x42 steps: - uses: actions/checkout@v4 - - name: Build both corrected exact solvers + - name: Build exact exporter and proof-DAG extractor run: | set -euo pipefail g++ -std=c++17 -O3 -march=native -DNDEBUG -Wall -Wextra -Wpedantic \ - chomp_three_openings.cpp -o chomp_scalar + chomp_export_p_ranks.cpp -o chomp_export_p_ranks g++ -std=c++17 -O3 -march=native -DNDEBUG -Wall -Wextra -Wpedantic \ - chomp_three_openings_fast.cpp -o chomp_fast + chomp_proof_dag.cpp -o chomp_proof_dag - - name: Run complete small-state-space cross-check + - name: Complete small certificate regression run: | set -euo pipefail - python3 bruteforce_crosscheck.py ./chomp_scalar | tee small-crosscheck.log - grep -F 'ALL SMALL EXACT CROSS-CHECKS PASSED' small-crosscheck.log + ./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 - - name: Reproduce published 6x13 regression + - name: Export complete 10x42 P-rank database run: | set -euo pipefail - ./chomp_scalar 6 13 > regression.out 2> regression.err - grep -F '6x13 openings=2' regression.out - grep -F '(13,13,13,11,11,11)' regression.out - grep -F '(13,13,13,13,8,8)' regression.out - grep -F 'max=2 P=895 prefixes=8567' regression.out + /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 - - name: Run complete corrected scalar computation + - name: Measure shared proof DAG up to two million nodes run: | set -euo pipefail - /usr/bin/time -v ./chomp_scalar 10 42 > scalar.out 2> scalar.err + 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 - - name: Run complete corrected bit-window computation - run: | - set -euo pipefail - /usr/bin/time -v ./chomp_fast 10 42 > fast.out 2> fast.err - - - name: Compare full outputs and exact target + - name: Write feasibility summary + if: always() run: | - set -euo pipefail - cmp scalar.out fast.out - grep -F '10x42 openings=3' scalar.out - grep -F '(42,42,42,42,35,35,35,35,35,35)' scalar.out - grep -F '(42,42,42,42,42,42,29,29,29,29)' scalar.out - grep -F '(42,42,42,42,42,42,42,25,25,25)' scalar.out - grep -F 'max=3 P=107342138 prefixes=3042311754' scalar.out - grep -F 'FOUND at width 42' scalar.err - grep -F 'FOUND at width 42' fast.err + { + echo '# Chomp 10x42 kernel-certificate feasibility' + echo + echo '## Full P database' + tail -n 20 p10x42-export.log 2>/dev/null || true + echo + echo '## Shared proof DAG' + cat p10x42-dag.out 2>/dev/null || true + tail -n 30 p10x42-dag.log 2>/dev/null || true + } | tee certificate-feasibility.md - - name: Upload exact transcripts + - name: Upload feasibility report if: always() uses: actions/upload-artifact@v4 with: - name: chomp-10x42-exact-audit + name: chomp-10x42-kernel-certificate-feasibility path: | - proofs/chomp-10x42/small-crosscheck.log - proofs/chomp-10x42/regression.out - proofs/chomp-10x42/regression.err - proofs/chomp-10x42/scalar.out - proofs/chomp-10x42/scalar.err - proofs/chomp-10x42/fast.out - proofs/chomp-10x42/fast.err + proofs/chomp-10x42/certificate-feasibility.md + proofs/chomp-10x42/p4x10-export.log + proofs/chomp-10x42/p4x10-dag.log + proofs/chomp-10x42/p10x42-export.out + proofs/chomp-10x42/p10x42-export.log + proofs/chomp-10x42/p10x42-dag.out + proofs/chomp-10x42/p10x42-dag.log if-no-files-found: warn From d81aa821d9cf67ff300df39951d7579c2b511e59 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 01:40:15 -0700 Subject: [PATCH 07/37] Add reproducible kernel certificate feasibility audit --- proofs/chomp-10x42/run_kernel_feasibility.sh | 42 ++++++++++++++++++++ 1 file changed, 42 insertions(+) create mode 100644 proofs/chomp-10x42/run_kernel_feasibility.sh diff --git a/proofs/chomp-10x42/run_kernel_feasibility.sh b/proofs/chomp-10x42/run_kernel_feasibility.sh new file mode 100644 index 00000000..91310186 --- /dev/null +++ b/proofs/chomp-10x42/run_kernel_feasibility.sh @@ -0,0 +1,42 @@ +#!/usr/bin/env bash +set -euo pipefail + +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 From a412aca785b13b401a6f69ebd385a610d0ddc477 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 01:42:07 -0700 Subject: [PATCH 08/37] Trigger installed Chomp kernel feasibility audit --- proofs/chomp-10x42/run_kernel_feasibility.sh | 2 ++ 1 file changed, 2 insertions(+) diff --git a/proofs/chomp-10x42/run_kernel_feasibility.sh b/proofs/chomp-10x42/run_kernel_feasibility.sh index 91310186..c6c0e33d 100644 --- a/proofs/chomp-10x42/run_kernel_feasibility.sh +++ b/proofs/chomp-10x42/run_kernel_feasibility.sh @@ -1,6 +1,8 @@ #!/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 \ From 3ecb3ec28b52fc898fdc90b1235b2ecf3e268b90 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 01:43:24 -0700 Subject: [PATCH 09/37] Keep existing exact audit unchanged --- .github/workflows/chomp-10x42-audit.yml | 94 +++++++++++-------------- 1 file changed, 42 insertions(+), 52 deletions(-) diff --git a/.github/workflows/chomp-10x42-audit.yml b/.github/workflows/chomp-10x42-audit.yml index f7db81ea..1aeb31ba 100644 --- a/.github/workflows/chomp-10x42-audit.yml +++ b/.github/workflows/chomp-10x42-audit.yml @@ -1,4 +1,4 @@ -name: Chomp 10x42 kernel certificate feasibility +name: Chomp 10x42 exact audit on: pull_request: @@ -12,85 +12,75 @@ permissions: contents: read concurrency: - group: chomp-10x42-kernel-${{ github.event.pull_request.number || github.ref }} + group: chomp-10x42-${{ github.event.pull_request.number || github.ref }} cancel-in-progress: true jobs: - certificate-feasibility: + exact-audit: runs-on: ubuntu-latest - timeout-minutes: 90 + timeout-minutes: 30 defaults: run: working-directory: proofs/chomp-10x42 steps: - uses: actions/checkout@v4 - - name: Build exact exporter and proof-DAG extractor + - name: Build both corrected exact solvers run: | set -euo pipefail g++ -std=c++17 -O3 -march=native -DNDEBUG -Wall -Wextra -Wpedantic \ - chomp_export_p_ranks.cpp -o chomp_export_p_ranks + chomp_three_openings.cpp -o chomp_scalar g++ -std=c++17 -O3 -march=native -DNDEBUG -Wall -Wextra -Wpedantic \ - chomp_proof_dag.cpp -o chomp_proof_dag + chomp_three_openings_fast.cpp -o chomp_fast - - name: Complete small certificate regression + - name: Run complete small-state-space cross-check run: | set -euo pipefail - ./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 + python3 bruteforce_crosscheck.py ./chomp_scalar | tee small-crosscheck.log + grep -F 'ALL SMALL EXACT CROSS-CHECKS PASSED' small-crosscheck.log - - name: Export complete 10x42 P-rank database + - name: Reproduce published 6x13 regression run: | set -euo pipefail - /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 + ./chomp_scalar 6 13 > regression.out 2> regression.err + grep -F '6x13 openings=2' regression.out + grep -F '(13,13,13,11,11,11)' regression.out + grep -F '(13,13,13,13,8,8)' regression.out + grep -F 'max=2 P=895 prefixes=8567' regression.out - - name: Measure shared proof DAG up to two million nodes + - name: Run complete corrected scalar computation run: | set -euo pipefail - 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 + /usr/bin/time -v ./chomp_scalar 10 42 > scalar.out 2> scalar.err - - name: Write feasibility summary - if: always() + - name: Run complete corrected bit-window computation run: | - { - echo '# Chomp 10x42 kernel-certificate feasibility' - echo - echo '## Full P database' - tail -n 20 p10x42-export.log 2>/dev/null || true - echo - echo '## Shared proof DAG' - cat p10x42-dag.out 2>/dev/null || true - tail -n 30 p10x42-dag.log 2>/dev/null || true - } | tee certificate-feasibility.md + set -euo pipefail + /usr/bin/time -v ./chomp_fast 10 42 > fast.out 2> fast.err + + - name: Compare full outputs and exact target + run: | + set -euo pipefail + cmp scalar.out fast.out + grep -F '10x42 openings=3' scalar.out + grep -F '(42,42,42,42,35,35,35,35,35,35)' scalar.out + grep -F '(42,42,42,42,42,42,29,29,29,29)' scalar.out + grep -F '(42,42,42,42,42,42,42,25,25,25)' scalar.out + grep -F 'max=3 P=107342138 prefixes=3042311754' scalar.out + grep -F 'FOUND at width 42' scalar.err + grep -F 'FOUND at width 42' fast.err - - name: Upload feasibility report + - name: Upload exact transcripts if: always() uses: actions/upload-artifact@v4 with: - name: chomp-10x42-kernel-certificate-feasibility + name: chomp-10x42-exact-audit path: | - proofs/chomp-10x42/certificate-feasibility.md - proofs/chomp-10x42/p4x10-export.log - proofs/chomp-10x42/p4x10-dag.log - proofs/chomp-10x42/p10x42-export.out - proofs/chomp-10x42/p10x42-export.log - proofs/chomp-10x42/p10x42-dag.out - proofs/chomp-10x42/p10x42-dag.log + proofs/chomp-10x42/small-crosscheck.log + proofs/chomp-10x42/regression.out + proofs/chomp-10x42/regression.err + proofs/chomp-10x42/scalar.out + proofs/chomp-10x42/scalar.err + proofs/chomp-10x42/fast.out + proofs/chomp-10x42/fast.err if-no-files-found: warn From a2f89251d9f541195d4916f8efb2822df3115cbe Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 01:58:41 -0700 Subject: [PATCH 10/37] Strengthen finite game certificate with exact closure --- .../chomp-10x42/lean/KernelCertificate.lean | 142 +++++++++--------- 1 file changed, 73 insertions(+), 69 deletions(-) diff --git a/proofs/chomp-10x42/lean/KernelCertificate.lean b/proofs/chomp-10x42/lean/KernelCertificate.lean index ce67e135..59d93288 100644 --- a/proofs/chomp-10x42/lean/KernelCertificate.lean +++ b/proofs/chomp-10x42/lean/KernelCertificate.lean @@ -3,100 +3,104 @@ import FormalConjectures.Util.ProblemImports /-! # Kernel-checked finite game certificates -This module defines proof objects for finite normal-play games and a generic theorem turning a -valid ranked certificate into an actual inductive outcome proof. The certificate producer is -untrusted: only the proof of `Certificate.ValidAt` is used. +The certificate producer is untrusted. A certificate contains a finite collection of nodes, +an interpretation of each node as an actual game position, and proofs that its edge lists are +sound and complete for the real move relation. Lean reconstructs the normal-play outcome proof +by well-founded induction on a strictly decreasing rank. -/ namespace ChompKernel -/-- A finite proof that a state is losing (`false`) or winning (`true`). +/-- 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 state with a losing proof. Because this is an inductive type, every accepted -proof object is finite. -/ -inductive Outcome {S : Type} (Move : S → S → Prop) : S → Bool → Prop - | losing {s : S} (children : ∀ t, Move s t → Outcome Move t true) : Outcome Move s false - | winning {s t : S} (move : Move s t) (child : Outcome Move t false) : Outcome Move s true - -/-- A state has a kernel-checked losing proof. -/ -def IsLosing {S : Type} (Move : S → S → Prop) (s : S) : Prop := - Nonempty (Outcome Move s false) - -/-- A state has a kernel-checked winning proof. -/ -def IsWinning {S : Type} (Move : S → S → Prop) (s : S) : Prop := - Nonempty (Outcome Move s true) - -/-- A finite game presented by its children and a strictly decreasing natural-number rank. -/ -structure RankedGame (S : Type) [DecidableEq S] where - moves : S → Finset S - rank : S → ℕ - decreases : ∀ {s t : S}, t ∈ moves s → rank t < rank s +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 -namespace RankedGame +/-- A position has a kernel-checked losing proof. -/ +def IsLosing {P : Type} (Move : P → P → Prop) (p : P) : Prop := + Nonempty (Outcome Move p false) -variable {S : Type} [DecidableEq S] +/-- A position has a kernel-checked winning proof. -/ +def IsWinning {P : Type} (Move : P → P → Prop) (p : P) : Prop := + Nonempty (Outcome Move p true) -/-- The move relation represented by a ranked finite game. -/ -def Move (G : RankedGame S) (s t : S) : Prop := t ∈ G.moves s +/-- 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 -/-- An untrusted outcome labelling together with one proposed reply at winning states. -/ -structure Certificate (G : RankedGame S) where - label : S → Bool - reply : S → Option S +namespace RankedGame -namespace Certificate +variable {P : Type} {G : RankedGame P} {n : ℕ} -variable {G : RankedGame S} +/-- A finite, interpreted game certificate. -/-- Local certificate validity. +`children` is not trusted data by itself. `children_sound` and `children_complete` prove that +it lists exactly all real legal moves from every interpreted certificate node. -/ +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) + children_complete : ∀ (i : Fin n) (q : P), G.Move (pos i) q → + ∃ j, j ∈ children i ∧ pos j = q -* A losing-labelled node must have every legal child labelled winning. -* A winning-labelled node must name one legal losing-labelled reply. --/ -def ValidAt (C : Certificate G) (s : S) : Prop := - match C.label s with - | false => ∀ t, t ∈ G.moves s → C.label t = true - | true => ∃ t, C.reply s = some t ∧ t ∈ G.moves s ∧ C.label t = false +namespace Certificate -/-- A total valid ranked certificate yields genuine inductive outcome proofs. +/-- Local outcome-label validity. -For the generated Chomp certificate, the total functions are implemented by a finite ranked -array plus an unreachable default. Closure of every losing node and the recorded reply at every -winning node ensure that the default is never used below a certified root. +* Every child of a losing-labelled node is labelled winning. +* Every winning-labelled node names a legal child labelled losing. -/ -theorem outcome_of_valid (C : Certificate G) (hvalid : ∀ s, C.ValidAt s) (s : S) : - Outcome G.Move s (C.label s) := by - refine (measure_wf G.rank).induction s ?_ - intro s ih - cases hs : C.label s with +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. + +The key point is `children_complete`: at a losing node, an arbitrary real legal move is mapped +back to a certificate node before the induction hypothesis is used. No default labels or +unrepresented positions are trusted. -/ +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 + refine (measure_wf (fun i ↦ G.rank (C.pos i))).induction i ?_ + intro i ih + cases hi : C.label i with | false => - have hv : ∀ t, t ∈ G.moves s → C.label t = true := by - simpa [ValidAt, hs] using hvalid s - rw [hs] - exact Outcome.losing (fun t hm => by - have ht := ih t (G.decreases hm) - simpa [hv t hm] using ht) + have hv : ∀ j, j ∈ C.children i → C.label j = true := by + simpa [ValidAt, hi] using hvalid i + rw [hi] + exact Outcome.losing (fun q hq ↦ by + obtain ⟨j, hj, hpos⟩ := C.children_complete i q hq + subst q + have hout := ih j (G.decreases (C.children_sound hj)) + simpa [hv j hj] using hout) | true => - have hv : ∃ t, C.reply s = some t ∧ t ∈ G.moves s ∧ C.label t = false := by - simpa [ValidAt, hs] using hvalid s - obtain ⟨t, _, hm, htlabel⟩ := hv - rw [hs] - exact Outcome.winning hm (by - have ht := ih t (G.decreases hm) - simpa [htlabel] using ht) + 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 + rw [hi] + exact Outcome.winning (C.children_sound hj) (by + have hout := ih j (G.decreases (C.children_sound hj)) + simpa [hlabel] using hout) /-- A losing-labelled root of a valid certificate has a kernel-checked losing proof. -/ -theorem losing_of_valid (C : Certificate G) (hvalid : ∀ s, C.ValidAt s) {s : S} - (hs : C.label s = false) : IsLosing G.Move s := by +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 [hs] using C.outcome_of_valid hvalid s + 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) (hvalid : ∀ s, C.ValidAt s) {s : S} - (hs : C.label s = true) : IsWinning G.Move s := by +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 [hs] using C.outcome_of_valid hvalid s + simpa [hi] using C.outcome_of_valid hvalid i end Certificate end RankedGame From a541615dfeee1819ada5e9335c0b511bc600d94f Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 02:05:56 -0700 Subject: [PATCH 11/37] Require closure only where the losing rule needs it --- .../chomp-10x42/lean/KernelCertificate.lean | 28 +++++++++---------- 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/proofs/chomp-10x42/lean/KernelCertificate.lean b/proofs/chomp-10x42/lean/KernelCertificate.lean index 59d93288..882e8f34 100644 --- a/proofs/chomp-10x42/lean/KernelCertificate.lean +++ b/proofs/chomp-10x42/lean/KernelCertificate.lean @@ -3,17 +3,17 @@ import FormalConjectures.Util.ProblemImports /-! # Kernel-checked finite game certificates -The certificate producer is untrusted. A certificate contains a finite collection of nodes, -an interpretation of each node as an actual game position, and proofs that its edge lists are -sound and complete for the real move relation. Lean reconstructs the normal-play outcome proof -by well-founded induction on a strictly decreasing rank. +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 well-founded 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 +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 @@ -39,23 +39,24 @@ variable {P : Type} {G : RankedGame P} {n : ℕ} /-- A finite, interpreted game certificate. -`children` is not trusted data by itself. `children_sound` and `children_complete` prove that -it lists exactly all real legal moves from every interpreted certificate node. -/ +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) - children_complete : ∀ (i : Fin n) (q : P), G.Move (pos i) q → + 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 child of a losing-labelled node is labelled winning. -* Every winning-labelled node names a legal child labelled losing. +* 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 @@ -64,9 +65,8 @@ def ValidAt (C : Certificate G n) (i : Fin n) : Prop := /-- A valid finite interpreted certificate yields genuine outcome proofs for the actual game. -The key point is `children_complete`: at a losing node, an arbitrary real legal move is mapped -back to a certificate node before the induction hypothesis is used. No default labels or -unrepresented positions are trusted. -/ +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 refine (measure_wf (fun i ↦ G.rank (C.pos i))).induction i ?_ @@ -77,7 +77,7 @@ theorem outcome_of_valid (C : Certificate G n) (hvalid : ∀ i, C.ValidAt i) (i simpa [ValidAt, hi] using hvalid i rw [hi] exact Outcome.losing (fun q hq ↦ by - obtain ⟨j, hj, hpos⟩ := C.children_complete i q hq + obtain ⟨j, hj, hpos⟩ := C.losing_complete i hi q hq subst q have hout := ih j (G.decreases (C.children_sound hj)) simpa [hv j hj] using hout) From 7e9e7ae222c074f0455b46b5ff97bddcf51e3797 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 02:12:31 -0700 Subject: [PATCH 12/37] Repair rank induction in Chomp kernel certificate --- .../chomp-10x42/lean/KernelCertificate.lean | 67 +++++++++++++------ 1 file changed, 46 insertions(+), 21 deletions(-) diff --git a/proofs/chomp-10x42/lean/KernelCertificate.lean b/proofs/chomp-10x42/lean/KernelCertificate.lean index 882e8f34..6235078d 100644 --- a/proofs/chomp-10x42/lean/KernelCertificate.lean +++ b/proofs/chomp-10x42/lean/KernelCertificate.lean @@ -1,3 +1,19 @@ +/- +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.Util.ProblemImports /-! @@ -6,7 +22,7 @@ import FormalConjectures.Util.ProblemImports 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 well-founded induction on a decreasing rank. +Lean reconstructs the normal-play outcome proof by strong induction on a decreasing rank. -/ namespace ChompKernel @@ -69,26 +85,35 @@ An arbitrary real move from a losing node is brought into the finite certificate `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 - refine (measure_wf (fun i ↦ G.rank (C.pos i))).induction i ?_ - intro i ih - 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 - rw [hi] - exact Outcome.losing (fun q hq ↦ by - obtain ⟨j, hj, hpos⟩ := C.losing_complete i hi q hq - subst q - have hout := ih j (G.decreases (C.children_sound hj)) - 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 - rw [hi] - exact Outcome.winning (C.children_sound hj) (by - have hout := ih j (G.decreases (C.children_sound hj)) - simpa [hlabel] using hout) + 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 + rw [hi] + 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 + rw [hi] + 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} From 5ba5a551723facadc5989586b798ec64c0c902e1 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 02:26:04 -0700 Subject: [PATCH 13/37] Remove redundant label rewrites in certificate induction --- proofs/chomp-10x42/lean/KernelCertificate.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/proofs/chomp-10x42/lean/KernelCertificate.lean b/proofs/chomp-10x42/lean/KernelCertificate.lean index 6235078d..8c8ee749 100644 --- a/proofs/chomp-10x42/lean/KernelCertificate.lean +++ b/proofs/chomp-10x42/lean/KernelCertificate.lean @@ -95,7 +95,6 @@ theorem outcome_of_valid (C : Certificate G n) (hvalid : ∀ i, C.ValidAt i) (i | false => have hv : ∀ j, j ∈ C.children i → C.label j = true := by simpa [ValidAt, hi] using hvalid i - rw [hi] exact Outcome.losing (fun q hq ↦ by obtain ⟨j, hj, hpos⟩ := C.losing_complete i hi q hq subst q @@ -107,7 +106,6 @@ theorem outcome_of_valid (C : Certificate G n) (hvalid : ∀ i, C.ValidAt i) (i 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 - rw [hi] 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) From baa922a5298e962c632ab93ef4666b8906ebf390 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 02:27:10 -0700 Subject: [PATCH 14/37] Prove every legal Chomp move decreases area --- proofs/chomp-10x42/lean/ChompRank.lean | 74 ++++++++++++++++++++++++++ 1 file changed, 74 insertions(+) create mode 100644 proofs/chomp-10x42/lean/ChompRank.lean 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 From 2da8a4afb51122f8ad10b65b9e48be963b56caa9 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 02:27:36 -0700 Subject: [PATCH 15/37] Audit Chomp rank proof against canonical DTD branch --- .../oeis-a147983-chomp-lean-audit.yml | 18 +++++++++++------- 1 file changed, 11 insertions(+), 7 deletions(-) diff --git a/.github/workflows/oeis-a147983-chomp-lean-audit.yml b/.github/workflows/oeis-a147983-chomp-lean-audit.yml index 376ce907..4478487e 100644 --- a/.github/workflows/oeis-a147983-chomp-lean-audit.yml +++ b/.github/workflows/oeis-a147983-chomp-lean-audit.yml @@ -25,16 +25,16 @@ jobs: with: path: playground - - name: Checkout immutable DTD source commit + - 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 DTD source shell: bash - run: test "$(git -C formal-conjectures rev-parse HEAD)" = "5fa4e5d2f63eefdba1b001cdce5d44c2ec8cabda" + run: test "$(git -C formal-conjectures rev-parse HEAD)" = "9242e34d74bea32655e840a5e8637377de1431e4" - name: Install pinned Lean toolchain shell: bash @@ -52,22 +52,25 @@ jobs: set -euo pipefail lake exe cache get - - name: Compile exact Chomp catalog 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 - - name: Compile kernel certificate theorem + - name: Compile kernel certificate and Chomp rank theorems shell: bash working-directory: formal-conjectures run: | set -euo pipefail cp ../playground/proofs/chomp-10x42/lean/KernelCertificate.lean ./ChompKernelCertificate.lean + cp ../playground/proofs/chomp-10x42/lean/ChompRank.lean ./ChompRank.lean lake lean ChompKernelCertificate.lean 2>&1 | tee chomp-kernel-certificate.log - if grep -nE '\b(sorry|admit)\b|native_decide|unsafe|^axiom\b|Lean\.trustCompiler|Lean\.ofReduce|Lean\.ofReduceBool' \ - ChompKernelCertificate.lean chomp-kernel-certificate.log; then + lake lean ChompRank.lean 2>&1 | tee chomp-rank.log + if grep -nE '\b(sorry|admit)\b|native_decide|unsafe|^axiom\b|Lean\.trustCompiler|Lean\.ofReduce|Lean\.ofReduceBool|sorryAx' \ + ChompKernelCertificate.lean ChompRank.lean \ + chomp-kernel-certificate.log chomp-rank.log; then echo 'Forbidden placeholder or trust escape in kernel certificate development.' >&2 exit 1 fi @@ -80,4 +83,5 @@ jobs: path: | formal-conjectures/chomp-a147983-lean.log formal-conjectures/chomp-kernel-certificate.log + formal-conjectures/chomp-rank.log if-no-files-found: warn From d1f28c2e2f0dfc6f35acfd5da3732d6e83d68d6e Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 02:28:10 -0700 Subject: [PATCH 16/37] Add exact MDD compressor for Chomp P-set --- proofs/chomp-10x42/chomp_p_mdd.cpp | 248 +++++++++++++++++++++++++++++ 1 file changed, 248 insertions(+) create mode 100644 proofs/chomp-10x42/chomp_p_mdd.cpp 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; + } +} From 785406afa3756e4d1e0e02370436b93f36cbff1f Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 02:28:27 -0700 Subject: [PATCH 17/37] Record exact Chomp P-set MDD compression measurement --- proofs/chomp-10x42/MDD_COMPRESSION_REPORT.md | 51 ++++++++++++++++++++ 1 file changed, 51 insertions(+) create mode 100644 proofs/chomp-10x42/MDD_COMPRESSION_REPORT.md 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. From fda0bea8f57a2127bcccd787ff69decb0a9bbb55 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 02:29:55 -0700 Subject: [PATCH 18/37] Add kernel theorems for symbolic MDD language certificates --- proofs/chomp-10x42/lean/MDDCertificate.lean | 139 ++++++++++++++++++++ 1 file changed, 139 insertions(+) create mode 100644 proofs/chomp-10x42/lean/MDDCertificate.lean diff --git a/proofs/chomp-10x42/lean/MDDCertificate.lean b/proofs/chomp-10x42/lean/MDDCertificate.lean new file mode 100644 index 00000000..23c256d2 --- /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 FormalConjectures.Util.ProblemImports + +/-! +# 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 From b418a09345b90cc8b84bb6f397b4fd26844ddf84 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 02:30:16 -0700 Subject: [PATCH 19/37] Audit symbolic MDD certificate theorems --- .github/workflows/oeis-a147983-chomp-lean-audit.yml | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/.github/workflows/oeis-a147983-chomp-lean-audit.yml b/.github/workflows/oeis-a147983-chomp-lean-audit.yml index 4478487e..75f93ccc 100644 --- a/.github/workflows/oeis-a147983-chomp-lean-audit.yml +++ b/.github/workflows/oeis-a147983-chomp-lean-audit.yml @@ -59,18 +59,20 @@ jobs: set -euo pipefail lake lean FormalConjectures/OEIS/147983.lean 2>&1 | tee chomp-a147983-lean.log - - name: Compile kernel certificate and Chomp rank theorems + - name: Compile pure kernel theorem layers shell: bash working-directory: formal-conjectures run: | set -euo pipefail cp ../playground/proofs/chomp-10x42/lean/KernelCertificate.lean ./ChompKernelCertificate.lean + cp ../playground/proofs/chomp-10x42/lean/MDDCertificate.lean ./ChompMDDCertificate.lean cp ../playground/proofs/chomp-10x42/lean/ChompRank.lean ./ChompRank.lean lake lean ChompKernelCertificate.lean 2>&1 | tee chomp-kernel-certificate.log + lake lean ChompMDDCertificate.lean 2>&1 | tee chomp-mdd-certificate.log lake lean ChompRank.lean 2>&1 | tee chomp-rank.log if grep -nE '\b(sorry|admit)\b|native_decide|unsafe|^axiom\b|Lean\.trustCompiler|Lean\.ofReduce|Lean\.ofReduceBool|sorryAx' \ - ChompKernelCertificate.lean ChompRank.lean \ - chomp-kernel-certificate.log chomp-rank.log; then + ChompKernelCertificate.lean ChompMDDCertificate.lean ChompRank.lean \ + chomp-kernel-certificate.log chomp-mdd-certificate.log chomp-rank.log; then echo 'Forbidden placeholder or trust escape in kernel certificate development.' >&2 exit 1 fi @@ -83,5 +85,6 @@ jobs: path: | formal-conjectures/chomp-a147983-lean.log formal-conjectures/chomp-kernel-certificate.log + formal-conjectures/chomp-mdd-certificate.log formal-conjectures/chomp-rank.log if-no-files-found: warn From 947a6374647fd6f87a1ac6e944eb5144714e999e Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 02:30:40 -0700 Subject: [PATCH 20/37] Add generic kernel theorem from a certified P-set --- proofs/chomp-10x42/lean/KernelPSet.lean | 85 +++++++++++++++++++++++++ 1 file changed, 85 insertions(+) create mode 100644 proofs/chomp-10x42/lean/KernelPSet.lean diff --git a/proofs/chomp-10x42/lean/KernelPSet.lean b/proofs/chomp-10x42/lean/KernelPSet.lean new file mode 100644 index 00000000..66d1ca8c --- /dev/null +++ b/proofs/chomp-10x42/lean/KernelPSet.lean @@ -0,0 +1,85 @@ +/- +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 + +/-! +# A certified P-set gives 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. + +This file turns those two symbolic facts into the inductive kernel proof objects used by the +Chomp formalization. +-/ + +namespace ChompKernel +namespace RankedGame + +variable {P : Type} {G : RankedGame P} + +/-- A predicate satisfying the two P-position kernel 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 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 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⟩ + +#print axioms outcomes_of_pSet +#print axioms losing_of_pSet +#print axioms winning_of_not_pSet + +end RankedGame +end ChompKernel From 8e47eccdb2db227c35231410ee7ad4c21a3876bc Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 02:30:59 -0700 Subject: [PATCH 21/37] Audit certified P-set kernel theorem --- .github/workflows/oeis-a147983-chomp-lean-audit.yml | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/.github/workflows/oeis-a147983-chomp-lean-audit.yml b/.github/workflows/oeis-a147983-chomp-lean-audit.yml index 75f93ccc..1f64394c 100644 --- a/.github/workflows/oeis-a147983-chomp-lean-audit.yml +++ b/.github/workflows/oeis-a147983-chomp-lean-audit.yml @@ -65,14 +65,17 @@ jobs: run: | set -euo pipefail cp ../playground/proofs/chomp-10x42/lean/KernelCertificate.lean ./ChompKernelCertificate.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 lake lean ChompKernelCertificate.lean 2>&1 | tee chomp-kernel-certificate.log + lake lean ChompKernelPSet.lean 2>&1 | tee chomp-kernel-pset.log lake lean ChompMDDCertificate.lean 2>&1 | tee chomp-mdd-certificate.log lake lean ChompRank.lean 2>&1 | tee chomp-rank.log if grep -nE '\b(sorry|admit)\b|native_decide|unsafe|^axiom\b|Lean\.trustCompiler|Lean\.ofReduce|Lean\.ofReduceBool|sorryAx' \ - ChompKernelCertificate.lean ChompMDDCertificate.lean ChompRank.lean \ - chomp-kernel-certificate.log chomp-mdd-certificate.log chomp-rank.log; then + ChompKernelCertificate.lean ChompKernelPSet.lean ChompMDDCertificate.lean ChompRank.lean \ + chomp-kernel-certificate.log chomp-kernel-pset.log \ + chomp-mdd-certificate.log chomp-rank.log; then echo 'Forbidden placeholder or trust escape in kernel certificate development.' >&2 exit 1 fi @@ -85,6 +88,7 @@ jobs: path: | formal-conjectures/chomp-a147983-lean.log formal-conjectures/chomp-kernel-certificate.log + formal-conjectures/chomp-kernel-pset.log formal-conjectures/chomp-mdd-certificate.log formal-conjectures/chomp-rank.log if-no-files-found: warn From a9405e5ed55971bb46d79158681a013a4b8e37cc Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 02:33:00 -0700 Subject: [PATCH 22/37] Prove legal Chomp moves preserve valid positions --- proofs/chomp-10x42/lean/ChompPosition.lean | 93 ++++++++++++++++++++++ 1 file changed, 93 insertions(+) create mode 100644 proofs/chomp-10x42/lean/ChompPosition.lean diff --git a/proofs/chomp-10x42/lean/ChompPosition.lean b/proofs/chomp-10x42/lean/ChompPosition.lean new file mode 100644 index 00000000..69ca1802 --- /dev/null +++ b/proofs/chomp-10x42/lean/ChompPosition.lean @@ -0,0 +1,93 @@ +/- +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⟩ + +/-- 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 Ferrers inequalities. -/ +theorem bite_isFerrers (t : ℕ) : ∀ i : ℕ, ∀ {p : List ℕ}, + IsFerrers p → IsFerrers (bite i t p) + | 0, p, 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⟩ + +#print axioms cutSuffix_isFerrers +#print axioms bite_isFerrers +#print axioms bite_head_pos +#print axioms move_preserves_position + +end OeisA147983 From bbf24344f7f681a09ceb3b7640955ba2edff70ea Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 02:33:22 -0700 Subject: [PATCH 23/37] Audit Chomp position-preservation theorems --- .github/workflows/oeis-a147983-chomp-lean-audit.yml | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/.github/workflows/oeis-a147983-chomp-lean-audit.yml b/.github/workflows/oeis-a147983-chomp-lean-audit.yml index 1f64394c..f4d93148 100644 --- a/.github/workflows/oeis-a147983-chomp-lean-audit.yml +++ b/.github/workflows/oeis-a147983-chomp-lean-audit.yml @@ -68,14 +68,17 @@ jobs: 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 lake lean ChompKernelCertificate.lean 2>&1 | tee chomp-kernel-certificate.log lake lean ChompKernelPSet.lean 2>&1 | tee chomp-kernel-pset.log lake lean ChompMDDCertificate.lean 2>&1 | tee chomp-mdd-certificate.log lake lean ChompRank.lean 2>&1 | tee chomp-rank.log + lake lean ChompPosition.lean 2>&1 | tee chomp-position.log if grep -nE '\b(sorry|admit)\b|native_decide|unsafe|^axiom\b|Lean\.trustCompiler|Lean\.ofReduce|Lean\.ofReduceBool|sorryAx' \ - ChompKernelCertificate.lean ChompKernelPSet.lean ChompMDDCertificate.lean ChompRank.lean \ + ChompKernelCertificate.lean ChompKernelPSet.lean ChompMDDCertificate.lean \ + ChompRank.lean ChompPosition.lean \ chomp-kernel-certificate.log chomp-kernel-pset.log \ - chomp-mdd-certificate.log chomp-rank.log; then + chomp-mdd-certificate.log chomp-rank.log chomp-position.log; then echo 'Forbidden placeholder or trust escape in kernel certificate development.' >&2 exit 1 fi @@ -91,4 +94,5 @@ jobs: formal-conjectures/chomp-kernel-pset.log formal-conjectures/chomp-mdd-certificate.log formal-conjectures/chomp-rank.log + formal-conjectures/chomp-position.log if-no-files-found: warn From b6f588ee6af2a0c771003a52d2fe2d6b09d9ef28 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 02:35:36 -0700 Subject: [PATCH 24/37] Prove totality and exclusivity for ranked normal-play games --- proofs/chomp-10x42/lean/KernelGameTheory.lean | 103 ++++++++++++++++++ 1 file changed, 103 insertions(+) create mode 100644 proofs/chomp-10x42/lean/KernelGameTheory.lean 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 From 4743a858a1f6f8bf768552c6fbd70c8eafe7f091 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 02:35:59 -0700 Subject: [PATCH 25/37] Bridge kernel losing outcomes to catalog P-positions --- .../chomp-10x42/lean/ChompCatalogBridge.lean | 86 +++++++++++++++++++ 1 file changed, 86 insertions(+) create mode 100644 proofs/chomp-10x42/lean/ChompCatalogBridge.lean diff --git a/proofs/chomp-10x42/lean/ChompCatalogBridge.lean b/proofs/chomp-10x42/lean/ChompCatalogBridge.lean new file mode 100644 index 00000000..c7af9cc8 --- /dev/null +++ b/proofs/chomp-10x42/lean/ChompCatalogBridge.lean @@ -0,0 +1,86 @@ +/- +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 + +/-! +# 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 decide + +@[category test, AMS 5] +theorem child₂_is_position : IsPosition child₂ := by decide + +@[category test, AMS 5] +theorem child₃_is_position : IsPosition child₃ := by decide + +/-- 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₃ + +#print axioms kernelPSet_isPSet +#print axioms isPPosition_of_losing +#print axioms three_openings_of_losing + +end OeisA147983 From a5ba846f4be2e2bbadfbd0d5b9c72967ffb62286 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 02:36:21 -0700 Subject: [PATCH 26/37] Audit ranked-game determinacy and catalog bridge --- .../workflows/oeis-a147983-chomp-lean-audit.yml | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/.github/workflows/oeis-a147983-chomp-lean-audit.yml b/.github/workflows/oeis-a147983-chomp-lean-audit.yml index f4d93148..b254abf9 100644 --- a/.github/workflows/oeis-a147983-chomp-lean-audit.yml +++ b/.github/workflows/oeis-a147983-chomp-lean-audit.yml @@ -65,20 +65,24 @@ jobs: run: | set -euo pipefail 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 lake lean ChompKernelCertificate.lean 2>&1 | tee chomp-kernel-certificate.log + lake lean ChompKernelGameTheory.lean 2>&1 | tee chomp-kernel-game-theory.log lake lean ChompKernelPSet.lean 2>&1 | tee chomp-kernel-pset.log lake lean ChompMDDCertificate.lean 2>&1 | tee chomp-mdd-certificate.log lake lean ChompRank.lean 2>&1 | tee chomp-rank.log lake lean ChompPosition.lean 2>&1 | tee chomp-position.log + lake lean ChompCatalogBridge.lean 2>&1 | tee 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 ChompKernelPSet.lean ChompMDDCertificate.lean \ - ChompRank.lean ChompPosition.lean \ - chomp-kernel-certificate.log chomp-kernel-pset.log \ - chomp-mdd-certificate.log chomp-rank.log chomp-position.log; then + 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 @@ -91,8 +95,10 @@ jobs: path: | 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 From ac5494dc2c86c9eb2464b7422453fd735fa9155b Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 02:41:26 -0700 Subject: [PATCH 27/37] Use canonical Formal Conjectures imports --- proofs/chomp-10x42/lean/KernelCertificate.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/proofs/chomp-10x42/lean/KernelCertificate.lean b/proofs/chomp-10x42/lean/KernelCertificate.lean index 8c8ee749..adef4049 100644 --- a/proofs/chomp-10x42/lean/KernelCertificate.lean +++ b/proofs/chomp-10x42/lean/KernelCertificate.lean @@ -14,7 +14,7 @@ See the License for the specific language governing permissions and limitations under the License. -/ -import FormalConjectures.Util.ProblemImports +import FormalConjecturesUtil /-! # Kernel-checked finite game certificates From c80f98d938379e3803b06b039bde6a3b4b983e2a Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 02:41:45 -0700 Subject: [PATCH 28/37] Use canonical Formal Conjectures imports for MDD checker --- proofs/chomp-10x42/lean/MDDCertificate.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/proofs/chomp-10x42/lean/MDDCertificate.lean b/proofs/chomp-10x42/lean/MDDCertificate.lean index 23c256d2..e79d6e99 100644 --- a/proofs/chomp-10x42/lean/MDDCertificate.lean +++ b/proofs/chomp-10x42/lean/MDDCertificate.lean @@ -14,13 +14,13 @@ See the License for the specific language governing permissions and limitations under the License. -/ -import FormalConjectures.Util.ProblemImports +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 +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 @@ -30,7 +30,7 @@ proved in Lean. namespace ChompKernel namespace MDD -/-- A deterministic finite-state acceptor. Layering is not needed for semantic correctness; +/-- 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) From 4fedd8fd155cbb65b3f8f1305a5c1fe90f1107bd Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 02:50:46 -0700 Subject: [PATCH 29/37] Compile Chomp support modules onto Lean import path --- .../oeis-a147983-chomp-lean-audit.yml | 20 ++++++++++++------- 1 file changed, 13 insertions(+), 7 deletions(-) diff --git a/.github/workflows/oeis-a147983-chomp-lean-audit.yml b/.github/workflows/oeis-a147983-chomp-lean-audit.yml index b254abf9..cead148d 100644 --- a/.github/workflows/oeis-a147983-chomp-lean-audit.yml +++ b/.github/workflows/oeis-a147983-chomp-lean-audit.yml @@ -71,13 +71,19 @@ jobs: 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 - lake lean ChompKernelCertificate.lean 2>&1 | tee chomp-kernel-certificate.log - lake lean ChompKernelGameTheory.lean 2>&1 | tee chomp-kernel-game-theory.log - lake lean ChompKernelPSet.lean 2>&1 | tee chomp-kernel-pset.log - lake lean ChompMDDCertificate.lean 2>&1 | tee chomp-mdd-certificate.log - lake lean ChompRank.lean 2>&1 | tee chomp-rank.log - lake lean ChompPosition.lean 2>&1 | tee chomp-position.log - lake lean ChompCatalogBridge.lean 2>&1 | tee chomp-catalog-bridge.log + 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 \ From ba12b9bd4814ce228514dbbd4d250c3b457da96f Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 02:57:49 -0700 Subject: [PATCH 30/37] Emit canonical Chomp catalog olean for support modules --- .github/workflows/oeis-a147983-chomp-lean-audit.yml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/.github/workflows/oeis-a147983-chomp-lean-audit.yml b/.github/workflows/oeis-a147983-chomp-lean-audit.yml index cead148d..e9629c0a 100644 --- a/.github/workflows/oeis-a147983-chomp-lean-audit.yml +++ b/.github/workflows/oeis-a147983-chomp-lean-audit.yml @@ -57,7 +57,11 @@ jobs: 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: Compile pure kernel theorem layers shell: bash From 3840e9a81c690fbc6ca535f67d1517f4e7793957 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 03:00:27 -0700 Subject: [PATCH 31/37] Build canonical Formal Conjectures utility library before Chomp audit --- .github/workflows/oeis-a147983-chomp-lean-audit.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/oeis-a147983-chomp-lean-audit.yml b/.github/workflows/oeis-a147983-chomp-lean-audit.yml index e9629c0a..dc6f0042 100644 --- a/.github/workflows/oeis-a147983-chomp-lean-audit.yml +++ b/.github/workflows/oeis-a147983-chomp-lean-audit.yml @@ -51,6 +51,7 @@ jobs: run: | set -euo pipefail lake exe cache get + lake build FormalConjecturesUtil - name: Compile exact canonical Chomp catalog module shell: bash From 93f012848e3cfed85272fdcf67967d1cae378b74 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 03:07:54 -0700 Subject: [PATCH 32/37] Split zero-row bite Ferrers proof by list shape --- proofs/chomp-10x42/lean/ChompPosition.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/proofs/chomp-10x42/lean/ChompPosition.lean b/proofs/chomp-10x42/lean/ChompPosition.lean index 69ca1802..91b5f94f 100644 --- a/proofs/chomp-10x42/lean/ChompPosition.lean +++ b/proofs/chomp-10x42/lean/ChompPosition.lean @@ -41,7 +41,9 @@ theorem bite_head_le (i t : ℕ) : ∀ p : List ℕ, /-- A bite preserves the Ferrers inequalities. -/ theorem bite_isFerrers (t : ℕ) : ∀ i : ℕ, ∀ {p : List ℕ}, IsFerrers p → IsFerrers (bite i t p) - | 0, p, h => by + | 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 From ba1f9ab180a7e0dffcdedf4932464496a0727bac Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 07:48:39 -0700 Subject: [PATCH 33/37] ci: run installed Chomp Lean audit --- .github/workflows/oeis-a147983-chomp-lean-audit.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/oeis-a147983-chomp-lean-audit.yml b/.github/workflows/oeis-a147983-chomp-lean-audit.yml index dc6f0042..96aa53f9 100644 --- a/.github/workflows/oeis-a147983-chomp-lean-audit.yml +++ b/.github/workflows/oeis-a147983-chomp-lean-audit.yml @@ -4,8 +4,8 @@ on: pull_request: branches: [main] paths: - - '.github/workflows/oeis-a147983-chomp-lean-audit.yml' - 'proofs/chomp-10x42/lean/**' + - '.github/workflows/oeis-a147983-chomp-lean-audit.yml' workflow_dispatch: permissions: From a2fbeea2bc8866bd1d5dec85bdc60f2fd33f3970 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 07:54:08 -0700 Subject: [PATCH 34/37] fix: prove concrete Chomp positions explicitly --- proofs/chomp-10x42/lean/ChompCatalogBridge.lean | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/proofs/chomp-10x42/lean/ChompCatalogBridge.lean b/proofs/chomp-10x42/lean/ChompCatalogBridge.lean index c7af9cc8..2553e7e0 100644 --- a/proofs/chomp-10x42/lean/ChompCatalogBridge.lean +++ b/proofs/chomp-10x42/lean/ChompCatalogBridge.lean @@ -57,13 +57,16 @@ theorem isPPosition_of_losing {p : List ℕ} exact ⟨kernelPSet, kernelPSet_isPSet, hp, hlosing⟩ @[category test, AMS 5] -theorem child₁_is_position : IsPosition child₁ := by decide +theorem child₁_is_position : IsPosition child₁ := by + norm_num [IsPosition, IsFerrers, child₁] @[category test, AMS 5] -theorem child₂_is_position : IsPosition child₂ := by decide +theorem child₂_is_position : IsPosition child₂ := by + norm_num [IsPosition, IsFerrers, child₂] @[category test, AMS 5] -theorem child₃_is_position : IsPosition child₃ := by decide +theorem child₃_is_position : IsPosition child₃ := by + norm_num [IsPosition, IsFerrers, child₃] /-- Three kernel losing proofs discharge the catalog theorem without any external axiom. -/ theorem three_openings_of_losing From 3e762920c2beba3de36479f6293d759bd6addb46 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 08:00:25 -0700 Subject: [PATCH 35/37] feat: add move-closed local P-set certificates --- proofs/chomp-10x42/lean/KernelPSet.lean | 66 ++++++++++++++++++++++--- 1 file changed, 60 insertions(+), 6 deletions(-) diff --git a/proofs/chomp-10x42/lean/KernelPSet.lean b/proofs/chomp-10x42/lean/KernelPSet.lean index 66d1ca8c..3cb8faae 100644 --- a/proofs/chomp-10x42/lean/KernelPSet.lean +++ b/proofs/chomp-10x42/lean/KernelPSet.lean @@ -17,15 +17,16 @@ limitations under the License. import ChompKernelCertificate /-! -# A certified P-set gives genuine normal-play outcome proofs +# 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. -This file turns those two symbolic facts into the inductive kernel proof objects used by the -Chomp formalization. +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 @@ -33,7 +34,7 @@ namespace RankedGame variable {P : Type} {G : RankedGame P} -/-- A predicate satisfying the two P-position kernel conditions produces actual losing and +/-- 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) @@ -61,7 +62,7 @@ theorem outcomes_of_pSet exact Outcome.winning hmove ((ih _ hlt q rfl).1 hq) exact all _ p rfl -/-- Membership in a certified P-set gives a kernel-checked losing proof. -/ +/-- 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) @@ -69,7 +70,7 @@ theorem losing_of_pSet {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 P-set gives a kernel-checked winning proof. -/ +/-- 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) @@ -77,9 +78,62 @@ theorem winning_of_not_pSet {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 From ee3bc2b66ffb38324de498b25ddbaca823ae5c33 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 08:05:18 -0700 Subject: [PATCH 36/37] feat: formalize the finite Chomp certificate domain --- proofs/chomp-10x42/lean/ChompPosition.lean | 36 ++++++++++++++++++++++ 1 file changed, 36 insertions(+) diff --git a/proofs/chomp-10x42/lean/ChompPosition.lean b/proofs/chomp-10x42/lean/ChompPosition.lean index 91b5f94f..aef45a00 100644 --- a/proofs/chomp-10x42/lean/ChompPosition.lean +++ b/proofs/chomp-10x42/lean/ChompPosition.lean @@ -31,6 +31,12 @@ theorem cutSuffix_isFerrers (t : ℕ) : ∀ {p : List ℕ}, IsFerrers p → IsFe 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 @@ -38,6 +44,17 @@ theorem bite_head_le (i t : ℕ) : ∀ p : List ℕ, | 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) @@ -87,9 +104,28 @@ theorem move_preserves_position {p q : List ℕ} 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 From ddac23bbfadf6b9e2a103d3d042bde31a5e0a323 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 08:10:28 -0700 Subject: [PATCH 37/37] feat: expose the final local symbolic-certificate theorem --- .../chomp-10x42/lean/ChompCatalogBridge.lean | 41 +++++++++++++++++++ 1 file changed, 41 insertions(+) diff --git a/proofs/chomp-10x42/lean/ChompCatalogBridge.lean b/proofs/chomp-10x42/lean/ChompCatalogBridge.lean index 2553e7e0..2748844e 100644 --- a/proofs/chomp-10x42/lean/ChompCatalogBridge.lean +++ b/proofs/chomp-10x42/lean/ChompCatalogBridge.lean @@ -16,6 +16,7 @@ limitations under the License. import ChompPosition import ChompKernelGameTheory +import ChompKernelPSet /-! # Bridge from kernel game outcomes to the catalog P-set definition @@ -68,6 +69,18 @@ theorem child₂_is_position : IsPosition child₂ := by 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₁) @@ -82,8 +95,36 @@ theorem three_openings_of_losing · 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