# 帶符號整數的3進因子抽取 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-p-adic-valuation-integers/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-p-adic-valuation-integers-01 · ocme-new142-reader-adoption-20261021 ## 目標與範圍 v₃(−108)=3、v₃(18)=2、v₃(−1944)=5、v₃(−90)=2；零用infinity。 prime3的exact extraction、product與sum laws實例及一般unequal-sum論證，不作completion。 ## 已知條件與符號 - calc - G1 — p=3為prime，a=−108,b=18；v_p(0)唯一序列化字串sentinel為infinity。 - u,v — 去prime後units，可負 - v_p(0) — infinity字串 ## 規則與來源 - calc · prerequisite — 假設精確整數算術、帶餘除法、整除與gcd的定義；同餘等式始終綁定明示模數。假設整數唯一質因數分解與prime不整除兩個因子時也不整除乘積。 - mko_definition · cited — prime p≥2；a≠0時以|a|=p^k*u且p不整除u的唯一k定義v_p(a)，負a合法並先取絕對值。固定可序列化sentinel `infinity` 表示v_p(0)。exact families核factor extraction、v_p(ab)=v_p(a)+v_p(b)與v_p(a+b)≥min；只有v_p(a)≠v_p(b)時保證sum equality。nonprime base不屬p-adic valuation，含零identity依infinity convention分開。 · mko-p-adic-valuation-integers ## 逐步主鏈 S01 · implies操作前 p=3,\quad a=-108 操作後 |a|=108=3^3\cdot4,\quad3\nmid4\Rightarrow v_3(a)=3 條件：無 規則：calc · 依賴：G1 葉節點依據：calc 負號先取絕對值，連除3得到36、12、4，最後4不再被3整除。 S02 · implies操作前 b=18 操作後 18=3^2\cdot2,\quad3\nmid2\Rightarrow v_3(b)=2 條件：無 規則：calc · 依賴：G1, S01 葉節點依據：calc 完整抽取18→6→2，得到另一個非零輸入的unit。 S03 · implies操作前 ab=-1944 操作後 |ab|=3^{3+2}(4\cdot2)=3^5\cdot8,\quad3\nmid8\Rightarrow v_3(ab)=5 條件：無 規則：calc · 依賴：G1, S01, S02 葉節點依據：calc prime不整除兩unit的乘積，因此product的抽取指數恰為和5。 S04 · implies操作前 a+b=-90 操作後 90=3^2\cdot10,\quad3\nmid10\Rightarrow v_3(a+b)=2=\min(3,2) 條件：無 規則：calc · 依賴：G1, S01, S02 葉節點依據：calc 和的直接抽取給不等valuation時的等號實例。 S05 · implies操作前 a=p^ru,\quad b=p^sv,\quad r1 條件：無 規則：calc · 依賴：G1, S05 葉節點依據：calc 相等valuation不保證sum等於最小值，這裡因括號1+2被3整除而升高。 S07 · implies操作前 -108+108=0 操作後 v_3(0)=\texttt{infinity},\quad\texttt{infinity}>k\ (k\in\mathbb N_0) 條件：無 規則：mko_definition · 依賴：G1, S01, S06 葉節點依據：mko_definition 完全抵消時固定字串infinity；它大於每個非負整數，min(infinity,k)=k、infinity+k=infinity，並另定infinity+infinity=infinity及min(infinity,infinity)=infinity。 S08 · implies操作前 v_p(a)=r,\quad v_p(b)=s\text{ finite} 操作後 p^{\min(r,s)}\mid a+b\Rightarrow v_p(a+b)\ge\min(r,s) 條件：無 規則：calc · 依賴：G1, S05, S06, S07 葉節點依據：calc 兩項皆被較低prime power整除，故和也被整除；和為零則infinity仍符合下界。 S09 · implies操作前 \text{base }4,\quad a=b=2 操作後 v_4(2)=0,\quad v_4(4)=1\ne0+0 條件：無 規則：calc · 依賴：G1, S03, S08 葉節點依據：calc 合數底的最高整除次數可能破product law，因此不能稱本定義的p-adic valuation。 ## 局部子步與引理 本稿無局部子步。 ## 逐步反向審查 - S09 · premise_audit · G1, S03, S08 — 這不否證prime3的證書，而是指出prime base不可省。 - S08 · premise_audit · G1, S05, S06, S07 — 只有r≠s由S05保證等號，r=s不可升格。 - S07 · premise_audit · G1, S01, S06 — 若一個輸入為零，乘積為零，其 valuation 為 infinity；和等於另一個輸入，因此和的 valuation 等於另一輸入的 valuation。若兩個輸入皆為零，和仍為零，其 valuation 為 infinity，皆符合這套約定。 - S06 · premise_audit · G1, S05 — 反例只否證總有等號，仍符合sum inequality。 - S05 · premise_audit · G1, S04 — a或b可負，u、v亦可負；nondivisibility仍成立。 - S04 · premise_audit · G1, S01, S02 — −90先取絕對值；不以有理近似log計指數。 - S03 · premise_audit · G1, S01, S02 — 這裡unit乘積8不被3整除；不是只驗3⁵整除就停止。 - S02 · premise_audit · G1, S01 — 兩個輸入均非零，有限整數valuation3、2可直接相加。 - S01 · premise_audit · G1 — 若只除到12會低估valuation；最高次需最後unit檢查。 ## 錯誤控制與反例 最高次|a|=p^k u後必核p不整除u才定k。 零sentinel零唯一用字串infinity，不用0或未標記NaN。 - 負整數a無valuation。 → reject — 按絕對值抽取，−108值3。 - 所有sum valuation都等於min。 → reject — 3+6=9，2>1。 - 合數底4也保留product law。 → reject — 2·2=4使1≠0+0。 ## 結論與限制 v₃(−108)=3、v₃(18)=2、v₃(−1944)=5、v₃(−90)=2；零用infinity。 ## 驗證及來源綁定 3 個本稿宣告算術檢查；只支持所列算式。 - source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f - adopted source SHA-256: 95c4e2650117d3d500f2fb521401fae53535c51db055a8d4462a820e89c80a8d - original source SHA-256: 1baa04ecf21c750d6a25a649db9321d708caa5c1eac27fabb94edf46138ffe75 - Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW [同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-p-adic-valuation-integers-01.json)