Bifurcation Interfaces for Discrete Systems in Lean

Begin with an equation that can be solved completely

For a real parameter \(\mu\), define

A fixed point satisfies \(F_\mu(x)=x\). Cancelling \(x\) gives

This identity determines every real fixed point:

• if \(\mu\lt0\), no real square equals \(\mu\), so there is no fixed point;
• if \(\mu=0\), the only fixed point is \(x=0\); and
• if \(\mu\gt0\), the two fixed points are \(x=\sqrt\mu\) and \(x=-\sqrt\mu\).

The algebra establishes the three cases. The diagram explains their relationship but supplies no additional proof.

Kuznetsov analyzes \(x\mapsto\alpha+x+x^2\) and immediately notes the variant \(x\mapsto\alpha+x-x^2\). The project family is exactly the latter after renaming \(\alpha\) to \(\mu\) in the scalar map fold discussion. The present module checks this family directly. It does not formalize the generic scalar fold theorem, which assumes a smooth \(f(x,\alpha)\) with \(f(0,0)=0\), \(f_x(0,0)=1\), \(f_{xx}(0,0)\ne0\), and \(f_\alpha(0,0)\ne0\).

Why literal fixed-point sets are the wrong primary test

Suppose a family has one fixed point that moves continuously with the parameter. The literal subsets of the chosen coordinate space are different at nearby parameters, but the maps may still be topologically conjugate. A definition based on equality of those subsets would report coordinate motion as a qualitative change.

The module therefore follows the standard idea of detecting topological inequivalence at arbitrarily close parameters, as summarized by Guckenheimer. Its first formal predicate is a whole-state-space conjugacy bifurcation: maps not topologically conjugate to \(F_\mu\) by a homeomorphism of the entire state space occur arbitrarily near \(\mu\):

def IsGlobalTopologicalBifurcationAt
    (family : ParameterizedFamily P X) (μ : P) : Prop :=
  ¬∀ᶠ ν in 𝓝 μ, AreTopologicallyConjugate (family ν) (family μ)

𝓝 μ is the neighborhood filter. ∀ᶠ ν in 𝓝 μ, ... means that the statement holds throughout some neighborhood of \(\mu\). Negating it means that every neighborhood contains parameters where the statement fails. The equivalent theorem isGlobalTopologicalBifurcationAt_iff_frequently_not_conjugate exposes that frequent form.

In the Lean declaration name, Global modifies the domain of the conjugating homeomorphism. It does not classify the quadratic event as a global bifurcation in the literature’s local/global sense: the fold-type fixed-point event is local in that taxonomy. The definition does not yet cover local conjugacy near one invariant set. It also requires no continuous choice of conjugating homeomorphisms as the parameter varies. Those are separate, stronger interfaces.

Classifiers are witnesses, not replacements for equivalence

Some topological inequivalences are easier to establish through a selected classifier. The project defines

def IsClassificationChangeAt (classify : P → C) (μ : P) : Prop :=
  ¬∀ᶠ ν in 𝓝 μ, classify ν = classify μ

An arbitrary classifier does not automatically describe qualitative dynamics. The bridge theorem asks for the missing fact explicitly: whenever the nearby map is conjugate to the reference map, its classifier value must equal the reference value. Under that hypothesis, a classifier change implies the whole-state-space conjugacy bifurcation predicate.

Two safe classifiers are included:

• HasFixedPoint f says that some state satisfies IsFixedPt f x;
• HasSpecifiedPeriodPoint f n says that some state satisfies IsPeriodicPt f n x.

The previous Conjugacy milestone identifies corresponding fixed and specified-period points. This module lifts those pointwise theorems to existence equivalences, then uses propext to turn equivalence of propositions into the equality expected by the generic classifier interface.

The implications are one-way. A fixed-point-existence change establishes a bifurcation under this whole-state-space equivalence. Constancy of fixed-point existence does not establish conjugacy and does not rule out a bifurcation involving stability, a periodic orbit, an invariant curve, or another feature.

Branches are selections satisfying equations

For a parameter set \(S\), a fixed-point branch is represented by a function \(b : P\to X\) satisfying

The Lean predicate is deliberately pointwise:

def IsFixedPointBranchOn (family : ParameterizedFamily P X)
    (branch : P → X) (s : Set P) : Prop :=
  ∀ μ ∈ s, IsFixedPt (family μ) (branch μ)

IsSpecifiedPeriodBranchOn family n branch s replaces IsFixedPt with IsPeriodicPt ... n. No continuity, differentiability, uniqueness, or maximality is hidden in either definition.

Every fixed point returns after every natural number of updates. Consequently, every fixed-point branch is also a specified-period branch for every n, including zero. This theorem does not turn it into a branch of least period n. Exact least period needs additional exclusions.

For the quadratic family, Real.sqrt and fun μ ↦ -√μ are fixed-point branches on Set.Ici 0. The source proves that they give all fixed points there and that they are distinct for a positive parameter. At zero the two branch expressions coincide.

The checked witness at zero

quadraticFixedPointFamily_hasFixedPoint_iff proves

Mathlib’s frequently_lt_nhds supplies negative real parameters arbitrarily near zero. At those parameters the classifier is false, while at zero it is true. The theorem quadraticFixedPointFamily_isFixedPointExistenceChangeAt_zero packages this filter argument.

Finally, quadraticFixedPointFamily_isGlobalTopologicalBifurcationAt_zero applies the generic invariant-classifier theorem. The logical path is complete:

1. the fixed-point equation gives existence exactly for nonnegative parameters;
2. negative parameters occur arbitrarily near zero;
3. fixed-point existence therefore changes at zero;
4. global topological conjugacy preserves fixed-point existence; and
5. nearby negative maps cannot all be globally conjugate to the map at zero.

This is a theorem about the selected whole-state-space predicate and this exact family. It is not a sampled numerical diagnosis.

Isolated parameters form a boundary case

If the singleton \(\{\mu\}\) is open, then some neighborhood contains only \(\mu\). Every classifier is constant on that neighborhood. The theorem not_isClassificationChangeAt_of_isOpen_singleton records this boundary.

That fact matters for finite teaching models. A finite type with its usual discrete topology can illustrate different regimes, fixed-point counts, and specified periods. Its adjacent entries do not by themselves form a topological parameter continuum, so the table alone does not establish this module’s real-parameter bifurcation predicate.

Declaration-complete source map

Six #print axioms commands audit the generic filter equivalence, the classifier bridge, fixed-point invariance, the fixed-point witness bridge, the complete square-root classification, and the final example theorem. The formal release gate shows only standard propext, Classical.choice, and Quot.sound dependencies as applicable, with no sorryAx.

Reproduce the checks

The finite regime table is a standalone tutorial importing only Std:

elan run leanprover/lean4:v4.32.0 lean \
  site/content/knowledge-base/deep-dives/parameter-families-branches-and-bifurcation-in-discrete-time/finite-branch-table.lean

The project module is a full project check using the repository’s 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/Bifurcation.lean

Lean’s elaborator constructs candidate proof terms and its kernel checks them against the formal statements. That check does not establish that this whole-state-space convention covers every use of “bifurcation” in the literature.

The Deep Dive develops the example and finite worksheet more slowly. The bifurcation point glossary chapter gives a shorter entry point.

Exact nonclaims

The module does not formalize local phase-space equivalence, continuity or differentiability of a family, continuous or smooth branch regularity, derivatives, Jacobians, multipliers, hyperbolicity, genericity, transversality, codimension, center manifolds, fold or flip normal-form classification, Neimark-Sacker bifurcation, stability exchange, least-period branches, continuation, numerical detection, structural stability in a function-space topology, chaos, entropy, mixing, symbolic coding, stochastic systems, or ODE bifurcations.

Different fixed-point existence values obstruct conjugacy. Equal existence values do not establish conjugacy. A branch may persist through a bifurcation, and a bifurcation may concern a classifier not included here.

References

• John Guckenheimer, “Bifurcation,” Scholarpedia 2(6):1517 (2007), DOI 10.4249/scholarpedia.1517. The definition uses arbitrarily close parameters with topologically inequivalent dynamics.
• Yuri A. Kuznetsov, Elements of Applied Bifurcation Theory, 3rd ed., Applied Mathematical Sciences 112, Springer (2004), Chapter 2 on equivalence and bifurcations and Chapter 4 on one-parameter bifurcations of fixed points in discrete time, DOI 10.1007/978-1-4757-3978-7.
• Yuri A. Kuznetsov, “Saddle-node bifurcation for maps,” Scholarpedia 3(4):4399 (2008), DOI 10.4249/scholarpedia.4399.
• Yuri A. Kuznetsov and Hil G. E. Meijer, Numerical Bifurcation Analysis of Maps: From Theory to Software, Cambridge University Press (2019), Chapter 2, DOI 10.1017/9781108585804.
• Mathlib 4.32.0, pinned revision 81a5d257, Dynamics.PeriodicPts.Defs, Topology.Order.LeftRight, and Analysis.Real.Sqrt.