チョコナ (Chocona) を、4 つのルールセット内蔵でブラウザに実装した。n×n の盤面のいくつかのマスを黒く塗る。数字の書かれた領域はちょうどその数だけ黒マスを含み、**黒マスの連結成分（塊）はすべて「隙間なく埋まった長方形」**でなければならない。塊は領域境界をまたいでよく、角で接するのもよい——辺で接した瞬間だけ 1 つの塊に融合する。ソルバー内蔵パズル第 40 弾。
デモ: https://sen.ltd/portfolio/chocona/
リポジトリ: https://github.com/sen-ltd/chocona
このパズルを選んだ理由は 2 つ。
大域則に、正確な局所の分身がいる
「すべての塊が長方形」は、塊を丸ごと眺めないと確認できない形の性質に見える。ところがこれは、「どの 2×2 窓にも黒がちょうど 3 つあってはならない」という 1 つの局所テストと正確に同値だ。0 個・1 個・2 個・4 個は全部合法で、3 個だけが違法。片方向は簡単（3 つの黒は必ず L 字をなし、L の bounding box には白が 1 マス残るので、長方形には埋まらない）。逆方向——「どの窓にも 3 がなければ全塊が長方形」——が定理の本体だ。
この同値がチョコナに連作でも独特の手筋を与える。ほとんどの塗りパズルは「2×2 全黒禁止」型で、四角が埋まりかけたら白で逃がす。チョコナは逆で、2×2 に黒が 3 つ並んだら、4 つ目は黒で確定する。L 字から逃げる唯一の道は、完成させることだからだ。
実装では、この定理をエンジンに「分担」させた:
-
バリデータは定義そのもので判定する: flood fill で塊を取り、
塊のサイズ == bounding box の面積を見る。2×2 窓は一度も見ない。 -
ルールラダー（後述の
corner）は局所の分身だけで推論する。 - 総当たりは bounding box の枝刈りだけで探索する。
- 全数アンカーは第 3 の定式化——「同じ塊に属する任意の 2 マスについて、そのペアの bounding box が全部黒」——で列挙する（これも同値になる。証明は 4 隅を渡り歩くだけの短い演習）。
別々の定式化を持つエンジン同士の解数一致は、テストであると同時に同値定理の機械検証になる。結果は後で。
ルールは 4 段
| レベル | ルール |
|---|---|
quota |
領域の数え上げ、両方向: 数字に達したら残りは白、自由マスが不足分ちょうどなら全部黒。単独では領域境界を越えられない |
corner |
局所の分身: 2×2 に黒 3 つ禁止。3 つ並べば 4 つ目は黒、白 1 つの隣で黒 2 つなら残りは白 |
box |
大域に戻した長方形則: 塊の bounding box は埋まる（fill）。塊を覆える「実行可能長方形」（内部に白なし、境界の外側に黒が触れない）が 1 つもなければ矛盾。どの実行可能長方形にも届かない隣接マスは白確定——完成した長方形の縁が通る堀（moat） |
probe |
1 マスに色を仮置きし、下位ルールを fixpoint まで回して矛盾したら棄却 |
実測 — 生のストリームには情報がほぼ無い
300 盤/サイズの生の生成ストリーム（ランダム分割・領域最大 5 マス + ランダム長方形詰め込み + 全領域に数字）。推測なしの fixpoint だけで完成する率:
| 盤面 | quota | +corner | +box | +probe | ストリーム中の一意解率 |
|---|---|---|---|---|---|
| 6×6 | 0.0% | 0.3% | 0.3% | 1.0% | 1.0% |
| 8×8 | 0.0% | 0.0% | 0.0% | 0.3% | 0.3% |
| 10×10 | 0.0% | 0.0% | 0.0% | 0.0% | 0.0% |
前作アクレの同じ表（6×6 で 21.3%、8×8 で 7.7%）と比べても壊滅的だ。理由は合法盤面の数にある。ヒントなしの合法盤面は 2×2 / 3×3 / 4×4 で 12 / 208 / 10,148 通り。アクレは 14 / 219 / 798 だった——あちらは 4 連禁止が両色に効いて空間を刈り込むのに対し、チョコナの長方形則は塗らない自由を一切奪わない（全白も合法）。空間が広すぎて、数字を全部印刷しても盤面は決まらない。
Ablation — 同値な 2 つの定式化は、伝播器としても交換可能
全ラダーから 1 ルールずつ抜く:
| 盤面 | full | −quota | −corner | −box |
|---|---|---|---|---|
| 6×6 | 1.0% | 0.0% | 1.0% | 1.0% |
| 8×8 | 0.3% | 0.0% | 0.3% | 0.3% |
| 10×10 | 0.0% | 0.0% | 0.0% | 0.0% |
−corner も −box も、成績が 1 盤も落ちない。 局所の 2×2 推論と大域の長方形推論は、probe の下では完全に互いの代役を務める——法として同値な 2 つの定式化は、伝播器としても交換可能だという、同値定理のもう 1 つの顔だ。設計時は「corner は box の高速な部分集合」程度の読みだったが、テストを書いていて逆方向にも驚いた: 対角の黒ペア + 白 1 つから残りを白に確定する corner の手筋を、box も moat 経由で独立に再発見する（「ペアを覆う長方形は白を飲むか、もう 1 つの黒に触れる」）。1 つの演繹に 2 通りの証明が付く——ミニチュアの同値定理がテストケースに転がっていた。
抜いて崩壊するのは quota だけ。数字を読む唯一のルールという点はアクレと同じだが、アクレは「どれを抜いても全崩壊」（全ルールが probe のセンサーとして急所）だった。チョコナは冗長性が構造的に 2 重化されている——同じ法を 2 つの言語で書いたのだから当然、と言いたくなるが、その「当然」を数字で確認できるのがこのシリーズの楽しみだ。
作者のダイヤルには崖、答えのダイヤルには坂
分割の粒度（作者のダイヤル）、8×8・各点 150 盤:
| maxSize | 平均領域数 | 一意 | probe 解決 | quota 単独解決 |
|---|---|---|---|---|
| 1 | 64.0 | 100.0% | 100.0% | 100.0% |
| 2 | 45.9 | 2.7% | 2.7% | 0.0% |
| 3 | 35.9 | 0.0% | 0.0% | 0.0% |
| 5 | 25.8 | 0.0% | 0.0% | 0.0% |
| 8 | 18.4 | 0.0% | 0.0% | 0.0% |
| 12 | 13.5 | 0.0% | 0.0% | 0.0% |
アクレの粒度ダイヤルは 100% → 46% → 22% → 3.3% と全域を掃く坂だった。チョコナは 100% → 2.7% → 0.0% の崖。1 マス領域（=答えの印刷）から一段でも粗くすると情報はほぼ消滅し、数字の保持率ダイヤル（密度）に至っては 8×8 で全点 0.0% の完全な死に領域だ。
代わりにチョコナには、連作初の 3 本目のダイヤルがある。長方形の最大サイズ（maxRect）——分割でも数字でもなく、答えそのものの形状を回すダイヤルだ:
| maxRect | 平均長方形数 | 黒率 | 一意 | probe 解決 |
|---|---|---|---|---|
| 1 | 23.4 | 36.5% | 0.0% | 0.0% |
| 2 | 13.0 | 35.9% | 0.0% | 0.0% |
| 3 | 9.1 | 37.6% | 0.0% | 0.0% |
| 4 | 7.0 | 41.6% | 0.7% | 0.7% |
| 5 | 5.8 | 41.6% | 1.3% | 1.3% |
1×1 の紙吹雪より、少数の大きな板の方が情報を運ぶ。黒率はどの目盛でも 36–42% の帯に収まるのに、一意率だけが動く——同じ量の黒でも、まとまり方が情報量を変える。
生成器 — 探索の代わりに、ダーツを投げる
チョコナの合法盤面は「辺で接しない長方形の詰め込み」と 1 対 1 だ。だから生成器は探索しない。ランダムな長方形を 2n² 回投げ、セルと四辺のストリップがまだ空いているものだけ受け入れる。1 投は O(面積) で必ず着地か棄却が決まり、バックトラックも重い裾もリスタート上限も要らない——アクレの生成器を 8 時間ハングさせたランダム化 DFS の古典的病理が、構造的に起こり得ない。「合法盤面が既知の組合せ対象と対応するなら、探索せず直接サンプルせよ」という連作の教訓（陰陽で 9,000 倍を出したやつ）の、最も気持ちのいい適用例になった。
Bank — 中段は作れるが、最上段が釣れない
出荷 bank は 6×6 / 8×8 / 10×10 × 4 グレード。ランダム分割の全開示が 0% の世界でどう作るかというと、アクレと同じく答えの色境界に沿った単色分割（全領域 all-or-nothing、quota だけで解ける）から出発し、目標レベルで数字を間引く。これで quota / corner / box 級は全サイズで量産できる。
釣れないのは probe 級だ。間引き後に「box では止まり probe でだけ解ける」盤面が残る確率は attempt の 1–2%、10×10 では 10,000 attempt で 3 枚（2,041 / 6,149 / 8,553 attempt 目）。ぬりみさきでは下位グレードが消え、アクレでは中段が消えた。チョコナは最上段だけが薄い——同値な 2 つの伝播器が互いを埋め合う設計では、「伝播で解けないが一意」という隙間そのものが希少になる。UI の Rules メニューは足りないグレードをグレーアウトする。
出荷盤面の一意性証明は全サイズで探索分岐の中央値 0——fixpoint が単独で証明を完結する。数字の中央値は 6×6 で 21 領域中 14.5、10×10 で 54.5 領域中 40.5。
probe = 一意の法則、復活
連作が追いかけている法則「一意解の盤面は probe の fixpoint で完成できる」は、クロットで初めて破れ、ぬりみさきで復活し、アクレで再び破れた。チョコナでは見つかった一意盤 69 枚すべてで成立（section 1 プールの 4 枚に加え、一意率が生きている maxSize 2 ストリーム 400 盤/サイズで 6×6: 52 枚中 0、8×8: 13 枚中 0 が probe 不能）。破れ 2、成立 2。法則は「成り立つ方が普通だが保証はない」——スコアボードは次のパズルに持ち越しだ。
検証
- 解数の突き合わせ: ラダーとコードを共有しない総当たり（行優先 DFS、枝刈りは領域集計と bounding box のみ、葉は独立バリデータ採点）と 4 レベル各々の伝播付き探索の解数が、完走した全 (盤面, レベル) ペアで一致——536/536。伝播の弱いレベルの探索は 24 ペアが 30 万分岐上限に達しスキップ（数え落としではなく計測対象外として報告）。ラダーは 2×2 窓でしか推論せず、総当たりは bounding box でしか刈らないので、この一致が局所⟺大域の同値の機械検証になっている。
- 全数アンカー: ヒントなし 2×2 / 3×3 / 4×4 盤を、ペア bounding box 式の第 3 エンジンで全列挙——12 / 208 / 10,148 盤で総当たり・探索エンジンと一致。
- Bank の整合性: 出荷全 58 盤は探索エンジンで一意性を再確認済み、grade は「推測なしで完成できる最弱レベル」で付与。
全 42 テスト。npm test で回る。
まとめ
- チョコナの長方形則は「2×2 に黒ちょうど 3 つ禁止」という局所則と同値。3 つ並んだら 4 つ目は黒——塗りパズルの直感が反転する。
- 定理を 3 つのエンジン（定義・局所・第 3 定式化）に分担させ、解数一致 536/536 で機械検証した。
- ablation では −corner も −box も無傷: 法として同値な定式化は、伝播器としても交換可能。急所は数字を読む quota だけ。
- 合法盤面空間は広大（4×4 で 10,148 盤）で、生ストリームの情報はほぼゼロ。作者のダイヤルは崖、密度ダイヤルは死に、代わりに「答えの形状」という第 3 のダイヤルが一意率を動かす。
- 生成は探索なしのダーツ投げ O(n²)。アクレを 8 時間ハングさせた病理が構造的に消えた。
- probe = 一意の法則は 69/69 で復活。連作スコアは破れ 2、成立 2。
TypeScript + Vite、ランタイム依存なし。コードは全部公開している。