# 逐代表計算φ(12)

[← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-euler-totient-function/)

這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。

derivation-mko-euler-totient-function-01 · ocme-new142-reader-adoption-20261021



## 目標與範圍

φ(12)=4，φ(1)=1，且本例φ(3·4)=φ(3)φ(4)。

固定1≤k≤n的完整有限代表系；乘法性只核互質實例。





## 已知條件與符號


- calc


- G1 — n=12，以gcd(k,12)=1計數，代表恰為1、2、3、4、5、6、7、8、9、10、11、12。


- \varphi(n) — 互質代表數
- U_n — 完整reduced代表系





## 規則與來源


- calc · prerequisite — 假設精確整數算術、帶餘除法、整除與gcd的定義；同餘等式始終綁定明示模數。
- mko_definition · cited — 本輪一致使用1≤k≤n的完整代表範圍，以gcd(k,n)=1計數。乘法性只核gcd(m,n)=1的明示實例，不由非互質實例外推。 · mko-euler-totient-function





## 逐步主鏈

S01 · implies操作前

1\le k\le12

操作後

K=\{1,2,3,4,5,6,7,8,9,10,11,12\}

條件：無

規則：calc · 依賴：G1

葉節點依據：calc

先完整列12個代表，無0也沒有重複終點。



S02 · implies操作前

k=1,2,3,4,5,6

操作後

\gcd(k,12)=1,2,3,4,1,6\text{ respectively}

條件：無

規則：calc · 依賴：G1, S01

葉節點依據：calc

完整前六項以整除計gcd；只有1與5互質。



S03 · implies操作前

k=7,8,9,10,11,12

操作後

\gcd(k,12)=1,4,3,2,1,12\text{ respectively}

條件：無

規則：calc · 依賴：G1, S01

葉節點依據：calc

後六項全部核完，互質者為7與11。



S04 · implies操作前

U_{12}=\{1,5,7,11\}

操作後

\varphi(12)=|U_{12}|=4

條件：無

規則：mko_definition · 依賴：G1, S02, S03

葉節點依據：mko_definition

兩段完整gcd清單給所有且只有四個互質代表。



S05 · implies操作前

n=1,\quad K_1=\{1\}

操作後

\gcd(1,1)=1\Rightarrow\varphi(1)=1

條件：無

規則：calc · 依賴：G1

葉節點依據：calc

按同一1到n慣例，n=1有一個合法且互質的代表。



S06 · implies操作前

K_3=\{1,2,3\},\quad K_4=\{1,2,3,4\}

操作後

U_3=\{1,2\},\quad U_4=\{1,3\},\quad\varphi(3)=2,\ \varphi(4)=2

條件：無

規則：calc · 依賴：G1

葉節點依據：calc

分別完整gcd清單為(1,1,3)與(1,2,1,4)，得到兩個值。



S07 · implies操作前

\gcd(3,4)=1,\quad12=3\cdot4

操作後

\varphi(12)=4=2\cdot2=\varphi(3)\varphi(4)

條件：無

規則：calc · 依賴：G1, S04, S06

葉節點依據：calc

互質前提成立，再以已算值核本次乘法性實例。



S08 · implies操作前

U_2=\{1\},\quad U_8=\{1,3,5,7\}

操作後

\varphi(2)\varphi(4)=1\cdot2=2\ne4=\varphi(8)

條件：無

規則：calc · 依賴：G1, S06, S07

葉節點依據：calc

完整模8 gcd清單(1,2,1,4,1,2,1,8)顯示非互質乘數2、4不能無條件相乘。







## 局部子步與引理

本稿無局部子步。





## 逐步反向審查


- S08 · premise_audit · G1, S06, S07 — 此反例否證省略互質假設，不否證S07。
- S07 · premise_audit · G1, S04, S06 — 只是指定互質實例，不由此推一般乘法性定理。
- S06 · premise_audit · G1 — 兩個小代表系皆含自己的終點，但終點不互質。
- S05 · premise_audit · G1 — 不能套n≥2時n不互質的觀察到n=1。
- S04 · premise_audit · G1, S02, S03 — 未計互質數對或proper divisors；φ只數此代表集合。
- S03 · premise_audit · G1, S01 — 12在代表系中但gcd(12,12)=12，不能誤算為unit。
- S02 · premise_audit · G1, S01 — 例如gcd(5,12)=1因12=2·5+2且5=2·2+1。
- S01 · premise_audit · G1 — 本輪採1到n，不得另加0再計一次同類。





## 錯誤控制與反例

代表系全稿使用1至n，不混用0至n−1。

互質門檻乘法性題先核gcd(m,n)=1。


- φ(12)=5因0也互質。 → reject — 0不在1到12，且gcd(0,12)=12。
- φ(1)=0。 → reject — 唯一代表1與1互質。
- 任意m,n均有φ(mn)=φ(m)φ(n)。 → reject — m=2,n=4給4≠2。





## 結論與限制

φ(12)=4，φ(1)=1，且本例φ(3·4)=φ(3)φ(4)。







## 驗證及來源綁定

2 個本稿宣告算術檢查；只支持所列算式。


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: ca0b196e2434f2d382e24c3145852b45b5cf3005501150b6d891d5af24fa9d03
- original source SHA-256: ca0b196e2434f2d382e24c3145852b45b5cf3005501150b6d891d5af24fa9d03
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

[同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-euler-totient-function-01.json)