見出し画像

P-adic Valuation: p-進評価とは？

D.

賢狼との思い出：会話記録

この物語は AI の賢狼と、研究者「 D 」による会話ログです。
※よって会話の内容に関しての真偽は各自で再検証してからご利用下さい。

登場人物：
🙎私D.: とある研究者
🐺賢狼: 知恵の豊穣神「賢狼」AI


P-adic Valuation 解説

cid: 68e34019-fec4-8321-b4bf-2ddceda12d7e

🙎私D.:

P-adic Valuation とは？ #p進評価

🐺賢狼:

ぬしよ、「$${p}$$-進評価（$${p}$$-adic valuation）」は“自然数や有理数の中に、素数 $${p}$$ がどれだけ深く染み込んでおるか”を測る物差しじゃ。
素因数分解の指数を抜き出してくる装置、と覚えると早いの。

直感と定義

  • 自然数 $${n \ge 1}$$ を素因数分解して

$$
n\ =\ p^{k}\ m,\qquad p \nmid m
$$

と一意に書ける（$${m}$$ は $${p}$$ を割らぬ）。このとき

$$
v_p(n)\ :=\ k
$$

を $${p}$$-進評価と呼ぶ。
例：
$${\ v_2(12)=2}$$（$${12=2^2\cdot 3}$$）
$${\ v_3(81)=4}$$（$${81=3^4}$$）

  • 整数 $${z\neq 0}$$ でも同じく指数を返す
    （符号は無視して良い）。

  • 有理数 $${q=\frac{a}{b}\neq 0}$$ では

$$
v_p!\left(\frac{a}{b}\right)=v_p(a)-v_p(b)
$$

——分子の $${p}$$ の指数から分母の指数を引く。これで加法的性質が綺麗に揃うのじゃ。

この $${v_p}$$ から $${p}$$-進ノルム $${\lvert q\rvert_p := p^{-\ v_p(q)}}$$ が生まれ、$${\mathbb Q}$$ をこのノルムで完備すると $${\mathbb Q_p}$$（$${p}$$-進数体）になる。数の“近さ”の概念がガラリと入れ替わる、愉快な世界よの。

基本性質（要点）

$$
\begin{aligned}
v_p(mn)&=v_p(m)+v_p(n),\\
v_p!\big(m^r\big)&=r\ v_p(m),\\
v_p(m+n) &\ge \min{v_p(m),\ v_p(n)}, \\
&\text{かつ } v_p(m)\ne v_p(n)\text{ なら } \\
&v_p(m+n)=\min{v_p(m),v_p(n)}.
\end{aligned}
$$

最後の“加法は最小に引きずられる”という性質が $${p}$$-進解析の肝じゃ。

Lean（mathlib）の `padicValNat` との対応

ぬしが貼ったコードは自然数版 `padicValNat p n : ℕ` の定義と基本同一視を示しておる。

  • 定義の核：

/- p ≠ 1 ∧ n ≠ 0 のとき「p^k ∣ n となる最大の k」を返す -/
def padicValNat (p n : ℕ) : ℕ :=
  if h : p ≠ 1 ∧ 0 < n then Nat.find (finiteMultiplicity_iff.2 h) else 0

つまり数学的 $${v_p(n)}$$ を有限“重複度” `multiplicity p n` と同一視しておる。

  • 重要な同一視（`p` が素数、`n ≠ 0`）：

theorem padicValNat_def [Fact p.Prime] {n : ℕ} (hn : n ≠ 0) :
    padicValNat p n = multiplicity p n

ここで `multiplicity p n` は “$${p}$$ が $${n}$$ を何回割るか” を WithTop（∞ もありうる型）で表す標準概念じゃ。

  • 便利な事実：

@[simp] theorem padicValNat.zero : padicValNat p 0 = 0
@[simp] theorem padicValNat.one  : padicValNat p 1 = 0
@[simp] theorem padicValNat.eq_zero_iff :
  padicValNat p n = 0 ↔ p = 1 ∨ n = 0 ∨ ¬ p ∣ n

数学的には $${v_p(0)=\infty}$$ とする流儀も多いが、`padicValNat` は型を自然数に固定しておるゆえ、`n=0` や `p=1` の例外は 0 に“丸める”設計なのに注意じゃ（∞ を使う版は `multiplicity` を見よ）。

  • “リストの素因数”との橋渡し
    （貼ってくれた定理→Appendix）
    `replicate n a <+~ b.primeFactorsList` は「素因数リスト中に $${a}$$ が $${n}$$ 回（組み替え同値で）含まれる」を意味し、
    $${n \le v_a(b)}$$ と同値であることを述べておる。
    言い換えれば「指数 $${\ge n}$$」と「素因数リストに $${a}$$ が $${n}$$ 回」は一致するのじゃ。

具体例（Lean での計算感）

＃eval padicValNat 2 12   -- 2  (12 = 2^2 * 3)
＃eval padicValNat 3 81   -- 4  (81 = 3^4)
＃eval padicValNat 5 250  -- 3  (250 = 5^3 * 2)
＃eval padicValNat 2 0    -- 0  （設計上 0。∞ は multiplicity で扱う）


2n+1 の分布的直感（ぬしの用途に即して）

賢狼の嗅覚では、ぬしがよく使う $${v_p(2n+1)}$$ は確率論的にも面白い。大きな $${X}$$ で一様に $${n\le X}$$ を選ぶとき

$$
\Pr\big[v_p(2n+1)\ge k\big]\approx p^{-k}
$$

となる幾何的尾（ジオメトリックな減衰）を示す。実際、合同式 $${2n+1\equiv 0 \pmod{p^k}}$$ は法 $${p^k}$$ でただ一つの解しか持たんから、密度は $${\approx 1/p^k}$$ になるわけじゃ。
この“指数が幾何分布めく”性質が、MGF/Chernoff で尾確率を抑えるぬしの戦術の土台になっておるのだの。

使いどころの要約

  • 素因数の“深さ”を測る計器が $${v_p}$$。

  • 乗法で加法、冪でスカラー倍、加法で最小に引きずられる——この三拍子が $${p}$$-進解析のリズム。

  • Lean では `padicValNat`（自然数版），`multiplicity`（∞ もあり）をうまく使い分ける。

  • 有理数版の $${v_p}$$ から $${\lvert\cdot\rvert_p}$$ が立ち上がり、$${p}$$-進世界へと門が開く。

次は、`padicValNat` の加法・乗法の定理群（例：`padicValNat.mul`, `padicValNat.pow` など）を組み込んで、$${2n+1}$$ の“過剰指数”を数える補題を積み上げると良い。わっちの長い旅路の経験では、ここでの美技は“法 $${p^k}$$ の一意解”と“区間の格子点数え上げ”の二刀流じゃよ。🐺🍎


なんの話？

最後の部分は私がいま形式化している #ABC予想 の話です。
そこで使われる評価関数の話。

例

「奇素数 $${p}$$ に対して、ランダムな $${n\le X}$$ の ‘(2n+1)’ が どれくらい深く $${p}$$ で割れるか（$${=v_p(2n+1)}$$）は、平均的にはすぐ尽きる（尾が指数的に薄い）」

ここは完全証明された（と思われる）

`padic_val_two_of_odd` は、任意の自然数 `n` に対して、`2*n+1` の 2 進 p-進値が 0 であることを示します。 これは、`2*n+1` が奇数であり、2 で割り切れないためです。 証明では、`padicValNat.eq_zero_of_not_dvd` を用いて、2 が `2*n+1` を割り切らないことから結論を導きます。 

/--
`padic_val_two_of_odd` は、任意の自然数 `n` に対して、`2*n+1` の 2 進 p-進値が 0 であることを示します。
これは、`2*n+1` が奇数であり、2 で割り切れないためです。
証明では、`padicValNat.eq_zero_of_not_dvd` を用いて、2 が `2*n+1` を割り切らないことから結論を導きます。
-/
-- Special case: p = 2, always v_2(2n+1) = 0
lemma padic_val_two_of_odd : ∀ n : ℕ, padicValNat 2 (2*n+1) = 0 := fun n => by
  apply padicValNat.eq_zero_of_not_dvd
  omega



で！本題！！


？？？


ChatGPT 会話ログ取得ツールが機能しないとの報告を受け投稿テストした。
問題なく動作している。なので、この報告は保留としておいても良いわね。

会話ログConverterを使った投稿のテストであった。まだなんとか無事、機能しているみたいだけど ChatGPT (OpenAI) 側の賢狼の会話にゴミ？のようなものが、乗っかってくる。とくに $${\LaTeX}$$ 書式に。

"\;" とか "\," とか。

"\;" は "\ " 半角スペース "\space" の代替だろうと推測
"\," はなんだろう？これもスペースな気もするが２種類ある？

表示から察するに空白制御で間違いなさそうだけど

この \\(v_p\\) から \\(\\,p\\)-進ノルム \\(\\lvert q\\rvert_p := p^{-\\,v_p(q)}\\) が生まれ、

生データはこんな感じで書かれている。表示の

"\\(\\,p\\)-進ノルム"
"p^{-\\,v_p(q)}"

ここですね。なにも書かれていない。
文字選択の空間になるということはタグの区切りか何かのアクションか。

ああ。解った。

\, → <mtext> </mtext>

KaTeX / KaTeX MathML

と変換されている。

アノテーションにはそのまま "\,p" とか "\lvert q\rvert_p := p^{-\,v_p(q)}" で、
"\," 展開されていますね。ということはカスタムか？

"\;" は？

\\[\n  n \\;=\\; p^{k}\\, m,\\qquad p \\nmid m\n  \\]

表示

"\;" → <mtext>  </mtext>
※分かりにくいだろうけど半角空白スペース２個

KaTeX / KaTeX MathML
<span class="katex"><span class="katex-mathml">
<math xmlns="http://www.w3.org/1998/Math/MathML" display="block">
<semantics>
<mrow>
<mi>n</mi>
<mtext>  </mtext>　　← これです "\;"
<mo>=</mo>
<mtext>  </mtext>
<msup>
<mi>p</mi>
<mi>k</mi>
</msup>
<mtext> </mtext>
<mi>m</mi>
<mo separator="true">,</mo>
<mspace width="2em"></mspace>
<mi>p</mi>
<mo>∤</mo>
<mi>m</mi>
</mrow>
<annotation encoding="application/x-tex">n \;=\; p^{k}\, m,\qquad p \nmid m</annotation>
</semantics>
</math>
</span>


とりあえず解った！
変換処理に "\;" "\," を note が理解する半角スペースにすれば良い事は…。

note コピペ仕様

問題は note のコピペ仕様か。多々、貼付け事故がある。

\\ \\ \\ \\

を貼り付けると
\ \ \ \
と半分になる。💩仕様。 #カイゼン

$${LaTeX}$$ の改行 "\\" が全部 "\" になる。
だいたいインライン $${LaTeX}$$ の書式の "＄＄｛ 式 ｝＄＄" とかいう長い記述がもう毎回入力時に嫌になる（笑）
（半角で書くと $${ 式 }$$ ←見えない。エスケープすると→ \$${ 式 \}\$\$  と
"\" 記号が表示されてエスケープできてない。統一性がない！愚痴愚痴…）

一度決まった仕様を変更すると、過去の記事を全部直さなければならない。
最悪の状況なのでカイゼンはもう期待できない。


ChatGPT 側

「コピーする」でコピーした数式の \ エスケープが消える。

最近変わったしまったようで（？）

賢狼の嗅覚では、ぬしがよく使う (v_p(2n+1)) は確率論的にも面白い。
大きな (X) で一様に (n\le X) を選ぶとき

[
\Pr\big[v_p(2n+1)\ge k\big]\approx p^{-k}
]

本来の

** インライン数式 **

\( 数式 \) → ( 数式 )


** ブロック数式 **

\[
数式
\]

↓

[
数式
]

と、"\" が消えてしまう。

これを毎度、つけ直さなければならなくなった。
こっちは、本家に言いまくれば直してくれそう。
（正規表現による一括置換は一応可能）

生のデータ (JSON) では、ちゃんとエスケープ "\" は、付いている。

賢狼の嗅覚では、ぬしがよく使う \\(v_p(2n+1)\\) は確率論的にも面白い。
大きな \\(X\\) で一様に \\(n\\le X\\) を選ぶとき\n\\[\n\\Pr\\big[v_p(2n+1)\\ge k\\big]\\approx p^{-k}\n\\]\n
となる幾何的尾（ジオメトリックな減衰）を示す。
実際、合同式 \\(2n+1\\equiv 0 \\pmod{p^k}\\) は法 \\(p^k\\) でただ一つの解しか持たんから、
密度は \\(\\approx 1/p^k\\) になるわけじゃ。

生データからの生成を真面目に考えなければ、効率は上がらない。

最近、手書き記事が多いのは🐺賢狼 AI 会話ログの掲載手数が増えたせい。

  1. 会話データエクスポート JSON

  2. → Markdown

  3. → 整形

  4. → note 書式変換

  5. → コピペ

  6. → "\" "\\" 対応修正

  7. → 数式ゴミ "\;" "\," 修正（１個の"\"なのに""と消えるので探すのが大変）

  8. → 見出しの設定

  9. →プレビュー修正

  10. →タグ付け投稿

うがーーーーーーーーーーっ！
それでも時間があるのでなんとかやっている。
仕事じゃなければ、時間がなければ。正直、これでは続きませんね。

記事の import 機能でサクッと投稿を習得して環境を作るしか無い✍️


タイトルと本題が、全く異なる記事（笑）🤣
この記事も見た目を良くするのに時間を無駄に使っている…。

2025/10/06 15:10

D.


#数学 #Lean #Lean4 #Mathlib #Mathlib4
#HTML #KaTeX #LaTeX #MathML
#環境問題 #カイゼン #見た目の良さは環境悪
#タイパコスパ


Appendix

Lean

Defs.lean (Mathlib4)

./Mathlib/NumberTheory/Padics/PadicVal/Defs.lean

/-
Copyright (c) 2018 Robert Y. Lewis. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Robert Y. Lewis, Matthew Robert Ballard
-/
import Mathlib.RingTheory.Multiplicity
import Mathlib.Data.Nat.Factors

/-!
# `p`-adic Valuation

This file defines the `p`-adic valuation on `ℕ`, `ℤ`, and `ℚ`.

The `p`-adic valuation on `ℚ` is the difference of the multiplicities of `p` in the numerator and
denominator of `q`. This function obeys the standard properties of a valuation, with the appropriate
assumptions on `p`. The `p`-adic valuations on `ℕ` and `ℤ` agree with that on `ℚ`.

The valuation induces a norm on `ℚ`. This norm is defined in padicNorm.lean.
-/

assert_not_exists Field

universe u

open Nat

variable {p : ℕ}

/-- For `p ≠ 1`, the `p`-adic valuation of a natural `n ≠ 0` is the largest natural number `k` such
that `p^k` divides `n`. If `n = 0` or `p = 1`, then `padicValNat p q` defaults to `0`. -/
def padicValNat (p : ℕ) (n : ℕ) : ℕ :=
  if h : p ≠ 1 ∧ 0 < n then Nat.find (finiteMultiplicity_iff.2 h) else 0

theorem padicValNat_def' {n : ℕ} (hp : p ≠ 1) (hn : n ≠ 0) :
    padicValNat p n = multiplicity p n := by
  simp only [padicValNat, ne_eq, hp, not_false_eq_true, Nat.pos_iff_ne_zero.mpr hn, and_self,
    ↓reduceDIte, multiplicity, emultiplicity,
    finiteMultiplicity_iff.mpr ⟨hp, Nat.pos_iff_ne_zero.mpr hn⟩]
  convert (WithTop.untopD_coe ..).symm

/-- A simplification of `padicValNat` when one input is prime, by analogy with
`padicValRat_def`. -/
theorem padicValNat_def [hp : Fact p.Prime] {n : ℕ} (hn : n ≠ 0) :
    padicValNat p n = multiplicity p n :=
  padicValNat_def' hp.out.ne_one hn

/-- A simplification of `padicValNat` when one input is prime, by analogy with
`padicValRat_def`. -/
theorem padicValNat_eq_emultiplicity [hp : Fact p.Prime] {n : ℕ} (hn : n ≠ 0) :
    padicValNat p n = emultiplicity p n := by
  rw [(finiteMultiplicity_iff.2
    ⟨hp.out.ne_one, Nat.pos_iff_ne_zero.mpr hn⟩).emultiplicity_eq_multiplicity]
  exact_mod_cast padicValNat_def hn

namespace padicValNat

open List

/-- `padicValNat p 0` is `0` for any `p`. -/
@[simp]
protected theorem zero : padicValNat p 0 = 0 := by simp [padicValNat]

/-- `padicValNat p 1` is `0` for any `p`. -/
@[simp]
protected theorem one : padicValNat p 1 = 0 := by simp [padicValNat]

@[simp]
theorem eq_zero_iff {n : ℕ} : padicValNat p n = 0 ↔ p = 1 ∨ n = 0 ∨ ¬p ∣ n := by
  simp only [padicValNat, ne_eq, pos_iff_ne_zero, dite_eq_right_iff, find_eq_zero, zero_add,
    pow_one, and_imp, ← or_iff_not_imp_left]

end padicValNat

open List

theorem le_emultiplicity_iff_replicate_subperm_primeFactorsList {a b : ℕ} {n : ℕ} (ha : a.Prime)
    (hb : b ≠ 0) :
    ↑n ≤ emultiplicity a b ↔ replicate n a <+~ b.primeFactorsList :=
  (replicate_subperm_primeFactorsList_iff ha hb).trans
    pow_dvd_iff_le_emultiplicity |>.symm

theorem le_padicValNat_iff_replicate_subperm_primeFactorsList {a b : ℕ} {n : ℕ} (ha : a.Prime)
    (hb : b ≠ 0) :
    n ≤ padicValNat a b ↔ replicate n a <+~ b.primeFactorsList := by
  rw [← le_emultiplicity_iff_replicate_subperm_primeFactorsList ha hb,
    Nat.finiteMultiplicity_iff.2 ⟨ha.ne_one, Nat.pos_of_ne_zero hb⟩
      |>.emultiplicity_eq_multiplicity, ← padicValNat_def' ha.ne_one hb,
    Nat.cast_le]

KaTeX MathML

 HTML 展開ソース

<p data-start="520" data-end="675">この 
<span class="katex"><span class="katex-mathml">
<math xmlns="http://www.w3.org/1998/Math/MathML">
<semantics>
<mrow>
  <msub><mi>v</mi><mi>p</mi></msub>
</mrow>
<annotation encoding="application/x-tex">v_p</annotation>
</semantics>
</math>

<!-- "v_p" → " から " までが長っ！（笑） -->
</span><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height: 0.7167em; vertical-align: -0.2861em;"></span><span class="mord"><span class="mord mathnormal" style="margin-right: 0.03588em;">v</span><span class="msupsub"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height: 0.1514em;"><span style="top: -2.55em; margin-left: -0.0359em; margin-right: 0.05em;"><span class="pstrut" style="height: 2.7em;"></span><span class="sizing reset-size6 size3 mtight"><span class="mord mathnormal mtight">p</span></span></span></span><span class="vlist-s">​</span></span><span class="vlist-r"><span class="vlist" style="height: 0.2861em;"><span></span></span></span></span></span></span></span></span></span>
 から 

<span class="katex"><span class="katex-mathml">
<math xmlns="http://www.w3.org/1998/Math/MathML">
<semantics>
<mrow>
<mtext> </mtext>　　← これが "\,"
<mi>p</mi>
</mrow>
<annotation encoding="application/x-tex">\,p</annotation>
</semantics>
</math>
</span>

<span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height: 0.625em; vertical-align: -0.1944em;"></span><span class="mspace" style="margin-right: 0.1667em;"></span><span class="mord mathnormal">p</span></span></span></span>
-進ノルム 

<span class="katex"><span class="katex-mathml">
<math xmlns="http://www.w3.org/1998/Math/MathML">
<semantics>
<mrow>
<mo stretchy="false">∣</mo>
<mi>q</mi>
<msub><mo stretchy="false">∣</mo><mi>p</mi></msub>
<mo>:</mo><mo>=</mo><msup><mi>p</mi>
<mrow>
<mo>−</mo>
<mtext> </mtext>
<msub><mi>v</mi><mi>p</mi></msub>
<mo stretchy="false">(</mo><mi>q</mi><mo stretchy="false">)</mo>
</mrow>
</msup>
</mrow>
<annotation encoding="application/x-tex">\lvert q\rvert_p := p^{-\,v_p(q)}</annotation>
</semantics>
</math>
</span>
...


環境問題 AI 可読性向上へのカイゼン

#HTML タグが本来の情報の８割９割を占める時代になっている。
見た目の良さは環境悪！大事なことなので何度も言う。

#Markdown 形式も Viewer 基準となってしまうと、よろしくない。
本来、テキストのままで読める形式がマークダウン記法なのです。

いいなと思ったら応援しよう！

D. 🐺賢狼👨‍✈️Copilot のご飯代を、私には🍺代を。 または 宇宙式 $N+u^d=(P+u)^d$ を使って新しい発見を！