Start with a projection that forgets direction

Let four compass directions update by one clockwise quarter turn:

currentnextaxisnext axis
northeastverticalhorizontal
eastsouthhorizontalvertical
southwestverticalhorizontal
westnorthhorizontalvertical

Project north and south to vertical, and east and west to horizontal. The target system toggles its axis. For every direction \(d\),

\[ \operatorname{axis}(\operatorname{turn}(d)) {} = \operatorname{toggle}(\operatorname{axis}(d)). \]

The four rows exhaust the finite source type, so the calculation establishes this equation for the model. North and south have the same image, however. The projection retains the axis alternation and discards orientation.

North turns to east across the top while vertical toggles to horizontal across the bottom; projecting at either endpoint makes both routes finish at horizontal.
FigureThe one-step square commutes: update then project agrees with project then update. The dashed projection is many-to-one, so this figure explains semiconjugacy rather than conjugacy.

The accompanying Deep Dive packages this model as a standalone tutorial using only Lean and Std. The project module begins with Mathlib’s general Function.Semiconj relation instead of defining a second algebraic predicate.

Four interfaces, not one overloaded word

For maps \(f : X \to X\), \(g : Y \to Y\), and \(\varphi : X \to Y\), the algebraic relation is

\[ \varphi(f(x))=g(\varphi(x))\qquad(x\in X). \]

Mathlib names it Function.Semiconj φ f g. The new module then records three topological refinements and one existential relation:

def IsTopologicalSemiconjugacy (φ : X → Y) (f : X → X) (g : Y → Y) : Prop :=
  Continuous φ ∧ Semiconj φ f g

def IsTopologicalFactorMap (φ : X → Y) (f : X → X) (g : Y → Y) : Prop :=
  IsTopologicalSemiconjugacy φ f g ∧ Surjective φ

def IsTopologicalConjugacy (e : X ≃ₜ Y) (f : X → X) (g : Y → Y) : Prop :=
  Semiconj e f g

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

Continuous φ supplies the limit-preservation gate. Surjective φ says that each target state has a source representative. X ≃ₜ Y is a homeomorphism: a bijection whose forward and inverse maps are continuous. The specified predicate keeps the coordinate change visible; the existential relation says only that some such change exists.

An algebraic semiconjugacy branches to a continuous topological semiconjugacy and to a homeomorphic conjugacy; adding surjectivity to the continuous branch gives a factor map.
FigureData gates: continuity, surjectivity, and a continuous inverse play different roles. The interface does not infer distance preservation, a convergence rate, or the project’s uniform-space forward-stability predicate from topology alone.

One step controls every iterate

The theorem semiconj_iterate_apply states

\[ \varphi(f^n(x))=g^n(\varphi(x)) \qquad(n\in\mathbb N). \]

It delegates the induction to Mathlib’s Function.Semiconj.iterate_right. Time zero is included: both iterates are identities. No continuity, injectivity, or surjectivity enters this algebraic proof.

One idea, three languages Read across, then read the syntax map
A human says
Projecting the source state after n updates gives the same target state as projecting first and then applying n target updates.
On paper
\(\varphi(f^n(x))=g^n(\varphi(x))\) for every \(n\in\mathbb N\).
In Lean
theorem semiconj_iterate_apply\n    (h : Semiconj φ f g) (n : ℕ) (x : X) :\n    φ (f^[n] x) = g^[n] (φ x)
Syntax map
f^[n] and g^[n] are function iterates. h.iterate_right n lifts the one-step relation to the two iterate families, and .eq x evaluates the result at the chosen state.

This identity also sends fixed and specified-period points forward. A many-to-one projection may merge distinct periodic points, so forward mapping does not by itself recover the source point or its least period.

Continuity transports attraction forward

Suppose \(f^n(x) \to p\). The iterate identity rewrites the projected sequence as \(g^n(\varphi(x))\). If \(\varphi\) is continuous at \(p\), then

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

IsAttractedTo.map_semiconj records exactly these two hypotheses: ContinuousAt φ p and Semiconj φ f g. The wrapper IsTopologicalSemiconjugacy.map_isAttractedTo projects continuity from the bundled topological semiconjugacy.

Surjectivity enters only when a conclusion quantifies over every target state. IsTopologicalFactorMap.map_isGloballyAttractingFixedPoint starts with a target state \(y\), selects \(x\) with \(\varphi(x)=y\), and transports global attraction from that representative. It also maps the source fixed point to a target fixed point using the semiconjugacy equation.

This direction is one-way. A factor can forget distinctions in the source, so target attraction does not automatically lift through an arbitrary factor.

A homeomorphism supplies the return path

For a specified conjugacy \(e : X \simeq_{\mathrm{top}} Y\), IsTopologicalConjugacy.symm proves that e.symm intertwines \(g\) with \(f\). IsTopologicalConjugacy.trans composes two coordinate changes. At the existential level, areTopologicallyConjugate_refl, AreTopologicallyConjugate.symm, and AreTopologicallyConjugate.trans show that topological conjugacy is reflexive, symmetric, and transitive across possibly different state types.

The inverse equation gives two-way statements:

  • IsTopologicalConjugacy.isFixedPt_iff identifies corresponding fixed points;
  • IsTopologicalConjugacy.isPeriodicPt_iff identifies points having a specified natural-number period;
  • IsTopologicalConjugacy.isAttractedTo_iff identifies attraction of corresponding point orbits;
  • IsTopologicalConjugacy.basin_preimage describes the source basin as an exact preimage;
  • IsTopologicalConjugacy.image_basin describes the target basin as an exact image;
  • IsTopologicalConjugacy.isLocallyAttractingFixedPoint_iff transports the basin-neighborhood condition in both directions; and
  • IsTopologicalConjugacy.isGloballyAttractingFixedPoint_iff transports global attraction in both directions.

The periodic theorem uses IsPeriodicPt f n p, which says that \(n\) is a period. It does not assert that \(n\) is the least positive period. Conjugacy does preserve the displayed specified-period statement exactly.

Declaration-complete source map

The source candidate contains twenty public declarations:

DeclarationRole
IsTopologicalSemiconjugacycontinuity plus algebraic semiconjugacy
IsTopologicalFactorMapcontinuous surjective semiconjugacy
IsTopologicalConjugacyspecified homeomorphism intertwining two maps
AreTopologicallyConjugateexistence of a specified conjugacy
semiconj_iterate_applyall-iterate orbit identity
IsAttractedTo.map_semiconjcontinuity-at-limit attraction transport
IsTopologicalSemiconjugacy.map_isAttractedTobundled forward attraction map
IsTopologicalFactorMap.map_isGloballyAttractingFixedPointglobal attractor descends to a factor
IsTopologicalConjugacy.symminverse homeomorphism conjugates back
IsTopologicalConjugacy.transspecified conjugacies compose
IsTopologicalConjugacy.isFixedPt_iffcorresponding fixed points
IsTopologicalConjugacy.isPeriodicPt_iffcorresponding specified periods
IsTopologicalConjugacy.isAttractedTo_iffcorresponding point attraction
IsTopologicalConjugacy.basin_preimageexact basin preimage
IsTopologicalConjugacy.image_basinexact basin image
IsTopologicalConjugacy.isLocallyAttractingFixedPoint_ifflocal attraction equivalence
IsTopologicalConjugacy.isGloballyAttractingFixedPoint_iffglobal attraction equivalence
areTopologicallyConjugate_reflreflexivity
AreTopologicallyConjugate.symmsymmetry
AreTopologicallyConjugate.transtransitivity

Six #print axioms commands audit the iterate theorem, factor endpoint, specified-period equivalence, attraction equivalence, local-attraction equivalence, and existential transitivity. Warning-fatal project validation must show no sorryAx before the milestone is recorded as green.

Reproduce the checks

The finite quarter-turn model is a standalone tutorial importing only Std:

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 exact module is a full project check using pinned Lean and Mathlib dependencies. Initial setup may require substantial disk space and build time:

git clone https://github.com/tdj28/nonlinear-dynamics-lean.git
cd nonlinear-dynamics-lean/formalization
lake env lean -DwarningAsError=true \
  NonlinearDynamics/Deterministic/Discrete/Conjugacy.lean

lake env lean selects the pinned environment. Lean’s elaborator constructs candidate proof terms and the kernel checks them against the formal statements. That check does not by itself establish that this interface covers every convention called a factor or conjugacy in the literature.

The paired Deep Dive develops the finite model and syntax gradually. The Semiconjugacy and conjugacy glossary chapter gives a shorter first pass. The later Bifurcation Interfaces Research Note uses conjugacy invariance to turn selected fixed- and periodic-point existence changes into sufficient bifurcation witnesses.

Exact nonclaims

The module proves no preservation theorem for forward stability , uniform equicontinuity, distances, Lipschitz constants, or convergence rates. A homeomorphism preserves topology, not a chosen metric. The module also proves no entropy, transitivity, mixing, chaos, symbolic coding, structural stability, parameter robustness, measure conjugacy, stochastic result, time-reparameterized orbit equivalence, ODE result, or algorithm for finding a conjugacy.

A semiconjugacy need not be injective or surjective. A factor map is surjective but may still lose information. A specified-period statement does not identify the least period. Dynamical conjugacy here is not matrix similarity, complex conjugation, or the unitary-conjugacy relation used elsewhere in the random-matrix track.

References