# Discrete-time dynamical system: iterating T(x)=(3x+1) mod 7 on seven states [← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-discrete-dynamical-system/) This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented. derivation-mko-discrete-dynamical-system-01 · production-20261019-adopted-96 ## Goal and scope State space X={0,1,2,3,4,5,6}, update map T(x)=(3x+1) mod 7. From x_0=0 compute the orbit given by x_(n+1)=T(x_n), prove x_(n+6)=x_n for every natural number n and use it to find x_2026; enumerate the fixed points completely; decide that A={0,1,2,4,5,6} is forward invariant while B={0,1} is not, and prove that the orbit from 0 never reaches the fixed point. Treats only this one completely specified finite system (MKO assumptions a1 and a2). Every conclusion is an exact statement about these 7 states: periodicity is proved by induction, fixed points and invariant subsets by complete enumeration. Nothing is extrapolated to continuous time, other affine parameters, asymptotic stability or chaos. It does not change the canonical MKO or its English edition. ## Givens and symbols - function_def - division_algorithm - nat_induction - subset_def - image_preimage_def - G1 — X={0,1,2,3,4,5,6}; time is indexed by the natural numbers including 0. - G2 — T:X→X, T(x)=(3x+1) mod 7, where m mod 7 is the remainder r (0≤r<7) of the integer m on division by 7. - G3 — Initial state x_0=0, and x_(n+1)=T(x_n) for every natural number n. - G4 — Subsets to be tested: A={0,1,2,4,5,6} and B={0,1}. - X — the state space {0,1,2,3,4,5,6} - T — the update map T(x)=(3x+1) mod 7 - x_n — the state at time n - m\bmod 7 — the remainder of the integer m on division by 7 - T(A) — the image of A under T - A,\ B — the two subsets to be tested ## Rules and sources - function_def · prerequisite — Function: f:A→B assigns to each a∈A exactly one f(a)∈B. Two functions are equal ⇔ they have the same domain and codomain and agree at every a. - division_algorithm · prerequisite — Division algorithm: for an integer a and a positive integer b there are unique integers q, r with a=bq+r and 0≤r0 Rule: division_algorithm · Uses: G1, G2 Leaf basis: division_algorithm + function_def For each x∈X, 3x+1 is an integer; the division algorithm gives unique integers q, r with 3x+1=7q+r and 0≤r<7, so T(x)=r is exactly one element of X. Existence says T has a value at every state (total), uniqueness says that value is determined (a function), and 0≤r<7 says it lies in X (a self-map). This is what MKO assumption a1 requires. S03 · equivalentBefore T(0),T(1),T(2),T(3),T(4),T(5),T(6) After 1,\ 4,\ 0,\ 3,\ 6,\ 2,\ 5 Conditions: none Rule: numeric_evaluation · Uses: S02 Leaf basis: numeric_evaluation + division_algorithm List the complete value table of T, computed in S03.1 and S03.2. Since X has only 7 states, this table is all the data of T, and every later enumeration rests on it. S04 · impliesBefore x_0=0 After x_1=1,\ x_2=4,\ x_3=6,\ x_4=5,\ x_5=2,\ x_6=0 Conditions: none Rule: eq_replace · Uses: G3, S03 Leaf basis: eq_replace + numeric_evaluation Apply the recurrence using the table: 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. Each step uses only the previous state; this is the iteration algorithm. S05 · impliesBefore x_6=0,\ x_0=0 After x_6=x_0 Conditions: none Rule: eq_refl_symm_trans · Uses: S04, G3 Leaf basis: eq_refl_symm_trans Both x_6 and x_0 equal 0, so symmetry and transitivity of equality give x_6=x_0: the orbit returns to its start at step 6. S06 · impliesBefore x_6=x_0 After \forall n\in\mathbb{N}:\ x_{n+6}=x_n Conditions: none Rule: L_period · Uses: S05, L_period Leaf basis: nat_induction + eq_congruence By Lemma L_period (proved by induction in S06.1 to S06.3). The key is determinism: the next state depends only on the current state, so once two times share a state they stay in step forever. This is not an extrapolation from six values. S07 · impliesBefore \forall n:\ x_{n+6}=x_n After \forall q,r\in\mathbb{N}:\ x_{6q+r}=x_r Conditions: none Rule: L_reduce · Uses: S06, L_reduce Leaf basis: nat_induction + L_period By Lemma L_reduce (proved by induction on q in S07.1 to S07.3): adding 6 to the time leaves the state unchanged, so any number of 6s can be removed at once. S08 · equivalentBefore 2026 After 2026=6\cdot 337+4,\ 0\le 4<6 Conditions: 6>0 Rule: division_algorithm · Uses: division_algorithm Leaf basis: division_algorithm + numeric_evaluation Divide the time 2026 by the period 6: 6·337=2022 and 2026−2022=4, with remainder 4 satisfying 0≤4<6. S09 · equivalentBefore x_{2026} After x_{2026}=x_{6\cdot 337+4}=x_4=5 Conditions: none Rule: L_reduce · Uses: S07, S08, S04 Leaf basis: L_reduce + eq_replace + eq_refl_symm_trans Rewrite the index by S08, then L_reduce with q=337 and r=4 gives x_2026=x_4, and S04 gives x_4=5. This value is proved, not guessed from the look of the first few terms. S10 · equivalentBefore \{x\in X\mid T(x)=x\} After \{3\} Conditions: none Rule: case_analysis · Uses: S03, G1, mko_dds_props Leaf basis: case_analysis + set_extensionality + set_builder Compare each table entry: 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. The seven cases are all the states of X, so the enumeration is complete and proves that the set of fixed points is exactly {3}. S11 · equivalentBefore 3x+1\equiv x\pmod 7 After x\equiv 3\pmod 7 Conditions: 4\cdot 2\equiv 1\pmod 7 Rule: mod7_arith · Uses: G2, S10 Leaf basis: mod7_arith + eq_congruence An independent algebraic cross-check. For x∈X, x is its own remainder, so T(x)=x is equivalent to 3x+1≡x (mod 7). Subtracting x+1 from both sides gives 2x≡−1≡6; multiplying both sides by 4 (since 4·2≡1) gives x≡24≡3. The unique representative of this class in X is 3, agreeing with the enumeration of S10. S12 · impliesBefore y_0=3,\ y_{n+1}=T(y_n) After \forall n:\ y_n=3 Conditions: none Rule: nat_induction · Uses: S10, G2 Leaf basis: nat_induction + eq_replace The orbit starting at the fixed point (written y_n) is constant: base y_0=3; if y_n=3 then y_(n+1)=T(3)=3. By induction this holds for all n. S13 · impliesBefore T(A),\ A=\{0,1,2,4,5,6\} After T(A)=\{1,4,0,6,2,5\}=A\subseteq A Conditions: none Rule: mko_dds_props · Uses: S03, G4, mko_dds_props Leaf basis: image_preimage_def + subset_def + set_extensionality Take images element by element: T(0)=1, T(1)=4, T(2)=0, T(4)=6, T(5)=2, T(6)=5, so T(A)={1,4,0,6,2,5}, which has the same elements as A. Every image is in A, so T(A)⊆A and A is forward invariant. S14 · impliesBefore T(1)=4,\ B=\{0,1\} After 4\notin B\ \Rightarrow\ T(B)\not\subseteq B Conditions: none Rule: quantifier_negation · Uses: S03, G4, mko_dds_props Leaf basis: quantifier_negation + subset_def Forward invariance requires the image of every element of B to lie in B. 1∈B but T(1)=4∉B; one counterexample negates the 'for every element', so B is not forward invariant, and T(0)=1∈B does not rescue it. S15 · impliesBefore x_0=0\in A,\ T(A)\subseteq A After \forall n:\ x_n\in A,\ \text{hence }x_n\neq 3 Conditions: none Rule: nat_induction · Uses: S13, G3, G4 Leaf basis: nat_induction + image_preimage_def + subset_def Base: x_0=0∈A. Step: if x_n∈A then x_(n+1)=T(x_n)∈T(A)⊆A. So every x_n lies in A, and since 3∉A, x_n≠3 for every n: the orbit from 0 never reaches the fixed point 3. This is a proof for all n, not an observation of a finite prefix. S16 · impliesBefore \text{proved facts about }(X,T) After x_{n+6}=x_n,\ x_{2026}=5,\ \mathrm{Fix}(T)=\{3\},\ T(A)\subseteq A,\ T(B)\not\subseteq B Conditions: none Rule: and_intro_elim · Uses: S06, S09, S10, S13, S14, S15 Leaf basis: and_intro_elim Combine the conclusions: the orbit from 0 repeats with period 6 and x_2026=5; the only fixed point is 3; A is forward invariant and B is not; the orbit never reaches 3. All are exact statements about this finite system. ## Substeps and lemmas S03.1 · equivalentBefore 3x+1\ \text{for }x=0,1,2,3,4,5,6 After 1,\ 4,\ 7,\ 10,\ 13,\ 16,\ 19 Conditions: none Rule: numeric_evaluation · Uses: G2 Leaf basis: numeric_evaluation Compute 3x+1 one by one: 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 · equivalentBefore 1,4,7,10,13,16,19\ \bmod 7 After 1,\ 4,\ 0,\ 3,\ 6,\ 2,\ 5 Conditions: 0\le r<7 Rule: division_algorithm · Uses: S03.1, division_algorithm Leaf basis: division_algorithm + numeric_evaluation Write out the division algorithm: 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. Each remainder lies between 0 and 6, so by uniqueness it is the value mod 7. S06.1 · induction_baseBefore n=0 After x_{0+6}=x_0 Conditions: none Rule: nat_induction · Uses: S05 Leaf basis: nat_induction Base: let P(n) be x_(n+6)=x_n. P(0) is x_6=x_0, given by S05. S06.2 · induction_stepBefore x_{n+6}=x_n After x_{(n+1)+6}=x_{n+1} Conditions: none Rule: eq_congruence · Uses: G3, G2 Leaf basis: eq_congruence + function_def Inductive step: assume x_(n+6)=x_n. Apply the function T to both sides: T(x_(n+6))=T(x_n). By the recurrence the left side is x_(n+7) and the right side is x_(n+1), so x_((n+1)+6)=x_(n+1). S06.3 · impliesBefore P(0),\ \forall n\,(P(n)\Rightarrow P(n+1)) After \forall n\in\mathbb{N}:\ x_{n+6}=x_n Conditions: none Rule: nat_induction · Uses: S06.1, S06.2 Leaf basis: nat_induction By the principle of induction, P(n) holds for every natural number n. S06.1 to S06.3 together prove Lemma L_period. S07.1 · induction_baseBefore q=0 After x_{6\cdot 0+r}=x_r Conditions: none Rule: nat_induction · Uses: G3 Leaf basis: nat_induction + mul_zero + add_zero Fix an arbitrary natural number r and let R(q) be x_(6q+r)=x_r. R(0) holds since 6·0+r=r. S07.2 · induction_stepBefore x_{6q+r}=x_r After x_{6(q+1)+r}=x_r Conditions: none Rule: L_period · Uses: S06 Leaf basis: L_period + distributive + add_assoc + add_comm + eq_refl_symm_trans Assume R(q). Since 6(q+1)+r=(6q+r)+6, L_period with n=6q+r gives x_(6(q+1)+r)=x_(6q+r), which equals x_r by the inductive hypothesis. S07.3 · impliesBefore R(0),\ \forall q\,(R(q)\Rightarrow R(q+1)) After \forall q,r:\ x_{6q+r}=x_r Conditions: none Rule: nat_induction · Uses: S07.1, S07.2 Leaf basis: nat_induction + forall_intro By induction R(q) holds for every q; r was arbitrary, so by generalization it holds for every r too. S07.1 to S07.3 together prove Lemma L_reduce. ## Reverse audits - S16 · sufficient_goal_reduction · S06, S09, S10, S13, S14, S15, and_intro_elim — Goal G: the determinations listed in the goal. Sufficient condition H: S06, S09, S10, S13, S14 and S15, each already proved (H⇒G by conjunction introduction). H is derived forwards from the givens; G is never used as a premise. - S15 · premise_audit · S13, nat_induction, image_preimage_def — It needs the initial state in A and the forward invariance of A; without either, the conclusion fails. - S14 · premise_audit · S03, quantifier_negation, subset_def — Negating a universal statement needs one counterexample, x=1; it is not claimed that every element of B leaves B. - S13 · premise_audit · S03, image_preimage_def, subset_def, mko_dds_props — It needs all six elements of A to be checked, and all are listed here. Checking only some elements would not give the inclusion. - S12 · premise_audit · S10, nat_induction, eq_replace — It needs only T(3)=3. It does not mean that other orbits approach 3 (see S15). - S11 · inverse_equivalence · mod7_arith, eq_congruence — Multiplying by 4 and by 2 undo each other modulo 7 (8≡1), and subtracting and adding x+1 undo each other, so each move holds both ways. - S10 · inverse_equivalence · case_analysis, set_extensionality, S03 — Both inclusions of the set equality: 3 is in the set (T(3)=3), and every element of the set is 3 (the other six fail). Completeness comes from X having exactly these seven states. - S09 · inverse_equivalence · L_reduce, S08, S04, eq_refl_symm_trans — This is a chain of equalities, each with a reason (equal indices, the lemma, a computation); equality is symmetric, so the step holds both ways. - S08 · inverse_equivalence · division_algorithm, numeric_evaluation — 6·337+4 evaluates back to 2026; the division algorithm makes the quotient and remainder unique. - S07.3 · premise_audit · S07.1, S07.2, nat_induction, forall_intro — Generalization is allowed because no extra condition was placed on r in the proof. - S07.2 · premise_audit · S06, distributive, add_assoc, add_comm, eq_refl_symm_trans — It needs the index rewrite 6(q+1)+r=(6q+r)+6 (distributivity, associativity and commutativity of addition) and L_period; that is a different, already proved lemma, not L_reduce itself. - S07.1 · premise_audit · nat_induction, mul_zero, add_zero — It uses only 6·0=0 and 0+r=r. - S07 · premise_audit · L_reduce — It depends on the lemma, which uses only L_period. - S06.3 · premise_audit · S06.1, S06.2, nat_induction — The two premises of induction are S06.1 and S06.2, with n arbitrary in the inductive step. - S06.2 · premise_audit · G3, eq_congruence, function_def — It needs T to be a function (equal inputs give equal outputs) and the recurrence for every n. No converse is claimed: going back from x_(n+7)=x_(n+1) to x_(n+6)=x_n would need T to be injective, which is not used. - S06.1 · premise_audit · S05, nat_induction — The base needs only the computation of S05. - S06 · premise_audit · L_period — It depends on the lemma, which uses only S05 and that T is a function. - S05 · premise_audit · S04, eq_refl_symm_trans — This is one computed equality; by itself it says nothing about later states, which needs the induction of S06. - S04 · premise_audit · G3, S03, eq_replace — It needs x_0 and the complete table; each value is determined by the previous one. Whether x_5 could be recovered uniquely from x_6 is not claimed. - S03.2 · inverse_equivalence · division_algorithm, numeric_evaluation — Each equation 7q+r expands back to the original number; the condition 0≤r<7 makes this the unique decomposition. - S03.1 · inverse_equivalence · numeric_evaluation — Exact evaluation of integer expressions; both sides are the same number. - S03 · inverse_equivalence · numeric_evaluation, division_algorithm — Each entry names one number in two ways and can be recomputed independently; backwards, write r back into 3x+1=7q+r. - S02 · premise_audit · division_algorithm, function_def — It needs the divisor 7>0. The step does not claim that T is a bijection; that can be read off the table in S03 but is not used later. - S01 · premise_audit · G1, G2, G3, mko_dds — This step only states the system and the orbit and derives no new fact; that T really is a total self-map of X is checked in S02. ## Error controls and negative controls A few iterates do not prove long-run behaviourThe MKO names the misconception of taking a few iterates as proof of long-run behaviour. x_0 to x_5 are pairwise distinct, which looks as if the orbit never repeats, but x_6 returns to 0. Even after seeing the return, 'x_(n+6)=x_n for all n' still needs an argument: here it is the induction of S06, which rests on T being a function (determinism), not on computing more terms. Whether the state space is finite or infinite, finite observations without the update rule do not automatically prove long-run behaviour. Under a known deterministic rule, however, a return propagates by the same induction and establishes periodicity without assuming a finite state space. A discrete update is not a differential equationHere x_(n+1)=T(x_n) specifies states only at integer times; it specifies no state between n and n+1, and x_(n+1)−x_n is not a derivative. The states are remainders modulo 7, with no continuous-time parameter, required topology or interpolation rule supplied. An external embedding and interpolation may be added, but that is an additional model, not states or dynamics already defined by this recurrence. This guide makes no continuous-time, flow or stability claim. X alone is not enough; T is neededThe same X with T′(x)=(x+1) mod 7 gives x_n=n mod 7 from 0, so x_2026=3 instead of 5, and there is no fixed point at all. The MKO says the initial state and the update map together determine the orbit; the state set and initial value alone answer none of the questions here. - x_0 to x_5 are pairwise distinct, so this orbit never repeats → reject — x_6=T(2)=0=x_0 (S05), and from then on it repeats every 6 steps (S06). - The fixed point 3 attracts the other states, so the orbit from 0 eventually stays at 3 → reject — S15 proves x_n∈A for all n, and 3∉A, so the orbit never reaches 3. - B={0,1} is forward invariant because T(0)=1∈B → reject — Forward invariance concerns every element; T(1)=4∉B (S14). - Knowing X={0,1,2,3,4,5,6} and x_0=0 is enough to determine x_2026 → reject — With T′(x)=(x+1) mod 7 one gets x_2026=2026 mod 7=3 (N11), unlike 5 for this system. ## Result and limitations For X={0,1,2,3,4,5,6} and T(x)=(3x+1) mod 7: the orbit from 0 is 0,1,4,6,5,2,0, and induction proves x_(n+6)=x_n for all n, so x_2026=x_4=5; complete enumeration shows that the only fixed point is 3; A={0,1,2,4,5,6} is forward invariant, while B={0,1} is not because T(1)=4; the orbit from 0 stays in A forever and never reaches 3. - N5 and N8 are finite checks over all 7 states of X; since X has exactly these 7 states they cover the whole state space of this system, but they say nothing about other moduli or other maps. - Attraction, stability and the classification of the family T(x)=(ax+b) mod m are outside this guide; they belong to the MKO's formal next step. ## Verification and source binding 11 declared checks for this guide; only the listed expressions are covered. - source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f - adopted source SHA-256: f4f2e74cd790417e54c77f714258d8957de8bb95a06fb7dd5979e531097dd264 - original source SHA-256: 13f802958297845385be7005be78cf9e3990a132a4a30724815269c12dedd6a6 - Lean: NOT_RUN · independent AI: NOT_MEASURED [Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-discrete-dynamical-system-01.json)