単射一本で上界を出す — 紙の二行が Lean でも短いままか

格子の辺を、どのプラケット（単位正方形）も高々一本しか含まないように選ぶとき、辺は何本まで選べるか。

03 と同じ題材です。あちらは「ちょうど一本」の族が在るかを有限判定で確かめました。ここでは条件を「高々一本」に緩めて、選べる本数の上限を出します。上限を出す道具は一つだけ——単射です。

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

選ばれた辺は「方向 μ と始点 x」の組で表せます。この組に始点 x だけを対応させます。

もし同じ始点 x から二つの方向 μ ≠ ν に辺が出ていたら、その 2 本は同じプラケット (x; μ, ν) の 2 辺です。プラケットは高々一本しか含まないので、これは起こりません。つまり対応は単射で、選ばれた辺の本数は頂点の数以下です。

辺の総数は「方向の数 × 頂点の数」なので、密度でいえば 1/d 以下という意味になります。紙で二行です。短い証明が Lean でも短いままかどうかが、このページで見たいことです。

頂点の型を決めずに書く

紙の証明は「格子」の性質をほとんど使っていません。使うのは「方向 i に一歩進める」という写像があることだけです。そこで、頂点の型を X のまま・一歩進める写像を sh のままにして書きました。

こうすると、周期の格子 (ZMod L)^d と無限格子 ℤ^d の両方に同じ補題が使えます。頂点の型を ZMod L に決めて書くと、ℤ^d の版でもう一度同じ証明を書くことになります。証明が何を使っているかを見て、使っていないものを型から外すのが、二度書かないための手です。

「マッチング」と言わない

紙で考えているときは「選ばれた辺はマッチング（どの二本も頂点を共有しない）になる」と言いたくなります。これは格子全体では偽です。同じ方向に一直線に並ぶ 2 本 (μ, x) と (μ, x + e_μ) は頂点 x + e_μ を共有しますが、共通のプラケットには載らないので、いくらでも繋げられます。

言えるのは「各頂点で正の向きの辺は高々一本」であり、上界にはそれで足ります。この区別を確かめるために、実際に繋がった例を Lean に入れてあります。

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

theorem Line_atMostOne : AtMostOne Line := by decide

/--
**`I` はマッチングでない**：`Line` には頂点を共有する二辺（一直線に並ぶ `(0, x)` と `(0, x+e_0)`）
が在る。紙の証明が「単位立方体に切ってからマッチング」と言っていたのは、まさにこのため。
-/
theorem Line_not_matching : ∃ x : Wp 2 4, Line 0 x = true ∧ Line 0 (shiftp x 0) = true := by
  decide

LeanPlaquettePacking.Line_atMostOne・PlaquettePacking.Line_not_matching。「高々一本」を満たしながらマッチングでない族が実在するので、紙の言葉づかいの方を直すことになります。

辺の集合を Finset の filter で作る

族は 03 と同じく Bool 値の関数 I です。本数を数えるにはそれを Finset に直す必要があるので、Fin d × 頂点 の全体から条件で絞ります。

/-- `I` の辺の集合（`Fin d × 頂点` の部分集合）。 -/
def edgeSet [NeZero L] (I : Fin d → Wp d L → Bool) : Finset (Fin d × Wp d L) :=
  Finset.univ.filter (fun p => I p.1 p.2 = true)

[NeZero L] は「L は 0 でない」という仮定です。ZMod 0 は ℤ そのもので有限でないため、これが無いと Finset.univ が作れません。型の側に仮定が付く形で、紙では書かない類の条件です。

/--
`Packing sh I`：頂点の型 `X`・「方向 `i` に一歩進める」写像 `sh` を持つ格子の上で、
辺の族 `I : Fin d → X → Bool`（`I μ x` は `x` から `sh x μ` への辺）が
**どのプラケットも高々一本しか含まない**。

プラケット `(x; μ, ν)` の 4 辺は `(μ, x)`・`(μ, sh x ν)`・`(ν, x)`・`(ν, sh x μ)`。
-/
def Packing (sh : X → Fin d → X) (I : Fin d → X → Bool) : Prop :=
  ∀ μ ν : Fin d, μ ≠ ν → ∀ x : X,
    (I μ x).toNat + (I μ (sh x ν)).toNat + (I ν x).toNat + (I ν (sh x μ)).toNat ≤ 1

紙の二行が、そのまま三つの補題になります。

/-- **芯（一方向性）**：`I` の辺が一つの頂点から二方向へ出ることはない。 -/
theorem not_two_dirs {sh : X → Fin d → X} {I : Fin d → X → Bool} (h : Packing sh I)
    {μ ν : Fin d} (hμν : μ ≠ ν) {x : X} (hμ : I μ x = true) (hν : I ν x = true) : False

/-- 写像 `(μ, x) ↦ x` は `I` の辺の集合の上で単射。 -/
theorem snd_injOn {sh : X → Fin d → X} {I : Fin d → X → Bool} (h : Packing sh I)
    {p q : Fin d × X} (hp : I p.1 p.2 = true) (hq : I q.1 q.2 = true) (hpq : p.2 = q.2) :
    p = q := by
  by_cases hd : p.1 = q.1
  · exact Prod.ext hd hpq
  · exact absurd (not_two_dirs h hd hp (hpq ▸ hq)) id

周期格子に降ろすと、頂点の数が L^d と書けます。

/--
**主定理**：どのプラケットも高々一本しか含まない族の辺の本数は、頂点の数 `L^d` 以下。
-/
theorem card_edgeSet_le [NeZero L] {I : Fin d → Wp d L → Bool} (h : AtMostOne I) :
    (edgeSet I).card ≤ L ^ d := by
  have := card_le_card_vertices (X := Wp d L) (sh := shiftp) h
  rwa [card_Wp] at this

LeanPlaquettePacking.not_two_dirs・snd_injOn・card_le_card_vertices・card_edgeSet_le。周期を仮定しない版もあります——有限の箱 S の中から出る辺は高々 |S| 本という形です。

/--
**箱の版**：`ℤ^d` のパッキング `J` の辺が有限集合 `S` の頂点からしか出ていないなら、
そのような辺は高々 `|S|` 本。（`S` は箱でも何でもよい。周期性を仮定しない。）
-/
theorem card_le_of_support [DecidableEq (Wz d)] {J : Fin d → Wz d → Bool} (h : AtMostOneZ J)
    (S : Finset (Wz d)) (T : Finset (Fin d × Wz d))
    (hT : ∀ p ∈ T, J p.1 p.2 = true ∧ p.2 ∈ S) : T.card ≤ S.card

芯の補題

theorem not_two_dirs {sh : X → Fin d → X} {I : Fin d → X → Bool} (h : Packing sh I)
    {μ ν : Fin d} (hμν : μ ≠ ν) {x : X} (hμ : I μ x = true) (hν : I ν x = true) : False := by
  have hle := h μ ν hμν x
  rw [hμ, hν] at hle
  simp only [Bool.toNat_true] at hle
  omega

四行です。何をしているか。

• have hle := h μ ν hμν x — 仮定「どのプラケットも高々一本」を、方向の組 (μ, ν) と基点 x に当てます。これで (I μ x).toNat + (I μ (sh x ν)).toNat + (I ν x).toNat + (I ν (sh x μ)).toNat ≤ 1 という不等式が手に入ります。
• rw [hμ, hν] at hle — 仮定から I μ x = true と I ν x = true が分かっているので、その二箇所を true に書き換えます。
• simp only [Bool.toNat_true] at hle — true.toNat を 1 に直します。不等式は 1 + a + 1 + b ≤ 1 の形になります。
• omega — 自然数の線形算術を解く tactic です。1 + a + 1 + b ≤ 1 は自然数では成り立たないので、矛盾（False）が出ます。

この四行が紙の「同じプラケットの 2 辺だから」に対応しています。紙では一言ですが、Lean では「仮定を当てる・値を入れる・形を整える・算術で潰す」の四段になります。増えているのは手数だけで、考えることは増えていません。

単射から濃度へ

theorem card_le_card_vertices [Fintype X] [DecidableEq X] {sh : X → Fin d → X}
    {I : Fin d → X → Bool} (h : Packing sh I) :
    (Finset.univ.filter (fun p : Fin d × X => I p.1 p.2 = true)).card ≤ Fintype.card X := by
  classical
  rw [← Finset.card_univ (α := X)]
  refine Finset.card_le_card_of_injOn (fun p => p.2) (fun p _ => Finset.mem_univ _) ?_
  intro p hp q hq hpq
  simp only [Finset.coe_filter, Finset.mem_univ, true_and, Set.mem_ofPred_eq] at hp hq
  exact snd_injOn h hp hq hpq

• classical — 決定可能性を気にせず場合分けできるようにします。上界の主張なので、計算できる形である必要がありません。
• rw [← Finset.card_univ …] — 右辺の「型 X の要素数」を「X の全体集合の濃度」に書き換えます。両辺を Finset の濃度に揃えるためです。
• Finset.card_le_card_of_injOn — ここが芯です。「集合 A から B への写像が A の上で単射なら |A| ≤ |B|」という mathlib の補題で、写像（fun p => p.2）と行き先が B に入ること、単射であることの三つを渡します。
• intro … / simp only … / exact snd_injOn … — 残った単射の証明を、上で作った補題に渡します。simp only の行は、Finset.filter の membership を「述語が真」の形に戻しているだけです。

七行です。紙の一行に対して、増えたのは「濃度の言葉に揃える」手続きだけでした。数え上げのような和の付け替えが要らないので、ここは短いままで済みます。

このページの上界（辺の本数 ≤ 頂点の数）と、04 の数え上げの等式（「ちょうど一本」の族なら 4·(辺の本数) = d·L^d）を並べると、次元が決まります。

/-- **主定理（二行）**：周期格子に完全な族が在れば `d ≤ 4`。 -/
theorem perfect_torus_d_le_four [NeZero L] {I : Fin d → Wp d L → Bool} (h : PerfectP I) :
    d ≤ 4 := by
  rcases Nat.lt_or_ge d 2 with hd | hd
  · omega
  have h1 : 4 * (edgeSet I).card = d * L ^ d := four_mul_card_eq h hd
  have h2 : (edgeSet I).card ≤ L ^ d := card_edgeSet_le (perfectP_atMostOne h)
  have hL : 0 < L ^ d := pow_pos (Nat.pos_of_ne_zero (NeZero.ne L)) d
  have h3 : d * L ^ d ≤ 4 * L ^ d := by
    rw [← h1]
    exact Nat.mul_le_mul_left 4 h2
  exact Nat.le_of_mul_le_mul_right h3 hL

LeanPlaquetteCounting.perfect_torus_d_le_four。中身は本当に二行です。d·L^d = 4·|I| ≤ 4·L^d を L^d > 0 で割るだけで、d ≤ 1 の場合は結論が自明なので omega が片付けます。

二つの上界の住み分けも数で見えます。このページの上界は密度 1/d、04 の上界は密度 1/4 で、d = 4 でちょうど一致します。d = 3・L = 2 では頂点の上界 8 より 04 の上界 6 が強く、d = 5・L = 2 では逆に 1/d の側が効きます。両方が Lean にあり、達成する族も入っています。

Leanすべて機械検査済み。上界が在ることと、その上界が達成されることは別の主張です。達成の側は具体的な族を書いて decide で確かめています（03 と同じ手順）。

「5 次元以上には『ちょうど一本』の族が無い」は、上の道とは別に、まったく違う道でも Lean に入っています。結論の文だけを見ると同じに見えますが、言明は違います。並べます。

/-- **定理（格子版）**：`d ≥ 5` の `ℤ^d` には完全な族が無い（周期性は仮定しない）。 -/
theorem no_perfectZ_of_five {d : ℕ} (hd : 5 ≤ d) (J : Fin d → W d → Bool) : ¬ PerfectZ J :=
  fun hJ => no_perfect_of_five hd _ (restrict_perfect hJ)

LeanPerfectFamily.no_perfectZ_of_five。どちらも他方を含みません。トーラス版は「周期 L の族」しか排除しないので、周期を持たない族について何も言いません。格子版は周期を仮定しませんが、道は長く、03 の有限判定を芯に据えて「方向 μ の辺の位置は 2 座標の外で一致すれば同じ辺」という最小距離の議論を通ります。

結論の文が同じでも、仮定と型が違えば別の定理です。片方を引いて他方の話をしないために、こういう表を先に作ります。言明の読み方そのものは 言明を読む手順にあります。

lake env lean PlaquetteCounting.lean

864 行・エラー 0・警告 0・約 9 秒。公理の出力はこうなります。

'PlaquettePacking.not_two_dirs' depends on axioms: [propext, Quot.sound]
'PlaquettePacking.snd_injOn' depends on axioms: [propext, Quot.sound]
'PlaquettePacking.card_le_card_vertices' depends on axioms: [propext, Classical.choice, Quot.sound]
'PlaquettePacking.card_edgeSet_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'PlaquettePacking.Line_not_matching' depends on axioms: [propext, Classical.choice, Quot.sound]

芯の二本（not_two_dirs・snd_injOn）に Classical.choice が出ていないのが見どころです。選択公理を使っていないことが、この二本については読み取れます。濃度の補題から先は classical を書いたので出ます。どちらも標準三公理の内側で、sorryAx と Lean.ofReduceBool はありません。

短い証明の側で確かめておくこと。この四行の補題は omega で終わっていますが、omega は公理を足しません。自然数と整数の線形算術を決定する手続きで、出す証明は Lean の中で組み立てられます。強い tactic を使うと公理が増えるのではないか、という心配は #print axioms がそのまま答えます。

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

周期 L の格子 (ZMod L)^d の上の族 I が「どのプラケットも高々一本」を満たすなら、I が選ぶ「方向と始点の組」の個数は L^d 以下である。

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

• 「この上界が達成される」とは言っていません。達成は別の主張で、d = 4, 5 では達成する族が在り（bound_tight_d4・bound_tight_d5）、d = 3 では達成されません。上界の定理は「ここより上は無い」だけを言い、「ここに届く」は言いません。
• 「辺の集合」が数えているのは「方向と始点の組」です。格子の辺を幾何的な対象として数えているのではなく、Fin d × 頂点 の部分集合の要素を数えています。この二つが一対一であることは、正の向きへの正規化から従いますが、言明そのものには入っていません。
• 周期を持たない族については何も言っていません。それが要るときは card_le_of_support（箱の版）か no_perfectZ_of_five（格子版）です。

二つめが、この種の形式化でいちばん見落としやすい借りです。数えている集合が、数えたかった対象と一対一かどうかは、濃度の定理の外にあります。続きは 通っても、言いたいことが言えているかへ。

出典と再現

次は 06 級数と不等式——有限の組合せから離れて、無限和を扱います。用語は 12 用語集。