こんにちは｜こんばんは。カエルのアイコンで活動しております @kyamaz です。
はじめに
1999年、NASA の火星探査機 Mars Climate Orbiter が火星の大気圏で失われました。原因は今でも語り草になっているようです。地上ソフトウェアの一部が力積をヤード・ポンド法（$lbf \cdot s$）で出力していたのに、受け取った側はそれを SI 単位（$N \cdot s$）だと思って読んでいた、というものです。単位の取り違え、たったそれだけで1億ドル超のミッションが消えたというエピソードです。
「長さと時間は足せない」というのは、日本の義務教育で小学３年生頃にはそんな感覚を身につけられるそうです。「エネルギーと力は等号で結べない」中高の理科（物理）でも、そういった感覚は養われます。物理量の次元が合っているかどうかのチェックは、いわば工学計算における型検査のようなものです。私たちは普段これを暗黙的にやっています。例えば、速さ＝距離÷時間は「はじき計算」として暗記している方も多いのではないでしょうか。
さて、この物理量の次元を数学として定式化して、機械に検証させてみようというのが今回の試みです。
本稿では、次の3つを順に見ていきます。
- 次元解析の数学的構造 — 物理量の次元の全体の構造は、数学におけるアーベル群（可換群）の構造をなしています。
- SI単位系 — 2019年に改定された現在の SI は「7つの定数を固定する」体系です。その定数の値と、そこから7つの基本単位が導かれる仕組みを確認します。
- バッキンガムのπ定理 — その正体は線形代数の『階数・退化次数の定理』です。 定理のステートメントとその証明を紹介します。
そして各トピックについて、定理証明支援系 Lean 4 による形式化を並べて眺めてみましょう。本稿の元にするのは、2025年9月にarXiv公開された論文『Formalizing Dimensional Analysis Using the Lean Theorem Prover（arXiv:2509.13142）1 』とその実装リポジトリです。
実装は全体で約1,000行と小さく、通読できるサイズなのが嬉しいところです。
なお、本稿では Lean の予備知識は仮定しません。コードは雰囲気だけ眺めていただいても内容は追えると思います。Lean の知識を深めた方であればより楽しめるかもしれません。また本稿は生成AIの支援を受けて書いていますが、内容は検証しており文責は私 
にあります。もし間違いなどお気づきの点がございましたら、ご指摘ください。
次元とは何か
物理量・次元・単位
物理量は「数値 × 単位」の形で表されます。$3.0 m$、$9.81 m/s^2$、$6.02 \times 10^{23} mol^{-1}$ といった具合です。ここで単位を張り替えても（$m$ を $ft$ にしても）、ものさしの違いによりその値は変わりますが、物理的な量の種類そのものは変わりません。この「単位の取り方によらない、量の種類」のことを次元（dimension）と呼びます。速度の次元は $\mathsf{L} \cdot \mathsf{T}^{-1}$、力の次元は $\mathsf{M} \cdot \mathsf{L} \cdot \mathsf{T}^{-2}$ です。
国際量体系（ISQ：International System of Quantities）では、7つの基本次元とその次元を表すための基本単位を、次表のように定義しています。
| 基本次元 | 記号 | 対応するSI基本単位 |
|---|---|---|
| 時間 | $\mathsf{T}$ | 秒 $s$ |
| 長さ | $\mathsf{L}$ | メートル $m$ |
| 質量 | $\mathsf{M}$ | キログラム $kg$ |
| 電流 | $\mathsf{I}$ | アンペア $A$ |
| 熱力学温度 | $\mathsf{\Theta}$ | ケルビン $K$ |
| 物質量 | $\mathsf{N}$ | モル $mol$ |
| 光度 | $\mathsf{J}$ | カンデラ $cd$ |
世の中のどんな物理量の次元も、これらのべき積 $\mathsf{T}^{\alpha} \mathsf{L}^{\beta} \mathsf{M}^{\gamma} \mathsf{I}^{\delta} \Theta^{\varepsilon} \mathsf{N}^{\zeta} \mathsf{J}^{\eta}$ の形に書けます。また、指数がすべて 0 の量を無次元と呼びます。
次元斉次性の原理
物理の等式には鉄則があります。両辺の次元が一致していなければならない、というものです。また sin や exp、log といった超越関数の引数（係数ではなく引数）は無次元でなければなりません。これを次元斉次性（dimensional homogeneity）の原理と呼びます。
$x = x_0 + vt + \frac{1}{2}at^2$ が意味を持つのは、各項がすべて次元 $\mathsf{L}$ を持っているからです。この原理は「物理法則は単位の選び方に依存しない」という要請から従います。後でπ定理を証明するときに、この要請を数学的に厳密な形（スケーリング不変性）で述べ直しますので、頭の隅に置いておいてください。
次元のなす代数構造
次元はアーベル群をなす
次元同士の演算規則を、少し丁寧に観察してみましょう。
- 乗法があります：$\mathsf{L} \times \mathsf{T}^{-1} = \mathsf{L}\mathsf{T}^{-1}$（←速度の例）
（指数同士は足されます） - 可換です：$\mathsf{L}\mathsf{T} = \mathsf{T}\mathsf{L}$
- 単位元があります：無次元「1」
- 逆元があります：$\mathsf{L}$ に対して $\mathsf{L}^{-1}$
つまり次元の全体は、乗法について 可換群（アーベル群） をなしています。さらに指数に注目すると、$\mathsf{T}^{\alpha}\mathsf{L}^{\beta}\cdots$ という次元は指数ベクトル $(\alpha, \beta, \dots) \in \mathbb{Q}^7$ と同一視できます。この同一視のもとで
- 次元の乗算 ⟷ ベクトルの加算
- 次元のべき乗 ⟷ スカラー倍
が対応しますから、次元の空間は $\mathbb{Q}$ 上のベクトル空間 $\mathbb{Q}^7$ と同型である、ということになります2。
この同一視が、実は次元解析のほとんど全てです。「次元の勘定」は指数ベクトルの線形代数にすぎず、後で扱うπ定理も、この見方からほとんど自動的に出てきます。
Lean で書いてみる
さて、この構造が Lean ではどう書かれるか見てみましょう。リポジトリの DimensionalAnalysis/Basic.lean を開くと、次元の定義がたった1行で書かれています。
-- 次元 = 基本次元の集合 B から指数の環 E への写像
def dimension (B : Type u) (E : Type v) [CommRing E] := B → E
次元とは、基本次元の集合 B から指数の環 E への関数である。先ほどの「次元＝指数ベクトル」をそのまま型にしたものです。基本次元の集合 B は抽象化されていて、ISQ の7次元は次のように帰納型として別に与えられます（ISQ.lean）。
inductive ISQ
| time | length | current | temperature | amount | luminosity | mass
【余談】ここで面白い記述があります。このプログラムには物理の7つの次元のほかに、通貨の基本次元クラスが定義されています。物理量の次元を語るときには必要ないですが、紛れて定義されているようです。
-- Here is a base dimension for currency class HasBaseCurrency (B : Type u) where [dec : DecidableEq B] Currency : B次元解析は物理量に限った理論ではなく「乗法で合成されるタグ付きの量」に適用できる一般の理論なのだということを、この実装自身が語っているように思われます。
さて次に演算の実装です。次元の乗法と除法は、その指数の加算・減算として定義されます。
protected def mul : dimension B E → dimension B E → dimension B E
| a, b => fun i => a i + b i
protected def div : dimension B E → dimension B E → dimension B E
| a, b => fun i => a i - b i
そして「次元はアーベル群をなす」という先ほどの主張は、Mathlib の CommGroup 型クラスのインスタンスとして、証明つきで宣言されています。
instance : CommGroup (dimension B E) where
mul := dimension.mul
div := dimension.div
inv a := dimension.pow a (-1)
one := dimensionless B E
mul_assoc := dimension.mul_assoc
mul_comm := dimension.mul_comm
one_mul := dimension.one_mul
mul_one := dimension.mul_one
div_eq_mul_inv a := dimension.div_eq_mul_inv a
inv_mul_cancel a := dimension.mul_left_inv a
-- npow / zpow などは省略
ここで各フィールドに埋めているのは、設定値ではなく証明項です。結合律・可換律・単位元・逆元、どれか一つでも証明できなければコンパイルが通りません。教科書的な「次元はアーベル群をなす」という事実が、ここでは機械検証済みのプログラムになっている、というわけです。
さて物理量そのものは、PhysicalVariables/Basic.lean で次のように定義されます。ここが一番の勘所です。
structure PhysicalVariable {B : Type u} {V : Type v} [Field V]
(dim : dimension B V) where
value : V
次元 dim が、フィールドではなく型のパラメータになっていることに注目してください。この設計と実装によって、「長さの物理量」PhysicalVariable (dimension.length B V) と「エネルギーの物理量」PhysicalVariable (dimension.energy B V) は、Lean にとっては別々の型になります。
その効果は演算の型に現れます。
-- 乗算：次元も掛け算されて、結果の型が決まる
protected def Mul {d1 d2 : dimension B V} :
PhysicalVariable d1 → PhysicalVariable d2 → PhysicalVariable (d1 * d2)
| a, b => PhysicalVariable.mk (a.value * b.value)
-- 加算：同じ次元 d 同士でしか定義されていない
protected def Add {d : dimension B V} :
PhysicalVariable d → PhysicalVariable d → PhysicalVariable d
| a, b => ⟨a.value + b.value⟩
乗算は「値を掛け、次元も掛ける」ですから「速度 × 時間」を計算すれば、結果の型に次元 $\mathsf{L}\mathsf{T}^{-1} \cdot \mathsf{T} = \mathsf{L}$ が自動的についてきます。そして加算は、同じ次元同士でしか型が定義されません。長さ ＋ 時間は書いた瞬間に型エラーとなります。つまり、次元斉次性の原理が、型として強制的に制約されることになります。
また固定の次元 $d$ の物理量が加法について群をなすことも、きちんと宣言されています。
instance {d : dimension B V} : AddCommGroup (PhysicalVariable d) where
add := PhysicalVariable.Add
add_assoc := PhysicalVariable.add_assoc
zero := 0
...
１つの物理次元ごとに１つの加法可換群がある、という構造です3。
SI単位系 — 定義定数から単位を導く
次元は物理量の「種類」を定めますが、実際に測るには単位、つまり各次元の基準量が必要です。それを定めるのが国際単位系（SI）です。
2019年5月に発効した SI の改定は、単位の定義方法を根本から変えました。それまでキログラムは「国際キログラム原器（パリ郊外に保管された合金の塊）の質量」でした。ところが現在の SI に、人工物は一切登場しません。代わりに、7つの物理定数の数値を厳密値として固定することが、そのまま単位の定義になっています。
次表が SI の7つの定義定数です。
| 定義定数 | 記号 | 固定された厳密値 |
|---|---|---|
| セシウム133の超微細遷移周波数 | $\Delta\nu_{\mathrm{Cs}}$ | 9 192 631 770 $\mathrm{Hz}$ |
| 真空中の光速 | $c$ | 299 792 458 $\mathrm{m/s}$ |
| プランク定数 | $h$ | 6.626 070 15 × $10^{-34}$ $\mathrm{J \cdot s}$ |
| 素電荷 | $e$ | 1.602 176 634 × $10^{-19}$ $\mathrm{C}$ |
| ボルツマン定数 | $k$ | 1.380 649 × $10^{-23}$ $\mathrm{J/K}$ |
| アボガドロ定数 | $N_A$ | 6.022 140 76 × $10^{23}$ $\mathrm{mol^{-1}}$ |
| 視感効果度（540 THz単色放射） | $K_{cd}$ | 683 $\mathrm{lm/W}$ |
ここで「固定」の意味に注意してください。これらは測定値ではありません。定義により誤差ゼロの厳密値です。改定前は「キログラム原器を基準にしてプランク定数 $h$ を測る」方向でしたが、改定後は「プランク定数 $h$ を厳密値と宣言し、そこから kg を定める」方向に逆転したこととなります。
7つの基本単位を導いてみる
定義定数の単位表現をほどいていくと、7つの基本単位が順に定まります。実際にやってみましょう。
a） 秒：$\Delta\nu_{\mathrm{Cs}} = 9\ 192\ 631\ 770\ \mathrm{Hz} = 9\ 192\ 631\ 770\ \mathrm{s}^{-1}$ ですから
$$1\ \mathrm{s} = \frac{9\ 192\ 631\ 770}{\Delta\nu_{\mathrm{Cs}}}$$
つまり「セシウム133の超微細遷移の周期の $9\ 192\ 631\ 770$ 倍」が$1$秒です。
b）メートル：$c = 299\ 792\ 458\ \mathrm{m/s}$ から
$$1\ \mathrm{m} = \frac{c}{299\ 792\ 458}\ \mathrm{s}$$
「光が $1/299\ 792\ 458$ 秒に進む距離」ですね。ここで一つ前に既に定まった秒を使っています。
c）キログラム：$h = 6.626\ 070\ 15 \times 10^{-34}\ \mathrm{J \cdot s} = 6.626\ 070\ 15 \times 10^{-34}\ \mathrm{kg\ m^2\ s^{-1}}$ から
$$1\ \mathrm{kg} = \frac{h}{6.626\ 070\ 15 \times 10^{-34}}\ \mathrm{m}^{-2}\ \mathrm{s}$$
d）アンペア：$e = 1.602\ 176\ 634 \times 10^{-19}\ \mathrm{C} = 1.602\ 176\ 634 \times 10^{-19}\ \mathrm{A \cdot s}$ から
$$1\ \mathrm{A} = \frac{e}{1.602\ 176\ 634 \times 10^{-19}}\ \mathrm{s}^{-1}$$
e）ケルビン：$k = 1.380\ 649 \times 10^{-23}\ \mathrm{J/K}$ から
$$1\ \mathrm{K} = \frac{1.380\ 649 \times 10^{-23}}{k}\ \mathrm{kg}\ \mathrm{m}^2\ \mathrm{s}^{-2}$$
f）モル：$N_A = 6.022\ 140\ 76 \times 10^{23}\ \mathrm{mol}^{-1}$ より、$1 mol$ は要素粒子がちょうど $6.022\ 140\ 76 \times 10^{23}$ 個の集まりです。
g）カンデラ：$K_{cd} = 683\ \mathrm{lm/W}$ から
$$1\ \mathrm{cd} = \frac{K_{cd}}{683}\ \mathrm{kg}\ \mathrm{m}^2\ \mathrm{s}^{-3}\ \mathrm{sr}^{-1}$$
導出の依存関係が「秒 → メートル → キログラム → …」と連なっているのがお分かりでしょうか。7つの定数の固定が、循環することなく7つの単位を一意に定めています。これは単位の定義集合としてよくできています。形式手法をやってみると、2019年の改定は SI のリファクタリングだったのだと感じます。
Lean で書いてみる
「定義＝定数の固定」という構造は、そのまま Lean の実装に反映できます。PhysicalVariables/Basic.lean の Units 名前空間を見てみましょう。秒の定義は次のようになっています。
def casesium133GroundStateHyperfineOscillationDuration {B : Type u} {V : Type v} [Field V] [HasBaseTime B] :
PhysicalVariable (dimension.time B V) := ⟨1⟩
def second (B : Type u) (V : Type v) [Field V] [HasBaseTime B] :
PhysicalVariable (dimension.time B V) :=
9192631770 • casesium133GroundStateHyperfineOscillationDuration
先ほどの「セシウム133の超微細遷移の周期の 9 192 631 770 倍」が、そのままコードになっています4。戻り値の型 PhysicalVariable (dimension.time B V) が「これは時間次元の量である」と宣言している点にも注目してください。
それ以外のSI単位系の定義も次のとおりです。
def meter (B : Type u) (V : Type v) [Field V] [HasBaseLength B] : PhysicalVariable (dimension.length B V) := ⟨1⟩
def kilogram (B : Type u) (V : Type v) [Field V] [HasBaseMass B] : PhysicalVariable (dimension.mass B V) := ⟨1⟩
def ampere (B : Type u) (V : Type v) [Field V] [HasBaseCurrent B] : PhysicalVariable (dimension.current B V) := ⟨1⟩
def kelvin (B : Type u) (V : Type v) [Field V] [HasBaseTemperature B] : PhysicalVariable (dimension.temperature B V) := ⟨1⟩
def mole (B : Type u) (V : Type v) [Field V] [HasBaseAmount B] : PhysicalVariable (dimension.amount B V) := ⟨1⟩
def candela (B : Type u) (V : Type v) [Field V] [HasBaseLuminosity B] : PhysicalVariable (dimension.luminosity B V) := ⟨1⟩
定義定数のほうは、次元がそのまま型に書き込まれます。
def SpeedOfLight (B : Type u) (V : Type v) [Field V] [HasBaseLength B] [HasBaseTime B] :
PhysicalVariable (dimension.length B V / dimension.time B V) :=
299792458 • meter B V / second B V
def PlancksConstant (B : Type u) (V : Type v) [Field V] [HasBaseLength B] [HasBaseTime B] [HasBaseMass B] [SMul Float V]:
PhysicalVariable (dimension.mass B V * dimension.length B V ^ 2 / dimension.time B V) :=
6.62607015e-34•(kilogram B V * (meter B V).Pow 2 / second B V)
def ElementaryCharge (B : Type u) (V : Type v) [Field V] [HasBaseCurrent B] [HasBaseTime B] [SMul Float V]:
PhysicalVariable (dimension.current B V * dimension.time B V) :=
1.602176634e-19 • (ampere B V * second B V)
def BoltzmannConstant (B : Type u) (V : Type v) [Field V]
[HasBaseMass B] [HasBaseLength B] [HasBaseTime B] [HasBaseTemperature B] [SMul Float V]:
PhysicalVariable (dimension.mass B V * dimension.length B V ^ 2 / (dimension.time B V ^ 2 * dimension.temperature B V)) :=
1.380649e-23 • (kilogram B V * (meter B V).Pow (2 : ℕ) / ((second B V).Pow 2 * kelvin B V))
def AvogadrosNumber (B : Type u) (V : Type v) [Field V] [HasBaseAmount B] [Pow V V] [SMul Float V]:
PhysicalVariable ((dimension.amount B V) ^(-1:ℤ)) :=
6.02214076e23 • (mole B V).Pow (-1:ℤ)
/-! 立体角の単位（無次元） --/
def steradian (B : Type u) (V : Type v) [Field V] [HasBaseLength B] [Pow V V] :
PhysicalVariable (dimension.dimensionless B V) :=
1 • ↑((meter B V).Pow 2 / (meter B V).Pow 2)
def MonochromaticRadiation540THz (B : Type u) (V : Type v) [Field V] [Pow V V]
[HasBaseLength B] [HasBaseTime B] [HasBaseMass B] [HasBaseLuminosity B] :
PhysicalVariable ((dimension.luminosity B V * dimension.time B V ^ 3) / (dimension.mass B V * dimension.length B V ^ 2)) :=
683 • ↑(candela B V * steradian B V * (second B V).Pow 3)/ (kilogram B V * (meter B V).Pow 2)
光速の型は $\mathsf{L}/\mathsf{T}$、プランク定数の型は $\mathsf{M}\mathsf{L}^2/\mathsf{T}$、素電荷の型は $\mathsf{I}\cdot\mathsf{T}$。先ほどの表の「J·s」「C」が、基本次元まで展開された形で型に現れています。派生単位のほうは、基本単位のスカラー倍として素直に積み上がります（centimeter = (1/100) • meter など）。
ただし、$h, e, k, N_A$ は [SMul Float V] と浮動小数リテラルとして実装されています。SI単位系でこれらを誤差ゼロの厳密値（定義定数）としているのをふまえると、ここは形式化としては惜しいところです。
【注意】BoltzmannConstant $k$ の次元は J/K、すなわち $\mathsf{M}\mathsf{L}^2\mathsf{T}^{-2}\Theta^{-1}$ のはずですが、本稿執筆時の
PhysicalVariables/Basic.leanの実装には質量が入っていません。おそらく定義に kg を書き忘れるミスが混入しているようなので修正したソースコードにして掲載しました。さらに、MonochromaticRadiation540THz の次元は lm/W なので $\mathsf{T}^{3}$ が分母ではなく分子でなければなりません。こちらもミスが混入しているとして修正したソースコードを掲載。
バッキンガムのπ定理
さて、いよいよ次元解析のハイライトです。1914年に E. Buckingham が定式化したこの定理は「現象を支配する変数のリストだけから、実験や理論に先立って、法則の形をどこまで絞り込めるか」を教えてくれます。せっかくですので、厳密なステートメントと証明を書いていきます。ちなみに、定理の名称にある「π」は円周率を表す記号ではなく、論文等で無次元量（パラメータ）を表す変数としてギリシャ文字の $\pi_1, \pi_2 \dots $ が使われたことに由来しているのだとか。
準備：次元行列
物理量 $q_1, \dots, q_n$（すべて正の実数値とします）を考え、基本次元を $L_1, \dots, L_k$ とします。各 $q_j$ の次元を
$$[q_j] = L_1^{d_{1j}} L_2^{d_{2j}} \cdots L_k^{d_{kj}}$$
と書き、指数を並べた $k \times n$ 行列
$$D = (d_{ij}) \in \mathbb{Q}^{k \times n}$$
を次元行列（dimensional matrix）と呼びます。第 $j$ 列が変数 $q_j$ の指数ベクトルです。
ここでべき積 $q_1^{a_1} q_2^{a_2} \cdots q_n^{a_n}$（$a \in \mathbb{Q}^n$）を考えると、その次元の指数ベクトルは、「乗算＝指数の加算」でしたから $Da$ になります。したがって、次のことが言えます。
補題（無次元積の特徴づけ）
べき積 $\prod_j q_j^{a_j}$ が無次元 $\iff Da = 0 \iff a \in \ker D$
無次元べき積の全体が、指数の空間 $\mathbb{Q}^n$ の部分空間 $\ker D$ と1対1に対応するわけです。ここまで来ると、線形代数の 階数・退化次数の定理 $\dim \ker D = n - \operatorname{rank} D$ が使えそうです。独立な無次元量の個数は、もう決まったことになります。あとはこれを「法則の書き換え」につなげるだけです。
定理のステートメント
次元斉次性を厳密に述べるために、「単位の取り替え」を数学の言葉にしておきます。基本次元 $L_i$ の単位を $1/\lambda_i$ 倍に取り替える（$\lambda_i > 0$）と、各量の数値は
$$q_j \; \longmapsto \; \lambda_1^{d_{1j}} \lambda_2^{d_{2j}} \cdots \lambda_k^{d_{kj}} \, q_j \tag{ * } $$
と変換されます。これは群 $( \mathbb{R} _{>0} )^k$ から $ ( \mathbb{R} _{>0} ) ^n$ への作用になっています。
定義（次元斉次性）
関係 $f(q_1, \dots, q_n) = 0$ が次元斉次であるとは、任意の $\lambda = (\lambda_1, \dots, \lambda_k) \in (\mathbb{R}_{>0})^k$ に対して $$f(q_1, \dots, q_n) = 0 \iff f(\lambda \cdot q_1, \dots, \lambda \cdot q_n) = 0$$ が成り立つことをいう（$\lambda \cdot q_j$ は $(*)$ の変換）。つまり「法則が成り立つかどうかは、単位の選び方によらない」ということ。
定理（Buckingham のπ定理）
$q_1, \dots, q_n$ を正値の物理量、$D$ をその次元行列、$r = \operatorname{rank} D$ とする。関係式 $$f(q_1, \dots, q_n) = 0$$ が次元斉次であるならば、$p = n - r$ 個の独立な無次元べき積 $\pi_1, \dots, \pi_p$（それぞれ $q_j$ たちのべき積）と関数 $F$ が存在して、この関係は $$F(\pi_1, \dots, \pi_p) = 0$$ と同値に書き直せる。しかも $\pi_1, \dots, \pi_p$ は無次元べき積として独立であり、これ以上独立な無次元量を追加することはできない。
この定理により、 $n$ 個あった変数が $n - r$ 個に圧縮されます。$r$ は基本次元の個数 $k$ 以下ですから、変数が多くて次元が少ないほど、圧縮がよく効くことになります。
証明
証明は3段階に分けます。使う道具は 階数・退化次数の定理と、群作用による規格化だけです。
Step 1：無次元積の空間の次元は $n - r$。
先ほどの補題より、無次元べき積は $\ker D \subset \mathbb{Q}^n$ の元と対応します。階数・退化次数の定理から
$$\dim \ker D = n - \operatorname{rank} D = n - r = p.$$
したがって独立な無次元べき積はちょうど $p$ 個取れて、それ以上は独立に取れません。
Step 2：$\pi_1, \dots, \pi_p$ を構成する。
$\operatorname{rank} D = r$ ですから、$D$ の列から一次独立なものが $r$ 本選べます。変数の番号を付け替えて、先頭の $r$ 列（$q_1, \dots, q_r$ に対応）が一次独立であるとしてよいでしょう。この $q_1, \dots, q_r$ を次元的に独立な変数と呼びます（例えば流体の問題なら、密度・速度・代表長さがこれにあたります）。
残りの各変数 $q_{r+l}$（$l = 1, \dots, p$）の列ベクトル $d^{(r+l)}$ を考えます。$\operatorname{rank} D = r$ ということは $D$ の列空間が先頭 $r$ 列で張られるということですから、有理数 $c_{1l}, \dots, c_{rl}$ が一意に存在して
$$d^{(r+l)} = \sum_{i=1}^{r} c_{il} \, d^{(i)}$$
と書けます。そこで
$$\pi_l := \frac{q_{r+l}}{\, q_1^{c_{1l}} \, q_2^{c_{2l}} \cdots q_r^{c_{rl}} \,} \qquad (l = 1, \dots, p)$$
と定めましょう。$\pi_l$ の指数ベクトルは $d^{(r+l)} - \sum_i c_{il} d^{(i)} = 0$、すなわち $\pi_l$ は無次元です。また $\pi_l$ は変数 $q_{r+l}$ をちょうど1回ずつ含み、他の $\pi$ には $q_{r+l}$ が現れませんから、$\pi_1, \dots, \pi_p$ は独立です（対応する指数ベクトルが $\ker D$ の基底をなします）。
Step 3：スケーリングで $q_1, \dots, q_r$ を消す。
Step 2 の定義を $q_{r+l}$ について解くと $q_{r+l} = \pi_l \cdot q_1^{c_{1l}} \cdots q_r^{c_{rl}}$ です。これを $f$ に代入すれば、関係 $f = 0$ は
$$g(q_1, \dots, q_r, \pi_1, \dots, \pi_p) = 0$$
という形になります（$g$ は $f$ から定まる関数）。
ここで次元斉次性を使います。単位の取り替え $(*)$ のもとで、$\pi_l$ は無次元ですから不変であり、変換は $(q_1, \dots, q_r)$ にだけ作用します。その作用を具体的に見ると $q_i \mapsto (\prod_j \lambda_j^{d_{ji}}) q_i$ ですので、対数を取れば
$$\log q_i \; \longmapsto \; \log q_i + \sum_{j=1}^{k} d_{ji} \log \lambda_j \qquad (i = 1, \dots, r)$$
となります。これは $(\log \lambda_1, \dots, \log \lambda_k) \in \mathbb{R}^k$ を行列 $D_r^{\mathsf{T}}$（$D$ の先頭 $r$ 列からなる $k \times r$ 行列の転置）で写して平行移動する作用です。先頭 $r$ 列は一次独立でしたから、$D_r^{\mathsf{T}} : \mathbb{R}^k \to \mathbb{R}^r$ は全射です。ということは、任意の出発点 $(q_1, \dots, q_r)$ を任意の目標点 — たとえば $(1, \dots, 1)$ — へ写す $\lambda$ が存在します。
次元斉次性より、この変換で関係の成立・不成立は変わりません。したがって
$$g(q_1, \dots, q_r, \, \pi) = 0 \iff g(1, \dots, 1, \, \pi) = 0$$
が成り立ちます。そこで $F(\pi_1, \dots, \pi_p) := g(1, \dots, 1, \pi_1, \dots, \pi_p)$ と定めれば
$$f(q_1, \dots, q_n) = 0 \iff F(\pi_1, \dots, \pi_p) = 0. \qquad \blacksquare$$
証明を振り返ってみると、本質は2つしかありません。(i) 無次元積の自由度は 階数・退化次数の定理 で $n - r$ と数えられる。(ii) 次元斉次性、すなわちスケーリング不変性を使うと、次元的に独立な $r$ 個の変数は「単位をうまく選んで 1 に規格化」でき、法則から消えてしまう。π定理が魔法のように変数を減らして見えるのは、単位の選択という $r$ 次元分の恣意性が、そもそも法則には含まれ得ないからです。
なおテクニカルな注意として、指数を $\mathbb{Q}$ で考えても $\mathbb{R}$ で考えても rank は変わりません（有理係数行列の階数は体の拡大で不変）。また変数の正値性は、$q_i^c$（$c \in \mathbb{Q}$）と対数を自由に使うために仮定しました。
レイノルズ数を導出してみる
定理だけでは実感が湧きませんので、実際に使ってみましょう。管内の流れの圧力損失を調べたいとします。関係しそうな変数は、流体の密度 $\rho$、流速 $v$、代表長さ（管径）$L$、粘性係数 $\mu$ の4つです。次元を並べると次のようになります。
| $\rho$ | $v$ | $L$ | $\mu$ | |
|---|---|---|---|---|
| M | 1 | 0 | 0 | 1 |
| L | −3 | 1 | 1 | −1 |
| T | 0 | −1 | 0 | −1 |
これが次元行列 $D$（3×4）です。$\operatorname{rank} D = 3$ ですから、無次元量の個数は $p = 4 - 3 = 1$。ちょうど1個です。核(ker)を求めるために $Da = 0$ を解いてみましょう。
- M 行：$a_\rho + a_\mu = 0$
- T 行：$-a_v - a_\mu = 0$
- L 行：$-3a_\rho + a_v + a_L - a_\mu = 0$
$a_\mu = -1$ と正規化すると $a_\rho = 1,\ a_v = 1,\ a_L = 1$ が得られます。つまり（スカラー倍を除いて）唯一の無次元量は
$$\pi = \frac{\rho v L}{\mu} = \mathrm{Re}$$
これがレイノルズ数です。π定理により、この4変数で書ける次元斉次な法則はすべて $F(\mathrm{Re}) = 0$ の形になる、すなわち「流れの様相は Re だけで決まる」ということになります。層流から乱流への遷移が、管の太さや流体の種類によらず Re ≈ 2300 あたりで起きるという実験事実は、この定理の帰結を目で見ているわけですね。
Lean で書いてみる
実装は、ここまでの構造を Mathlib の線形代数の上にそのまま載せています（DimensionalAnalysis/Basic.lean の末尾）。
-- 変数リスト（次元の列）から次元行列を作る
def dimensional_matrix {n : ℕ} [Fintype B] (d : Fin n → dimension B E)
(perm : Fin (Fintype.card B) → B) :
Matrix (Fin (Fintype.card B)) (Fin n) E := ...
-- 無次元パラメータの個数 = n − rank(D)
noncomputable def number_of_dimensionless_parameters {n : ℕ} [Fintype B]
(d : Fin n → dimension B E) (perm : Fin (Fintype.card B) → B) :=
n - Matrix.rank (dimensional_matrix d perm)
-- 無次元パラメータそのもの = D の核（基底の取り方には任意性がある）
def dimensionless_numbers_matrix {n : ℕ} [Fintype B] (d : Fin n → dimension B E)
(perm : Fin (Fintype.card B) → B) :=
LinearMap.ker (Matrix.toLin' (dimensional_matrix d perm))
Matrix.rank も LinearMap.ker も Mathlib の定義ですし、Step 1 で使った 階数・退化次数の定理も Mathlib に形式化済みです。定義がそのまま数学の言葉になっているのが気持ちいいですね。
ただ、正直に付記しておきますと、現時点の実装が与えているのはこの枠組み（次元行列・個数・核の形式的な定義）までです。Step 3 のスケーリング不変性から $F(\pi) = 0$ を導く部分を含む、定理の完全な一般形は、形式証明されているとはいえません。π定理の完全形式化は、このライブラリの自然な次の目標となるでしょう。
一方で、個別の結果はきちんと定理になっています。先ほど手計算したレイノルズ数の無次元性は、次のように証明されています。
theorem reynolds_eq_dimless : reynolds_number B E = dimensionless B E := by
rw [reynolds_number, mass_density, volume, velocity, dynamic_viscocity,
← one_eq_dimensionless, div_eq_one]
rw [mul_assoc, mul_comm (length B E / time B E), mul_div, pow_three, ...]
手計算では「指数を足したら全部 0 になった」で済ませていた勘定が、ここでは書き換えの列として Lean のカーネルに検証されています。この種の証明を自動化するタクティック evalAutoDim も用意されていて、次元斉次性の確認の多くは1行で済むようになっています。
応用：Lennard-Jones ポテンシャル
論文の応用例も一つ見ておきましょう。分子間相互作用でおなじみの Lennard-Jones ポテンシャルです。
$$V(r) = 4\varepsilon \left[ \left(\frac{\sigma}{r}\right)^{12} - \left(\frac{\sigma}{r}\right)^{6} \right]$$
$\varepsilon$ はエネルギー次元、$\sigma$ は長さ次元を持ちます。これを、次元の制約を型に明示して定義します。
noncomputable def LennardJonesPotentialEnergy
(σ : PhysicalVariable (dimension.length B V))
(ε : PhysicalVariable (dimension.energy B V))
(r : PhysicalVariable (dimension.length B V)) :
PhysicalVariable (dimension.energy B V) :=
4 • ↑(ε * (↑(σ/r).Pow 12 - (σ/r).Pow 6))
$\sigma/r$ は L/L で無次元、その12乗も6乗も無次元、その差も無次元、$\varepsilon$ を掛けてエネルギーとなります。この次元の勘定が、定義の型検査そのものになっています。もし右辺の次元がエネルギーにならない式を書けば、コンパイルエラーとなります。
その上で、物理的な性質も定理として証明されています。
theorem LJ_zero_energy (σ : ...) (ε : ...) (hσ : σ.value ≠ 0) :
LennardJonesPotentialEnergy σ ε σ = ⟨0⟩ := ...
「$r = \sigma$ のとき $V = 0$」ですので、仮定に σ.value ≠ 0 が付いているのも、いかにも形式化らしいところです。手計算では無意識に流してしまう「$\sigma/\sigma = 1$ とするには $\sigma \neq 0$ が要る」を、証明器は見逃してくれません。
さらに、微分の定義も気が利いています。
protected noncomputable def deriv {d1 d2 : dimension B V}
(f : PhysicalVariable d1 → PhysicalVariable d2) (x : PhysicalVariable d1) :
PhysicalVariable (d2 / d1) := ...
$d_2$ 次元の量を $d_1$ 次元の量で微分すると、結果は $d_2/d_1$ 次元となり、微分の次元が型のレベルで自動的に計算されているわけです。ですからポテンシャル $V$（エネルギー次元）を $r$（長さ次元）で微分すれば、$\mathsf{M}\mathsf{L}^2\mathsf{T}^{-2} / \mathsf{L} = \mathsf{M}\mathsf{L}\mathsf{T}^{-2}$、つまり力の次元が勝手に出てきます。この上で $F = -dV/dr$ を具体的に計算した定理（LJ_deriv）まで形式化されています。数値計算のコードと、その物理的な正しさの証明が、同じLean言語の中で同居しているといえます。
検査と証明 — 既存の単位型システムとの違い
ここまで読まれて「単位を型で扱う話なら既にあるのでは？」と思われた方もいらっしゃるでしょう。おっしゃるとおりです。
| 技術 | 仕組み | 保証のレベル |
|---|---|---|
| F# units of measure | 言語組み込みの単位型 | コンパイル時検査 |
| C++ mp-units / Boost.Units | テンプレートメタプログラミング | コンパイル時検査 |
| Python pint | 実行時の単位オブジェクト | 実行時検査 |
| Rust uom | 型レベル整数で次元を表現 | コンパイル時検査 |
| Lean + 本ライブラリ | 依存型＋定理証明 | 検査＋任意の性質の証明 |
既存の単位型システムは「次元の合わない演算をはじく」ことをやってくれます。これだけでも十分有用です。ただ、Lean ではその先の証明が実装されています。「レイノルズ数(Re) は無次元である」「無次元量の個数は $n - \operatorname{rank} D$ である」「$V(\sigma) = 0$ である」といった、他の言語では表現できない命題を定理として記述できて、それを機械的に検証できます。次元解析という理論そのもの（アーベル群の構造、階数・退化次数の定理、π定理）を形式化の対象にしているところが、他の言語処理系との決定的な違いなのではないでしょうか。
そして先ほど見つけた
HasBaseCurrencyは、通貨の基本次元です。JPY と USD の混同、UTC とローカル時刻の取り違え、ワールド座標とスクリーン座標の混線など、私たちが実務で踏んでしまう齟齬は少なからず「単位バグ」であって、次元解析はそのままそれらの認識間違いの対処法になります。物理に興味がなくても、この理論は身近にある理論かもしれません。
終わりに
さて終わりに、本稿で見てきたことを、あらためて整理しておきましょう。
- 次元の全体は乗法についてアーベル群、指数で見れば $\mathbb{Q}$ 上のベクトル空間をなします。Lean では
dimension B E = B → Eと直截に定義され、群であることはCommGroupインスタンスとして証明つきで宣言されています。 - 2019年改定後の SI単位系 は、7つの定義定数（$\Delta\nu_{\mathrm{Cs}}, c, h, e, k, N_A, K_{cd}$）の厳密値を固定することが、単位の定義そのものになっています。秒 → メートル → キログラム → … と循環なく導出される構造は、そのまま Lean の定義の並びに写せます。
- バッキンガムのπ定理は、(i) 階数・退化次数の定理、(ii) スケーリング不変性による次元独立変数の規格化、の2段で完全に証明できます。レイノルズ数はその実例でした。
- Lean 実装は次元行列・無次元パラメータの個数・核を Mathlib の線形代数の上に定義しています。また、個別の例として「レイノルズ数(Re) の無次元性」「Lennard-Jones の性質」を形式化して証明しています。なお、π定理の一般形の完全形式化は今後の課題として残されているようです。
変数のリストを書けば、法則の形が絞れる。π定理は、物理を知らなくても線形代数を知っていれば、証明まで含めて理解できてしまう定理でした。そして定理証明支援系は、その理解をコードとして固定し、壊れないようにしてくれます。次元のことは、もう暗算しなくても、Lean に任せてしまうことができるかもしれませんね。
ここまで、ご一読いただきまして有り難うございます。
（●）（●）Happy Hacking!
/""＿＿""\
参考文献
- ATOMSLab, LeanDimensionalAnalysis (Apache License 2.0). https://github.com/ATOMSLab/LeanDimensionalAnalysis
- BIPM, The International System of Units (SI), 9th edition (2019). — 定義定数の値の一次出典
- E. Buckingham, "On Physically Similar Systems; Illustrations of the Use of Dimensional Equations," Phys. Rev. 4, 345–376 (1914).
-
M. P. Bobbin, C. Jones, J. Velkey, T. R. Josephson, Formalizing Dimensional Analysis Using the Lean Theorem Prover, arXiv:2509.13142 (2025). ↩
-
指数を有理数まで許すのは $\sqrt{\mathsf{L}}$ のような量を扱うためです。整数に限れば自由アーベル群 $\mathbb{Z}^7$ になります。 ↩
-
リポジトリには、次元を型パラメータではなく構造体のフィールドとして持つ別バージョン（
Basic_implicityDimension.lean）も同梱されています。そちらは物理量をリストにまとめるといった柔軟さがある一方、次元の合わない加算が型エラーにならないため、「等しい次元どうしなら結果はその次元、そうでなければ規定しない」という部分関数をClassical.epsilonで表現するという凝った処理が必要になっています。型レベルに上げるか値レベルに留めるかというトレードオフを、2つの実装で読み比べられるのは面白いところです。 ↩ -
細かいことですが、ソースの綴りは
casesium（正しくは caesium / cesium）になっています。ここでは実際のソースコードに忠実に引用しました。 ↩