Start with a four-state factor

Consider the clockwise cycle

\[ \text{north}\mapsto\text{east}\mapsto\text{south} \mapsto\text{west}\mapsto\text{north}. \]

Now keep only the axis. North and south become vertical; east and west become horizontal. The target update toggles between these two labels.

source statesource nextprojected statetarget next
northeastverticalhorizontal
eastsouthhorizontalvertical
southwestverticalhorizontal
westnorthhorizontalvertical

Every row says that update-then-project agrees with project-then-update. Because the rows exhaust the source type, they establish the one-step relation for this finite model.

A clockwise four-cycle of north, east, south, and west projects onto a two-cycle of vertical and horizontal axes; opposite directions share each target image.
FigureA many-to-one factor: the target retains alternation between axes. It cannot recover orientation because north and south both map to vertical, while east and west both map to horizontal. Surjectivity does not imply injectivity.

This is a semiconjugacy. It is also a factor in the finite discrete topology because the projection is continuous and onto. It is not a conjugacy: there is no inverse that reconstructs which opposite direction was present.

Read the commuting equation

Let \(f : X \to X\) and \(g : Y \to Y\) be update rules. A map \(\varphi : X \to Y\) semiconjugates \(f\) to \(g\) when

\[ \varphi\circ f=g\circ\varphi. \]

Evaluated at \(x \in X\), this is

\[ \varphi(f(x))=g(\varphi(x)). \]

The equation has a direction. It sends source dynamics through \(\varphi\) to target dynamics. Nothing in it says that \(\varphi\) is continuous, injective, or surjective.

One idea, three languages Read across, then read the syntax map
A human says
Applying the source update and then the coordinate map gives the same target state as applying the coordinate map first and then the target update.
On paper
\(\varphi(f(x))=g(\varphi(x))\) for every \(x\in X\).
In Lean
Function.Semiconj φ f g :=\n  ∀ x, φ (f x) = g (φ x)
Syntax map
Semiconj comes from Mathlib. The first argument is the map between state spaces. The next two arguments are the source and target self-maps. A proof can be applied directly to a state x.

Repeat the square along the orbit

One commuting square gives all natural-number iterates:

\[ \varphi(f^n(x))=g^n(\varphi(x)). \]

At time zero, both sides reduce to \(\varphi(x)\). For the induction step, apply the one-step equation after the induction hypothesis. Mathlib already packages this induction as Semiconj.iterate_right; the project theorem semiconj_iterate_apply exposes the evaluated identity.

At times zero through four, the source row cycles north, east, south, west, north and the target row toggles vertical, horizontal, vertical, horizontal, vertical; a projection arrow joins each column.
FigureSynchronized time: every column is one instance of the iterate identity. The factor changes the state description, not the natural-number clock. It is not an orbit equivalence with time reparameterization.

The ladder also explains a limitation. The target sequence records only axes. It cannot distinguish the north start from the south start. All-iterate transport does not undo information loss.

Add topology only when limits enter

An orbit approaching a point is a topological statement. Suppose

\[ f^n(x)\longrightarrow p. \]

The algebraic identity identifies the projected sequence, but the conclusion

\[ g^n(\varphi(x))\longrightarrow\varphi(p) \]

also needs \(\varphi\) to be continuous at \(p\). This is the exact split in IsAttractedTo.map_semiconj: one hypothesis supplies the limit, one supplies continuity at the limit point, and one supplies orbit intertwining.

The definition IsTopologicalSemiconjugacy packages global continuity with the algebraic relation. Its method map_isAttractedTo uses continuity at the needed point. It does not add surjectivity.

A topological factor map adds surjectivity. That gate matters for a global claim about every target start. Given \(y \in Y\), surjectivity supplies \(x \in X\) with \(\varphi(x)=y\). If every source orbit approaches a fixed point \(p\), then every target orbit approaches \(\varphi(p)\). The theorem IsTopologicalFactorMap.map_isGloballyAttractingFixedPoint formalizes this argument.

Conjugacy adds a reversible coordinate change

A homeomorphism \(e : X \simeq_{\mathrm{top}} Y\) is a bijection with a continuous forward map and continuous inverse. The project calls it a topological conjugacy when

\[ e(f(x))=g(e(x)). \]

The inverse satisfies the reverse equation. This is IsTopologicalConjugacy.symm. Specified conjugacies compose through IsTopologicalConjugacy.trans.

In the standalone worksheet, the two axis labels are encoded as Bool: vertical becomes false, horizontal becomes true. A decoding function returns the original axis, and both inverse identities are checked by cases. That finite encoding is invertible and intertwines the two toggles. It models conjugacy without claiming a nontrivial topological theorem.

At the existential level,

def AreTopologicallyConjugate (f : X → X) (g : Y → Y) : Prop :=
  ∃ e : X ≃ₜ Y, IsTopologicalConjugacy e f g

the source proves reflexivity, symmetry, and transitivity. Those relations compare systems across possibly different state types.

What the inverse lets us transport

The source proves the following equivalences for corresponding points:

  • fixedness via IsTopologicalConjugacy.isFixedPt_iff;
  • having a specified natural-number period via IsTopologicalConjugacy.isPeriodicPt_iff;
  • point attraction via IsTopologicalConjugacy.isAttractedTo_iff;
  • local attraction via IsTopologicalConjugacy.isLocallyAttractingFixedPoint_iff; and
  • global attraction via IsTopologicalConjugacy.isGloballyAttractingFixedPoint_iff.

The basin identities retain set-level information:

\[ e^{-1}(B_g(e(p)))=B_f(p), \qquad e(B_f(p))=B_g(e(p)). \]

They appear as IsTopologicalConjugacy.basin_preimage and IsTopologicalConjugacy.image_basin. The local-attraction proof uses the fact that a homeomorphism is an open map, so the image of a basin neighborhood is a neighborhood of the image point.

The specified-period theorem is deliberately narrow. IsPeriodicPt f n p means that \(n\) is a period. It does not say that \(n\) is the least positive period. Under a noninjective semiconjugacy, a least period may collapse; the two-way conjugacy theorem only states the exact predicate present in the source.

Standalone Lean tutorial

The bundled quarter-turn-factor.lean is a standalone tutorial importing only Std. It proves the commuting square by cases, proves all-iterate transport by induction, exhibits noninjectivity, and checks the inverse axis encoding.

theorem axisOf_directionOrbit (d : Direction) :
    ∀ n, axisOf (directionOrbit d n) = axisOrbit (axisOf d) n := by
  intro n
  induction n with
  | zero => rfl
  | succ n ih =>
      simp only [directionOrbit, axisOrbit, axisOf_quarterTurn, ih]

theorem axisOf_not_injective : ¬Function.Injective axisOf := by
  intro h
  exact north_ne_south (h rfl)

Run it on macOS or Linux with the pinned compiler:

elan run leanprover/lean4:v4.32.0 lean \
  site/content/knowledge-base/deep-dives/conjugacy-semiconjugacy-and-orbit-transport-in-discrete-time/quarter-turn-factor.lean

The worksheet has finite types and recursive natural-number orbits. It does not define TopologicalSpace, continuity, filters, or homeomorphisms.

Try the full project interface

The following is a full project check using pinned Lean and Mathlib dependencies. Initial setup may require substantial disk space and build time.

import NonlinearDynamics.Deterministic.Discrete.Conjugacy

#check IsTopologicalSemiconjugacy
#check IsTopologicalFactorMap
#check IsTopologicalConjugacy
#check semiconj_iterate_apply
#check IsTopologicalConjugacy.isAttractedTo_iff
#check IsTopologicalConjugacy.image_basin
Try it in the repository NonlinearDynamics/Deterministic/Discrete/Conjugacy.lean
The copied checks form a reader worksheet. The authoritative source is NonlinearDynamics/Deterministic/Discrete/Conjugacy.lean; the command below checks the complete module in the repository’s pinned environment.
Full project check, from the repository root
cd formalization
lake env lean -DwarningAsError=true NonlinearDynamics/Deterministic/Discrete/Conjugacy.lean

Resource note: this exact file uses the repository's pinned Lean and Mathlib dependencies. Initial project setup can require substantial disk space and build time. For a lightweight first step on macOS or Linux, use the page's standalone Lean-core or Std tutorial.

Boundaries

This interface supplies no preservation theorem for forward stability , distances, Lipschitz constants, or rates. Topological conjugacy keeps open sets, convergence, and neighborhood structure; it need not keep a chosen metric. The source also proves no entropy, mixing, transitivity, chaos, symbolic coding, structural stability, parameter robustness, measurable conjugacy, stochastic statement, ODE result, or algorithm for constructing a conjugacy.

Semiconjugacy is directional. A target conclusion does not lift without inverse data. A factor map is onto but may remain many-to-one. Dynamical conjugacy is also distinct from matrix similarity, complex conjugation, and the unitary-conjugacy orbits used in random-matrix theory.

Continue with the shorter Semiconjugacy and conjugacy glossary chapter or inspect the declaration-complete Research Note. The next Deep Dive, Parameter Families, Branches, and Bifurcation in Discrete Time, uses fixed- and specified-period preservation as conjugacy obstructions.

References