数え上げを Finset で書く — 二重数え上げを写すと何が出てくるか

どのプラケット（単位正方形）もちょうど一本を含むように格子の辺を選ぶと、選ばれた辺は辺全体のどれだけか。

03 でそういう選び方が 4 次元に在ることを確かめ、05 で「高々一本」なら本数が頂点の数以下だと分かりました。ここでは比率を出します。答えはちょうど 1/4 で、次元にも周期の大きさにも依りません。

道具は二重数え上げ——同じものを二通りに数えて等式を作る、組合せのいちばん基本の手です。その基本の手を Lean に写すと何が起きるかが、このページの中身です。格子の上の場の理論で強結合域の定数を見積もるときに出てくる組合せで、連続極限や質量ギャップ——ミレニアム問題の本体——への主張はありません。

数えるのは「（選ばれた辺 e、e を含むプラケット p）の組」です。

プラケットの側から数える。どのプラケットもちょうど一本を含むので、組の数はプラケットの枚数に等しい。方向の組が d(d−1)/2 通り、基点が L^d 通りなので、枚数は d(d−1)L^d/2 です。

辺の側から数える。方向 μ・始点 x の辺は、もう一つの方向 ν ≠ μ を選ぶごとに、その方向へのプラケット 2 枚（x を基点にするものと x − e_ν を基点にするもの）に含まれます。ν の選び方が d−1 通りなので、辺 1 本あたり 2(d−1) 枚。組の数は 2(d−1)|I| です。

二つを等号で結んで整理すると、こうなります。

紙では 5 行です。Lean に写すときに引っかかるのは、この 5 行のうち「d−1」と「プラケット 2 枚」の二箇所です。

頂点を Fin d → ZMod L にする

和を取るので頂点は有限でなければなりません。ZMod L は「L で割った余り」の型で、Fin d → ZMod L は周期 L のトーラスです。選んだ理由は、平行移動 x ↦ x + e_ν が全単射になることです。有限の箱にすると縁で平行移動が外へ出てしまい、数え上げが縁の補正だらけになります。

プラケットを「順序対と基点」で数える

紙ではプラケットを「方向の組 {μ, ν}（無順序）と基点」で数え、d(d−1)/2 という因子が出ました。Lean では順序対 (μ, ν)（μ ≠ ν）と基点で数えます。同じプラケットを 2 回数えることになりますが、両辺が同じだけ 2 倍になるので結論は変わりません。

得るものは対称性です。無順序の組で書くと Finset (Fin d) の濃度 2 の部分集合を走ることになり、和の付け替えのたびに「どちらが μ か」の場合分けが出ます。順序対なら ∑ μ, ∑ ν ∈ univ.erase μ——「全部の μ について、μ 以外の全部の ν について」——と素直に書けます。

プラケットの中の本数に名前を付ける

数え上げの主役は「一枚のプラケットに入っている本数」なので、それを定義にします。

/-- プラケット `(x; μ, ν)` の 4 辺のうち `I` に入っている本数。 -/
def plaqCount (I : Fin d → Wp d L → Bool) (μ ν : Fin d) (x : Wp d L) : ℕ :=
  (I μ x).toNat + (I μ (shiftp x ν)).toNat + (I ν x).toNat + (I ν (shiftp x μ)).toNat

/-- 方向 `μ` の辺の本数。 -/
def dirCount [NeZero L] (I : Fin d → Wp d L → Bool) (μ : Fin d) : ℕ :=
  ∑ x : Wp d L, (I μ x).toNat

これで仮定が読みやすい形に言い換わります。名前を付け替えただけなので、証明は Iff.rfl（定義から同じ）です。

theorem atMostOne_iff_plaqCount (I : Fin d → Wp d L → Bool) :
    AtMostOne I ↔ ∀ μ ν : Fin d, μ ≠ ν → ∀ x : Wp d L, plaqCount I μ ν x ≤ 1 := Iff.rfl

theorem perfectP_iff_plaqCount (I : Fin d → Wp d L → Bool) :
    PerfectP I ↔ ∀ μ ν : Fin d, μ ≠ ν → ∀ x : Wp d L, plaqCount I μ ν x = 1 := Iff.rfl

LeanPlaquetteCounting.plaqCount・dirCount・atMostOne_iff_plaqCount・perfectP_iff_plaqCount。証明が Iff.rfl の補題は、読み手のためだけに在ります。あとの証明で「仮定 AtMostOne I は plaqCount ≤ 1 のことだ」を確かめずに読めるので、書いておく価値があります。

紙の証明に出てくる 2(d−1)|I| を、そのまま自然数で書くと危ないことになります。自然数の引き算は 0 で止まります。

/-- 自然数の引き算は 0 で止まる。 -/
example : (2 : ℕ) - 3 = 0 := by decide

これは Lean の欠陥ではなく、自然数の型で引き算を全域の関数にするための決めごとです。困るのは、d − 1 と書いた式が d = 0 のときに黙って 0 になり、証明したい等式が「成り立つけれど中身が無い」状態になりうることです。整数に移せば済みますが、濃度は自然数なので移すたびに型変換が増えます。

ここでとった手は、引き算を式に出さない形に言明を書き換えることです。S = 4(d−1)N ではなく S + 4N = 4dN と書きます。

/-- **恒等式（本体）**：プラケットの中の `I` の本数を順序対 `(μ,ν)` と基点 `x` で総和すると
`4(d−1)|I|`（引き算を避けた形 `S + 4|I| = 4d|I|`）。**`I` に仮定は要らない。** -/
theorem sum_plaqCount_add [NeZero L] (I : Fin d → Wp d L → Bool) :
    (∑ μ : Fin d, ∑ ν ∈ Finset.univ.erase μ, ∑ x : Wp d L, plaqCount I μ ν x)
      + 4 * (edgeSet I).card = 4 * d * (edgeSet I).card

この形にすると、d = 0 でも d = 1 でも言明が正しく、しかも意味を失いません（両辺が 0 になるだけです）。等式から |I| を取り出す段は、算術の補題として切り出します。

/-- 補助（自然数の算術）：`S + u = n·u` と `S + v = n·v` なら `u = v`（`n ≥ 2`）。 -/
theorem eq_of_add_eq_mul {S u v n : ℕ} (hn : 2 ≤ n) (hu : S + u = n * u) (hv : S + v = n * v) :
    u = v

/-- 補助（自然数の算術）：`S + u = n·u`・`W + v = n·v`・`S ≤ W` なら `u ≤ v`（`n ≥ 2`）。 -/
theorem le_of_add_eq_mul {S W u v n : ℕ} (hn : 2 ≤ n) (hu : S + u = n * u) (hv : W + v = n * v)
    (hSW : S ≤ W) : u ≤ v

LeanPlaquetteCounting.sum_plaqCount_add・eq_of_add_eq_mul・le_of_add_eq_mul。n ≥ 2 という仮定がここに集まりました。紙の d−1 で割る操作が、Lean では「d ≥ 2 を仮定した算術の補題」として姿を現します。どこで d ≥ 2 を使ったかが、証明を読まなくても仮定欄で分かる形です。

紙の証明のもう一つの引っかかりは「辺 1 本あたりプラケット 2 枚」です。周期 L = 2 の格子では x + e_ν と x − e_ν が同じ点なので、「2 枚」が実は 1 枚に潰れているのではないかと疑う必要があります。

答えは潰れません。ただし理由は「2 枚が相異なるから」ではなく、数え方が枚数を経由していないからです。Lean の証明は、辺ごとにプラケットを数えるのではなく、和の側を平行移動で写します。

/-- `x ↦ x + e_ν` は `(ZMod L)^d` の上の全単射（逆は `x ↦ x − e_ν`）。 -/
theorem shiftp_bijective [NeZero L] (ν : Fin d) :
    Function.Bijective (fun x : Wp d L => shiftp x ν)

/-- 平行移動での添字の付け替え：`∑_x f(x + e_ν) = ∑_x f(x)`。 -/
theorem sum_shiftp [NeZero L] (f : Wp d L → ℕ) (ν : Fin d) :
    ∑ x : Wp d L, f (shiftp x ν) = ∑ x : Wp d L, f x :=
  Fintype.sum_bijective _ (shiftp_bijective ν) _ _ (fun _ => rfl)

使っているのは「x ↦ x + e_ν が全単射」だけです。L の大きさに条件は要りません。L = 2 では平行移動が対合（二度やると戻る）になりますが、全単射であることは変わらないので、和の付け替えは同じように通ります。

これは Lean の都合で選んだ道ではなく、紙の証明の穴を塞いだ結果です。「各辺が 2(d−1) 枚のプラケットに含まれる」という言い方は、枚数が相異なることを暗に使っています。和の付け替えに書き換えると、その暗黙の仮定が要らなくなります。

/-- **枠の数え直し**：一つのプラケットの 4 枠を `x` 全体で足すと `2·(方向 μ) + 2·(方向 ν)`。
平行移動の全単射だけを使うので `L = 2` でも同じ。 -/
theorem sum_x_plaqCount [NeZero L] (I : Fin d → Wp d L → Bool) (μ ν : Fin d) :
    ∑ x : Wp d L, plaqCount I μ ν x = 2 * dirCount I μ + 2 * dirCount I ν

/-- **(2) 数え上げの上界**：どのプラケットも高々一本なら `4|I| ≤ d·L^d`（密度 `≤ 1/4`）。 -/
theorem four_mul_card_le [NeZero L] {I : Fin d → Wp d L → Bool} (h : AtMostOne I) (hd : 2 ≤ d) :
    4 * (edgeSet I).card ≤ d * L ^ d

/-- **(1) 完全な族の密度はちょうど `1/4`**：`4|I| = d·L^d`。 -/
theorem four_mul_card_eq [NeZero L] {I : Fin d → Wp d L → Bool} (h : PerfectP I) (hd : 2 ≤ d) :
    4 * (edgeSet I).card = d * L ^ d

/-- **系（割り切れ条件）**：完全な族が在れば `4 ∣ d·L^d`。 -/
theorem four_dvd_of_perfect [NeZero L] {I : Fin d → Wp d L → Bool} (h : PerfectP I) (hd : 2 ≤ d) :
    4 ∣ d * L ^ d

有理数の形も入れてあります。こちらが「密度ちょうど 1/4」の字面どおりの言明です。

theorem density_eq_quarter [NeZero L] {I : Fin d → Wp d L → Bool} (h : PerfectP I) (hd : 2 ≤ d) :
    ((edgeSet I).card : ℚ) / ((d : ℚ) * (L : ℚ) ^ d) = 1 / 4

LeanPlaquetteCounting.sum_x_plaqCount・four_mul_card_le・four_mul_card_eq・four_dvd_of_perfect・density_eq_quarter。自然数の形と有理数の形を両方置くのは、前者が後の証明で使いやすく、後者が読み手に意味が伝わるからです。

割り切れ条件は副産物ですが、独立に働きます。d = 3・L = 3 なら 4 ∤ 3·27 = 81 なので完全な族はありません——これは 05 の d ≤ 4 では落ちない枡です。逆に d = 5・L = 2 は 4 ∣ 160 を満たすので割り切れでは落ちず、d ≤ 4 の側で落ちます。二つの系は互いに他方を含みません。

枠の数え直し

theorem sum_x_plaqCount [NeZero L] (I : Fin d → Wp d L → Bool) (μ ν : Fin d) :
    ∑ x : Wp d L, plaqCount I μ ν x = 2 * dirCount I μ + 2 * dirCount I ν := by
  have h1 : (∑ x : Wp d L, (I μ (shiftp x ν)).toNat) = ∑ x : Wp d L, (I μ x).toNat :=
    sum_shiftp (fun y => (I μ y).toNat) ν
  have h2 : (∑ x : Wp d L, (I ν (shiftp x μ)).toNat) = ∑ x : Wp d L, (I ν x).toNat :=
    sum_shiftp (fun y => (I ν y).toNat) μ
  simp only [plaqCount, dirCount]
  rw [Finset.sum_add_distrib, Finset.sum_add_distrib, Finset.sum_add_distrib, h1, h2]
  ring

• have h1 … / have h2 … — 平行移動した項の和を、移動しない和に等しいと先に用意します。4 枠のうち 2 枠が平行移動を含むので、2 本要ります。
• simp only [plaqCount, dirCount] — 名前を定義に戻します。simp ではなく simp only にしているのは、余計な整理が入って形が変わると、次の rw が当たらなくなるからです。
• rw [Finset.sum_add_distrib, …, h1, h2] — 「和の和は和の和」で 4 項に分け、そのうち 2 項を h1・h2 で書き換えます。sum_add_distrib が 3 回出るのは、4 項を分けるのに 3 回割るからです。
• ring — 残った a + a + b + b = 2a + 2b を整理します。

紙の「辺 1 本あたり 2 枚」が、ここでは「4 項のうち 2 項を平行移動で写す」になりました。枚数の話が和の話に変わったので、周期の大きさが出てきません。

非対角の和 — d−1 を出さずに潰す

∑ μ, ∑ ν ≠ μ の内側を足し上げる段が、この証明でいちばん手が掛かります。効くのは Finset.sum_erase_add——「一点を外した和にその一点を足すと全体の和」という補題です。手元で短い形を確かめます。

/-- 一点を外した和に、その一点を足すと、全体の和になる。
`d − 1` を書かずに `d` 倍の形にできるのは、この補題が効くため。 -/
example {n : ℕ} (A : Fin n → ℕ) (μ : Fin n) :
    (∑ _ν ∈ Finset.univ.erase μ, A μ) + A μ = n * A μ := by
  rw [Finset.sum_erase_add _ _ (Finset.mem_univ μ), Finset.sum_const, Finset.card_univ,
    Fintype.card_fin, smul_eq_mul]

• Finset.sum_erase_add _ _ (Finset.mem_univ μ) — 左辺を「全体についての和」に直します。ここで μ が全体に入っていること（Finset.mem_univ μ）を渡します。
• Finset.sum_const — ν に依らない項の和は「個数 × 項」です。
• Finset.card_univ・Fintype.card_fin — 「個数」を n に直します。
• smul_eq_mul — Finset.sum_const が出す作用（•）を普通の掛け算に直します。

五つの書き換えで、d − 1 が一度も出ないまま d 倍の形になりました。本体の補題（sum_erase_two）はこれを二回——ν に依らない項と ν の項に分けて、それぞれに——使っています。

ここは Finset.sum_comm（和の順序の交換）では通りません。非対角の和は ν の範囲が μ に依るので、素直に交換すると範囲の条件が残ります。「一点を外す・一点を足す」に持ち込むほうが、範囲の依存を最初から消せます。

恒等式が本当にその値を出すかを、いちばん小さい枡で見ます。d = 2・周期 4 の格子で、方向 0・x 1 = 0 の 4 本の辺（閉じた一直線）をとります。恒等式の値は 4(d−1)|I| = 4 · 1 · 4 = 16 のはずです。

import Mathlib

/-- 周期格子 `(ZMod L)^d` の頂点。 -/
abbrev Wp (d L : ℕ) : Type := Fin d → ZMod L

/-- 第 `i` 座標を 1 だけ進める。 -/
def shiftp {d L : ℕ} (x : Wp d L) (i : Fin d) : Wp d L := Function.update x i (x i + 1)

/-- プラケット `(x; μ, ν)` の 4 辺のうち `I` に入っている本数。 -/
def plaqCount {d L : ℕ} (I : Fin d → Wp d L → Bool) (μ ν : Fin d) (x : Wp d L) : ℕ :=
  (I μ x).toNat + (I μ (shiftp x ν)).toNat + (I ν x).toNat + (I ν (shiftp x μ)).toNat

/-- `d = 2`・周期 4 の格子で、方向 0・`x 1 = 0` の 4 本の辺。 -/
def Line (μ : Fin 2) (x : Wp 2 4) : Bool := (μ == 0) && (x 1 == 0)

/-- 辺は 4 本。 -/
example : (Finset.univ.filter (fun p : Fin 2 × Wp 2 4 => Line p.1 p.2 = true)).card = 4 := by
  decide

/-- 二重数え上げの値：`4(d−1)|I| = 4 · 1 · 4 = 16`。 -/
example : (∑ μ : Fin 2, ∑ ν ∈ Finset.univ.erase μ, ∑ x : Wp 2 4, plaqCount Line μ ν x) = 16 := by
  decide

Lean手元で検査して通ったもの。decide が和を実際に計算して 16 を出します（03 と同じ道具です）。恒等式を証明したあとに、その恒等式の値を別の道（kernel の計算）で確かめるのが、この一行の役目です。証明の側と計算の側の両方が同じ数を出せば、言明の書き間違いは相当に絞られます。

同じ形の陽性対照が本体にも入っています（sum_plaq_Line）。陰性対照も一本。全部の辺をとった族は上界を破る、という形で「仮定が働いている」ことを確かめます。

/-- 陰性対照：全部の辺を採る族（`d=2`・`L=4`）は上界を破る。
`4·32 = 128 > 32 = 2·4^2` ⟹ 仮定 `AtMostOne` は働いている。 -/
theorem full_violates_bound :
    ¬ (4 * (edgeSet (fun (_ : Fin 2) (_ : Wp 2 4) => true)).card ≤ 2 * 4 ^ 2) := by
  decide

lake env lean PlaquetteCounting.lean

864 行・エラー 0・警告 0・約 9 秒。公理の出力から数本を抜きます。

'PlaquetteCounting.shiftp_bijective' depends on axioms: [propext, Classical.choice, Quot.sound]
'PlaquetteCounting.sum_shiftp' depends on axioms: [propext, Classical.choice, Quot.sound]
'PlaquetteCounting.eq_of_add_eq_mul' depends on axioms: [propext, Quot.sound]
'PlaquetteCounting.sum_plaqCount_add' depends on axioms: [propext, Classical.choice, Quot.sound]
'PlaquetteCounting.four_mul_card_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'PlaquetteCounting.density_eq_quarter' depends on axioms: [propext, Classical.choice, Quot.sound]

すべて標準三公理の内側で、sorryAx と Lean.ofReduceBool はありません。算術の補題 eq_of_add_eq_mul に Classical.choice が出ていないのが読みどころです。§04 で切り出した「等式から |I| を取り出す」段は、選択公理を使わずに閉じています。

four_mul_card_eq が言っているのは次のことです。

周期 L の格子 (ZMod L)^d（d ≥ 2・L ≥ 1）の上の族 I が「どのプラケットもちょうど一本」を満たすなら、4 · |I| = d · L^d が成り立つ。

言っていないことを三つ。

• 「そういう族が在る」とは言っていません。条件つきの等式で、条件を満たす族が無い枡（たとえば d = 5）でも正しく成り立ちます。「密度はちょうど 1/4」と書くと在るように読めますが、言明は「在れば」です。在ることは 03 の具体例が別に示しています。
• d ≥ 2 は落とせません。d = 1 ではプラケットが一枚も無いので条件が空虚に真になり、全部の辺が採れて等式は破れます。仮定欄の 2 ≤ d はそこに効いています。
• 「辺」は「方向と始点の組」です。05 と同じ借りで、Finset (Fin d × 頂点) の要素を数えています。これが格子の辺と一対一であることは、言明には入っていません。

一つめが、この種の等式でいちばん読み違えやすいところです。条件つきの等式は、条件が満たされない枡でも真になります。存在と併せて読まないと、言っていないことを言ったように見えます。続きは 通っても、言いたいことが言えているかへ。

出典と再現

次は 05 単射一本で上界を出す——同じ題材を、和を使わずに閉じます。用語は 12 用語集。