結果の読み方と用語集
試すページに出る結果の読み方と、このサイトで使う言葉の意味をまとめる。
結果カードの見方
「全部計算する」を押すと、問いごとに 1 枚のカードが並ぶ。
- 上の段：問いの記号（Id、Q1〜Q11）と名前、確かさの種類の札、かかった時間。
- 要約：答えを 1 行で表したもの。
- 詳細：開くと、答えの説明、検査器のメモ、よりどころにする Lean の定理、値・前提・仮定・誤り確率の上界・統計・理由のうち付いているもの、証明書の全体が見られる。証明書のダウンロードと、検査器でのもう一度の検査もここからできる（「証明書と検査」）。
- 一覧の上：「確定 n/全体」で、確定の答えがいくつあるかを示す。
カードには、答えのほかに次の状態が出ることがある。
| 表示 | 意味 |
|---|---|
| 計算中・待ち・順番待ち | 計算している、ほかの答えを待っている、計算サーバーの順番を待っている。「取り消す」で止められる |
| 省略 | 計算しなかった。たとえば Q4 で保存量が見つからなかったときの Q5 |
| 対象外 | その問いがこの系には当てはまらない。たとえば対称性を宣言していない系の Q6 |
| エラー | 入力が読めないなど。理由が出る |
計算した結果は履歴として、このブラウザに残る（「消去」で消せる）。
確かさの種類
| 種類 | 意味 | 付いてくるもの |
|---|---|---|
| 確定 | 検査に通り、Lean で証明した定理から従う数学的な主張 | 前提（あれば） |
| 確率的に確定 | 正しいことが、誤りの確率の上界つきで保証される | 誤り確率の上界 |
| 復元値 | 書かれた仮定のもとで、一意に決まる値 | 仮定（例：歩数の大きさが B 以下） |
| 統計 | 標本にもとづく推定。定理ではない | 統計量 |
| 結果なし | 主張しない | 理由（例：軌道が歩く上限より長い、検査に通らなかった） |
前提：確定の答えでも、前提が付くことがある。たとえば大きい q で s や t が正則かどうかを決めきれないとき、正則であることを前提とした答えになる。前提は答えに明示される。
Id(s, t) の答えの形
| 答え | 読み方 |
|---|---|
| t = σⁿ s ⇔ n ≡ r (mod M) | n を M で割って r 余るときに限り、n 歩で t に着く。M はふつう軌道の周期 |
| 道なし | どの歩数でも、進めても戻しても t に着かない |
| s は正則でない（t には n 歩で着く） | s の軌道は途中で式が定義されなくなって途切れる。途切れる前に t に着くなら、その歩数 n（ほかの歩数では着かない） |
| s は正則でない | 上と同じで、途切れる前に t には着かない |
| （ℚ 上）t = σⁿ s, n = −3（全解：n ≡ r (mod M)） | ℚ 上で n 歩（この例では 3 歩戻る）で着くことを、そのとおりに計算して確かめた。ほかに解があるとしたら、それは n ≡ r (mod M) の形 |
用語集
| 用語 | 意味 |
|---|---|
| 系 | 状態と、それを 1 歩進める規則の組 |
| 状態 | 数の組。たとえば (2, 5)。成分の数は変数の数 |
| 1 歩（σ） | 規則を 1 回使うこと。σⁿ は n 回使うことで、n が負なら逆向きにたどる |
| 軌道 | ある状態から進めたり戻したりして得られる状態の並び |
| 周期 | 有限体の上で、軌道が元に戻るまでの歩数 |
| サイクルと鎖 | 有限体の上では、どの状態も、周期のある輪（サイクル）か、両端で途切れる有限の鎖の上にある（規則がそもそも定義されない状態を除く） |
| 正則 | 進めても戻しても、どこまでも式が定義され続ける状態。試すページでは「作用亜群の状態」とも言う。有限体の上では、サイクルの上にあることと同じ |
| 道なし | t がどの歩数でも現れないこと |
| Id(s, t) | s から t への道（歩数）の集まり。型理論で等しさの証拠の集まりを表す記号にならった |
| 有限体 𝔽_q | 素数 q で割った余りだけで計算する数の世界。値はいつも 0 から q − 1 の整数で、誤差がない |
| 有理数体 ℚ | 分数を分数のまま、正確に計算する数の世界 |
| 歩数の上界 B | ℚ 上の問いで、歩数 n を探す範囲 |n| ≤ B |
| 保存量 | 軌道に沿って値が変わらない式 |
| 可逆（双有理） | 1 歩を逆向きにたどる式があること |
| 可積分 | 互いに独立な保存量が「変数の数 − 1」個あり、どの軌道も曲線の上に乗ること |
| 対称性 | 状態を回しても系が変わらないような変換のまとまり。系ファイルで、それが保つ 2 次式（例：x^2 + y^2）を書いて宣言する |
| 恒等式 | どの値を入れても成り立つ式の等しさ。Structure Computer は多くの主張をこの形で証明する |
| ホロノミー | 軌道が対称性の分を除いて戻ってきたときに、状態がどれだけ回されているか |
| 生成元と語 | 複数の 1 歩（生成元）を持つ系で、それらを並べて作る道。例：r s^-1 r^2 |
| アフィンな座標の取り替え | x ↦ Mx + c の形の座標の取り替え（M は逆行列を持つ行列） |
| 既知の族 | 定理にもとづいて、大きい q でも軌道をたどらずに答えられる系の種類。Lyness 写像、Euler のコマの離散化、行列式 1 の線形写像、双曲面上の測地線の離散化の一つ。座標を取り替えて書かれていても見抜く |
| 系ファイル | 変数・パラメータ・1 歩の式などを書いた短いテキスト（「系ファイルの書き方」） |
| 証明書 | 答えと、それを確かめるための手がかりをまとめた JSON の文書 |
| 検査器 | 証明書だけを使って答えを確かめ直す、計算する部分とは別のプログラム |
| Lean | 数学の証明をコンピュータが 1 行ずつ確かめる証明支援系 |
| 種 | 計算の中の乱択に使う数。同じ種なら同じ証明書になる |
| 歩く上限 | 既知の族ではない系で、軌道をたどる歩数の上限 |