一つの例外を許す対称性

Let G be a finite simple undirected graph with vertex partition V(G) = {z} ⊔ ⨆ᵢ₌₁ᵐ {aᵢ,bᵢ}. Suppose every aᵢbᵢ is an edge, and the simultaneous interchange τ(aᵢ)=bᵢ, τ(bᵢ)=aᵢ is an automorphism of G−z. No restriction is imposed on the neighborhood of z. Under normal-play Arc Kayles, the Sprague–Grundy value of G is m mod 2.

The statement is proved below. Its exact general formulation was not located in the primary sources examined; the symmetry-response and mex-induction techniques are established methods.

m に関する強い帰納法で示す。p = (m+1) mod 2 と置き、合法手を四種類に分ける。

ペア内辺 aᵢbᵢ。三角形を保ったまま m−1 ペアになり、帰納仮定より値は m mod 2 = 1−p。

X 内の辺。X の二頂点が消え、残る一頂点が任意接続の一例外になる。T1 より値は m mod 2 = 1−p。

X の頂点 x とペアの片側 aᵢ を結ぶ辺。一手後の局面には、X の残り二頂点を結ぶ辺が残る。その辺を取ると、bᵢ を例外とする m−1 ペアの T1 の局面になり、値は (m−1) mod 2 = p。したがって一手後の局面の値は p ではない。辺 xbᵢ も同じである。

ペアをまたぐ辺。T1 と同じく鏡像の辺で応じると、m−2 ペアと三角形 X の局面になり、帰納仮定より値は p。したがって一手後の値は p ではない。

以上で、どの選択肢も値 p を持たない。p = 1 のとき、X 内の辺を取る手が値0の選択肢を与えるので、mex は p となる。m = 0 では X 内の辺しか手がなく、値は1である。□

本体は {0,1}, {2,3}, {4,5}, {6,7}、クリークは {8,9,10,11,12}。追加する接続辺は {0,8}, {2,9}, {4,10}, {6,11} だけとする。これは K₅ の異なる4頂点に、長さ2のパスを一本ずつ付けたグラフである。

4本のペア内辺と10本のクリーク内辺の後は全て値1、4本の接続辺の後は全て値0。従って g = mex{0,1} = 2 で、旧予想の (4+2) mod 2 = 0 と異なる。こちらは勝敗も旧予想と異なる。

python odd_clique_counterexample_verify.py を実行すると、二つの反例の値と全ての一手後の値を検算し、同じ場所へJSONを保存する。

"""Refutations of conjecture K; normal-play Arc Kayles, standard library only.
Run: python odd_clique_counterexample_verify.py
Two independent state representations: remaining vertices and remaining edges.
"""
from functools import lru_cache
from itertools import combinations
from pathlib import Path
import json


def mex(values):
    result = 0
    while result in values:
        result += 1
    return result


def verify(m, attachments):
    n = 2 * m + 5
    pairs = [(2*i, 2*i+1) for i in range(m)]
    clique = list(combinations(range(2*m, n), 2))
    edges = tuple(sorted(pairs + clique + attachments))
    assert len(set(edges)) == len(edges)
    core = set(pairs)
    tau = lambda v: v ^ 1
    assert all(tuple(sorted((tau(a), tau(b)))) in core for a, b in core)
    assert all(a < 2*m <= b < n for a, b in attachments)
    moves = tuple((1 << a) | (1 << b) for a, b in edges)

    @lru_cache(None)
    def by_vertices(mask):
        return mex({by_vertices(mask ^ move) for move in moves
                    if mask & move == move})

    @lru_cache(None)
    def by_edges(remaining):
        # The state is an immutable edge set; isolated vertices have no moves.
        options = set()
        for a, b in remaining:
            child = tuple((u, v) for u, v in remaining
                          if a not in (u, v) and b not in (u, v))
            options.add(by_edges(child))
        return mex(options)

    full = (1 << n) - 1
    first_moves = []
    for edge, move in zip(edges, moves):
        a, b = edge
        child = tuple((u, v) for u, v in edges
                      if a not in (u, v) and b not in (u, v))
        value = by_vertices(full ^ move)
        assert value == by_edges(child)
        kind = 'pair' if edge in pairs else 'clique' if edge in clique else 'attachment'
        first_moves.append({'edge': list(edge), 'kind': kind, 'grundy': value})
    vertex_value, edge_value = by_vertices(full), by_edges(edges)
    predicted = (m + 2) % 2
    assert vertex_value == edge_value != predicted
    return {'m': m, 'k': 2, 'vertices': n, 'pairs': pairs,
            'clique_vertices': list(range(2*m, n)), 'attachments': attachments,
            'edges': edges, 'prediction_of_retracted_K': predicted,
            'grundy_by_vertices': vertex_value, 'grundy_by_edges': edge_value,
            'first_move_value_set': sorted({row['grundy'] for row in first_moves}),
            'first_moves': first_moves}


if __name__ == '__main__':
    examples = [verify(3, [(0, 6), (0, 9), (2, 7), (4, 8)]),
                verify(4, [(0, 8), (2, 9), (4, 10), (6, 11)])]
    report = {'status': 'conjecture_K_refuted', 'examples': examples,
              'scope': 'two explicit counterexamples; no minimality claim'}
    text = json.dumps(report, ensure_ascii=False, indent=2) + '\n'
    Path(__file__).with_name('odd_clique_counterexample_results.json').write_text(text)
    print(text, end='')

2026 09 15に、Arc Kayles / Cram と 2-lift・signed graph・double cover・fixed-point-free involution・Tweedledum–Tweedledee・matched involution の組合せも検索した。この追加範囲でも、任意接続の一例外まで含む T1 と同一の一般命題は未確認だった。

2-lift による正確な言い換え。H = G−z、M = {aᵢbᵢ : 1 ≤ i ≤ m} とする。各ペアを基底の一頂点と見れば、H から M の辺だけを除いたグラフは、次の対応で符号付き多重グラフの 2-lift として表せる。正の辺を同じ層へ、負の辺を交差させて持ち上げる構成は既知であり、この対応を T1 の本体へ適用したものが下表である。[11]

同じ二頂点間に正負の辺が両方あってよい。したがって基底を単純グラフに限定しない。H は、この 2-lift に各ペアを結ぶ完全マッチング M を加えたものである。この記述なら、ペア内辺をループで表す規約が不要になる。

レビューの「各頂点に負のループを置く」という表現は、規約を補えば使える。通常のループ（whole-loop）を交換置換で持ち上げるとペア間に平行二辺が生じる一方、half-loop の規約なら一本の辺に対応する。平行辺を単純化する場合には、単純化後を同じ意味での被覆とは呼べない。両者を区別する文献を確認した。[12]

本体の構造には既知の名前もある。H の交換自己同型は、strictly matched involution のうち固定点を持たない場合に該当する。参照論文は各非固定点とその像が隣接することを条件とし、固定点集合が空である場合も明示的に許している。ただし、そこで扱われるゲームは直交彩色ゲームである。この構造名の一致は、Arc Kayles の T1 が既知だという証拠とは分けて扱う。また、z を含む G 全体に同じ自己同型を要求してはいない。[6]

さらに、用語の導入元である2019年の著者公開原稿も確認した。§5.1 の Theorem 7 / Corollary 8 は、固定点クリーク C を許した形でグラフを特徴づけており、C が空の場合が H に対応する。C = {z} として全体の交換対称性を要求すると、z は各ペアの両端に同じように隣接しなければならない。T1 はその制限を課さない。この原稿中にも Arc Kayles の T1 や例外なしの値の公式は見つからなかった。なお、同論文には、strictly matched involution を持つグラフの同型類の個数の下界を弱める訂正記事が出ている。訂正の対象は §5.1 の特徴付けではない。[13]構造の既知性を明記した上で、任意一例外を許すゲーム値の命題を候補として残す。[7]

保存したファイルを python paired_core_verify.py で実行する。標準出力と同じ内容を実行場所の JSON ファイルへ書き出す。

from functools import lru_cache
from itertools import combinations
import random,json

def sg(n,edges):
    moves=tuple((1<<u)|(1<<v) for u,v in edges)
    @lru_cache(None)
    def g(mask):
        seen={g(mask^e) for e in moves if mask&e==e}
        x=0
        while x in seen:x+=1
        return x
    return g((1<<n)-1)

def core(m,bits):
    edges=[(2*i,2*i+1) for i in range(m)]
    k=0
    for i,j in combinations(range(m),2):
        for flip in (0,1):
            if bits>>k&1:edges.extend([(2*i,2*j+flip),(2*i+1,2*j+1-flip)])
            k+=1
    return edges
report=[]
for m in range(4):
    count=0
    for bits in range(1<<(m*(m-1))):
        e=core(m,bits)
        for a in range(1<<(2*m)):
            edges=e+[(2*m,j) for j in range(2*m) if a>>j&1]
            value=sg(2*m+1,edges)
            assert value==m%2,(m,bits,a,value)
            count+=1
    report.append({'pairs':m,'exhaustive_labeled_graphs':count})
rng=random.Random(20260915)
for m,counts in [(4,2000),(5,1000),(6,300),(7,30)]:
    for _ in range(counts):
        bits=rng.randrange(1<<(m*(m-1)));a=rng.randrange(1<<(2*m))
        edges=core(m,bits)+[(2*m,j) for j in range(2*m) if a>>j&1]
        assert sg(2*m+1,edges)==m%2
    report.append({'pairs':m,'random_graphs':counts,'seed':20260915})
print(json.dumps(report,indent=2))
open('paired_core_results.json','w').write(json.dumps(report,indent=2))

python weighted_verify.py で実行する。

"""Independent WAK verification by direct capacity-state mex, without clone reduction.
Python standard library only. Run: python weighted_verify.py
"""
from functools import lru_cache
from itertools import product
from pathlib import Path
import json,random

def wak_grundy(capacities,edges):
    edges=tuple(edges)
    @lru_cache(None)
    def dp(caps):
        options=set()
        for a,b in edges:
            if caps[a] and caps[b]:
                nxt=list(caps);nxt[a]-=1;nxt[b]-=1
                options.add(dp(tuple(nxt)))
        g=0
        while g in options:g+=1
        return g
    return dp(tuple(capacities)),dp.cache_info().currsize

def core_edges(m,mask):
    edges=[(2*i,2*i+1) for i in range(m)]
    bit=0
    for i in range(m):
        for j in range(i+1,m):
            for flip in range(2):
                if mask>>bit&1:
                    edges.extend([(2*i,2*j+flip),(2*i+1,2*j+1-flip)])
                bit+=1
    return edges

def evaluate(m,c,coremask,adjmask):
    z=2*m
    capacities=[v for x in c for v in (x,x)]+[1]
    edges=core_edges(m,coremask)+[(i,z) for i in range(z) if adjmask>>i&1]
    got,states=wak_grundy(capacities,edges)
    expected=sum(c)%2
    return got,expected,states

def main():
    report={'method':'capacity tuple dynamic programming with mex; no clone reduction used by verifier',
            'seed':20260915,'exhaustive':[],'random':{},'counterexample':{},'total_checked':0,'violations':[]}
    states=0
    for m in (1,2):
        checked=0;observed={}
        for c in product(range(1,4),repeat=m):
            for cm in range(1<<(m*(m-1))):
                for am in range(1<<(2*m)):
                    got,expected,numstates=evaluate(m,c,cm,am)
                    states+=numstates;checked+=1
                    observed[got]=observed.get(got,0)+1
                    if got!=expected:report['violations'].append(dict(m=m,c=c,coremask=cm,adjmask=am,got=got,expected=expected))
        report['exhaustive'].append(dict(pairs=m,capacities='each c_i in 1..3',symmetric_core_count=1<<(m*(m-1)),exception_neighbor_count=1<<(2*m),cases=checked,grundy_histogram=observed))
        report['total_checked']+=checked
    rng=random.Random(report['seed']);m=3;seen=set();observed={}
    while len(seen)<200:
        c=tuple(rng.randint(1,3) for _ in range(m));cm=rng.randrange(1<<(m*(m-1)));am=rng.randrange(1<<(2*m))
        key=(c,cm,am)
        if key in seen:continue
        seen.add(key)
        got,expected,numstates=evaluate(m,c,cm,am)
        states+=numstates;observed[got]=observed.get(got,0)+1
        if got!=expected:report['violations'].append(dict(m=m,c=c,coremask=cm,adjmask=am,got=got,expected=expected))
    report['random']=dict(pairs=3,cases=200,capacities='each c_i in 1..3',sampling='uniform draws without duplicate parameter tuples',grundy_histogram=observed)
    report['total_checked']+=200
    g,n=wak_grundy([1,1,2],[(0,1),(0,2),(1,2)])
    report['counterexample']=dict(graph='triangle',capacities=[1,1,2],core_pairs=[[0,1]],exception=2,actual_grundy=g,claimed_parity_if_generalized=1,option_grundy_values=[0,1])
    report['sum_dp_states_across_cases']=states
    dest=Path(__file__).with_name('weighted_verify.json')
    dest.write_text(json.dumps(report,indent=2,ensure_ascii=False)+'\n')
    print(json.dumps(report,indent=2,ensure_ascii=False))
    assert not report['violations']
    assert g==2
if __name__=='__main__':main()

これは一つのスクリプトの生出力ではない。main_theorem は主定理スクリプトの出力リスト、weighted_corollary は重み付きスクリプトの出力オブジェクトを、そのまま格納している。外側に記録種別と実験日を付けた。JSONの日付は機械処理向けに YYYY-MM-DD、本文の日付は「2026 09 15」の形で書く。

{
  "record_type": "combined_script_outputs",
  "date": "2026-09-15",
  "main_theorem": [
    {
      "pairs": 0,
      "exhaustive_labeled_graphs": 1
    },
    {
      "pairs": 1,
      "exhaustive_labeled_graphs": 4
    },
    {
      "pairs": 2,
      "exhaustive_labeled_graphs": 64
    },
    {
      "pairs": 3,
      "exhaustive_labeled_graphs": 4096
    },
    {
      "pairs": 4,
      "random_graphs": 2000,
      "seed": 20260915
    },
    {
      "pairs": 5,
      "random_graphs": 1000,
      "seed": 20260915
    },
    {
      "pairs": 6,
      "random_graphs": 300,
      "seed": 20260915
    },
    {
      "pairs": 7,
      "random_graphs": 30,
      "seed": 20260915
    }
  ],
  "weighted_corollary": {
    "method": "capacity tuple dynamic programming with mex; no clone reduction used by verifier",
    "seed": 20260915,
    "exhaustive": [
      {
        "pairs": 1,
        "capacities": "each c_i in 1..3",
        "symmetric_core_count": 1,
        "exception_neighbor_count": 4,
        "cases": 12,
        "grundy_histogram": {
          "1": 8,
          "0": 4
        }
      },
      {
        "pairs": 2,
        "capacities": "each c_i in 1..3",
        "symmetric_core_count": 4,
        "exception_neighbor_count": 16,
        "cases": 576,
        "grundy_histogram": {
          "0": 320,
          "1": 256
        }
      }
    ],
    "random": {
      "pairs": 3,
      "cases": 200,
      "capacities": "each c_i in 1..3",
      "sampling": "uniform draws without duplicate parameter tuples",
      "grundy_histogram": {
        "1": 102,
        "0": 98
      }
    },
    "counterexample": {
      "graph": "triangle",
      "capacities": [
        1,
        1,
        2
      ],
      "core_pairs": [
        [
          0,
          1
        ]
      ],
      "exception": 2,
      "actual_grundy": 2,
      "claimed_parity_if_generalized": 1,
      "option_grundy_values": [
        0,
        1
      ]
    },
    "total_checked": 788,
    "violations": [],
    "sum_dp_states_across_cases": 130057
  }
}

python exception_family_verify.py で実行する。手元の環境では約10秒で終わる。結果はスクリプトと同じ場所に保存する。

"""Checks for the fifth edition: pendant tufts on 2xn ladders and odd-clique exception sets.
Python standard library only. Run: python exception_family_verify.py
Every value is computed by plain mex recursion over vertex subsets; no formula is built in.
"""
from functools import lru_cache
from itertools import combinations, combinations_with_replacement, product
from pathlib import Path
import json
import random

SEED = 20260915


def sg(n, edges):
    moves = tuple({(1 << u) | (1 << v) for u, v in edges})

    @lru_cache(None)
    def g(mask):
        seen = {g(mask ^ e) for e in moves if mask & e == e}
        k = 0
        while k in seen:
            k += 1
        return k
    return g((1 << n) - 1)


def ladder(n):
    """2xn grid; column i is the pair (2i, 2i+1)."""
    return ([(2 * i, 2 * i + 1) for i in range(n)]
            + [(2 * i, 2 * i + 2) for i in range(n - 1)]
            + [(2 * i + 1, 2 * i + 3) for i in range(n - 1)])


def core(m, bits):
    """Pairs (2i, 2i+1) with pair edges; each bit adds one swap-invariant orbit of two edges."""
    edges = [(2 * i, 2 * i + 1) for i in range(m)]
    k = 0
    for i, j in combinations(range(m), 2):
        for flip in (0, 1):
            if bits >> k & 1:
                edges += [(2 * i, 2 * j + flip), (2 * i + 1, 2 * j + 1 - flip)]
            k += 1
    return edges


def exception_set(m, x_edges, c, bits, adj):
    """m symmetric pairs plus an exception set X of c vertices (labels 2m..2m+c-1).
    x_edges is the graph on X; adj chooses every X-to-pair edge independently (no symmetry)."""
    edges = core(m, bits) + [(2 * m + a, 2 * m + b) for a, b in x_edges]
    edges += [(2 * m + z, v) for z in range(c) for v in range(2 * m) if adj >> (z * 2 * m + v) & 1]
    return sg(2 * m + c, edges)


def histogram(values):
    out = {}
    for v in values:
        out[str(v)] = out.get(str(v), 0) + 1
    return dict(sorted(out.items()))


def main():
    rng = random.Random(SEED)
    report = {'seed': SEED, 'ladder_tufts': {}, 'odd_clique_exceptions': {},
              'controls': {}, 'strictly_matched_fixed_clique': {}, 'paw': {}}

    # 1. Tufts on 2xn ladders. A tuft is a star whose centre is a grid vertex.
    one, two, three, multi = [], [], [], []
    for n in range(1, 9):
        base = sg(2 * n, ladder(n))
        assert base == n % 2
        bad1 = sum(sg(2 * n + 1, ladder(n) + [(v, 2 * n)]) != base for v in range(2 * n))
        pairs = list(combinations_with_replacement(range(2 * n), 2))
        bad2 = [p for p in pairs
                if sg(2 * n + 2, ladder(n) + [(p[0], 2 * n), (p[1], 2 * n + 1)]) != base]
        one.append({'n': n, 'placements': 2 * n, 'changed': bad1})
        two.append({'n': n, 'placements': len(pairs), 'changed': len(bad2), 'examples': bad2[:3]})
        assert bad1 == 0
        assert (len(bad2) == 0) == (n >= 2)
    for n in range(2, 7):
        base = n % 2
        checked = bad = 0
        for v, w in combinations_with_replacement(range(2 * n), 2):
            for a, b in product(range(1, 4), repeat=2):
                if 2 * n + a + b > 18:
                    continue
                edges = ladder(n) + [(v, 2 * n + i) for i in range(a)] + [(w, 2 * n + a + j) for j in range(b)]
                checked += 1
                bad += sg(2 * n + a + b, edges) != base
        multi.append({'n': n, 'leaf_counts': '1..3 per tuft', 'placements': checked, 'changed': bad})
        assert bad == 0
        triples = list(combinations_with_replacement(range(2 * n), 3))
        bad3 = [t for t in triples
                if sg(2 * n + 3, ladder(n) + [(x, 2 * n + i) for i, x in enumerate(t)]) != base]
        three.append({'n': n, 'placements': len(triples), 'changed': len(bad3), 'examples': bad3[:3]})
        assert bad3
    report['ladder_tufts'] = {'one_leaf': one, 'two_single_leaves': two,
                              'two_tufts_multi_leaf': multi, 'three_single_leaves': three}

    # 2. Exception set inducing K3 or K5, with arbitrary edges to the pairs.
    K3 = list(combinations(range(3), 2))
    K5 = list(combinations(range(5), 2))
    k3 = []
    for m in (0, 1, 2):
        vals = [exception_set(m, K3, 3, bits, adj)
                for bits in range(1 << (m * (m - 1))) for adj in range(1 << (6 * m))]
        assert set(vals) == {(m + 1) % 2}
        k3.append({'m': m, 'mode': 'exhaustive', 'cases': len(vals), 'values': histogram(vals)})
    vals = [exception_set(3, K3, 3, rng.getrandbits(6), rng.getrandbits(18)) for _ in range(400)]
    assert set(vals) == {0}
    k3.append({'m': 3, 'mode': 'random', 'cases': 400, 'values': histogram(vals)})
    k5 = []
    vals = [exception_set(1, K5, 5, 0, adj) for adj in range(1 << 10)]
    assert set(vals) == {1}
    k5.append({'m': 1, 'mode': 'exhaustive', 'cases': len(vals), 'values': histogram(vals)})
    for m, count in ((2, 400), (3, 100)):
        vals = [exception_set(m, K5, 5, rng.getrandbits(m * (m - 1)), rng.getrandbits(10 * m))
                for _ in range(count)]
        assert set(vals) == {(m + 2) % 2}
        k5.append({'m': m, 'mode': 'random', 'cases': count, 'values': histogram(vals)})
    report['odd_clique_exceptions'] = {'K3_predicted': '(m+1) mod 2', 'K3': k3,
                                       'K5_predicted': '(m+2) mod 2', 'K5': k5}

    # 3. Other exception graphs on 3 or 5 vertices do not keep a single value.
    controls = {'P3': (3, [(0, 1), (1, 2)]), 'K2+K1': (3, [(0, 1)]), '3K1': (3, []),
                'C5': (5, [(i, (i + 1) % 5) for i in range(5)]),
                'K5-e': (5, [e for e in K5 if e != (0, 1)]),
                'bowtie': (5, [(0, 1), (0, 2), (1, 2), (2, 3), (2, 4), (3, 4)])}
    for name, (c, xe) in controls.items():
        vals = [exception_set(2, xe, c, rng.getrandbits(2), rng.getrandbits(4 * c)) for _ in range(300)]
        controls_hist = histogram(vals)
        assert len(controls_hist) > 1
        report['controls'][name] = {'m': 2, 'cases': 300, 'values': controls_hist}

    # 4. Strictly matched involutions: fixed-point clique C, every z in C symmetric to each pair.
    for c in range(6):
        rows = []
        for m in range(0, 5 if c <= 3 else 4):
            vals = []
            for _ in range(200):
                edges = core(m, rng.getrandbits(max(1, m * (m - 1))))
                edges += [(2 * m + a, 2 * m + b) for a, b in combinations(range(c), 2)]
                for z in range(c):
                    for i in range(m):
                        if rng.random() < .5:
                            edges += [(2 * m + z, 2 * i), (2 * m + z, 2 * i + 1)]
                vals.append(sg(2 * m + c, edges))
            rows.append({'m': m, 'cases': 200, 'values': histogram(vals),
                         'floor_half_order_mod2': (2 * m + c) // 2 % 2})
            if c % 2 == 1 or c == 0:
                assert set(vals) == {(2 * m + c) // 2 % 2}
        report['strictly_matched_fixed_clique'][str(c)] = rows

    # 5. Symmetric two-point clique already fails: the paw with a pendant at the triangle apex.
    paw = [(0, 1), (2, 0), (2, 1), (2, 3)]  # pair {0,1}; C = {2,3}
    report['paw'] = {'edges': paw, 'pair': [0, 1], 'fixed_clique': [2, 3],
                     'grundy': sg(4, paw), 'floor_half_order_mod2': 0}
    assert report['paw']['grundy'] == 2

    dest = Path(__file__).with_name('exception_family_results.json')
    dest.write_text(json.dumps(report, ensure_ascii=False, indent=2) + '\n')
    print(json.dumps(report, ensure_ascii=False, indent=2))


if __name__ == '__main__':
    main()

{
  "seed": 20260915,
  "ladder_tufts": {
    "one_leaf": [
      {
        "n": 1,
        "placements": 2,
        "changed": 0
      },
      {
        "n": 2,
        "placements": 4,
        "changed": 0
      },
      {
        "n": 3,
        "placements": 6,
        "changed": 0
      },
      {
        "n": 4,
        "placements": 8,
        "changed": 0
      },
      {
        "n": 5,
        "placements": 10,
        "changed": 0
      },
      {
        "n": 6,
        "placements": 12,
        "changed": 0
      },
      {
        "n": 7,
        "placements": 14,
        "changed": 0
      },
      {
        "n": 8,
        "placements": 16,
        "changed": 0
      }
    ],
    "two_single_leaves": [
      {
        "n": 1,
        "placements": 3,
        "changed": 1,
        "examples": [
          [
            0,
            1
          ]
        ]
      },
      {
        "n": 2,
        "placements": 10,
        "changed": 0,
        "examples": []
      },
      {
        "n": 3,
        "placements": 21,
        "changed": 0,
        "examples": []
      },
      {
        "n": 4,
        "placements": 36,
        "changed": 0,
        "examples": []
      },
      {
        "n": 5,
        "placements": 55,
        "changed": 0,
        "examples": []
      },
      {
        "n": 6,
        "placements": 78,
        "changed": 0,
        "examples": []
      },
      {
        "n": 7,
        "placements": 105,
        "changed": 0,
        "examples": []
      },
      {
        "n": 8,
        "placements": 136,
        "changed": 0,
        "examples": []
      }
    ],
    "two_tufts_multi_leaf": [
      {
        "n": 2,
        "leaf_counts": "1..3 per tuft",
        "placements": 90,
        "changed": 0
      },
      {
        "n": 3,
        "leaf_counts": "1..3 per tuft",
        "placements": 189,
        "changed": 0
      },
      {
        "n": 4,
        "leaf_counts": "1..3 per tuft",
        "placements": 324,
        "changed": 0
      },
      {
        "n": 5,
        "leaf_counts": "1..3 per tuft",
        "placements": 495,
        "changed": 0
      },
      {
        "n": 6,
        "leaf_counts": "1..3 per tuft",
        "placements": 702,
        "changed": 0
      }
    ],
    "three_single_leaves": [
      {
        "n": 2,
        "placements": 20,
        "changed": 4,
        "examples": [
          [
            0,
            1,
            2
          ],
          [
            0,
            1,
            3
          ],
          [
            0,
            2,
            3
          ]
        ]
      },
      {
        "n": 3,
        "placements": 56,
        "changed": 10,
        "examples": [
          [
            0,
            1,
            2
          ],
          [
            0,
            1,
            3
          ],
          [
            0,
            1,
            4
          ]
        ]
      },
      {
        "n": 4,
        "placements": 120,
        "changed": 8,
        "examples": [
          [
            0,
            1,
            2
          ],
          [
            0,
            1,
            3
          ],
          [
            0,
            1,
            4
          ]
        ]
      },
      {
        "n": 5,
        "placements": 220,
        "changed": 8,
        "examples": [
          [
            0,
            1,
            2
          ],
          [
            0,
            1,
            3
          ],
          [
            0,
            1,
            4
          ]
        ]
      },
      {
        "n": 6,
        "placements": 364,
        "changed": 8,
        "examples": [
          [
            0,
            1,
            2
          ],
          [
            0,
            1,
            3
          ],
          [
            0,
            1,
            4
          ]
        ]
      }
    ]
  },
  "odd_clique_exceptions": {
    "K3_predicted": "(m+1) mod 2",
    "K3": [
      {
        "m": 0,
        "mode": "exhaustive",
        "cases": 1,
        "values": {
          "1": 1
        }
      },
      {
        "m": 1,
        "mode": "exhaustive",
        "cases": 64,
        "values": {
          "0": 64
        }
      },
      {
        "m": 2,
        "mode": "exhaustive",
        "cases": 16384,
        "values": {
          "1": 16384
        }
      },
      {
        "m": 3,
        "mode": "random",
        "cases": 400,
        "values": {
          "0": 400
        }
      }
    ],
    "K5_predicted": "(m+2) mod 2",
    "K5": [
      {
        "m": 1,
        "mode": "exhaustive",
        "cases": 1024,
        "values": {
          "1": 1024
        }
      },
      {
        "m": 2,
        "mode": "random",
        "cases": 400,
        "values": {
          "0": 400
        }
      },
      {
        "m": 3,
        "mode": "random",
        "cases": 100,
        "values": {
          "1": 100
        }
      }
    ]
  },
  "controls": {
    "P3": {
      "m": 2,
      "cases": 300,
      "values": {
        "1": 270,
        "3": 30
      }
    },
    "K2+K1": {
      "m": 2,
      "cases": 300,
      "values": {
        "1": 236,
        "3": 64
      }
    },
    "3K1": {
      "m": 2,
      "cases": 300,
      "values": {
        "0": 69,
        "1": 126,
        "3": 105
      }
    },
    "C5": {
      "m": 2,
      "cases": 300,
      "values": {
        "0": 248,
        "2": 52
      }
    },
    "K5-e": {
      "m": 2,
      "cases": 300,
      "values": {
        "0": 283,
        "2": 17
      }
    },
    "bowtie": {
      "m": 2,
      "cases": 300,
      "values": {
        "0": 260,
        "2": 40
      }
    }
  },
  "strictly_matched_fixed_clique": {
    "0": [
      {
        "m": 0,
        "cases": 200,
        "values": {
          "0": 200
        },
        "floor_half_order_mod2": 0
      },
      {
        "m": 1,
        "cases": 200,
        "values": {
          "1": 200
        },
        "floor_half_order_mod2": 1
      },
      {
        "m": 2,
        "cases": 200,
        "values": {
          "0": 200
        },
        "floor_half_order_mod2": 0
      },
      {
        "m": 3,
        "cases": 200,
        "values": {
          "1": 200
        },
        "floor_half_order_mod2": 1
      },
      {
        "m": 4,
        "cases": 200,
        "values": {
          "0": 200
        },
        "floor_half_order_mod2": 0
      }
    ],
    "1": [
      {
        "m": 0,
        "cases": 200,
        "values": {
          "0": 200
        },
        "floor_half_order_mod2": 0
      },
      {
        "m": 1,
        "cases": 200,
        "values": {
          "1": 200
        },
        "floor_half_order_mod2": 1
      },
      {
        "m": 2,
        "cases": 200,
        "values": {
          "0": 200
        },
        "floor_half_order_mod2": 0
      },
      {
        "m": 3,
        "cases": 200,
        "values": {
          "1": 200
        },
        "floor_half_order_mod2": 1
      },
      {
        "m": 4,
        "cases": 200,
        "values": {
          "0": 200
        },
        "floor_half_order_mod2": 0
      }
    ],
    "2": [
      {
        "m": 0,
        "cases": 200,
        "values": {
          "1": 200
        },
        "floor_half_order_mod2": 1
      },
      {
        "m": 1,
        "cases": 200,
        "values": {
          "0": 99,
          "2": 101
        },
        "floor_half_order_mod2": 0
      },
      {
        "m": 2,
        "cases": 200,
        "values": {
          "1": 99,
          "3": 101
        },
        "floor_half_order_mod2": 1
      },
      {
        "m": 3,
        "cases": 200,
        "values": {
          "0": 55,
          "2": 145
        },
        "floor_half_order_mod2": 0
      },
      {
        "m": 4,
        "cases": 200,
        "values": {
          "1": 71,
          "3": 129
        },
        "floor_half_order_mod2": 1
      }
    ],
    "3": [
      {
        "m": 0,
        "cases": 200,
        "values": {
          "1": 200
        },
        "floor_half_order_mod2": 1
      },
      {
        "m": 1,
        "cases": 200,
        "values": {
          "0": 200
        },
        "floor_half_order_mod2": 0
      },
      {
        "m": 2,
        "cases": 200,
        "values": {
          "1": 200
        },
        "floor_half_order_mod2": 1
      },
      {
        "m": 3,
        "cases": 200,
        "values": {
          "0": 200
        },
        "floor_half_order_mod2": 0
      },
      {
        "m": 4,
        "cases": 200,
        "values": {
          "1": 200
        },
        "floor_half_order_mod2": 1
      }
    ],
    "4": [
      {
        "m": 0,
        "cases": 200,
        "values": {
          "0": 200
        },
        "floor_half_order_mod2": 0
      },
      {
        "m": 1,
        "cases": 200,
        "values": {
          "1": 160,
          "3": 40
        },
        "floor_half_order_mod2": 1
      },
      {
        "m": 2,
        "cases": 200,
        "values": {
          "0": 82,
          "2": 118
        },
        "floor_half_order_mod2": 0
      },
      {
        "m": 3,
        "cases": 200,
        "values": {
          "0": 11,
          "1": 100,
          "3": 89
        },
        "floor_half_order_mod2": 1
      }
    ],
    "5": [
      {
        "m": 0,
        "cases": 200,
        "values": {
          "0": 200
        },
        "floor_half_order_mod2": 0
      },
      {
        "m": 1,
        "cases": 200,
        "values": {
          "1": 200
        },
        "floor_half_order_mod2": 1
      },
      {
        "m": 2,
        "cases": 200,
        "values": {
          "0": 200
        },
        "floor_half_order_mod2": 0
      },
      {
        "m": 3,
        "cases": 200,
        "values": {
          "1": 200
        },
        "floor_half_order_mod2": 1
      }
    ]
  },
  "paw": {
    "edges": [
      [
        0,
        1
      ],
      [
        2,
        0
      ],
      [
        2,
        1
      ],
      [
        2,
        3
      ]
    ],
    "pair": [
      0,
      1
    ],
    "fixed_clique": [
      2,
      3
    ],
    "grundy": 2,
    "floor_half_order_mod2": 0
  }
}

任意の拡張 D′ を固定し、その非巡回性を使って後続局面から帰納する。s ∈ S、k = c(s) とする。条件1により、s の選択肢に値0,…,k−1が全てある。S 内の選択肢は条件2と帰納仮定により値 k ではない。

S 外の選択肢 u には、条件3により値 k の局面 t への手が残る。mex の定義から g(u) ≠ k。したがって s の全選択肢から値 k が除外され、下位値は全てそろうので g(s) = k。U の値の確定は不要である。□

全拡張で S の指定値が保存されると仮定する。*j は、値が j の通常のNimの山を表す。以下の追加ゲームは元の D に戻る手を持たない私有のコピーなので、必ず許される有限非巡回な拡張になる。

条件2。S 内の辺が同じ指定値 k を結ぶなら、保存された実際の Grundy 値も同じになってしまう。局面は自分と同じ値の選択肢を持てないので矛盾。

条件1。s から S 内の値 j < c(s) への手がないとする。全ての u ∈ U に、新たな選択肢 *j を一個ずつ追加する。これで全ての g(u) ≠ j。保存を仮定している S 内にも該当する後続値がないため、s は値 j の選択肢を一つも持たず、g(s) ≤ j < c(s) となり矛盾。

条件3。s → u、u ∈ U に対する同値への応手が欠けるとし、k = c(s) と置く。U のうち u 以外の各局面には *k を追加する。u には *0,…,*(k−1) を追加する（k = 0 なら追加なし）。u の U 内の後続は値 k ではなく、S 内の後続にも指定値 k はない。一方、u の下位値は全て補われるので g(u) = k。s が自分と同じ値の選択肢を持つことになり矛盾。

いずれも「全指定値が保存される」という仮定への矛盾である。作った拡張で壊れるのは少なくとも一つの指定値であり、選んだ s だけが必ず変わるとまでは主張しない。□

m = 0 では総重量が W 未満なので手がない。p = m mod 2 とし、m に関する強い帰納法を用いる。

本体 B_i を取れば、条件を保って m−1 本体になる。例外に触れる手 e ⊆ E ∪ B_i では、残り E′ = (E ∪ B_i) ∖ e を新しい例外集合とする。重量は w(E′) = ρ + W − W = ρ であり、m−1 本体が残る。

ここで条件が保たれることを確かめる。旧 E ∪ B_i 内の手は残れない。残るなら E′ 内に重量 W の集合があることになり、ρ < W に反する。旧 E ∪ B_j または旧 B_i ∪ B_j にあった残存手は、新しい E′ ∪ B_j に収まる。それらが E′ に触れなければ、正の重みと重量 W から B_j 全体に等しい。i を含まない二本体内の手は、その補集合とともに丸ごと残る。各未除去本体も残る。よって新しい分割でも全条件が成立し、以上二種類の手の直後の値は 1−p。

二本体にまたがる手 e の後には、互いに素な合法補集合が残る。その応手で二本体を取り切れば、m−2 本体の同族で値 p。従って e の直後の局面は値 p を持てない。全ての選択肢が p と異なり、p = 1 のときは本体を取る値0の選択肢があるので、mex は p となる。□

各資源の重量を1、W = 3 とし、本体を 012、345、678 とする。数字列はその数字の頂点集合を表す。追加の合法手を、補集合の四対 015 / 234、025 / 134、027 / 168、356 / 478 とする。全11手で g = 1 となる。

このハイパーグラフは恒等写像以外の自己同型を持たない。以下で確認できる。次数は0〜5が4、6〜8が3。各頂点に接続する超辺について、他の二頂点の次数の組を多重集合として集めると、自己同型で保たれる四群 X = {0,2,3,5}、Y = {1,4}、Z = {6,7}、{8} に分かれる。

X のうち、Y の二頂点と同じ超辺に入るのは3だけなので3が固定される。残る X の頂点0,2,5が3と共有する超辺数は順に0,1,2であり、全て固定される。Y の1,4では1,3、Z の6,7では1,0と区別できる。8はもともと単独群である。よって全頂点が固定される。局所的な補集合条件は、全体の対称性を要求していない。

python meta_robust_verify.py で実行。結果はスクリプトと同じ場所に保存する。

"""Check the robust partial-Grundy characterization on all labeled DAGs up to 4 vertices.
The order is fixed; every edge goes from a larger index to a smaller index.
Only standard Python is required. Additional followers are private Nim heaps.
"""
from itertools import product
from pathlib import Path
import json
import random


def grundy(edges, extra):
    values = []
    for i, followers in enumerate(edges):
        # Each k in extra[i] is the value of a private Nim heap option *k.
        options = {values[j] for j in followers} | set(extra[i])
        value = 0
        while value in options:
            value += 1
        values.append(value)
    return values


def first_violation(edges, labels):
    for s, c in labels.items():
        inner = {labels[t] for t in edges[s] if t in labels}
        if c in inner:
            return ('same_label', s, None)
        for k in range(c):
            if k not in inner:
                return ('missing_lower', s, k)
        for u in edges[s]:
            if u not in labels and not any(t in labels and labels[t] == c for t in edges[u]):
                return ('missing_return', s, u)
    return None


def main():
    rng = random.Random(20260915)
    report = {'seed': 20260915, 'label_range': [0, 1, 2], 'max_vertices': 4,
              'labelled_order': 'edge i -> j allowed exactly when i > j',
              'templates': 0, 'valid_certificates': 0, 'random_completions_checked': 0,
              'invalid_certificates': 0, 'constructed_counterexamples': 0,
              'violation_types': {}, 'by_vertices': []}
    for n in range(1, 5):
        potential = [(i, j) for i in range(n) for j in range(i)]
        count = 0
        for edge_mask in range(1 << len(potential)):
            edges = [[] for _ in range(n)]
            for bit, (i, j) in enumerate(potential):
                if edge_mask >> bit & 1:
                    edges[i].append(j)
            for s_mask in range(1, 1 << n):
                anchors = [i for i in range(n) if s_mask >> i & 1]
                unknown = [i for i in range(n) if not (s_mask >> i & 1)]
                for c in product(range(3), repeat=len(anchors)):
                    labels = dict(zip(anchors, c))
                    report['templates'] += 1
                    count += 1
                    violation = first_violation(edges, labels)
                    if violation is None:
                        report['valid_certificates'] += 1
                        for _ in range(5):
                            extra = [set() for _ in range(n)]
                            for u in unknown:
                                extra[u] = {k for k in range(7) if rng.getrandbits(1)}
                            got = grundy(edges, extra)
                            assert all(got[s] == value for s, value in labels.items())
                            report['random_completions_checked'] += 1
                    else:
                        report['invalid_certificates'] += 1
                        kind, s, witness = violation
                        report['violation_types'][kind] = report['violation_types'].get(kind, 0) + 1
                        extra = [set() for _ in range(n)]
                        if kind == 'missing_lower':
                            # Every unknown now has an option *k, so none has value k.
                            for u in unknown:
                                extra[u] = {witness}
                        elif kind == 'missing_return':
                            # Other unknowns cannot equal k; u is forced to k if all
                            # anchor labels survive. Otherwise robustness already fails.
                            k = labels[s]
                            for u in unknown:
                                extra[u] = set(range(k)) if u == witness else {k}
                        assert all(k <= max(c) for opts in extra for k in opts)
                        got = grundy(edges, extra)
                        assert any(got[s] != value for s, value in labels.items()), (edges, labels, violation, extra, got)
                        report['constructed_counterexamples'] += 1
        report['by_vertices'].append({'vertices': n, 'templates': count})
    report['violations_of_theorem'] = 0
    report['counterexample_heap_bound'] = 'every added Nim option *k has k <= max prescribed label'
    dest = Path(__file__).with_name('meta_robust_results.json')
    dest.write_text(json.dumps(report, ensure_ascii=False, indent=2) + '\n')
    print(json.dumps(report, ensure_ascii=False, indent=2))


if __name__ == '__main__':
    main()

python meta_structure_verify.py で実行。結果は実行場所に保存する。各仮定を外した反例も含む。

from functools import lru_cache
from itertools import combinations,product
import random,json

def sg(n,edges):
    moves=tuple(set(sum(1<<v for v in e) for e in edges))
    @lru_cache(None)
    def g(mask):
        seen={g(mask^e) for e in moves if mask&e==e}
        k=0
        while k in seen:k+=1
        return k
    mask=(1<<n)-1
    return g(mask),sorted({g(mask^e) for e in moves})

def params(r,m,q):
    bs=[set(range(r*i,r*(i+1))) for i in range(m)]
    ex=set(range(r*m,r*m+q))
    orbits=[]
    for a,b in combinations(bs,2):
        allv=a|b
        for e in combinations(sorted(allv),r):
            f=tuple(sorted(allv-set(e)))
            if set(e) not in (a,b) and e<f:orbits.append([e,f])
    for b in bs:
        for e in combinations(sorted(b|ex),r):
            if set(e)&ex:orbits.append([e])
    return [tuple(sorted(b)) for b in bs],orbits

def instance(r,m,q,bits):
    blocks,orbits=params(r,m,q)
    return blocks+[e for i,orb in enumerate(orbits) if bits>>i&1 for e in orb]

if __name__=='__main__':
    report={'exhaustive':[],'random':[],'examples':{},'seed':20260915}
    for r,m,q in [(3,1,0),(3,1,1),(3,1,2),(3,2,0),(3,2,1)]:
        bs,orbits=params(r,m,q)
        for bits in range(1<<len(orbits)):
            es=bs+[e for i,orb in enumerate(orbits) if bits>>i&1 for e in orb]
            val,_=sg(r*m+q,es)
            assert val==m%2,(r,m,q,bits,val)
        report['exhaustive'].append({'r':r,'m':m,'q':q,'count':1<<len(orbits)})
    rng=random.Random(20260915)
    for r,m,q,count in [(3,2,2,500),(3,3,2,500),(3,4,2,300),(4,2,3,300),(4,3,3,300)]:
        bs,orbits=params(r,m,q)
        for _ in range(count):
            bits=rng.getrandbits(len(orbits))
            es=bs+[e for i,orb in enumerate(orbits) if bits>>i&1 for e in orb]
            val,_=sg(r*m+q,es)
            assert val==m%2,(r,m,q,bits,val)
        report['random'].append({'r':r,'m':m,'q':q,'count':count})
    # Worked examples. Blocks are A=012 and B=345 unless noted; values are recorded, not asserted.
    # r3_transfer: exception E=67 (weight 2 < 3); 670 and 712 lie in E+A, 634 in E+B; m=2, value 0.
    # missing_complement: 013 meets A and B, but its complement 245 is absent (condition 3 fails).
    # exception_two_blocks: E=6 and the move 603 meets both A and B (condition 4 fails).
    # exception_too_large: one block A=012 and E=345 with w(E)=3=W (rho<W fails); 340 and 512 touch E.
    # missing_block: the intended block 012 is not a legal move (condition 1 fails); value 0, not 1.
    # mixed_size: the weighted example of the text with a,b,c,d,e,z = 0..5 (sg ignores the weights).
    examples={
      'r3_transfer':(8,[(0,1,2),(3,4,5),(0,1,3),(2,4,5),(6,7,0),(6,3,4),(7,1,2)]),
      'missing_complement':(6,[(0,1,2),(3,4,5),(0,1,3)]),
      'exception_two_blocks':(7,[(0,1,2),(3,4,5),(6,0,3)]),
      'exception_too_large':(6,[(0,1,2),(3,4,0),(5,1,2)]),
      'missing_block':(3,[]),
      'mixed_size':(6,[(0,1),(2,3,4),(0,2),(1,3,4),(5,0),(5,2),(5,3,4)])
    }
    for name,(n,es) in examples.items():
        value,opts=sg(n,es)
        report['examples'][name]={'n':n,'edges':es,'grundy':value,'option_values':opts}
    # three_blocks: search for a move meeting three blocks A, B, C=678, which breaks condition 3.
    # Optional orbits and triple moves are pruned while the value stays different from 3 mod 2 = 1.
    bs,orbits=params(3,3,0)
    cross3=list(product(range(3),range(3,6),range(6,9)))
    for t in range(10000):
        chosen=[orb for orb in orbits if rng.random()<.08]
        es=bs+[e for orb in chosen for e in orb]+[e for e in cross3 if rng.random()<.08]
        val,opts=sg(9,es)
        if val!=1:
            # Remove optional core-orbits/triple moves greedily, preserve failed value.
            groups=chosen+[[e] for e in es[len(bs)+sum(map(len,chosen)):]]
            change=True
            while change:
                change=False
                for i in range(len(groups)):
                    cand=groups[:i]+groups[i+1:]
                    nv,_=sg(9,bs+[e for group in cand for e in group])
                    if nv!=1:groups=cand;change=True;break
            es=bs+[e for group in groups for e in group]
            val,opts=sg(9,es)
            report['examples']['three_blocks']={'n':9,'edges':es,'grundy':val,'option_values':opts}
            break
    print(json.dumps(report,indent=2))
    open('meta_structure_results.json','w').write(json.dumps(report,indent=2))

提供されたレビューを受け、反例の最小性を頂点数・辺数・連結性に分けて明記し、統合JSONの由来を説明した。追加の別名検索とループ規約の確認を記録し、操作名・添字・図の可読性を修正した。本文の日付は従来の形式を保ち、JSON内は機械処理向けの形式にした。主定理 T1 と系 W1 の仮定・結論・証明は変更していない。

抽象度を上げる探索から、第09節に定理 M と R を追加した。M は任意の非巡回な拡張から指定値を保護する必要十分条件、R は局所的な補集合と例外移送による等重量除去ゲームの定理である。小Nimによる必要性の反証構成、非対称な本体の具体例、独立監査・有限検査・先行研究との境界を記録した。従来の T1 と W1 の証明は維持した。新しい命題も専門家査読・証明支援系による形式検証は未実施。

T1 を M へ適用する際、ラベルを残存頂点数だけで定義し、対分けによらないことと、Case C の直後が別の分解で S に入る場合の扱いを明記した。M の計算検査は私有Nim追加に限ると報告範囲を正確にした。M は標準的な議論を選んだ拡張クラスの同値条件として整理する命題と位置づけ、必要性の拡張クラスへの依存を前面に出した。定理の仮定・結論・証明と検証コードの処理は変更していない。

位置づけと構成。主結果 T1 を「命題」から「定理」に、標準的な議論の整理である M を「定理」から「命題」に改めた。冒頭に09節を含む全体の構成を書き、探索切替の記録を付録へ移した。R が T1 と一致する範囲（重み1・W = 2）と、自己同型を仮定しないことが効く範囲を明記した。

新規性照合。[2] の初版に、梯子へ tuft を加える証明なしの記述があることを確認し、葉一枚の場合を「既述の特殊例」とした。第4版の「P₄ に衝突し得る」という評価は、全列挙の結果「計算した範囲では n = 1 でのみ衝突」に修正した。Cram データベース、Game of Cycles、strictly matched involution の訂正記事、可逆な選択肢の標準理論を出典に加えた。

新しい結果。例外集合が三角形の場合の命題 K3 を証明付きで加え、奇数クリークへの予想 K、固定点が二個なら対称でも破れる反例を記録した。対応する検証コードと結果を収録した。

細部。ルール説明の係り方、デモの注記（「*2 を外して」）、実験図の辺が他の頂点に重ならないようにする描画、Case B の図の高さ、静的な説明文とJavaScriptの説明文の食い違い、R の検証コードの例へのコメント、本文の日付表記、参考文献番号の初出順を直した。T1・W1・M・R の仮定・結論・証明と、既存の検証コードの処理結果は変更していない。

提供された第5版をもとに、K3 の証明と R・T1 の対応を独立に確認し、第5版の追加検証コードを再実行して、収録JSONの全フィールドとの一致を確認した。K3 は証明付きの命題、この版の時点では奇数クリーク一般を未証明の予想として保持した。その後、第6版で反例を確認して撤回した。

梯子の二枚・三枚の葉の記述を実際の有限検査範囲へ限定し、固定点クリークの各 (c,m) と試行数を明記した。非クリークの対照実験から必要条件を主張しないこと、例外なしの R から T1 への対応も補った。

初版の tuft の記述をPDF本文で確認した。Game of Cycles の Theorem 6 の面に関する仮定、Cram データベースの収録範囲が未確認であること、訂正記事の参照番号を修正した。日付を YYYY MM DD に統一した。定理 T1・W1・M・R・K3 の結論と検証コードの処理は変更していない。これらの監査は、学術的新規性の確定や証明支援系による形式検証には当たらない。

追加査読の反例指摘を受け、K₅ と3ペアの11頂点例で g = 3（旧予想1）、K₅ と4ペアの13頂点例で g = 2（旧予想0）を確認した。残存頂点・残存辺集合の二方式で、根の値だけでなく全ての一手後の値も照合した。反例の図、完全な辺集合、再現コード、検算結果JSONを収録した。

予想 K の状態を反証済み・撤回へ更新し、冒頭・本文・検査表・今後の課題をそろえた。第5版の標本内で一致した事実は履歴として保持する。T1・W1・K3・M・R の仮定・結論・証明は変更していない。今回は追加の一般化を行わず、この内容を完成稿とする。学術的新規性の確定や証明支援系による形式検証は引き続き未実施である。

2026 09 16 の再点検で、04節と07節の一マス欠けの扱いを修正した。欠損が端の列にある盤面は、2×(n−1) の梯子の角に葉を一枚付けた形と一致するため、既存の tuft の記述の範囲に含まれる。欠損に関する新規性の候補は内側の列の場合に限定し、その形を「相方が左右の格子をつなぐ切断点になる形」と正確に書き直した。

[3] の Theorem 4.6 が扱うのは四隅のうち3か所または4か所に突起を付けた梯子であることを本文で再確認し、注記を具体化した。tuft が複数の葉を持つ場合に06節の補題を併用することも明記した。T1・W1・K3・M・R の仮定・結論・証明と、検証コード・収録JSONは変更していない（同梱の再現コード6本を再実行し、収録JSONとの一致を確認）。