Discrete-time dynamical system: iterating T(x)=(3x+1) mod 7 on seven states

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≤r<b.
• nat_induction · prerequisite — Principle of induction: for a family P(n) starting at n₀, if P(n₀) holds and P(n)⇒P(n+1) for every n≥n₀, then P(n) holds for every n≥n₀.
• subset_def · prerequisite — Subset: A⊆B means every element of A is an element of B, i.e. ∀x (x∈A⇒x∈B).
• image_preimage_def · prerequisite — Image and preimage: f(S)={f(a) ∣ a∈S}; f⁻¹(T)={a∈A ∣ f(a)∈T}. The preimage notation does not presuppose that f has an inverse.
• def_intro · prerequisite — Introducing a definition: a statement, expression or object may be given a name, after which the name and what it stands for are interchangeable.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• eq_replace · prerequisite — Replacement of equals: an expression inside a statement may be replaced by an equal expression without changing whether the statement is true.
• eq_refl_symm_trans · prerequisite — Properties of equality: u=u; if u=v then v=u; if u=v and v=w then u=w.
• eq_congruence · prerequisite — Congruence of equality: if u=v, applying the same defined operation f to both sides gives f(u)=f(v). Operating on one side only is not an instance of this rule.
• mul_zero · prerequisite — Multiplying by zero: u·0=0. Reason: u·0=u·(0+0)=u·0+u·0; subtracting u·0 from both sides gives 0=u·0.
• add_zero · prerequisite — Additive identity: u+0=u.
• distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
• add_assoc · prerequisite — Associativity of addition: (u+v)+w=u+(v+w).
• add_comm · prerequisite — Commutativity of addition: u+v=v+u.
• forall_intro · prerequisite — ∀-introduction (generalization): if a statement is proved for an arbitrary element x, with no extra assumption on x, it holds for every x in the domain.
• case_analysis · prerequisite — Proof by cases: if P∨Q holds and both P⇒R and Q⇒R are proved, then R holds. The cases must cover every possibility.
• set_extensionality · prerequisite — Set equality: A=B if and only if A⊆B and B⊆A, i.e. they have the same elements.
• set_builder · prerequisite — Set-builder notation: x∈{y∈A ∣ P(y)} if and only if x∈A and P(x).
• quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• mko_dds · cited — A discrete-time dynamical system consists of a state space X and a self-map T:X→X. From x_0∈X, the recurrence x_(n+1)=T(x_n) defines a forward orbit. · mko-discrete-dynamical-system
• mko_dds_props · cited — A fixed point satisfies T(x)=x; a forward-invariant subset A satisfies T(A)⊆A. With finitely many states these local properties can be enumerated completely. · mko-discrete-dynamical-system
• mod7_arith · prerequisite — Congruence modulo 7: u≡v (mod 7) means 7∣(u−v); congruence is compatible with addition and multiplication; since 4·2=8≡1 (mod 7), 2 has the inverse 4 modulo 7; each congruence class has exactly one representative in X.
• L_period · lemma — For every natural number n, x_(n+6)=x_n.
• L_reduce · lemma — For all natural numbers q and r, x_(6q+r)=x_r.

Main derivation

\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

Substeps and lemmas

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

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 behaviour

The 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 equation

Here 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 needed

The 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)