Proving Properties of $φ$-Representations with the Walnut Theorem-Prover

この論文は、Walnut 定理証明器を用いて Frougny と Sakarovitch の古典的定理をより計算直接的に再証明し、$\phi$-表現に関する既存および新たな結果を統一的かつ自動的に導出する手法を提示しています。

要約

この論文は、数学という少し堅い世界で、**「黄金比（φ）」**という不思議な数字を使って数を表す方法について、新しい「自動計算機」を使って解明したお話しです。

Jeffrey Shallit さんという研究者が書きました。彼が使ったのは「Walnut（クルミ）」という、まるで魔法の箱のようなソフトウェアです。

この論文の内容を、難しい数式を使わずに、日常のたとえ話で説明してみましょう。

1. 黄金比（φ）という「新しい通貨」

私たちが普段使っているのは「10 進法」です。1, 2, 3... と 10 ずつ増えていきますよね。
でも、この論文では**「黄金比（φ）」**という、1.618... という不思議な数字を「10」の代わりに使います。

• 10 進法： 10 円玉、100 円玉、1000 円玉...
• 黄金比法： φ（1.618 円）、φ²（2.618 円）、φ³（4.236 円）...

この「黄金比通貨」で数を表すとき、「11」という並びは禁止というルールがあります（2 つの 1 が隣り合わない）。これを「標準的な書き方（Canonical）」と呼んでいます。

2. 「Walnut」という魔法の探偵

以前、Frougny さんと Sakarovitch さんという二人の学者が、「この黄金比の数を、**自動機械（オートマトン）**で処理できるよ！」と証明しました。でも、その説明はすごく難しくて、機械の設計図（図）も載っていなかったんです。

Shallit さんは、**「Walnut」という無料のソフトウェアを使って、その設計図を「自動で描いて」**しまいました。

• Walnut の役割： 人間が「もしこうなら、ああなるよね？」と推測して証明する代わりに、Walnut は「ありとあらゆるパターンを試して、正解か不正解かを瞬時に判定する」探偵のようなものです。
• 結果： 複雑な証明が、ボタン一つで「正解（TRUE）」と返ってくるようになりました。まるで、パズルのピースを自動で組み合わせて完成図を見せるようなものです。

3. この研究で何がわかったの？（3 つの発見）

この「魔法の機械」を使って、Shallit さんはいくつかの面白いことを発見しました。

① 過去の難問を「自動で」解決

以前、Dekking さんや Van Loon さんという学者が、「黄金比で表した時に、特定のルール（11 で終わらないなど）を満たす書き方が何通りあるか」を計算するとても難しい方法を考えていました。
Shallit さんは、Walnut に「ルールを指定して、数え上げて！」と命令しただけで、**「あ、これでした！」**と即座に答えを出しました。まるで、複雑な料理のレシピを、AI に「材料を全部混ぜて」と頼むだけで、完璧な料理が出てくるようなものです。

② 「鏡文字」や「反転文字」の数の発見

• 鏡文字（パレンドローム）： 「121」のように、前から読んでも後ろから読んでも同じ数字。
• 反転文字（アンチパレンドローム）： 「0110」のように、0 と 1 を入れ替えると鏡文字になる数字。

「黄金比で表した時に、鏡文字になる数はどんな数？」という問いに対して、Walnut は「この 12 個の機械（オートマトン）を通れば、鏡文字になる数だけを通るよ」という設計図を自動で作ってくれました。これにより、今まで誰も知らなかった数の並び（数列）が見つかりました。

③ 「垂直な 1 の列」の長さ

数字を縦に並べて見たとき、「1」が何個連続するかという話です。
「11111」という 5 つの 1 が並ぶのは、特定の位置（桁）でしか起こらないことがわかりました。Walnut は、この「1 が並ぶ長さ」が、ルカスの数（フィボナッチ数列の親戚のような数）と関係していることを、自動的に見つけ出しました。

4. なぜこれがすごいのか？

これまでは、数学の定理を証明するには、人間が「もし A なら B、そして C なら D...」と、何ページにもわたって論理的な文章を書き連ねる必要がありました。これは非常に時間がかかり、間違いも起きやすいです。

しかし、この論文では、**「Walnut というツールにルールを教えれば、機械が自動的に証明し、新しい発見までしてくれる」**ことを示しました。

• 昔のやり方： 手作業でパズルを解く（大変、時間がかかる）。
• 今回のやり方： パズルのピースを機械に放り込み、「完成図を出して！」と命令する（瞬時、正確）。

まとめ

この論文は、**「数学の難しい問題を、コンピュータの力を使って、もっと簡単で、そして自動的に解けるようにした」**という画期的な成果です。

Walnut という「魔法の箱」を使えば、黄金比という不思議な数の世界で、これまで誰も気づかなかった「鏡文字」や「並び方」の秘密を、誰でも（少なくとも研究者なら）簡単に引き出せるようになりました。これは、数学の探検家にとって、新しい地図とコンパスを手に入れたようなものです。

技術概要

論文「Proving Properties of φ-Representations with the Walnut Theorem-Prover」の技術的概要

1. 問題の背景と目的

本論文は、黄金比 $\phi = (1 + \sqrt{5})/2$ を底とする数値表現（$\phi$-表現）の性質を、自動機理論と決定手続きを用いて体系的に証明・解析することを目的としています。

• 背景: 1957 年に Bergman が、非負実数を $\phi$ を底とする展開（$\phi$-展開）で表すことができることを示しました。特に、隣接する 1 が現れない（$a_i a_{i+1} \neq 1$）という制約を課した「標準的（canonical）」な表現は一意に定まります。
• 既存研究の課題: Frougny と Sakarovitch は、非負整数の標準的 $\phi$-表現を計算する有限オートマトンの存在を証明しましたが、そのオートマトンの具体的な構成や、それを用いた性質の証明は複雑で、読みにくいものでした。また、Dekking や Van Loon による近年の研究（Knott 展開や自然展開など）においても、証明には複雑な帰納法や手計算が必要とされていました。
• 目的: 定理証明支援ツール「Walnut」を用いて、Frougny-Sakarovitch のオートマトンを明示的に構成し、既存の結果を「自動的」かつ「帰納法なし」で再証明するとともに、新たな結果を導出することです。

2. 手法とアプローチ

本研究の核心は、Walnut（Hamoon Mousavi によって開発された、自動列とプレスブルガー算術の拡張に関する決定手続きを実装したフリーソフトウェア）を駆使した計算機支援証明にあります。

2.1 基礎となる表現系

整数の表現として以下の 2 系を使用します。

1. Zeckendorf 表現: 非負整数をフィボナッチ数の和として表す（隣接する 1 を持たない）。
2. NegaFibonacci 表現: 整数（正・負・零）を負のフィボナッチ数の和として表す。

2.2 Frougny-Sakarovitch オートマトンの再構成

$\phi$-表現 $z = [x.y]_\phi$ が整数 $n$ と等しいための条件を、Zeckendorf 表現と NegaFibonacci 表現の線形結合として式変形します。

• 左部分 $x$ は $\phi$ の係数と定数項の和として表現されます。
• 右部分 $y$ は同様に表現されます。
• これらの条件を第一階述語論理（First-order logic）で記述し、Walnut に渡すことで、入力 $n$（Zeckendorf 表現）、左部 $x$、右部 $y$（反転した文字列 $y^R$）を受け取り、$n = [x.y]_\phi$ かどうかを判定する有限オートマトンを自動的に生成します。

2.3 証明の自動化

生成されたオートマトンを用いて、以下のタスクを自動化します。

• 性質の検証: 特定の数列（フィボナッチ数、ルカス数など）に対する $\phi$-表現の構造を、オートマトンの受理経路を解析することで証明します。
• 線形表現（Linear Representation）の導出: 特定の性質を満たす $n$ の個数や、桁和などの関数を計算する線形表現（行列とベクトルを用いた形式）を自動生成し、漸近的な挙動や閉形式を導出します。
• 半群トリック（Semigroup Trick）: 生成された線形表現の最小多項式の根を解析することで、数列がフィボナッチ自動列（Fibonacci-automatic sequence）であることを示し、漸近評価を行います。

3. 主要な貢献と結果

3.1 Frougny-Sakarovitch オートマトンの明示的構成

Walnut を用いて、Frougny-Sakarovitch の定理に対応するオートマトンを 116 状態（標準的な制約を加えると 39 状態）で明示的に構成しました。これにより、複雑な手作業なしに $\phi$-表現の基礎的な性質を扱えるようになりました。

3.2 既存結果の自動再証明

• フィボナッチ数・ルカス数の $\phi$-表現: 標準的 $\phi$-表現が周期 4 のパターンに従うことなどを、オートマトンの構造解析から簡潔に証明しました。
• Dekking-Van Loon の結果:
  • Knott 展開: 整数 $n$ の「Knott 展開」（011 で終わらない $\phi$-表現）の個数 $Tot_\kappa(n)$ について、複雑な帰納法を使わずに線形表現を導き、$n$ がフィボナッチ数やルカス数の場合の閉形式を再証明しました。
  • 自然展開（Natural expansions）: 左右の桁数が等しい展開の個数についても同様に証明しました。
  • DVL 展開: 特定の条件（$d_1 d_0 = 11$ かつ $d_{-1}=0$ のみ許可）を満たす展開の性質についても、垂直ラン（vertical runs）の長さの規則性を自動証明しました。

3.3 新規結果の導出

• Gerdemann の予想の証明: Zeckendorf 表現の桁和が、標準的 $\phi$-表現の桁和以下であるという 2012 年の予想を、重み付きグラフの最小経路問題（Bellman-Ford 法）として定式化し、証明しました。
• 左部・右部の桁和: $\phi$-表現の左部と右部のそれぞれの桁和の線形表現を導出し、その漸近的な性質を明らかにしました。
• 垂直ランの長さ: 標準的 $\phi$-表現における「1 の垂直ラン」の長さが、ルカス数を用いた明示的な式で記述されることを発見・証明しました（Dekking と Van Loon が「規則性はない」と主張していたことへの反証）。
• パレイドロムと反パレイドロム: $\phi$-表現がパレイドロム（対称）または反パレイドロム（ビット反転対称）となる整数の集合を特徴づけるオートマトンを構成し、対応する整数列（OEIS 登録）を特定しました。
• 代数的整数への拡張: $\mathbb{Z}[\phi]$ に属する代数的整数 $m\phi + n$ についても、同様の手法で $\phi$-表現を計算するオートマトンを構成し、左右の桁数が等しい場合の条件を自動証明しました。

4. 意義と結論

本論文は、数論的性質（特に $\phi$-展開）の解析において、**「定理証明支援ツールによる計算機駆動アプローチ」**の有効性を示す重要な事例です。

• 帰納法の不要化: 従来の数論的証明で多用されていた複雑な帰納法を、オートマトンの状態遷移や線形表現の代数解析に置き換えることで、証明を単純化・自動化しました。
• 統一された枠組み: 異なる種類の展開（標準的、Knott、自然、DVL など）に対して、同じ手法（Walnut とオートマトンの交差・積）を適用することで、統一的かつ体系的な解析が可能であることを示しました。
• 新発見の促進: 手計算では見逃されがちな微細な規則性（垂直ランの長さの公式など）を、自動生成されたオートマトンの構造解析から発見しました。

結論として、Walnut を用いることで、$\phi$-表現に関する古典的な定理から最新の未解決問題まで、広範な結果を「自動的」かつ「厳密に」処理できることが実証されました。この手法は、$\phi$ だけでなく、他の二次ピソット数（Pisot number）$\beta$ に対する $\beta$-展開の解析にも応用可能であるとしています。