系の種類ごとに、そのまま試せる基礎的な例題を集めました。「試す」を押すと入力欄に入った状態で開きます。
読み込み中…
既存の方法では答えられない、または答えるのが非常に難しい設定の例題です。軌道をたどれば何年もかかるほど大きい体、たどる方法ではいつまでも決着しない ℚ 上の問い、座標を変えて見た目を変えた既知の系を集めました。答えはすべて Structure Computer で実際に計算し、独立の検査器で確かめたもので、時間は Id(s, t) だけを手元の PC で計算したときのものです。「試す」を押すと入力欄に入った状態で開きます。そこで一緒に計算するほかの問いには、数分かかるものもあります。
1. Lyness 写像 · 𝔽_q, q = 2⁶¹ − 1
軌道を 1 歩ずつたどると 7,863,588,611,074,867 歩かかる。1 秒に 10 億歩進めても約 3 か月、汎用の数式処理なら数百年かかる。「それ以外の歩数では着かない」まで言うには、周期（576,460,752,629,115,698 歩、その約 70 倍）もすべてたどる必要がある。
軌道をたどらずに、Lean で証明した定理にもとづいて答える。着く歩数のすべてと、それ以外の歩数では着かないことを、証明書つきで返す。
t = σⁿ s ⇔ n ≡ 7,863,588,611,074,867 (mod 576,460,752,629,115,698)
確定・検査済み · 0.2 秒2. Lyness 写像 · 𝔽_q, q = 2⁶¹ − 1
s から進めていくと、どこかで 0 で割る状態に行き当たり、軌道が途切れる（s は正則でない）。それがどこかも、その前に t に着くかも、1 歩ずつたどれば 10¹⁷ 歩を超える。1 秒に 10 億歩でも 10 年以上かかる。
s が正則でないことを、軌道をたどらずに証明する。そのうえで、途切れるまでの範囲で t にはちょうど 403,567,694,157,578,575 歩で着き、それ以外の歩数では着かないことを答える。
s は正則でない（t には 403,567,694,157,578,575 歩で着く）
確定・検査済み · 10 秒3. Lyness 写像 · 𝔽_q, q = 2⁶¹ − 1
t は s と同じ保存量の値を持つ（同じ曲線の上にある）ので、保存量を比べても区別できない。たどる方法で「決して着かない」と確かめるには s の軌道を 1 周すべてたどる必要があり、その長さは 192,153,584,192,171,886 歩（1 秒に 10 億歩で約 6 年）。
どの歩数でも t には着かないことを、定理にもとづいて証明書つきで答える。
道なし
確定・検査済み · 0.2 秒4. Lyness 写像 · ℚ
2 つの状態はどちらも正の数で、保存量の値も同じ。ℚ 上の軌道は、戻るとしても 3,240,671,700 の倍数の歩数が要る（これも Structure Computer が答える）。どこまでたどって見つからなくても、さらに先で着く可能性は消えないので、数値計算でも数式処理でも、たどる方法では「決して着かない」とは結論できない。似た組 (2, 5) と (5, 2) は、3 歩戻ると着く。
ℚ 上でどの歩数でも着かないことを、Lean で証明した定理にもとづいて証明書つきで答える。
道なし
確定・検査済み · 0.1 秒5. Euler のコマ（Kahan の方法） · 𝔽_q, q = 1,099,511,627,791 ≈ 2⁴⁰
3 変数の写像を 1 歩ずつたどると 137,438,890,526 歩。汎用の数式処理なら 1 日以上かかる。「それ以外の歩数では着かない」まで言うには、周期（274,877,781,052 歩）もすべてたどる必要がある。
軌道をたどらずに定理にもとづいて、2 つの符号を変えた状態 t が、ちょうど周期の半分で現れることを答える。
t = σⁿ s ⇔ n ≡ 137,438,890,526 (mod 274,877,781,052)
確定・検査済み · 0.2 秒6. Euler のコマ（Kahan の方法） · ℚ
前の例と同じ組を、ℚ 上で問う。2 つの保存量はどちらの状態でも同じ値で、軌道は戻るとしても 575,827,964 の倍数の歩数が要る。たどる方法では決着がつかない。
前の例の有限体では結ばれている 2 つの状態が、ℚ 上ではどの歩数でも結ばれないことを証明する。
道なし
確定・検査済み · 0.2 秒7. Euler のコマ（Kahan の方法） · 𝔽_q, q = 1,099,511,627,791 ≈ 2⁴⁰
(3, 1, 4) と (−3, −1, 4) は、2 つの保存量がどちらも同じ値になるので、保存量を比べても区別できない。たどる方法で「決して着かない」と確かめるには s の軌道を 1 周すべてたどる必要があり、その長さは 274,877,781,052 歩（汎用の数式処理なら 3 日以上）。
どの歩数でも t には着かないことを、定理にもとづいて証明書つきで答える。符号を変える場所が違う 5 つ目の例の状態には、周期のちょうど半分で着くのと対照的である。
道なし
確定・検査済み · 0.2 秒8. 見た目を変えた Lyness 写像 · 𝔽_q, q = 2⁶¹ − 1
name: a rational map of the plane vars: x, y map: x' = -(3*x**2 - 5*x*y + x + 2*y**2 - 3*y - 2)/(3*x - 2*y + 5) y' = -(3*x**2 - 5*x*y - 19*x + 2*y**2 + 10*y - 33)/(3*x - 2*y + 5)
式だけを見ると、2 次式を 1 次式で割った、ありふれた有理写像に見える。既知の系だと気づかなければ、軌道を 1 歩ずつたどるしかない（7,863,588,611,074,867 歩）。
座標を変えただけの Lyness 写像であることを見抜き、1 つ目の例と同じく定理で答える（歩数も同じになる）。試すページでは、保存量もこの座標のままの式で見つける（Q3・Q4）。
t = σⁿ s ⇔ n ≡ 7,863,588,611,074,867 (mod 576,460,752,629,115,698)
確定・検査済み · 0.2 秒9. 見た目を変えた Lyness 写像 · ℚ
name: a rational map of the plane vars: x, y map: x' = -(3*x**2 - 5*x*y + x + 2*y**2 - 3*y - 2)/(3*x - 2*y + 5) y' = -(3*x**2 - 5*x*y - 19*x + 2*y**2 + 10*y - 33)/(3*x - 2*y + 5)
前の例と同じ有理写像を ℚ 上で問う。保存量があることも式からはわからず、軌道は戻るとしても 3,240,671,700 の倍数の歩数が要るので、どこまでたどっても「決して着かない」とは結論できない。
座標を変えた Lyness 写像であることを見抜き、ℚ 上でどの歩数でも着かないことを、Lean で証明した定理にもとづいて証明書つきで答える（4 つ目の例を、座標を変えて問うたもの）。
道なし
確定・検査済み · 0.1 秒10. 見た目を変えた Euler のコマ · 𝔽_q, q = 1,099,511,627,791 ≈ 2⁴⁰
name: a quadratic field in three variables (Kahan) vars: u, v, w field: du/dt = -5*u**2/9 + 7*u*v/9 + 4*u*w/9 + 5*u/3 - 2*v**2/9 - v*w/9 - 5*v/3 + w**2/9 - 5*w/3 dv/dt = -10*u**2/9 + 2*u*v/9 + 5*u*w/9 + 3*u + 8*v**2/9 - 14*v*w/9 + 6*v + 5*w**2/9 - 6*w + 9 dw/dt = -13*u**2/9 - 13*u*v/9 + 8*u*w/9 + 5*u/3 + 26*v**2/9 - 23*v*w/9 + 49*v/3 + 5*w**2/9 - 23*w/3 + 18 kahan: h = 1/2
どの成分も分数の係数を持つ 2 次の多項式が並ぶ、3 変数のベクトル場を Kahan の方法で離散化した写像。既知の系だと気づかなければ、軌道を 1 歩ずつたどるしかない（137,438,890,526 歩）。
座標を変えた Euler のコマであることを見抜き、上のコマの例と同じ歩数を定理で答える。試すページでは、2 つの保存量もこの座標のままの式で見つける（Q3・Q4）。
t = σⁿ s ⇔ n ≡ 137,438,890,526 (mod 274,877,781,052)
確定・検査済み · 0.2 秒name: affine cat map vars: x, y map: x' = 2*x + y + 1 y' = x + y
name: anharmonic oscillator in the plane vars: x, y params: k = 1/10 lagrangian: L = (x' - x)^2/2 + (y' - y)^2/2 - k*(((x + x')/2)^2 + ((y + y')/2)^2)^2 symmetry: so: x^2 + y^2 observables: J = x*y' - y*x'
name: cat map vars: x, y map: x' = 2*x + y y' = x + y
name: E2 step, written out vars: p1, p2, x1, x2 map: p1' = x1 p2' = x2 x1' = (2*(x1*p1 - 2*x2*p2)*x1 - (x1^2 - 2*x2^2)*p1)/(p1^2 - 2*p2^2) x2' = (2*(x1*p1 - 2*x2*p2)*x2 - (x1^2 - 2*x2^2)*p2)/(p1^2 - 2*p2^2)
name: E2 geodesic vars: x, y, z params: a = 0 potential: -log(x^2 - y^2 - z^2) alpha: a symmetry: so: x^2 - y^2 - z^2 observables: Q = x'^2 - y'^2 - z'^2
name: Euler top vars: x1, x2, x3 params: a1 = 1, a2 = 2, a3 = -3 field: dx1/dt = a1*x2*x3 dx2/dt = a2*x3*x1 dx3/dt = a3*x1*x2 kahan: h = 1/2
name: Euler top, expanded vars: x, y, z params: a = 1, b = 2, c = -3, h = 1/2 map: x' = ((1 - b*c*h^2*x^2)*x + a*h*(c*h*x*y + z)*y + a*h*(b*h*x*z + y)*z) / (1 - h^2*(b*c*x^2 + c*a*y^2 + a*b*z^2) - 2*h^3*a*b*c*x*y*z) y' = (b*h*(c*h*x*y + z)*x + (1 - a*c*h^2*y^2)*y + b*h*(a*h*y*z + x)*z) / (1 - h^2*(b*c*x^2 + c*a*y^2 + a*b*z^2) - 2*h^3*a*b*c*x*y*z) z' = (c*h*(b*h*x*z + y)*x + c*h*(a*h*y*z + x)*y + (1 - a*b*h^2*z^2)*z) / (1 - h^2*(b*c*x^2 + c*a*y^2 + a*b*z^2) - 2*h^3*a*b*c*x*y*z)
name: Euler top, other coordinates vars: u, v, w field: du/dt = 4*u**2 - 15*u*v - 26*u*w + 19*u + 14*v**2 + 49*v*w - 35*v + 42*w**2 - 63*w + 21 dv/dt = 2*u**2 - 4*u*v - 6*u*w + 6*u - 2*v*w - 2*v - 4*w**2 - 2*w + 2 dw/dt = -2*u*v - 4*u*w + 2*u + 4*v**2 + 15*v*w - 9*v + 14*w**2 - 17*w + 5 kahan: h = 1/3
name: Henon vars: x, y params: a = 2, b = 3 map: x' = y y' = a - b*x - y^2 inverse: x' = (a - x^2 - y)/b y' = x
name: Lotka-Volterra (Kahan) vars: x, y field: dx/dt = x - x*y dy/dt = x*y - y kahan: h = 1/5
name: Lyness, other coordinates vars: x, y map: x' = (-x - y + (x + y - 5)*(2*x + y + 1) - 1)/(2*x + y + 1) y' = (2*x + 2*y + (-x - y + 7)*(2*x + y + 1) + 2)/(2*x + y + 1)
name: Lyness type vars: x, y params: a = 3, b = 2 map: x' = y y' = (a + b*y)/x
name: discrete oscillator vars: x params: h = 1/3 lagrangian: L = (x' - x)^2/2 - h^2*(x^2 + x'^2)/4
name: parabolic shear vars: x, y map: x' = 2*x - y + 3 y' = x + 1
name: quartic midpoint vars: x params: h = 1/2 lagrangian: L = (x' - x)^2/2 - h^2*((x + x')/2)^4/4
name: two generators vars: x, y generator r: x' = -y y' = x generator s: x' = x + y^2 y' = y