離散時間動力系統：在七個狀態上迭代 T(x)=(3x+1) mod 7

目標與範圍

狀態空間 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≤r<b。
• nat_induction · prerequisite — 數學歸納原理：對從 n₀ 起的命題族 P(n)，若 P(n₀) 成立，且對每個 n≥n₀ 都有 P(n)⇒P(n+1)，則所有 n≥n₀ 都有 P(n)。
• subset_def · prerequisite — 子集：A⊆B 表示 A 的每個元素都是 B 的元素，即 ∀x (x∈A⇒x∈B)。
• image_preimage_def · prerequisite — 像與原像：f(S)={f(a) ∣ a∈S}；f⁻¹(T)={a∈A ∣ f(a)∈T}。原像記號不預設 f 有反函數。
• def_intro · prerequisite — 引入定義：可為一個命題、式子或物件取名；之後名稱與被定義者可互相替換。
• numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
• eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
• eq_refl_symm_trans · prerequisite — 等號的性質：u=u；若 u=v 則 v=u；若 u=v 且 v=w 則 u=w。
• eq_congruence · prerequisite — 等式同用：若 u=v，對兩邊做同一個有定義的運算 f，得 f(u)=f(v)。只對一邊做運算不屬於此規則。
• mul_zero · prerequisite — 乘以零：u·0=0。理由：u·0=u·(0+0)=u·0+u·0，兩邊同減 u·0 得 0=u·0。
• add_zero · prerequisite — 加法單位元：u+0=u。
• distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
• add_assoc · prerequisite — 加法結合律：(u+v)+w=u+(v+w)。
• add_comm · prerequisite — 加法交換律：u+v=v+u。
• forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
• case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
• set_extensionality · prerequisite — 集合相等：A=B 當且僅當 A⊆B 且 B⊆A，即兩者有相同元素。
• set_builder · prerequisite — 集合建構式：x∈{y∈A ∣ P(y)} 當且僅當 x∈A 且 P(x)。
• quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
• and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
• mko_dds · cited — 離散時間動力系統由狀態空間 X 與自映射 T:X→X 組成。給定初始狀態 x_0∈X，以 x_(n+1)=T(x_n) 定義其前向軌道。 · mko-discrete-dynamical-system
• mko_dds_props · cited — 固定點滿足 T(x)=x；正向不變子集 A 滿足 T(A)⊆A。有限狀態時可完整枚舉這些局部性質。 · mko-discrete-dynamical-system
• mod7_arith · prerequisite — 模 7 同餘：u≡v (mod 7) 表示 7∣(u−v)；同餘與加法、乘法相容；因 4·2=8≡1 (mod 7)，2 在模 7 下有逆元 4；X 中每個同餘類恰有一個代表。
• L_period · lemma — 對每個自然數 n，x_(n+6)=x_n。
• L_reduce · lemma — 對所有自然數 q、r，x_(6q+r)=x_r。

逐步主鏈

\text{state space and update rule}

(X,T),\ X=\{0,1,2,3,4,5,6\},\ x_{n+1}=T(x_n),\ x_0=0

x\in X

T(x)=(3x+1)\bmod 7\in X

T(0),T(1),T(2),T(3),T(4),T(5),T(6)

1,\ 4,\ 0,\ 3,\ 6,\ 2,\ 5

x_0=0

x_1=1,\ x_2=4,\ x_3=6,\ x_4=5,\ x_5=2,\ x_6=0

x_6=0,\ x_0=0

x_6=x_0

x_6=x_0

\forall n\in\mathbb{N}:\ x_{n+6}=x_n

\forall n:\ x_{n+6}=x_n

\forall q,r\in\mathbb{N}:\ x_{6q+r}=x_r

2026

2026=6\cdot 337+4,\ 0\le 4<6

x_{2026}

x_{2026}=x_{6\cdot 337+4}=x_4=5

\{x\in X\mid T(x)=x\}

\{3\}

3x+1\equiv x\pmod 7

x\equiv 3\pmod 7

y_0=3,\ y_{n+1}=T(y_n)

\forall n:\ y_n=3

T(A),\ A=\{0,1,2,4,5,6\}

T(A)=\{1,4,0,6,2,5\}=A\subseteq A

T(1)=4,\ B=\{0,1\}

4\notin B\ \Rightarrow\ T(B)\not\subseteq B

x_0=0\in A,\ T(A)\subseteq A

\forall n:\ x_n\in A,\ \text{hence }x_n\neq 3

\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

局部子步與引理

3x+1\ \text{for }x=0,1,2,3,4,5,6

1,\ 4,\ 7,\ 10,\ 13,\ 16,\ 19

1,4,7,10,13,16,19\ \bmod 7

1,\ 4,\ 0,\ 3,\ 6,\ 2,\ 5

n=0

x_{0+6}=x_0

x_{n+6}=x_n

x_{(n+1)+6}=x_{n+1}

P(0),\ \forall n\,(P(n)\Rightarrow P(n+1))

\forall n\in\mathbb{N}:\ x_{n+6}=x_n

q=0

x_{6\cdot 0+r}=x_r

x_{6q+r}=x_r

x_{6(q+1)+r}=x_r

R(0),\ \forall q\,(R(q)\Rightarrow R(q+1))

\forall q,r:\ x_{6q+r}=x_r

逐步反向審查

• 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、反控制與修訂記錄）