チョコナ (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、ランタイム依存なし。コードは全部公開している。

リポジトリ: https://github.com/sen-ltd/chocona