有限の判定を decide に載せる — 格子の辺の選び方を一語で確かめる

4 次元の格子で、すべての小さな正方形がちょうど一本を含むような、辺の選び方は在るか。
（格子：整数の座標をもつ点を頂点とし、座標が一つだけ 1 だけ違う二点を辺で結んだ図形。プラケット＝小さな正方形：二つの方向 μ・ν と基点 x で決まる単位正方形で、その辺は 4 本あります。）

この組合せは、格子の上の場の理論で強結合域の定数を見積もるときに出てきます。ここで扱うのは組合せの部分だけで、連続極限や質量ギャップ——ミレニアム問題の本体——への主張はありません。

「在る」を示すには一つ作って見せればよく、作った式が本当に条件を満たすかは、有限個のプラケットを全部調べれば決まります。有限個を全部調べれば決まる主張は、Lean には decide の一語で渡せます。このページでは、その渡し方・渡し方を間違えたときに Lean が何と言うか・どの大きさから重くなるかを順に見ます。

4 つの方向を 0, 1, 2, 3 と番号で呼び、頂点の座標を x 0, x 1, x 2, x 3 と書きます。座標の偶奇だけを見ることにすると頂点は 16 通りで、次の 4 本の規則で辺を選びます。

プラケットは、方向の組 {μ, ν} が 6 通り・残り 2 座標の偶奇が 4 通りで 24 枚あります。その 24 枚について「4 本の辺のうち選ばれているものが 1 本だけ」を確かめれば証明は終わりで、紙に書けば 24 行の表です。ここで人がするのは「確かめる」であって「考える」ではありません。だから機械に渡します。

decide は、主張が「有限個の場合に分かれ、どの場合も計算で真偽が決まる」形になっていないと働きません。ですから定義の段階で、数え上げられる型と計算できる述語だけを使います。選択が三つあります。

頂点を Fin d → Bool にする

格子そのものは無限です。ここでは各座標の偶奇だけを見て、頂点を Fin d → Bool（d 個の真偽値の並び＝単位 d 立方体の頂点）としました。Fin d → Bool は要素が 2^d 個の有限型で、Lean が数え上げ方を知っています。

頂点を Fin d → ℤ にすれば格子そのものですが、無限なので「すべてのプラケットで」の ∀ が decide では閉じません。剰余 ZMod L にすれば有限で周期の格子になり、これは 数え上げで使う型です。偶奇だけを見る Bool の版は L = 2 に当たり、いちばん軽くなります。

辺の族を Bool 値の関数にする

辺の集合は Set でも Finset でも書けますが、ここでは I : Fin d → V d → Bool——方向と位置を受け取って「選んだか」を真偽値で返す関数——にしました。Set は述語であって計算できる保証がなく、Finset は重複の無い並びなので、族を式で書くときに余計な証明が付いてきます。Bool を返す関数なら、族の定義がそのまま計算の手順になります。

方向 μ の辺は「μ 座標以外の値」で決まります。x と「x の μ 座標を反転したもの」は同じ辺なので、x μ = false の側に正規化して (μ, x) と書きます。

「ちょうど一本」を toNat の和で書く

Bool を 0 か 1 に直す toNat を使い、プラケットの 4 枠の値を足して 1 に等しい、と書きます。「4 本のうちちょうど一本」は Finset の濃度でも書けますが、和なら評価が足し算だけで終わります。

ただしこの書き方は一つ借りを作ります。「4 枠の値の和が 1」が「4 本のうち一本」を意味するのは、4 枠が相異なる辺を指しているときだけです。これは別に証明しておく必要があり、実際に face_slots_ne という補題が入っています。書き方を軽くすると、軽くしたぶんが別の補題になって出てきます——この類の借りの見つけ方は 通っても、言いたいことが言えているかで扱います。

/-- 単位 `d` 立方体の頂点。 -/
abbrev V (d : ℕ) : Type := Fin d → Bool

/-- 第 `i` 座標を反転する（`x ↦ x + e_i`）。 -/
def flipAt (x : V d) (i : Fin d) : V d := Function.update x i (!x i)

/--
`I μ x`：方向 `μ`・位置 `x`（`x μ = false` に正規化）の辺が族に入る。

`Perfect I`：`μ ≠ ν`・`z μ = z ν = false` で決まるどの 2 次元の面についても、
その 4 本の辺 `(μ, z)`・`(μ, z+e_ν)`・`(ν, z)`・`(ν, z+e_μ)` のうちちょうど一本が `I` に入る。
-/
def Perfect (I : Fin d → V d → Bool) : Prop :=
  ∀ μ ν : Fin d, μ ≠ ν → ∀ z : V d, z μ = false → z ν = false →
    (I μ z).toNat + (I μ (flipAt z ν)).toNat
      + (I ν z).toNat + (I ν (flipAt z μ)).toNat = 1

紙で書いた 4 本の規則は、そのまま式になります。

/-- `d = 4` の完全な族の例。方向ごとに 2 本で、残り 3 座標で対心をなす。 -/
def I4 (μ : Fin 4) (x : V 4) : Bool :=
  if μ = 0 then ((x 1 == x 2) && !(x 2 == x 3))
  else if μ = 1 then ((x 2 == x 3) && !(x 3 == x 0))
  else if μ = 2 then ((x 0 == x 1) && (x 1 == x 3))
  else ((x 0 == x 2) && !(x 2 == x 1))

/-- `d = 4` には完全な族が在る。 -/
theorem perfect_I4 : Perfect I4 := by decide

LeanPerfectFamily.perfect_I4。証明は by decide の一語です。d = 3 と d = 2 にも例があり（perfect_I3・perfect_I2）、d ≤ 1 には 2 次元の面が無いのでどんな族も条件を満たします（perfect_of_le_one）。逆に d ≥ 5 には在りません——そちらは 単射一本で上界を出すで扱います。

上の decide は、そのままでは通りません。Perfect は Prop を返す def で書かれているので、Lean の実例探索が中を見てくれないのです。手元で確かめます。次のファイルを検査に掛けます。

import Mathlib

/-- 判定の対象。`Prop` を返す `def` で書いてある。 -/
def AtMostOne2 (I : Fin 2 → (Fin 2 → Bool) → Bool) : Prop :=
  ∀ μ ν : Fin 2, μ ≠ ν → ∀ z : Fin 2 → Bool, (I μ z).toNat + (I ν z).toNat ≤ 1

def J (μ : Fin 2) (x : Fin 2 → Bool) : Bool := if μ = 0 then !x 1 else false

theorem J_atMostOne : AtMostOne2 J := by decide

Lean はこう言います。

error: failed to synthesize
  Decidable (AtMostOne2 J)

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.

「この主張が判定できることを、私は知らない」という返事です。AtMostOne2 の中身（有限型についての ∀ と自然数の不等式）はどれも判定できるのに、def の名前で包んだところで探索が止まっています。直し方は、名前を開いてから探索を掛ける実例を一つ足すことだけです。

/-- `def` の中を開いてから実例探索を掛ける。 -/
instance instDecidableAtMostOne2 (I : Fin 2 → (Fin 2 → Bool) → Bool) :
    Decidable (AtMostOne2 I) := by
  unfold AtMostOne2; infer_instance

これを足すと by decide が通ります。元の Perfect にも同じ形の一行が付いています。

instance instDecidablePerfect (I : Fin d → V d → Bool) : Decidable (Perfect I) := by
  unfold Perfect; infer_instance

教訓は一行です。def … : Prop で名前を付けた述語を decide に載せるなら、判定の実例を自分で用意します。abbrev で書けば中が見えるので実例は要りませんが、そのぶん言明の表示が長くなります。

もう一つ、decide が「調べた結果、偽だった」と言う場合の文面も見ておきます。∀ b : Bool, b = true を渡すと次が出ます。

error: Tactic `decide` proved that the proposition
  ∀ (b : Bool), b = true
is false

この二つの文面は区別して読みます。前者は「判定の方法が無い」、後者は「判定して偽だった」です。前者は定義の書き方の問題、後者は主張そのものの問題で、直す場所が違います。

decide は魔法ではなく、次の三つを順に行います。

1. 判定の手続きを見つける。主張 P に対する Decidable P の実例を探索で組み立てます。有限型についての ∀ は「全要素を並べて全部調べる」手続きに、自然数の等式は「両辺を計算して比べる」手続きになります。
2. その手続きを kernel で走らせる。Lean の kernel（信頼する最小の部分）が、組み立てた手続きを定義に従って評価します。perfect_I4 なら、方向の順序対 12 通り × 位置 16 通りを全部当てて、条件を満たす 24 枚のプラケットで和が 1 であることを確かめます。
3. 結果が真なら証明に変える。「判定の手続きが真を返した」ことから元の主張を得る補題（of_decide_eq_true）を当てます。

この道の芯になっている補題は、真偽値 12 個についての全数判定です。

/-- 3 次元の部分立方体の 6 枚の面の「ちょうど一本」から、方向 `μ` の 4 辺のうち
ちょうど一本が族に入る。`2^12 = 4096` 通りの有限判定。 -/
theorem cube3_bool : ∀ m00 m01 m10 m11 n00 n01 n10 n11 l00 l01 l10 l11 : Bool,
    m00.toNat + m10.toNat + n00.toNat + n10.toNat = 1 →
    m01.toNat + m11.toNat + n01.toNat + n11.toNat = 1 →
    m00.toNat + m01.toNat + l00.toNat + l10.toNat = 1 →
    m10.toNat + m11.toNat + l01.toNat + l11.toNat = 1 →
    n00.toNat + n01.toNat + l00.toNat + l01.toNat = 1 →
    n10.toNat + n11.toNat + l10.toNat + l11.toNat = 1 →
    m00.toNat + m01.toNat + m10.toNat + m11.toNat = 1 := by decide

LeanPerfectFamily.cube3_bool。仮定の 6 本は 3 次元の部分立方体の 6 枚の面で、m が方向 μ の 4 辺・n が ν の 4 辺・l が lam の 4 辺です。3 次元のところで有限判定を一枚挟むと、そこから先は一般の次元 d について証明が進みます。「有限に落として decide、落とせない部分は手で」という分け方の、いちばん分かりやすい形です。

4096 通りは一瞬です。では、どこから重くなるか。真偽値 n 個についての全数判定を、n を動かして測りました。地の 5 秒（import Mathlib の読み込み）を引いた値です。

計算この端末（4 コア・RAM 15 GB）での実測。20 個のときに出るのは次の文面です。

error: (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached

Note: Use `set_option maxHeartbeats <num>` to set the limit.

set_option maxHeartbeats 0 で打ち切りを外せば通ります。目安は「場合の数が十万までは秒、百万からは分」です。

ただし場合の数だけでは決まりません。同じ 2^n 通りでも、「真偽値 n 個の ∀」ではなく「関数 Fin n → Bool 全部の ∀」の形にすると、この端末では n = 14（16,384 通り）で約 2 分かかりました。関数を一つずつ組み立てる手間が場合ごとに乗るためです。重いときは、場合の数ではなく「一件あたり何を計算しているか」を先に見ます。

もう一つ、深さの設定に当たることがあります。

set_option maxRecDepth 100000

再帰の深さの上限で、上限に当たると「maximum recursion depth has been reached」と出ます。こちらは計算量ではなく設定の問題なので、上げれば通ります。時間の打ち切り（heartbeats）と深さの打ち切り（recDepth）は別のものです。

by decide で通った、というだけでは安心の根拠になりません。条件を壊した族について「満たさない」が出ることも確かめます。満たさない側が出ないなら、条件が空虚に真だった（たとえば調べるべきプラケットが一枚も無かった）疑いが残ります。

/-- 陰性対照：空の族は完全でない（`d = 3`）。 -/
theorem not_perfect_empty3 : ¬ Perfect (fun (_ : Fin 3) (_ : V 3) => false) := by decide

/-- 陰性対照：全部の辺をとった族は完全でない（`d = 3`）。 -/
theorem not_perfect_full3 : ¬ Perfect (fun (_ : Fin 3) (_ : V 3) => true) := by decide

/-- 陰性対照：`I4` の方向 0 を全部に替えると完全でなくなる（`d = 4`）。 -/
theorem not_perfect_I4_broken :
    ¬ Perfect (fun (μ : Fin 4) (x : V 4) => if μ = 0 then true else I4 μ x) := by decide

LeanPerfectFamily.not_perfect_empty3・not_perfect_full3・not_perfect_I4_broken。三つめが効いています。通った族の一方向だけを壊すと落ちるのだから、判定は族の中身を実際に読んでいます。

検査は一つのファイルを Lean に通すだけです。

lake env lean PerfectFamily.lean

498 行・エラー 0・警告 0・約 7 秒。証明が何に依拠しているかは #print axioms がそのまま出します。

#print axioms PerfectFamily.cube3_bool
#print axioms PerfectFamily.perfect_I4
#print axioms PerfectFamily.not_perfect_I4_broken

'PerfectFamily.cube3_bool' does not depend on any axioms
'PerfectFamily.perfect_I4' depends on axioms: [propext, Classical.choice, Quot.sound]
'PerfectFamily.not_perfect_I4_broken' depends on axioms: [propext, Classical.choice, Quot.sound]

読み方を三点。

• propext・Classical.choice・Quot.sound は Lean と mathlib の標準三公理で、普通の数学がその上に立っています。この三つ以外が出ていないことが確かめたい点です（Lean とは何か）。
• cube3_bool は公理をまったく使っていません。真偽値の全数判定は、計算の定義だけで閉じるからです。perfect_I4 に Classical.choice が出るのは、Fin d → Bool の数え上げ方を組み立てる途中で mathlib の道具を経由するためで、主張の強さには関わりません。
• 出てはいけないものが二つあります。sorryAx は未証明の穴（sorry と書いた箇所）、Lean.ofReduceBool は native_decide の痕跡です。

上の表の「7 分 11 秒」は native_decide なら一瞬ですが、そちらは判定の手続きを機械語にコンパイルして走らせ、その実行結果を信じます。信頼の置き場が kernel からコンパイラと実行環境に移るので、ここでは使いません（01）。速さが足りないときの別の手は Lean では現実的に厳しいものにあります。

perfect_I4 : Perfect I4 が言っているのは、次のことです。

I4 という式で決まる辺の選び方について、単位 4 立方体のすべての 2 次元の面で、面の 4 枠のうちちょうど一枠が選ばれている。

言っていないことを三つ挙げます。

• 「格子全体で」とは言っていません。頂点の型は Fin 4 → Bool であって Fin 4 → ℤ ではありません。I4 を周期 2 に延ばした族が格子全体で条件を満たすかは、別の型の別の言明（周期を仮定しない PerfectZ）になります。それも Lean にありますが、同じ定理ではありません——違いは 05 で並べます。
• 「他に無い」とは言っていません。これは存在の主張で、族の分類ではありません。
• 「4 枠」が「4 本の相異なる辺」であることは、この言明の外にあります。toNat の和で書いた時点で作った借りで、別の補題 face_slots_ne が返しています。その補題が無ければ、この定理は「和が 1」という計算の事実であって「ちょうど一本」という幾何の事実ではありません。

三つめが、機械検査でいちばん落としやすい種類の穴です。decide は書いた式について正しく答えますが、書いた式が言いたいことだったかは答えません。続きは 通っても、言いたいことが言えているかへ。

出典と再現

次は 04 数え上げを Finset で書く——同じ題材で「何本選べるか」を数えます。用語は 12 用語集。