# 離散時間動力系統：在七個狀態上迭代 T(x)=(3x+1) mod 7 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-discrete-dynamical-system/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-discrete-dynamical-system-01 · production-20261019-adopted-96 ## 目標與範圍 狀態空間 X={0,1,2,3,4,5,6}，更新映射 T(x)=(3x+1) mod 7。由 x_0=0 依 x_(n+1)=T(x_n) 算出軌道，證明對所有自然數 n 有 x_(n+6)=x_n，據此求 x_2026；完整枚舉固定點；判定 A={0,1,2,4,5,6} 是正向不變子集而 B={0,1} 不是，並證明從 0 出發的軌道永遠不會到達固定點。 只處理這一個完整明示的有限系統（MKO 假設 a1、a2）。所有結論都是關於這 7 個狀態的精確陳述：週期性以數學歸納法證明，固定點與不變子集以完整枚舉證明。不外推到連續時間、其他仿射參數、漸近穩定性或混沌。不改動 canonical MKO 或英文 edition。 ## 已知條件與符號 - function_def - division_algorithm - nat_induction - subset_def - image_preimage_def - G1 — X={0,1,2,3,4,5,6}；時間索引為包含 0 的自然數。 - G2 — T:X→X，T(x)=(3x+1) mod 7，其中 m mod 7 是整數 m 除以 7 的餘數 r（0≤r<7）。 - G3 — 初始狀態 x_0=0，對每個自然數 n，x_(n+1)=T(x_n)。 - G4 — 待檢查的子集 A={0,1,2,4,5,6} 與 B={0,1}。 - X — 狀態空間 {0,1,2,3,4,5,6} - T — 更新映射 T(x)=(3x+1) mod 7 - x_n — 第 n 個時間的狀態 - m\bmod 7 — 整數 m 除以 7 的餘數 - T(A) — A 在 T 下的像 - A,\ B — 兩個待檢查的子集 ## 規則與來源 - function_def · prerequisite — 函數：f:A→B 對每個 a∈A 指定恰好一個 f(a)∈B。兩函數相等 ⇔ 定義域、對應域相同且對每個 a 都有相同值。 - division_algorithm · prerequisite — 帶餘除法：對整數 a 與正整數 b，存在唯一的整數 q、r 使 a=bq+r 且 0≤r0 規則：division_algorithm · 依賴：G1, G2 葉節點依據：division_algorithm + function_def 對每個 x∈X，3x+1 是整數；帶餘除法給出唯一的整數 q、r 使 3x+1=7q+r 且 0≤r<7，於是 T(x)=r 恰是 X 的一個元素。存在性說明 T 對每個狀態都有值（總映射），唯一性說明值是確定的（函數），0≤r<7 說明值落在 X 中（自映射）。這正是 MKO 假設 a1 的要求。 S03 · equivalent操作前 T(0),T(1),T(2),T(3),T(4),T(5),T(6) 操作後 1,\ 4,\ 0,\ 3,\ 6,\ 2,\ 5 條件：無 規則：numeric_evaluation · 依賴：S02 葉節點依據：numeric_evaluation + division_algorithm 完整列出 T 的值表，計算在 S03.1 與 S03.2。因為 X 只有 7 個狀態，這張表就是 T 的全部資料，之後的枚舉都以它為依據。 S04 · implies操作前 x_0=0 操作後 x_1=1,\ x_2=4,\ x_3=6,\ x_4=5,\ x_5=2,\ x_6=0 條件：無 規則：eq_replace · 依賴：G3, S03 葉節點依據：eq_replace + numeric_evaluation 依遞迴式查表：x_1=T(0)=1，x_2=T(1)=4，x_3=T(4)=6，x_4=T(6)=5，x_5=T(5)=2，x_6=T(2)=0。每一步只用到前一個狀態，這就是迭代演算法。 S05 · implies操作前 x_6=0,\ x_0=0 操作後 x_6=x_0 條件：無 規則：eq_refl_symm_trans · 依賴：S04, G3 葉節點依據：eq_refl_symm_trans x_6 與 x_0 都等於 0，依等號的對稱與傳遞得 x_6=x_0：軌道在第 6 步回到起點。 S06 · implies操作前 x_6=x_0 操作後 \forall n\in\mathbb{N}:\ x_{n+6}=x_n 條件：無 規則：L_period · 依賴：S05, L_period 葉節點依據：nat_induction + eq_congruence 依引理 L_period（在 S06.1 到 S06.3 以數學歸納法證明）。關鍵是決定性：下一個狀態只由目前狀態決定，所以兩個時刻狀態相同，之後就永遠同步。這不是由六個數值外推得到的。 S07 · implies操作前 \forall n:\ x_{n+6}=x_n 操作後 \forall q,r\in\mathbb{N}:\ x_{6q+r}=x_r 條件：無 規則：L_reduce · 依賴：S06, L_reduce 葉節點依據：nat_induction + L_period 依引理 L_reduce（在 S07.1 到 S07.3 對 q 歸納證明）：時間每加 6，狀態不變，所以可以一次去掉任意多個 6。 S08 · equivalent操作前 2026 操作後 2026=6\cdot 337+4,\ 0\le 4<6 條件：6>0 規則：division_algorithm · 依賴：division_algorithm 葉節點依據：division_algorithm + numeric_evaluation 把時間 2026 除以週期 6：6·337=2022，2026−2022=4，餘數 4 滿足 0≤4<6。 S09 · equivalent操作前 x_{2026} 操作後 x_{2026}=x_{6\cdot 337+4}=x_4=5 條件：無 規則：L_reduce · 依賴：S07, S08, S04 葉節點依據：L_reduce + eq_replace + eq_refl_symm_trans 依 S08 改寫指標，再依 L_reduce（q=337、r=4）得 x_2026=x_4，由 S04 得 x_4=5。這個值是證明出來的，不是由前幾項的樣子猜出來的。 S10 · equivalent操作前 \{x\in X\mid T(x)=x\} 操作後 \{3\} 條件：無 規則：case_analysis · 依賴：S03, G1, mko_dds_props 葉節點依據：case_analysis + set_extensionality + set_builder 依值表逐一比較：T(0)=1≠0，T(1)=4≠1，T(2)=0≠2，T(3)=3，T(4)=6≠4，T(5)=2≠5，T(6)=5≠6。七種情況就是 X 的全部狀態，所以這個枚舉是完整的，證明了固定點集合恰為 {3}。 S11 · equivalent操作前 3x+1\equiv x\pmod 7 操作後 x\equiv 3\pmod 7 條件：4\cdot 2\equiv 1\pmod 7 規則：mod7_arith · 依賴：G2, S10 葉節點依據：mod7_arith + eq_congruence 獨立的代數交叉核對。對 x∈X，x 就是自己的餘數，所以 T(x)=x 等價於 3x+1≡x (mod 7)。兩邊同減 x+1 得 2x≡−1≡6；兩邊同乘 4（因 4·2≡1）得 x≡24≡3。X 中這個同餘類的唯一代表是 3，與 S10 的枚舉一致。 S12 · implies操作前 y_0=3,\ y_{n+1}=T(y_n) 操作後 \forall n:\ y_n=3 條件：無 規則：nat_induction · 依賴：S10, G2 葉節點依據：nat_induction + eq_replace 從固定點出發的軌道（另記為 y_n）是常數：基底 y_0=3；若 y_n=3，則 y_(n+1)=T(3)=3。依歸納對所有 n 成立。 S13 · implies操作前 T(A),\ A=\{0,1,2,4,5,6\} 操作後 T(A)=\{1,4,0,6,2,5\}=A\subseteq A 條件：無 規則：mko_dds_props · 依賴：S03, G4, mko_dds_props 葉節點依據：image_preimage_def + subset_def + set_extensionality 逐元素取像：T(0)=1，T(1)=4，T(2)=0，T(4)=6，T(5)=2，T(6)=5，所以 T(A)={1,4,0,6,2,5}，與 A 元素相同。每個像都在 A 中，T(A)⊆A，A 是正向不變子集。 S14 · implies操作前 T(1)=4,\ B=\{0,1\} 操作後 4\notin B\ \Rightarrow\ T(B)\not\subseteq B 條件：無 規則：quantifier_negation · 依賴：S03, G4, mko_dds_props 葉節點依據：quantifier_negation + subset_def 正向不變要求 B 的每個元素的像都在 B 中。1∈B 但 T(1)=4∉B，找到一個反例就否定了「對所有元素」，所以 B 不是正向不變的；T(0)=1∈B 不能挽救。 S15 · implies操作前 x_0=0\in A,\ T(A)\subseteq A 操作後 \forall n:\ x_n\in A,\ \text{hence }x_n\neq 3 條件：無 規則：nat_induction · 依賴：S13, G3, G4 葉節點依據：nat_induction + image_preimage_def + subset_def 基底：x_0=0∈A。歸納步：若 x_n∈A，則 x_(n+1)=T(x_n)∈T(A)⊆A。所以每個 x_n 都在 A 中；而 3∉A，故對每個 n 有 x_n≠3：從 0 出發的軌道永遠不會到達固定點 3。這是對所有 n 的證明，不是觀察有限前綴。 S16 · implies操作前 \text{proved facts about }(X,T) 操作後 x_{n+6}=x_n,\ x_{2026}=5,\ \mathrm{Fix}(T)=\{3\},\ T(A)\subseteq A,\ T(B)\not\subseteq B 條件：無 規則：and_intro_elim · 依賴：S06, S09, S10, S13, S14, S15 葉節點依據：and_intro_elim 合併結論：從 0 出發的軌道週期為 6 且 x_2026=5；唯一固定點是 3；A 正向不變而 B 不是；軌道永不到達 3。全部是關於這個有限系統的精確陳述。 ## 局部子步與引理 S03.1 · equivalent操作前 3x+1\ \text{for }x=0,1,2,3,4,5,6 操作後 1,\ 4,\ 7,\ 10,\ 13,\ 16,\ 19 條件：無 規則：numeric_evaluation · 依賴：G2 葉節點依據：numeric_evaluation 逐一計算 3x+1：3·0+1=1，3·1+1=4，3·2+1=7，3·3+1=10，3·4+1=13，3·5+1=16，3·6+1=19。 S03.2 · equivalent操作前 1,4,7,10,13,16,19\ \bmod 7 操作後 1,\ 4,\ 0,\ 3,\ 6,\ 2,\ 5 條件：0\le r<7 規則：division_algorithm · 依賴：S03.1, division_algorithm 葉節點依據：division_algorithm + numeric_evaluation 寫出帶餘除法：1=7·0+1，4=7·0+4，7=7·1+0，10=7·1+3，13=7·1+6，16=7·2+2，19=7·2+5。每個餘數都在 0 到 6 之間，所以由唯一性它就是 mod 7 的值。 S06.1 · induction_base操作前 n=0 操作後 x_{0+6}=x_0 條件：無 規則：nat_induction · 依賴：S05 葉節點依據：nat_induction 基底：令 P(n) 為 x_(n+6)=x_n。P(0) 就是 x_6=x_0，已由 S05 給出。 S06.2 · induction_step操作前 x_{n+6}=x_n 操作後 x_{(n+1)+6}=x_{n+1} 條件：無 規則：eq_congruence · 依賴：G3, G2 葉節點依據：eq_congruence + function_def 歸納步：假設 x_(n+6)=x_n。兩邊同用函數 T：T(x_(n+6))=T(x_n)。依遞迴式左邊是 x_(n+7)，右邊是 x_(n+1)，所以 x_((n+1)+6)=x_(n+1)。 S06.3 · implies操作前 P(0),\ \forall n\,(P(n)\Rightarrow P(n+1)) 操作後 \forall n\in\mathbb{N}:\ x_{n+6}=x_n 條件：無 規則：nat_induction · 依賴：S06.1, S06.2 葉節點依據：nat_induction 依數學歸納原理，P(n) 對每個自然數 n 成立。S06.1 到 S06.3 合起來證得引理 L_period。 S07.1 · induction_base操作前 q=0 操作後 x_{6\cdot 0+r}=x_r 條件：無 規則：nat_induction · 依賴：G3 葉節點依據：nat_induction + mul_zero + add_zero 固定任意自然數 r，令 R(q) 為 x_(6q+r)=x_r。R(0) 成立，因為 6·0+r=r。 S07.2 · induction_step操作前 x_{6q+r}=x_r 操作後 x_{6(q+1)+r}=x_r 條件：無 規則：L_period · 依賴：S06 葉節點依據：L_period + distributive + add_assoc + add_comm + eq_refl_symm_trans 假設 R(q)。因 6(q+1)+r=(6q+r)+6，依 L_period（取 n=6q+r）得 x_(6(q+1)+r)=x_(6q+r)，再由歸納假設等於 x_r。 S07.3 · implies操作前 R(0),\ \forall q\,(R(q)\Rightarrow R(q+1)) 操作後 \forall q,r:\ x_{6q+r}=x_r 條件：無 規則：nat_induction · 依賴：S07.1, S07.2 葉節點依據：nat_induction + forall_intro 依歸納原理 R(q) 對所有 q 成立；r 是任意固定的，所以依全稱推廣對所有 r 也成立。S07.1 到 S07.3 合起來證得引理 L_reduce。 ## 逐步反向審查 - S16 · sufficient_goal_reduction · S06, S09, S10, S13, S14, S15, and_intro_elim — 目標 G：本稿目標列出的各項判定。足夠條件 H：S06、S09、S10、S13、S14、S15 各自已證（H⇒G 由合取引入）。H 由給定條件正向推出，沒有把 G 當作前提。 - S15 · premise_audit · S13, nat_induction, image_preimage_def — 需要初始狀態在 A 中與 A 的正向不變性；兩者缺一，結論都不成立。 - S14 · premise_audit · S03, quantifier_negation, subset_def — 否定全稱只需要一個反例 x=1；這裡不宣稱 B 中所有元素都會離開 B。 - S13 · premise_audit · S03, image_preimage_def, subset_def, mko_dds_props — 需要 A 的六個元素全部檢查過，這裡確實全部列出。只檢查部分元素不足以推出包含關係。 - S12 · premise_audit · S10, nat_induction, eq_replace — 只需要 T(3)=3。這不表示其他軌道會趨向 3（見 S15）。 - S11 · inverse_equivalence · mod7_arith, eq_congruence — 乘 4 與乘 2 在模 7 下互為反運算（8≡1），減 x+1 與加 x+1 互為反運算，所以每一步雙向成立。 - S10 · inverse_equivalence · case_analysis, set_extensionality, S03 — 集合相等的兩個包含：3 在集合中（T(3)=3）；集合中的元素必是 3（其他六個都不滿足）。完整性來自 X 只有這七個狀態。 - S09 · inverse_equivalence · L_reduce, S08, S04, eq_refl_symm_trans — 這是一串等式，每個等號都有理由（指標相等、引理、計算），等號對稱，雙向成立。 - S08 · inverse_equivalence · division_algorithm, numeric_evaluation — 6·337+4 可算回 2026；帶餘除法保證商與餘數唯一。 - S07.3 · premise_audit · S07.1, S07.2, nat_induction, forall_intro — 全稱推廣可用，因為證明中對 r 沒有附加任何條件。 - S07.2 · premise_audit · S06, distributive, add_assoc, add_comm, eq_refl_symm_trans — 需要指標的改寫 6(q+1)+r=(6q+r)+6（分配律、加法結合與交換）以及 L_period；這裡使用的是另一個已證引理，不是正在證明的 L_reduce。 - S07.1 · premise_audit · nat_induction, mul_zero, add_zero — 只用到 6·0=0 與 0+r=r。 - S07 · premise_audit · L_reduce — 依賴該引理；引理只用到 L_period。 - S06.3 · premise_audit · S06.1, S06.2, nat_induction — 歸納原理的兩個前提分別是 S06.1 與 S06.2，n 在歸納步中是任意的。 - S06.2 · premise_audit · G3, eq_congruence, function_def — 需要 T 是函數（同一輸入得同一輸出），以及遞迴式對每個 n 成立。不宣稱反向：由 x_(n+7)=x_(n+1) 推回 x_(n+6)=x_n 需要 T 單射，這裡沒有用到。 - S06.1 · premise_audit · S05, nat_induction — 基底只需要 S05 的計算。 - S06 · premise_audit · L_period — 依賴該引理；引理只用到 S05 與 T 是函數。 - S05 · premise_audit · S04, eq_refl_symm_trans — 只是一個已算出的等式；它本身尚未說明之後的狀態，那需要 S06 的歸納。 - S04 · premise_audit · G3, S03, eq_replace — 需要 x_0 與完整的值表；每個值由前一個值唯一決定。由 x_6 不能反推 x_5 是否唯一，這裡也不宣稱。 - S03.2 · inverse_equivalence · division_algorithm, numeric_evaluation — 每個等式 7q+r 都可展開回原數；餘數條件 0≤r<7 保證這是唯一的分解。 - S03.1 · inverse_equivalence · numeric_evaluation — 整數算式的精確求值，雙向都是同一個數。 - S03 · inverse_equivalence · numeric_evaluation, division_algorithm — 每一項都是同一個數的兩種寫法，可以獨立重算；反向即把 r 寫回 3x+1=7q+r。 - S02 · premise_audit · division_algorithm, function_def — 需要除數 7>0。此步不宣稱 T 是雙射；那件事可由 S03 的表看出，但後面沒有用到。 - S01 · premise_audit · G1, G2, G3, mko_dds — 此步只寫出系統與軌道的定義，不推出新事實；T 是否確實為 X 上的總自映射在 S02 檢查。 ## 錯誤控制與反例 幾個迭代值不是長期行為的證明MKO 指出常見誤解是把幾個迭代值當成長期行為的證明。x_0 到 x_5 互不相同，看起來像永不重複，但 x_6 回到 0。即使看到回到起點，「對所有 n 有 x_(n+6)=x_n」仍需論證：本稿用 S06 的歸納，依據是 T 為函數（決定性），而不是多算幾項。無論狀態空間是否有限，未結合更新規則的有限觀察都不能自動證明長期行為；但在已知的確定性規則下，一次返回可由同樣歸納推出週期性，無須假定狀態空間有限。 離散更新不是微分方程x_(n+1)=T(x_n) 在本模型只指定整數時間的狀態，沒有指定 n 與 n+1 之間的狀態；差 x_(n+1)−x_n 也不是導數。狀態是模 7 的餘數，本稿未給連續時間參數、所需拓撲或插值規則。可以另加外部嵌入與插值，但那是額外模型，並非本遞迴式已定義的狀態或動力學；本稿不作連續時間、流或穩定性的宣稱。 只有 X 不夠，還要 T同一個 X 配上 T′(x)=(x+1) mod 7，從 0 出發得 x_n=n mod 7，x_2026=3 而不是 5，且沒有任何固定點。MKO 說初始狀態與更新映射共同決定軌道；只知道狀態集合與初值，無法回答本稿的任何問題。 - x_0 到 x_5 互不相同，所以這條軌道永不重複 → reject — x_6=T(2)=0=x_0（S05），且之後每 6 步重複（S06）。 - 固定點 3 吸引其他狀態，從 0 出發的軌道最後會停在 3 → reject — S15 證明對所有 n 有 x_n∈A，而 3∉A，所以軌道永不到達 3。 - B={0,1} 正向不變，因為 T(0)=1∈B → reject — 正向不變要求每個元素；T(1)=4∉B（S14）。 - 只要知道 X={0,1,2,3,4,5,6} 與 x_0=0，就能決定 x_2026 → reject — 換成 T′(x)=(x+1) mod 7 時 x_2026=2026 mod 7=3（N11），與本系統的 5 不同。 ## 結論與限制 對 X={0,1,2,3,4,5,6} 與 T(x)=(3x+1) mod 7：從 0 出發的軌道為 0,1,4,6,5,2,0，並由歸納證明對所有 n 有 x_(n+6)=x_n，因此 x_2026=x_4=5；完整枚舉顯示唯一固定點是 3；A={0,1,2,4,5,6} 正向不變，B={0,1} 因 T(1)=4 而不是；從 0 出發的軌道永遠留在 A 中，不會到達 3。 - N5 與 N8 是對 X 全部 7 個狀態的有限核對；因為 X 恰有這 7 個狀態，它們涵蓋本系統的整個狀態空間，但對其他模數或其他映射不說明任何事。 - 吸引性、穩定性與參數族 T(x)=(ax+b) mod m 的分類不在本稿範圍內，屬於 MKO 的 formal next。 ## 驗證及來源綁定 11 個本稿宣告算術檢查；只支持所列算式。 - source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f - adopted source SHA-256: f4f2e74cd790417e54c77f714258d8957de8bb95a06fb7dd5979e531097dd264 - original source SHA-256: 13f802958297845385be7005be78cf9e3990a132a4a30724815269c12dedd6a6 - Lean: NOT_RUN · independent AI: NOT_MEASURED [同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-discrete-dynamical-system-01.json)