Pipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

✓ 10 results · all verified · 2 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 8 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Local bifurcation normal forms and numerical certificates

1 · Prerequisites

2 · Summary

This page develops the local equilibrium geometry for scalar folds, transcritical points, and symmetry-preserving pitchforks, then proves the simple Hopf branch and its stability from a parameterized center manifold and a fixed multilinear normalization. The interval procedure accepts only proof-carrying enclosures and strict nondegeneracy bounds. Its conclusions are local: an eigenvalue plot or a finite continuation trace does not establish global dynamics or branch completeness.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (gpt-6-luna)Open item page →

Hopf spectral and multilinear normal-form data

Definition

Let $f (x, λ)$ be a real $C^{3}$ vector field on an open subset of $R^{d} \times R$ , and suppose $f (0, 0) = 0$ . Put $A = D_{x} f (0, 0)$ . Assume $A$ has a simple pair of eigenvalues $i ω$ and $- i ω$ , where $ω > 0$ , and no other eigenvalue on the imaginary axis. Let $A_{C}$ be the complexification of $A$ . Choose $q, p \in C^{d}$ with

$A q = i ω q, A^{*} p = - i ω p, q^{*} q = 1, p^{*} q = 1.$

Here $u^{*} v = {\overset{ˉ}{u}}^{T} v$ is the standard Hermitian product. To obtain both normalizations, start with nonzero compatible eigenvectors $q_{0}, p_{0}$ and put $q = q_{0} / \sqrt{q_{0}^{*} q_{0}}$ . Simplicity gives $a : = p_{0}^{*} q \neq 0$ by For a simple eigenvalue, left and right eigenvectors pair nontrivially and may be normalized by $y^{*} x = 1$ . Set $p = p_{0} / \overline{a}$ ; then $q^{*} q = 1$ and $p^{*} q = a / a = 1$ , while both eigenvector equations are preserved. Write $B = D_{x}^{2} f (0, 0)$ and $C = D_{x}^{3} f (0, 0)$ for the symmetric real multilinear derivatives, extended complex multilinearly. Since zero and $2 i ω$ are not eigenvalues of $A$ , define

$G_{21} : = p^{*} ⁣ (C (q, q, \overset{ˉ}{q}) - 2 B ⁣ (q, A^{- 1} B (q, \overset{ˉ}{q})) + B ⁣ (\overset{ˉ}{q}, (2 i ω I - A)^{- 1} B (q, q)))$

and define the first Lyapunov coefficient in this normalization by

$ℓ_{1} : = \frac{Re G_{21}}{2 ω} .$

If $q$ is rescaled to $c q$ and the unit-norm condition is dropped while $p^{*} q = 1$ is preserved, then $ℓ_{1}$ rescales by $∣ c ∣^{2}$ ; under the declared condition $q^{*} q = 1$ , the remaining phase freedom leaves $ℓ_{1}$ unchanged. Its sign is the local cubic radial sign. The definition alone is not a bifurcation theorem.

For an equilibrium at arbitrary $(x_{*}, λ_{0})$ , apply this definition to the translated field $\hat{f} (y, μ) = f (x_{*} + y, λ_{0} + μ)$ at $(y, μ) = (0, 0)$ . Thus $A = D_{x} f (x_{*}, λ_{0})$ , $B = D_{x}^{2} f (x_{*}, λ_{0})$ and $C = D_{x}^{3} f (x_{*}, λ_{0})$ , and $p, q, ω$ refer to that same $A$ . Translation preserves these spatial derivatives and their Euclidean normalization. If the equilibrium is continued as $ξ (λ)$ , the further state change $y = x - ξ (λ)$ at each fixed parameter gives $\dot{y} = f (y + ξ (λ), λ)$ ; because $\dot{λ} = 0$ , no extra time-derivative term appears. Spatial jets at the critical parameter are still the same $A, B, C$ .

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (gpt-6-luna)Open item page →

Weighted trajectory space for a local center-manifold construction

Definition

Let $E$ be a finite-dimensional real normed space and let $η > 0$ . Define

$C_{η} (E) : = {u \in C (R, E) : ∥ u ∥_{η} : = \sup_{t \in R} e^{- η ∣ t ∣} ∥ u (t) ∥ < \infty} .$

The norm is $∥ u ∥_{η}$ . It permits at most the fixed exponential growth rate $η$ in either time direction. It does not say that a trajectory is bounded.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passOpen item page →

Characteristic roots preserve separated cluster counts under matrix perturbation

Statement

Let $A_{n}, A \in C^{d \times d}$ with $A_{n} \to A$ entrywise. Let $U_{1}, \dots, U_{s}$ be pairwise disjoint open disks whose boundaries contain no eigenvalue of $A$ and which together contain every eigenvalue of $A$ . Then, for all sufficiently large $n$ , each $U_{j}$ contains exactly the same number of eigenvalues of $A_{n}$ , counted with algebraic multiplicity, as of $A$ .

Facts & Assumptions

Given: Matrices $A_{n}, A$ , the open disks $U_{j}$ , and the hypotheses in the Statement.

[F1]

For $A \in M_{n} (F)$ , the characteristic polynomial is $χ_{A} (x) = \det (x I_{n} - A)$ when $n \geq 1$ , with $χ_{A} (x) = 1$ for the unique $0 \times 0$ matrix: $χ_{A} (z) = \det (z I - A)$ is monic of degree $d$ for $d \geq 1$ ; its coefficients are polynomial expressions in the entries of $A$ , and $χ_{A} = 1$ when $d = 0$ .

[F2]

A complex polynomial of degree $n$ has exactly $n$ roots counted with multiplicity: a degree- $d$ complex polynomial with $d \geq 1$ factors into exactly $d$ linear roots counted with multiplicity, and the multiset is unique.

[F3]

Bolzano-Weierstrass: every bounded real sequence has a convergent subsequence: every bounded real sequence has a convergent subsequence.

Proof

Given: $A_{n}, A, U_{1}, \dots, U_{s}$ as in the Statement.

1.1F1givenalgebra

If $d = 0$ , every characteristic polynomial is $1$ by [F1], so every disk contains zero roots and the conclusion is immediate. For the remainder assume $d \geq 1$ . The coefficients of $χ_{A_{n}}$ converge to those of $χ_{A}$ because determinants are finite sums of products of matrix entries. They are therefore uniformly bounded. For a monic polynomial $z^{d} + \sum_{k < d} a_{k} z^{k}$ , every root satisfies $∣ z ∣ \leq 1 + \max_{k < d} ∣ a_{k} ∣$ : outside that disk, $\sum_{k < d} ∣ a_{k} ∣ ∣ z ∣^{k} < ∣ z ∣^{d}$ by the finite geometric-sum bound, so the polynomial cannot vanish. Hence all roots of all sufficiently large $χ_{A_{n}}$ lie in one fixed bounded disk.

2.1F2F3step 1.1construct

For each $n$ , list the $d$ roots of $χ_{A_{n}}$ with multiplicity in the canonical lexicographic order by real part and then imaginary part; [F2] supplies the finite multiset, and this ordering requires no choice. The resulting sequence of root lists is bounded in $R^{2 d}$ . Applying [F3] successively to its $2 d$ real coordinates gives a subsequence on which every root in the list converges.

3.1F1F2step 1.1step 2.1algebra

Along that subsequence, the factorization $χ_{A_{n}} (z) = \prod_{k = 1}^{d} (z - λ_{n, k})$ converges coefficientwise to $\prod_{k = 1}^{d} (z - λ_{k})$ . By step 1.1 the same coefficient limit is $χ_{A}$ , so uniqueness in [F2] shows that the limiting list is exactly the root multiset of $χ_{A}$ , including multiplicities.

4.1step 2.1step 3.1givencontradiction∎

If the asserted disk counts failed for infinitely many $n$ , restrict to those indices and repeat step 2.1. Since no root of $χ_{A}$ lies on any disk boundary, each convergent root sequence from step 3.1 is eventually in the same disk as its limit, or outside all the disks if its limit is outside them; hence the disk counts eventually equal the multiplicities of the limiting roots. This contradicts the chosen indices. Therefore the counts agree for all sufficiently large $n$ .

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

A simple eigenpair has a regularity-matched gauge-fixed parameter branch

Statement

Let $k \geq 1$ and let $A (λ) \in C^{d \times d}$ be a $C^{k}$ matrix path. Let $ζ_{0}$ be a simple eigenvalue of $A (0)$ , and choose compatible left and right eigenvectors $p_{0}, q_{0}$ with $p_{0}^{*} q_{0} = 1$ . Then there are unique local $C^{k}$ functions $ζ (λ), q (λ)$ such that $A (λ) q (λ) = ζ (λ) q (λ), p_{0}^{*} q (λ) = 1, ζ (0) = ζ_{0}, q (0) = q_{0} .$ There is also a unique local $C^{k}$ left eigenvector $p (λ)$ with $A (λ)^{*} p (λ) = \overline{ζ (λ)} p (λ), p (λ)^{*} q (λ) = 1, p (0) = p_{0} .$ Moreover, $ζ^{'} (0) = p_{0}^{*} A^{'} (0) q_{0}$ .

Facts & Assumptions

Given: $A$ , $ζ_{0}$ , $p_{0}$ , $q_{0}$ and the hypotheses in the Statement.

[F1]

Compatible left and right eigenvectors for a simple eigenvalue: $A (0) q_{0} = ζ_{0} q_{0}$ and $p_{0}^{*} A (0) = ζ_{0} p_{0}^{*}$ .

[F2]

For a simple eigenvalue, left and right eigenvectors pair nontrivially and may be normalized by $y^{*} x = 1$ : compatible left and right eigenvectors for a simple eigenvalue can be normalized by $p_{0}^{*} q_{0} = 1$ .

[F3]

The parametrized implicit function theorem with $C^{k}$ regularity: a $C^{k}$ equation with an invertible derivative in the solved variables has a unique local $C^{k}$ solution branch for every $k \geq 1$ .

[F4]

A simple eigenvalue and a gauge-fixed right eigenvector admit local $C^{1}$ branches in the underlying real matrix space: the simple eigenvalue and the same gauge-fixed eigenvector have unique local $C^{1}$ branches.

[F5]

Along a differentiable matrix path, a simple eigenvalue satisfies $λ^{'} = y^{*} A^{'} x$ under the normalization $y^{*} x = 1$ : along compatible branches normalized by $p^{*} q = 1$ , $ζ^{'} = p^{*} A^{'} q$ .

Proof

Given: The data and hypotheses in the Statement.

1.1F1F2givenalgebra

Regard complex vector spaces as real spaces of twice the dimension and define $Φ (λ, ζ, q) : = ((A (λ) - ζ I) q, p_{0}^{*} q - 1) .$ This is $C^{k}$ by the matrix path hypothesis. Its derivative in $(ζ, q)$ at $(0, ζ_{0}, q_{0})$ sends $(a, v)$ to $((A (0) - ζ_{0} I) v - a q_{0}, p_{0}^{*} v)$ . If this derivative is zero, left multiplication of the first component by $p_{0}^{*}$ gives $- a = 0$ by [F1] and [F2]; then $v$ is in the eigenspace spanned by $q_{0}$ , and $p_{0}^{*} v = 0$ forces $v = 0$ . Thus the derivative is injective and, its finite-dimensional domain and codomain having equal real dimension, invertible.

2.1F3F4step 1.1

Apply [F3] to $Φ = 0$ in the solved variables $(ζ, q)$ . It gives unique $C^{k}$ branches satisfying the eigenvalue equation, gauge, and base values. By uniqueness they agree with the $C^{1}$ branches in [F4].

2.2F1F2F3step 1.1algebra

Apply the same implicit-function construction as step 1.1 to $A (λ)^{*}$ at eigenvalue ${\overset{ˉ}{ζ}}_{0}$ , with gauge $q_{0}^{*} p (λ) = 1$ . The same injectivity computation, with $q_{0}, p_{0}$ interchanged and conjugated, gives a unique $C^{k}$ left eigenvector branch $\tilde{p} (λ)$ ; its eigenvalue is $\overline{ζ (λ)}$ by uniqueness of the simple local branch.

3.1F1F2step 2.1step 2.2givenalgebra

Set $c (λ) = \tilde{p} (λ)^{*} q (λ)$ . It is $C^{k}$ and $c (0) = 1$ , so it stays nonzero after shrinking the interval. Define $p (λ) = \tilde{p} (λ) / \overline{c (λ)}$ ; then $p (λ)^{*} q (λ) = c (λ) / c (λ) = 1$ and its eigenvector equation is unchanged. If $\hat{p}$ is another such local branch, rescale it by $d (λ) = q_{0}^{*} \hat{p} (λ)$ , which is nonzero near zero and equals $1$ at zero. Then $\hat{p} / d$ satisfies the fixed gauge $q_{0}^{*} (\hat{p} / d) = 1$ and solves the same adjoint eigenpair equation, so IFT uniqueness from step 2.2 gives $\hat{p} / d = \tilde{p}$ . The normalization ${\hat{p}}^{*} q = 1$ then forces $d = 1 / \overline{c}$ , hence $\hat{p} = p$ .

4.1F1F2F5step 2.1algebra∎

Differentiate $A (λ) q (λ) = ζ (λ) q (λ)$ at zero and left-multiply by $p_{0}^{*}$ . The terms containing $q^{'} (0)$ cancel by [F1], and $p_{0}^{*} q_{0} = 1$ by [F2], leaving $ζ^{'} (0) = p_{0}^{*} A^{'} (0) q_{0}$ , also the interface stated in [F5].

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (gpt-6-luna)Open item page →

Local periodic-orbit, Poincare-return, and Floquet data

Definition

For a real $C^{1}$ vector field $\dot{x} = f (x)$ on an open subset of $R^{d}$ , a nonconstant solution $x_{*} (t)$ with least positive period $T$ has periodic orbit $Γ = {x_{*} (t) : 0 \leq t < T}$ . Its variational fundamental matrix $Y (t)$ solves

$\dot{Y} (t) = D f (x_{*} (t)) Y (t), Y (0) = I .$

The matrix $Y (T)$ is the monodromy matrix; its eigenvalues, counted with algebraic multiplicity, are the Floquet multipliers. The multiplier $1$ in the direction ${\dot{x}}_{*} (0)$ is called the phase multiplier.

A local Poincare section at $x_{*} (0)$ is a smooth codimension-one surface through that point whose tangent space does not contain $f (x_{*} (0))$ . The local return map, on a sufficiently small section neighborhood where the next return is defined, sends a point to its next intersection after one turn around $Γ$ . Its derivative at $x_{*} (0)$ is the Poincare derivative.

The orbit is orbitally asymptotically stable if it is Lyapunov stable as a set and the distance from every sufficiently nearby trajectory to $Γ$ tends to zero as time tends to $+ \infty$ . It is orbitally unstable if it is not Lyapunov stable as a set.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passOpen item page →

A hyperbolic fixed point of a local map is stable exactly when all multipliers contract

Statement

Let $P$ be a $C^{1}$ map from a neighborhood of $0$ in $R^{m}$ to $R^{m}$ with $P (0) = 0$ . If $D P (0)$ has no eigenvalue on the unit circle, then:

if every eigenvalue has modulus less than one, $0$ is a locally asymptotically stable fixed point;
if at least one eigenvalue has modulus greater than one, $0$ is an unstable fixed point.

Here local asymptotic stability means Lyapunov stability and convergence of all iterates from a neighborhood to $0$ ; instability means failure of Lyapunov stability.

Facts & Assumptions

Given: $P$ , its fixed point, and the spectral hypothesis in the Statement.

[F1]

Jordan form over the base field exists exactly when the characteristic polynomial splits: over $C$ , a finite-dimensional matrix whose characteristic polynomial splits has a Jordan form.

[F2]

A complex polynomial of degree $n$ has exactly $n$ roots counted with multiplicity: every complex characteristic polynomial splits and its roots are counted with algebraic multiplicity.

[F3]

On a convex open set, a uniform bound $∥ D f (z) v ∥_{2} \leq M ∥ v ∥_{2}$ implies $∥ f (y) - f (x) ∥_{2} \leq M ∥ y - x ∥_{2}$ : on a convex open Euclidean domain, $∥ D f (z) v ∥_{2} \leq M ∥ v ∥_{2}$ implies $∥ f (x) - f (y) ∥_{2} \leq M ∥ x - y ∥_{2}$ .

[F4]

$C^{k}$ Euclidean maps and diffeomorphisms: $C^{1}$ maps have continuous first derivatives.

Proof

Given: $P (0) = 0$ and $A : = D P (0)$ has no eigenvalue of modulus one.

1.1F1F2givenconstruct

If $m = 0$ , the space has only its fixed point, so local asymptotic stability is immediate. Henceforth let $m \geq 1$ . Suppose first every eigenvalue of $A$ has modulus less than one. By [F1]–[F2], put its complexification in Jordan form. On a Jordan block $λ I + N$ of size $k$ , conjugate by the diagonal matrix with entries $1, δ, \dots, δ^{k - 1}$ ; the superdiagonal becomes $δ$ , so the maximum row-sum norm is at most $∣ λ ∣ + δ$ . Choose $δ$ small for the finitely many blocks. Restricting the resulting equivalent norm to the real space gives an induced norm with $∥ A ∥ < q < 1$ .

2.1F3F4step 1.1givenalgebra

Fix constants $c, C > 0$ with $c ∥ v ∥_{2} \leq ∥ v ∥ \leq C ∥ v ∥_{2}$ for the adapted norm in step 1.1; the finite coordinate sums for the change of basis and its inverse give these bounds. Put $R (x) = P (x) - A x$ , so $D R (0) = 0$ . Choose $ϵ > 0$ with $q^{'} : = q + (C / c) ϵ < 1$ . By [F4], on a sufficiently small convex open Euclidean ball, $∥ D R (x) ∥_{2} \leq ϵ$ , so [F3] gives $∥ R (x) - R (y) ∥_{2} \leq ϵ ∥ x - y ∥_{2}$ . Consequently $∥ P (x) - P (y) ∥ \leq (q + (C / c) ϵ) ∥ x - y ∥ = q^{'} ∥ x - y ∥$ . Choose an adapted-norm ball inside that Euclidean ball. Since $P (0) = 0$ , every iterate from this smaller ball stays in it and satisfies $∥ P^{n} (x) ∥ \leq (q^{'})^{n} ∥ x ∥ \to 0$ . Norm equivalence also transfers Lyapunov stability to the Euclidean topology, proving local asymptotic stability.

2.2F1F2step 1.1givenalgebra

Now suppose $A$ has an eigenvalue of modulus greater than one. Its stable and unstable generalized eigenspaces give an invariant direct sum $E_{s} \oplus E_{u}$ . Applying the Jordan scaling in step 1.1 to $A ∣_{E_{s}}$ and $(A ∣_{E_{u}})^{- 1}$ gives equivalent norms and constants $a < 1 < b$ such that $∥ A_{s} s ∥ \leq a ∥ s ∥$ and $∥ A_{u} u ∥ \geq b ∥ u ∥$ .

3.1step 2.2F4algebra

Write $P (x) = A x + R (x)$ , where $D R (0) = 0$ . By continuity in [F4], on a sufficiently small ball $∥ R (x) ∥ \leq ϵ ∥ x ∥$ . In the cone $∥ s ∥ \leq ∥ u ∥$ , the product maximum norm gives $∥ x ∥ = ∥ u ∥$ ; hence $∥ u^{'} ∥ \geq (b - ϵ) ∥ u ∥$ and $∥ s^{'} ∥ \leq (a + ϵ) ∥ u ∥$ . Choose $ϵ > 0$ with $b - ϵ > 1$ and $a + ϵ < b - ϵ$ . The cone is forward invariant while the iterate remains in the ball, and its unstable component grows by the factor $b - ϵ > 1$ .

4.1step 3.1givencontradiction∎

Starting at any arbitrarily small nonzero $u \in E_{u}$ with $s = 0$ , step 3.1 forces an iterate to leave the fixed ball; otherwise its unstable component would grow without bound while staying in that ball. Thus arbitrarily small initial data escape this one fixed neighborhood of zero, so zero is not Lyapunov stable.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passOpen item page →

The weighted trajectory space is complete

Statement

If $E$ is finite-dimensional and complete, then $(C_{η} (E), ∥ \cdot ∥_{η})$ is a Banach space for every $η > 0$ . No choice principle is used.

Facts & Assumptions

Given: A finite-dimensional complete normed space $E$ , $η > 0$ , and the space $C_{η} (E)$ of Weighted trajectory space for a local center-manifold construction.

[F1]

Weighted trajectory space for a local center-manifold construction: $∥ u ∥_{η} = \sup_{t \in R} e^{- η ∣ t ∣} ∥ u (t) ∥$ .

[F2]

$R$ and $R^{n}$ for $n \geq 1$ with the Euclidean metric are complete, componentwise from the Cauchy criterion in $R$ proves completeness of $R$ and of Euclidean $R^{n}$ for $n \geq 1$ . In the present lemma, completeness of $E$ in its specified norm is a hypothesis, including when $E = {0}$ .

Proof

Given: $E$ , $η$ , and $C_{η} (E)$ as above.

1.1F1constructalgebra

Define $J_{η} u (t) : = e^{- η ∣ t ∣} u (t)$ . This is a linear isometry from $C_{η} (E)$ onto $C_{b} (R, E)$ with the supremum norm: its inverse sends $g$ to $u (t) = e^{η ∣ t ∣} g (t)$ , and both maps preserve continuity and the displayed norms.

1.2F2givenchoose

Let $(g_{n})$ be Cauchy in $C_{b} (R, E)$ . For each $t$ , $(g_{n} (t))$ is Cauchy in $E$ , so define $g (t)$ to be its unique limit. Given $ε > 0$ , choose $N$ such that $\sup_{t} ∥ g_{n} (t) - g_{m} (t) ∥ < ε / 3$ for $n, m \geq N$ ; letting $m$ tend to infinity pointwise gives $\sup_{t} ∥ g_{n} (t) - g (t) ∥ \leq ε / 3$ for $n \geq N$ . Thus $g_{n} \to g$ uniformly, which makes $g$ continuous, and the same bound with one fixed $n \geq N$ shows $g$ is bounded. Pointwise uniqueness defines $g$ without choice.

2.1step 1.1step 1.2∎

Therefore $C_{b} (R, E)$ is complete, and the isometry in step 1.1 transfers completeness to $C_{η} (E)$ .

Remarks

This result supplies only completeness of the trajectory space. The contraction used to construct the center manifold is verified separately in A parameterized C5 center manifold exists at a simple Hopf spectral split.

AlgorithmAlgorithm: AI-adaptedProof: Not applicablejudge pass (gpt-6-luna)Open item page →

Validate a proof-carrying local Hopf certificate

Definition

An admissible input is a finite proof-carrying record for one equilibrium of a $C^{5}$ vector field $f (x, λ)$ . The record names its critical parameter $λ_{0}$ and exact represented equilibrium $x_{*}$ (or its isolating data). All origin-based Hopf data mean those of $\hat{f} (y, μ) = f (x_{*} + y, λ_{0} + μ)$ at $(0, 0)$ , using Hopf spectral and multilinear normal-form data; for an isolated root this is the exact root established by its witness, not the center of its isolating ball. It contains:

an exact equilibrium, or a root-isolation record satisfying all hypotheses and inequalities of A bounded residual and derivative error give a local root certificate;
a Jacobian $A = D_{x} f$ and its derivative along the locally isolated equilibrium branch, with proof-carrying rational rectangle enclosures for the critical eigenvalue and left and right eigenvectors; exact witnesses verify $A q = i ω q$ , $A^{*} p = - i ω p$ , $q^{*} q = p^{*} q = 1$ , and a root-count certificate proves that each critical eigenvalue has algebraic multiplicity one;
rational rectangle enclosures with checked inclusion witnesses for every noncritical eigenvalue, the parameter derivative of $A$ , the multilinear data $B, C$ in Hopf spectral and multilinear normal-form data, and the entries of $A^{- 1}$ and $(2 i ω I - A)^{- 1}$ ; inverse witnesses verify the corresponding matrix products are the identity;
a multiplicity-cover record giving certified root counts in pairwise disjoint rectangles, with total multiplicity $d$ and the two critical roots counted once each, so the noncritical rectangles account for every remaining root of the characteristic polynomial.

A rational interval is a closed interval $[a, b]$ with exact rational endpoints $a \leq b$ ; a rational rectangle is a product of two such intervals, interpreted as a subset of $C$ . Every witness is a finite, exactly checkable proof tied to the same vector field, parameter, certified equilibrium or equilibrium branch, and named derivative or spectral value. It must establish the stated inclusion, identity, or root count by exact identities and outward rational interval calculations; rounded floating-point output is not a witness. The multiplicity-cover record proves that its rectangle counts sum to $d$ and that the rectangles cover the roots of the characteristic polynomial with their stated algebraic multiplicities. Missing, unsupported, or unproved witnesses make the result inconclusive; malformed intervals or contradictory fields make the input invalid.

The procedure outputs one of: certified-local-hopf with the branch side; inconclusive with the first failed strict hypothesis or missing witness; or invalid-input for malformed rational intervals or inconsistent record fields.

Procedure:

Check that every interval has exact rational endpoints in increasing order and that every rectangle is a product of two such intervals. If not, return invalid-input.
Check that the equilibrium witness is for the stated vector field and parameter. An exact point must satisfy $f (x, λ) = 0$ exactly. Otherwise check the supplied root-isolation record against every hypothesis and inequality in A bounded residual and derivative error give a local root certificate; if a witness is absent or an inequality is unproved, return inconclusive. Check that the Jacobian and all jet, parameter-derivative, and inverse witnesses are tied to this same certified root: they must prove $A = D_{x} f$ , $B = D_{x}^{2} f$ , $C = D_{x}^{3} f$ , the stated derivative $A^{'} = \frac{d}{d λ} D_{x} f (ξ (λ), λ)$ along the unique local equilibrium branch, and the claimed inverse matrix products. A contradictory field value returns invalid-input; missing or insufficient proof returns inconclusive.
Check the eigenpair equations, normalizations, simplicity root counts, positive lower bound for $ω$ , and multiplicity cover. The critical witnesses must prove exactly one simple root at each of $\pm i ω$ , and the noncritical real-part rectangles must each exclude zero. If any condition is unproved, return inconclusive.
Evaluate the outward rational interval expressions for $β^{'} = Re (p^{*} A^{'} q)$ and $ℓ_{1}$ using the enclosures in steps 2–3. The inclusion witnesses must prove each interval operation contains its exact value. If either interval intersects zero, return inconclusive.
If all checks pass, return certified-local-hopf. Here $β^{'} (0)$ means the derivative in $μ = λ - λ_{0}$ of the critical eigenvalue's real part along the translated equilibrium branch. The branch side in the original parameter is the sign condition $β^{'} (0) ℓ_{1} (λ - λ_{0}) < 0$ , with the signs determined by the two strict intervals.

Remarks

The result is intended to be consumed by A certified interval Hopf record verifies only the local Hopf hypotheses, which transfers a successful strict check to the local theorem. The procedure certifies no global orbit, global stability, or completeness of a numerical continuation trace.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

Hyperbolic return-map stability is orbital stability

Statement

Let $f$ be a $C^{1}$ autonomous vector field on an open subset of $R^{d}$ . Let $x_{*} (t)$ be a nonconstant periodic solution of least period $T$ , let $Γ = {x_{*} (t) : 0 \leq t < T}$ , and let $Σ$ be a local smooth Poincare section through $a = x_{*} (0)$ transverse to $f (a)$ . Assume locally $Σ = {y : ρ (y) = 0}$ for a smooth $ρ$ with $D ρ (a) f (a) \neq 0$ , and take a relatively compact section patch $W$ with $\overline{W} \cap Γ = {a}$ . If the derivative of the local return map $P$ at $a$ has no eigenvalue on the unit circle, then $Γ$ is orbitally asymptotically stable when all eigenvalues of $D P (a)$ have modulus less than one, and is orbitally unstable when at least one has modulus greater than one.

Facts & Assumptions

Given: The $C^{1}$ vector field, periodic solution, period, section, and return map in the Statement.

[F1]

Local periodic-orbit, Poincare-return, and Floquet data: the section is codimension one and transverse to the vector field; orbital stability is stability of the orbit as a set plus attraction in distance.

[F2]

C¹ Euclidean maximal flows, variational dependence and the finite C² upgrade: a $C^{1}$ autonomous vector field has a jointly $C^{1}$ maximal flow on an open time-state domain. Nearby initial states share every sufficiently short compact local time interval; the time derivative is the vector field, and uniqueness gives the flow law and finite composition along compact trajectory segments.

[F3]

The parametrized implicit function theorem with $C^{k}$ regularity: for a $C^{1}$ equation, a nonzero derivative in a scalar solved variable gives a $C^{1}$ local implicit function of the remaining variables.

[F4]

A hyperbolic fixed point of a local map is stable exactly when all multipliers contract: a $C^{1}$ fixed point with no unit-circle multiplier is locally asymptotically stable when all multipliers are inside and unstable when one is outside.

[F5]

The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ : derivatives of compositions obey the chain rule.

[F6]

For a nonempty subset of $R^{n}$ with $n \geq 1$ , compactness, closedness and boundedness, pseudocompactness, and attainment of extrema by every continuous real-valued function are equivalent: in finite-dimensional Euclidean space, closed bounded sets are compact and continuous real-valued functions on nonempty compact sets attain their extrema.

[F7]

The image of a compact metric space under a continuous map is compact, and so is the image of any compact subset: the image of a compact metric space under a continuous map is compact.

[F8]

Every continuous map from a nonempty compact Hausdorff space to a uniform space is uniformly continuous: a continuous map from a compact metric domain to a metric target is uniformly continuous.

Proof

Given: The data and spectral alternatives in the Statement.

1.1F1F2F3F5F6F7givenalgebra

The periodic solution over $[0, 2 T + 1]$ is a compact trajectory segment by [F6]–[F7]. Cover it by finitely many neighborhoods on which the local flow in [F2] exists, subdivide $[0, 2 T + 1]$ into finitely many pieces contained in those flow times, and compose the corresponding local flows. After shrinking the initial-state neighborhood, this gives a jointly $C^{1}$ map $(t, y) \mapsto ϕ_{t} (y)$ for $0 \leq t \leq 2 T + 1$ and $y$ near $a$ . Set $Ψ (t, y) = ρ (ϕ_{t} (y))$ . At $(T, a)$ , $Ψ (T, a) = 0$ and $\partial_{t} Ψ (T, a) = D ρ (a) f (a) \neq 0$ . Apply [F3] with $k = 1$ to obtain a $C^{1}$ return time $τ (y)$ near $T$ and hence a $C^{1}$ return map $P (y) = ϕ_{τ (y)} (y)$ on a section neighborhood.

2.1F1F2F3F5F6F7step 1.1givenalgebra

For each $s \in [0, T]$ , put $t_{s} = 2 T - s$ . Then $ϕ_{t_{s}} (x_{*} (s)) = a$ and $T \leq t_{s} \leq 2 T$ . Cover the compact segment from $x_{*} (s)$ to $a$ by finitely many flow neighborhoods from [F2] and compose them; this defines the flow near $(t_{s}, x_{*} (s))$ . Apply [F3] to $Ψ (t, x) = ρ (ϕ_{t} (x))$ there; its time derivative is $D ρ (a) f (a) \neq 0$ . This gives a $C^{1}$ positive hitting time near each $x_{*} (s)$ , bounded by $2 T + 1$ , whose flow endpoint lies on $Σ$ near $a$ . Compactness of $Γ$ from [F6]–[F7] gives finitely many such neighborhoods and a uniform neighborhood of $Γ$ on which this forward-to-section property holds. Continuity of the finitely composed flow on compact time subintervals also makes each initial segment, up to its hitting time, uniformly close to the corresponding segment of $Γ$ when the initial point is close to $Γ$ .

3.1F1F2F4F6F7F8step 1.1step 2.1given

Suppose all eigenvalues of $D P (a)$ lie inside the unit circle. By [F4], after shrinking the section neighborhood, every return iterate of a sufficiently close section point stays in that neighborhood and converges to $a$ . The return times are continuous and bounded below by $T / 2$ after another shrink. The flow is uniformly continuous on the compact time-section product by [F6] and [F8], so the orbit segment from each return point approaches one traversal of $Γ$ uniformly as the return point tends to $a$ . Since the return points converge to $a$ , distance to $Γ$ tends to zero along the full forward trajectory.

4.1F1F2F4F6F8step 1.1step 2.1step 3.1given

For Lyapunov stability, fix $ε > 0$ . For a relatively compact section patch $\overline{V}$ , the product $[0, T + 1] \times \overline{V}$ is closed and bounded in Euclidean space and hence compact by [F6]. The flow on this set is continuous by [F2] and the finite-composition construction in step 1.1, so [F8] makes it uniformly continuous. Shrink $V$ so every orbit segment starting in $V$ stays within $ε$ of $Γ$ until its next return. Fixed-point stability in [F4] gives a smaller neighborhood whose return iterates all remain in $V$ . Step 2.1 then supplies a neighborhood of $Γ$ whose points first reach the section inside that smaller neighborhood while their initial segments stay within $ε$ of $Γ$ . Thus all forward trajectories from this neighborhood remain within $ε$ of $Γ$ . Together with step 3.1 this proves orbital asymptotic stability.

5.1F1F4F6F7givencontradiction∎

Suppose instead that $D P (a)$ has an eigenvalue outside the unit circle. By [F4], there is a fixed section neighborhood $V$ and section points arbitrarily close to $a$ whose return iterates leave $V$ . Choose a relatively compact local section patch $W$ with $\overline{W} \cap Γ = {a}$ and then choose $V$ with $\overline{V} \subset W$ and $P (V) \subset W$ . The set $K = \overline{W} ∖ V$ is closed, bounded, and nonempty, hence compact by [F6]; it is disjoint from compact $Γ$ by construction. For each $x \in K$ , compactness of $Γ$ gives a closest point, so $d_{Γ} (x) : = dist (x, Γ) > 0$ . The triangle inequality gives $∣ d_{Γ} (x) - d_{Γ} (y) ∣ \leq ∥ x - y ∥$ , so $d_{Γ}$ is continuous; [F6] gives it a positive minimum on $K$ . Therefore the first return point outside $V$ lies a fixed positive distance from $Γ$ . Such initial points can be chosen arbitrarily close to $a \in Γ$ , so $Γ$ is not Lyapunov stable as a set. It is orbitally unstable.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passOpen item page →

A parameterized C5 center manifold exists at a simple Hopf spectral split

Statement

Let $f (x, λ)$ be $C^{5}$ near $(0, 0)$ in $R^{d} \times R$ , and suppose $f (0, λ) = 0$ for all sufficiently small $λ$ . Assume $A = D_{x} f (0, 0)$ has a simple pair $\pm i ω$ , $ω > 0$ , and every other eigenvalue has nonzero real part. Choose $q \neq 0$ with $A q = i ω q$ and set $E_{c} = {span}_{R} {Re q, Im q}$ . Let $E_{s}$ and $E_{u}$ be the real sums of generalized eigenspaces with eigenvalues of negative and positive real part, respectively, and set $E_{h} = E_{s} \oplus E_{u}$ . For the extended system $\dot{λ} = 0$ , there are neighborhoods $U \subset E_{c}$ and $J \subset R$ of zero and a $C^{5}$ map $h : U \times J \to E_{h}$ whose graph $x = z + h (z, λ)$ is tangent to $E_{c} \times R$ at the origin and contains every sufficiently small periodic trajectory that remains in the chosen neighborhood.

Write $A_{λ} = D_{x} f (0, λ)$ . Since $f$ is $C^{5}$ , this matrix path is $C^{4}$ ; let $ζ (λ)$ be its $C^{4}$ simple eigenvalue branch from A simple eigenpair has a regularity-matched gauge-fixed parameter branch. For each small $λ$ , the graph tangent plane $range D_{z} (z + h) (0, λ)$ is the invariant plane spanned by the right eigenvectors for $ζ (λ)$ and $\overline{ζ (λ)}$ .

Write $P_{c}, P_{h}$ for the spectral projections of $A$ and define

$f_{c} (z, h, λ) : = P_{c} f (z + h, λ), f_{h} (z, h, λ) : = P_{h} f (z + h, λ) .$

The graph satisfies the actual invariance equation

$D_{z} h (z, λ) f_{c} (z, h (z, λ), λ) = f_{h} (z, h (z, λ), λ), h (0, λ) = 0, D_{z} h (0, 0) = 0.$

On a smaller neighborhood it also satisfies $h (z, λ) = O (∥ z ∥^{2} + ∣ λ ∣ ∥ z ∥)$ . No Axiom of Choice is used.

Facts & Assumptions

Given: $f$ , $A$ , $ω$ , $E_{c}$ , $E_{s}$ , $E_{u}$ , and the hypotheses in the Statement.

[F1]

Hopf spectral and multilinear normal-form data: the critical eigenpair is simple, and the only eigenvalues of $A$ on the imaginary axis are $\pm i ω$ .

[F2]

Weighted trajectory space for a local center-manifold construction: $C_{η} (E) = {u \in C (R, E) : \sup_{t} e^{- η ∣ t ∣} ∥ u (t) ∥ < \infty}$ .

[F3]

The weighted trajectory space is complete: this weighted trajectory space is complete.

[F4]

A contraction of a nonempty complete metric space into itself has exactly one fixed point, the limit of the iterates from any starting point: a contraction of a nonempty complete metric space into itself has a unique fixed point, obtained by iteration.

[F5]

$C^{k}$ Euclidean maps and diffeomorphisms: $C^{5}$ means continuous derivatives through order five.

[F6]

The first fundamental theorem: if $f$ is integrable on $[a, b]$ and continuous at $c$ , then $F^{'} (c) = f (c)$ ; in particular a continuous $f$ has $F$ as a primitive: for a continuous integrand on a compact interval, its integral primitive differentiates to that integrand at every point, with one-sided derivatives at endpoints.

[F7]

The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ : derivatives of compositions obey the chain rule.

[F8]

Jordan form over the base field exists exactly when the characteristic polynomial splits and Jordan bases and Jordan canonical forms over the base field: when a finite-dimensional complex linear map has split characteristic polynomial, it has a Jordan basis, and each block is $J_{m} (α) = α I + N$ with $N^{m} = 0$ .

[F9]

A smooth bump between concentric Euclidean balls: there is a smooth cutoff equal to one on a smaller closed ball and supported in a larger open ball.

[F10]

On a convex open set, a uniform bound $∥ D f (z) v ∥_{2} \leq M ∥ v ∥_{2}$ implies $∥ f (y) - f (x) ∥_{2} \leq M ∥ y - x ∥_{2}$ : a uniform derivative bound on a convex open set gives the corresponding Lipschitz bound.

[F11]

For a nonempty subset of $R^{n}$ with $n \geq 1$ , compactness, closedness and boundedness, pseudocompactness, and attainment of extrema by every continuous real-valued function are equivalent: every nonempty closed bounded subset of $R^{d}$ is compact, and a continuous real-valued function on it attains a finite maximum.

[F12]

A simple eigenpair has a regularity-matched gauge-fixed parameter branch: a $C^{k}$ matrix path with a simple eigenvalue has a unique local $C^{k}$ eigenvalue and gauge-fixed right-eigenvector branch. Here $A_{λ}$ is $C^{4}$ because $f$ is $C^{5}$ , so these branches are $C^{4}$ .

[F13]

Characteristic roots preserve separated cluster counts under matrix perturbation: near a matrix with separated eigenvalue neighborhoods, each neighborhood retains the same algebraic root count under small perturbation.

[F14]

$R$ and $R^{n}$ for $n \geq 1$ with the Euclidean metric are complete, componentwise from the Cauchy criterion in $R$ : the ambient extended state space $R^{d + 1}$ with its Euclidean norm is complete.

[F15]

Every Euclidean linear map has a unique matrix and satisfies $∥ L h ∥_{2} \leq K ∥ h ∥_{2}$ for some $K \geq 0$ : every Euclidean linear map has a finite operator-norm bound.

[F16]

The complex exponential by its power series: $\exp z = \sum_{n \geq 0} z^{n} / n!$ for every $z \in C$ .

[F17]

The complex exponential is entire and its complex derivative is itself: $\frac{d}{d t} \exp (α t) = α \exp (α t)$ for $α \in C$ and real $t$ .

[F18]

$\exp (z + w) = \exp z \exp w$ , and the complex exponential extends the real exponential: $\exp (z + w) = \exp z \exp w$ for complex $z, w$ .

[F19]

$\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ : $∣ \exp (x + i y) ∣ = e^{x}$ for real $x, y$ .

[F20]

Newton–Leibniz needs only continuity on $[a, b]$ , differentiability on $(a, b)$ , and a Riemann-integrable extension of the interior derivative: if a scalar function is continuous on a compact interval and differentiable in its interior with continuous integrable derivative, integrating the derivative recovers the endpoint difference; apply this componentwise to finite-dimensional derivative arrays.

[F21]

The finite-dimensional product rule follows directly from total differentiability: for scalar maps $a, b$ , expand $a (y + h) = a (y) + D a (y) h + o (∥ h ∥)$ and $b (y + h) = b (y) + D b (y) h + o (∥ h ∥)$ and multiply. The linear part is $a (y) D b (y) h + b (y) D a (y) h$ , and all other terms are $o (∥ h ∥)$ . Applying this to each coordinate and summing proves the rule for every finite bilinear product and for evaluation of a multilinear array on varying arguments.

[F22]

$χ_{A} (x)$ is monic of degree $n$ ; for $n \geq 1$ its $x^{n - 1}$ coefficient is $- tr (A)$ and its constant coefficient is $(- 1)^{n} \det (A)$ , while $χ_{0 \times 0} = 1$ and A complex polynomial of degree $n$ has exactly $n$ roots counted with multiplicity: the extended matrix's characteristic polynomial has degree $d + 1 \geq 1$ and splits over $C$ .

[F23]

Finite componentwise sums/products and compositions of $C^{k}$ Euclidean maps are $C^{k}$ for every finite $k$ ( $C^{k}$ Euclidean maps are closed under componentwise algebra and composition). Thus the cutoff products and all finite derivative-array operations below retain their declared regularity.

Proof

1.1F1F7F8F15F16F17F18F19F21F22givenalgebra

On the extended state $(x, λ)$ , the linearization is $diag (A, 0)$ because $f (0, λ) \equiv 0$ . Its characteristic polynomial has positive degree and splits over $C$ by [F22], so [F8] gives the direct sum of complex generalized eigenspaces with Jordan blocks as defined by Jordan bases and Jordan canonical forms over the base field. The real and imaginary parts of $q$ are independent: otherwise $q$ would be a nonzero complex multiple of a real vector $r$ , forcing $A r = i ω r$ , impossible because $A r$ is real and $i ω r$ is nonreal. Since $A$ is real, conjugation maps the generalized eigenspace for $α$ onto the one for $\overset{ˉ}{α}$ ; grouping conjugate chains gives a real invariant splitting into the critical plane $E_{c}$ and $E_{s} \oplus E_{u}$ , and adjoining the parameter's zero coordinate gives center space $E_{c} \times R$ . To define the linear flow notation used below, on a Jordan block $J = α I + N$ with $N^{m} = 0$ put $T_{J} (t) : = \exp (α t) \sum_{k = 0}^{m - 1} t^{k} N^{k} / k!$ . By [F7], [F17] and [F21], $T_{J}^{'} (t) = J T_{J} (t)$ and $T_{J} (0) = I$ ; by [F18] and the finite binomial expansion, $T_{J} (t) T_{J} (s) = T_{J} (t + s)$ , since every term involving $N^{k}$ with $k \geq m$ vanishes. Conjugating these block operators by one fixed Jordan basis defines $e^{B t}$ on the center, stable and unstable summands; paired conjugate blocks give operators preserving the real subspaces. The simple critical pair has no nontrivial Jordan part and the parameter zero block is one-dimensional, so the center flow is bounded: on the critical blocks [F19] gives $∣ \exp (\pm i ω t) ∣ = 1$ , and on the parameter block it is the identity. On a stable block write $a = - Re α > 0$ and choose $0 < γ < a$ ; [F19] gives $∣ \exp (α t) ∣ = e^{- a t}$ . For each $k < m$ , $t^{k} e^{- (a - γ) t}$ is bounded on $[0, \infty)$ : on $[0, 1]$ it is at most $1$ , and for $t \geq 1$ [F16] and the real-extension clause of [F18] give $e^{(a - γ) t} \geq ((a - γ) t)^{k} / k!$ . The same argument with $- t$ applies to unstable blocks. There are finitely many blocks, so choose one $γ > 0$ smaller than every nonzero $∣ Re α ∣$ ; the finite sums and products have a common finite bound. The changes of basis, their inverses, and the projections have finite operator norms by [F15]; enlarging $K$ to include these and the bounded center flow gives $∥ e^{A_{c} t} ∥ \leq K$ , $∥ e^{A_{s} t} ∥ \leq K e^{- γ t}$ and $∥ e^{- A_{u} t} ∥ \leq K e^{- γ t}$ for $t \geq 0$ . If the hyperbolic complement is zero, its estimates are vacuous.

1.2F5F7F9F10F11F21F23givenconstructalgebra

In these coordinates write the extended state as $(v, w)$ , with $v = (z, λ) \in E_{c} \times R$ and $w = (w_{s}, w_{u}) \in E_{s} \oplus E_{u}$ , and write its equation as $\dot{v} = A_{c} v + N_{c} (v, w)$ and $\dot{w} = A_{h} w + N_{h} (v, w)$ . The nonlinear remainder $N$ has $N (0) = D N (0) = 0$ . On a small closed ball its second derivative is bounded; applying [F10] first to $D N$ and then to $N$ gives $∥ D N (y) ∥ \leq C ∥ y ∥$ and $∥ N (y) ∥ \leq C ∥ y ∥^{2}$ . Choose a fixed smooth bump $χ$ equal to one on the unit ball and supported in the ball of radius two, using [F9]. Its derivative has finite bound by [F11]; set $χ_{r} (y) = χ (y / r)$ , so [F7] gives $∥ D χ_{r} ∥ \leq C_{χ} / r$ . On the support ball, the product rule [F21] gives $∥ D (χ_{r} N) ∥ \leq C r + C r^{2} (C_{χ} / r) = C^{'} r$ . Extend $χ_{r} N$ by zero outside the coordinate domain; its support is compactly contained there, so [F23] makes the extension $C^{5}$ , compactly supported, and has bounded derivatives through order five.

2.1F9F10step 1.2algebra

The support of $χ_{r}$ lies in the radius- $2 r$ ball, where the preceding derivative estimate holds; outside it the derivative of the extended product is zero. The global derivative bound and [F10] make the cut-off remainder globally Lipschitz with constant at most $C^{'} r$ . Taking $r$ small makes this constant the required $ε$ , while the cutoff equals one on the radius- $r$ ball. Hence solutions staying in that smaller ball solve the original equation.

3.1F2F3F14step 1.1step 2.1givenalgebra

Let $E_{e x t} : = (E_{c} \times R) \oplus E_{s} \oplus E_{u}$ , identified with $R^{d + 1}$ by the invariant splitting in step 1.1 and equipped with the transported Euclidean norm; [F14] makes it complete and [F3] makes $C_{η} (E_{e x t})$ complete for every $η > 0$ . Choose $η > 0$ with $η_{6} : = 3^{6} η < γ$ and put $η_{j} = 3^{j} η$ for $0 \leq j \leq 6$ . For each center initial value $ξ \in E_{c} \times R$ , define a map on $C_{η_{0}} (E_{e x t})$ by $v (t) = e^{A_{c} t} ξ + \int_{0}^{t} e^{A_{c} (t - s)} N_{c} (v (s), w (s)) d s$ , $w_{s} (t) = \int_{- \infty}^{t} e^{A_{s} (t - s)} N_{s} (v (s), w (s)) d s$ , and $w_{u} (t) = - \int_{t}^{\infty} e^{A_{u} (t - s)} N_{u} (v (s), w (s)) d s$ , where $v (t) \in E_{c} \times R$ and $w (t) = (w_{s} (t), w_{u} (t))$ . The cut-off remainder is bounded, so these integrals define elements of the weighted space. For a weight $δ < γ$ , the center integral difference is bounded by $K ε / δ$ and each hyperbolic integral difference by $K ε / (γ - δ)$ . Choose the cutoff radius in step 2.1 small enough that $K ε (1 / η_{j} + 2 / (γ - η_{j})) < 1$ for all $0 \leq j \leq 6$ . In particular the map is a contraction on $C_{η_{0}} (E_{e x t})$ .

4.1F3F4F6F7F21step 1.1step 3.1algebra

By [F4], for each $ξ$ there is a unique fixed trajectory $Γ_{ξ}$ in this weighted space. For each $σ \in {s, u}$ , splitting the corresponding improper integral at a finite time $t_{0}$ and using the semigroup identity from step 1.1 gives $w_{σ} (t) = e^{A_{σ} (t - t_{0})} w_{σ} (t_{0}) + \int_{t_{0}}^{t} e^{A_{σ} (t - s)} N_{σ} (Γ_{ξ} (s)) d s$ ; for $σ = u$ this uses the minus sign in the defining future integral and the oriented integral from $t_{0}$ to $t$ . For the center component, factor $e^{A_{c} (t - s)} = e^{A_{c} t} e^{- A_{c} s}$ in its integral formula. The finite-interval integrands are continuous; componentwise [F6] differentiates their primitives, and [F7], [F21] differentiate the products with the linear flows. Thus $Γ_{ξ}$ solves the cut-off differential equation and has center coordinate $ξ$ at time zero.

5.1F2F3F4F5F7F14step 3.1step 4.1algebra

Let $X_{j} : = C_{η_{j}} (E_{e x t})$ for $0 \leq j \leq 6$ , and let $K$ denote the three integral operators in step 3.1. Write $T_{ξ} (u) = ι_{c} ξ + K (N \circ u)$ , where $ι_{c} ξ (t) = (e^{A_{c} t} ξ, 0, 0)$ , and define the formal linearization $L_{ξ} v : = K (D N (Γ_{ξ}) v)$ . This definition does not assert same-weight Fréchet differentiability of $T_{ξ}$ ; parameter derivatives are established below using increasing weights. The estimates in step 3.1 give $∥ L_{ξ} ∥_{X_{j} \to X_{j}} \leq κ_{j} : = K ε (1 / η_{j} + 2 / (γ - η_{j})) < 1$ for every $j \leq 6$ , so $(I - L_{ξ})^{- 1} = \sum_{n \geq 0} L_{ξ}^{n}$ on each $X_{j}$ . Define candidate derivatives recursively by $U_{1} [v] = (I - L_{ξ})^{- 1} ι_{c} v$ and, for $2 \leq j \leq 5$ , by the unique solution of $(I - L_{ξ}) U_{j} [v_{1}, \dots, v_{j}] = K \sum_{π \in Π_{j}, ∣ π ∣ \geq 2} D^{∣ π ∣} N (Γ_{ξ}) [U_{∣ B ∣} [v_{i} : i \in B] : B \in π]$ , where $Π_{j}$ is the set of partitions of ${1, \dots, j}$ . The recursion and induction make each $U_{j}$ symmetric multilinear in its direction arguments. In every forcing summand the positive block sizes $k_{i} : = ∣ B_{i} ∣$ sum to $j$ and $\sum_{i} η_{k_{i}} < η_{j}$ : for positive integers $a, b$ , $3^{a} + 3^{b} < 3^{a + b}$ , and iteration gives the strict inequality for every partition with at least two blocks. Since the derivatives of the cutoff remainder are bounded, each forcing term belongs to $X_{j}$ ; the Neumann series therefore defines a unique $U_{j} \in X_{j}$ .

6.1F5F7F21F23step 5.1algebra

The finite-dimensional partition rule used in step 5.1 follows by labelled-direction induction from [F7] and [F21]. At first order, $D (N \circ u) [v_{1}] = D N (u) D u [v_{1}]$ , the single partition of ${1}$ . Given the expression indexed by partitions of ${1, \dots, j - 1}$ , differentiate in a new direction $v_{j}$ . Differentiating the coefficient $D^{∣ π ∣} N (u)$ adds the singleton block ${j}$ ; differentiating a factor $D^{∣ B ∣} u [v_{i} : i \in B]$ inserts $j$ into that block $B$ . Every partition of ${1, \dots, j}$ arises exactly once: remove its singleton ${j}$ if present, or remove $j$ from its unique nonsingleton block. Hence the resulting sum is $\sum_{π \in Π_{j}} D^{∣ π ∣} N (u) [D^{∣ B ∣} u [v_{i} : i \in B] : B \in π]$ . Its one-block term is $D N (u) D^{j} u$ , which is the term moved to the left in step 5.1; all other terms use only lower derivatives of $u$ . For the difference-quotient argument in steps 7.1–8.1 this induction is first an algebraic identity for the candidate terms: the actual derivative limit is then established there, rather than assumed. Only derivatives of $N$ through order $j \leq 5$ occur, and [F23] licenses the finite-dimensional coefficient operations.

6.2F3F4F5step 3.1step 4.1step 5.1algebra

Set $U_{0} (ξ) : = Γ_{ξ}$ . Subtracting the fixed-point equations gives $∥ Δ U_{0} ∥_{X_{0}} \leq C ∣ δ ∣$ by the contraction estimate. After moving $L_{ξ} Δ U_{0}$ left, the Taylor remainder $K (N (Γ_{ξ} + Δ U_{0}) - N (Γ_{ξ}) - D N (Γ_{ξ}) Δ U_{0}) / δ$ tends to zero in $X_{1}$ : on bounded time intervals this follows from continuity of $D^{2} N$ , while on the tails it is bounded by $C ∣ δ ∣ e^{2 η_{0} ∣ t ∣}$ and $2 η_{0} < η_{1}$ . The inverse of $I - L_{ξ}$ on $X_{1}$ therefore gives $D_{ξ} U_{0} = U_{1}$ as defined in step 5.1.

7.1F5F7F20F21step 1.2step 3.1step 4.1step 5.1step 6.2algebra

For $2 \leq j \leq 5$ , write $F_{j - 1} (ξ)$ for the partition forcing in step 5.1, so $(I - L_{ξ}) U_{j - 1} (ξ) = F_{j - 1} (ξ)$ . Subtracting at $ξ + δ v$ and $ξ$ gives $(I - L_{ξ}) Δ U_{j - 1} = (L_{ξ + δ v} - L_{ξ}) U_{j - 1} (ξ + δ v) + Δ F_{j - 1}$ . Inductively the same identity for each lower $U_{k}$ gives $∥ Δ U_{k} ∥_{X_{k + 1}} \leq C ∣ δ ∣$ for $k < j - 1$ : the coefficient change in $L$ contributes $Δ Γ$ of weight $η_{0}$ times $U_{k}$ of weight $η_{k}$ , and each forcing difference changes either a coefficient $D^{m} N$ (controlled by bounded $D^{m + 1} N$ through componentwise [F20]) or a lower $U$ factor. The strict partition inequality in step 5.1 bounds these products in $X_{k + 1}$ . Consequently the displayed right side is $O (∣ δ ∣)$ in $X_{j}$ , since $η_{0} + η_{j - 1} < η_{j}$ and every forcing product has at least two positive-order factors; hence $Δ U_{j - 1} / δ$ is bounded in $X_{j}$ .

8.1F2F3F4F5F7F14F20F21F23step 1.2step 3.1step 4.1step 5.1step 6.1step 7.1algebra

Expand the coefficient and factor differences in step 7.1. Componentwise [F20] gives the first-order coefficient terms, the induction gives the compact-interval limits of lower difference quotients, and the labelled-direction identity of step 6.1 collects the limits into exactly the partition forcing defining $U_{j}$ in step 5.1. On the tails, every divided coefficient term has growth exponent at most $η_{0} + η_{j - 1} < η_{j}$ , and every divided lower-factor term has exponent a sum $\sum_{i} η_{k_{i}} < η_{j}$ over a partition with at least two blocks. Thus the residual after subtracting the defining equation for $U_{j}$ is bounded uniformly by $C e^{σ ∣ t ∣}$ for some $σ < η_{j}$ , and its $X_{j}$ tail beyond $T$ is at most $C e^{- (η_{j} - σ) T}$ . First choose $T$ large, then use compact-interval convergence to send $δ$ to zero. The residual tends to zero in $X_{j}$ , and $∥ (I - L_{ξ})^{- 1} ∥_{X_{j} \to X_{j}} \leq (1 - κ_{j})^{- 1}$ proves $D_{ξ} U_{j - 1} = U_{j}$ for every $j \leq 5$ .

9.1F2F3F4F5F7F14step 1.2step 3.1step 4.1step 5.1step 6.2step 7.1step 8.1algebra

Subtract the recursion equations without division. For $j < 5$ , coefficient changes are controlled by bounded $D^{m + 1} N$ and lower-factor changes by steps 6.2–8.1; each product has total derivative order at most $j$ , so its weight exponent is below $η_{j + 1}$ and $U_{j} (ξ + δ v) \to U_{j} (ξ)$ in $X_{j + 1}$ . For $j = 5$ , $D^{5} N$ is uniformly continuous because it is continuous with compact support; split into a bounded time interval and tails, where products have exponent below $η_{5} < η_{6}$ , to obtain continuity in $X_{6}$ . Evaluation at $t = 0$ is continuous on every $X_{j}$ , so $h (ξ) = Γ_{ξ} (0)_{h}$ is $C^{5}$ . All fixed points are unique; no Banach implicit-function or choice theorem is used.

10.1F4F7step 4.1step 5.1step 6.2step 9.1givenalgebra

Define $h (ξ)$ to be the hyperbolic component of $Γ_{ξ} (0)$ . Step 9.1 makes $h$ $C^{5}$ . For each small $λ$ , the constant extended trajectory $(x (t), λ (t)) = (0, λ)$ solves the cut-off equation because $f (0, λ) = 0$ ; it obeys the integral equations with center value $(0, λ)$ , so uniqueness in step 4.1 gives $h (0, λ) = 0$ . At the origin, $D N (0) = 0$ , and the parameter derivative $E_{c} v$ has zero hyperbolic component, so the equation for $U_{1}$ gives $D_{z} h (0, 0) = 0$ . If a fixed trajectory is shifted a sufficiently small time, the shifted trajectory still lies in the weighted space and solves the same integral equations with its new center value. Uniqueness in step 4.1 therefore makes the graph locally invariant. Differentiating that invariance relation using [F7] gives the displayed invariance equation.

11.1F10F20step 1.1step 3.1step 4.1step 10.1algebra

Since $h (0, λ) = 0$ , componentwise [F20] along $s \mapsto h (s z, λ)$ gives $h (z, λ) = \int_{0}^{1} D_{z} h (s z, λ) z d s$ . Bounded $D^{2} h$ on a smaller convex neighborhood and [F10] applied componentwise to $D_{z} h$ give $∥ D_{z} h (s z, λ) - D_{z} h (0, 0) ∥ \leq C (s ∥ z ∥ + ∣ λ ∣)$ ; since $D_{z} h (0, 0) = 0$ , integrating yields $h (z, λ) = O (∥ z ∥^{2} + ∣ λ ∣ ∥ z ∥)$ . If a periodic trajectory remains in the smaller neighborhood for all real time, its center component and its stable and unstable components are bounded. Letting the initial time tend to $- \infty$ in the stable variation formula and to $+ \infty$ in the unstable formula removes the homogeneous terms by the exponential bounds of step 1.1. The trajectory then satisfies the fixed-point equations of step 3.1 and, by uniqueness, lies on the graph.

12.1F12F13step 9.1step 10.1givenalgebra∎

Put $X (z, λ) = z + h (z, λ)$ and $g (z, λ) = f_{c} (z, h (z, λ), λ)$ . Differentiating the invariance equation at $z = 0$ gives $D_{z} X (0, λ) D_{z} g (0, λ) = A_{λ} D_{z} X (0, λ)$ , since $g (0, λ) = 0$ . The derivative $D_{z} X (0, 0)$ is the identity on $E_{c}$ , so it remains injective for small $λ$ ; its range is therefore a two-dimensional invariant subspace. Choose pairwise disjoint disks covering the finite spectrum of $A_{0}$ , with separate critical disks around $\pm i ω$ . These two disks cover the spectrum of $D_{z} g (0, 0)$ as well. Since $D_{z} g (0, λ) \to D_{z} g (0, 0)$ and $A_{λ} \to A_{0}$ , [F13] gives the same root counts in these disks for all sufficiently small $λ$ ; otherwise a violating sequence $λ_{n} \to 0$ would contradict [F13]. Thus $D_{z} g (0, λ)$ has one eigenvalue near each critical value. The restriction of $A_{λ}$ to the invariant range is conjugate to $D_{z} g (0, λ)$ , hence has that pair. Applying [F13] to $A_{λ}$ shows its full spectrum has exactly one eigenvalue in each critical disk; because $A_{λ}$ is real the roots are conjugates, and [F12] identifies them as $ζ (λ)$ and $\overline{ζ (λ)}$ . Thus the invariant plane is their span, as asserted.

Remarks

The cutoff is only a local construction device; all conclusions are restricted to the ball where it equals one. The proof uses unique Banach fixed points and finite-dimensional spectral decompositions, not arbitrary-index choice.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passOpen item page →

The first Lyapunov coefficient is the frequency-normalized radial cubic Hopf coefficient

Statement

Assume $f$ is $C^{5}$ near $(0, 0)$ and its Hopf data satisfy Hopf spectral and multilinear normal-form data. Since $A = D_{x} f (0, 0)$ has no zero eigenvalue, let $ξ (λ)$ be the unique local $C^{5}$ equilibrium branch with $ξ (0) = 0$ supplied by the parameterized implicit-function theorem, and set $A_{λ} : = D_{x} f (ξ (λ), λ)$ . This matrix path is $C^{4}$ . Let $ζ (λ) = β (λ) + i ω (λ)$ be its $C^{4}$ simple critical eigenvalue branch, with $β (0) = 0$ , $ω (0) = ω_{0}$ , and $β^{'} (0) \neq 0$ . After translating by $ξ (λ)$ , restricting to the parameterized center manifold of A parameterized C5 center manifold exists at a simple Hopf spectral split, and making a near-identity complex coordinate change, the reduced equation has the form

$\dot{z} = (β + i ω (β)) z + \frac{1}{2} G_{21} z ∣ z ∣^{2} + R (z, \overset{ˉ}{z}, β), R = O (∣ z ∣^{4} + ∣ β ∣ ∣ z ∣^{3}) .$

Thus its radial cubic coefficient at $β = 0$ is $Re (G_{21}) / 2 = ω_{0} ℓ_{1}$ , where $ℓ_{1}$ is the first Lyapunov coefficient defined in Hopf spectral and multilinear normal-form data. The remainder and its first derivative satisfy the corresponding bounds $D_{z} R = O (∣ z ∣^{3} + ∣ β ∣ ∣ z ∣^{2})$ .

Facts & Assumptions

Given: The vector field, simple critical eigenpair, normalization, derivatives $A, B, C$ , and parameter crossing in the Statement.

[F1]

Hopf spectral and multilinear normal-form data: $A q = i ω_{0} q$ , $A^{*} p = - i ω_{0} p$ , $q^{*} q = p^{*} q = 1$ , and $G_{21} = p^{*} ⁣ (C (q, q, \overset{ˉ}{q}) - 2 B (q, A^{- 1} B (q, \overset{ˉ}{q})) + B (\overset{ˉ}{q}, (2 i ω_{0} I - A)^{- 1} B (q, q))), ℓ_{1} = Re G_{21} / (2 ω_{0}) .$

[F2]

A parameterized C5 center manifold exists at a simple Hopf spectral split: the extended parameter system has a $C^{5}$ locally invariant center graph whose tangent plane at each parameter is the continued critical eigenspace; every sufficiently small periodic trajectory in the neighborhood lies on it.

[F3]

The parametrized implicit function theorem with $C^{k}$ regularity: an invertible derivative in the solved variables gives a unique smooth local implicit branch.

[F4]

A simple eigenpair has a regularity-matched gauge-fixed parameter branch: the simple critical eigenvalue and normalized left and right eigenvectors have the regularity of the matrix path, with $λ_{c}^{'} (0) = p^{*} A^{'} (0) q$ ; here they are $C^{4}$ because $f$ is $C^{5}$ .

[F5]

The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ : derivatives of the center-graph composition are computed by the chain rule.

Proof

Given: The data and hypotheses in the Statement.

1.1F3F4givenalgebra

Because $A$ has no zero eigenvalue, $D_{x} f (0, 0) = A$ is invertible. Apply [F3] to $f (x, λ) = 0$ to obtain the local $C^{5}$ equilibrium branch $ξ (λ)$ ; translate $x$ by $ξ (λ)$ , so the translated field vanishes at $x = 0$ for each small $λ$ . Its Jacobian path is $C^{4}$ . By [F4] the critical eigenpair is $C^{4}$ in $λ$ and $β^{'} (0) = Re (p^{*} A^{'} (0) q) \neq 0$ . Apply [F3] to $Re ζ (λ) - \hat{β} = 0$ in solved variable $λ$ ; its derivative is nonzero, so $\hat{β}$ is a valid local parameter, which we relabel $β$ .

1.2F1F2F5givenalgebra

At $β = 0$ , parameterize the center graph by $u = p^{*} x$ . From $p^{*} A = i ω_{0} p^{*}$ and $A \overset{ˉ}{q} = - i ω_{0} \overset{ˉ}{q}$ we get $2 i ω_{0} p^{*} \overset{ˉ}{q} = 0$ , hence $p^{*} \overset{ˉ}{q} = 0$ ; also $p^{*} q = 1$ . Its embedding is $H_{0} (u, \overset{ˉ}{u}) = u q + \overset{ˉ}{u} \overset{ˉ}{q} + h (u, \overset{ˉ}{u})$ with $h$ in the hyperbolic complement. Its reduced equation is $\dot{u} = i ω_{0} u + g_{2} (u, \overset{ˉ}{u}) + g_{3} (u, \overset{ˉ}{u}) + O (∣ u ∣^{4})$ , where $g_{j}$ is homogeneous of degree $j$ . The graph and reduced equation have the required derivatives by [F2] and the chain rule [F5].

2.1F2F3step 1.2algebra

Make a quadratic coordinate change $u = w + \sum_{j + k = 2} c_{j k} w^{j} {\overset{ˉ}{w}}^{k}$ . Along the linear flow, $D (w^{j} {\overset{ˉ}{w}}^{k}) (i ω_{0} w, - i ω_{0} \overset{ˉ}{w}) = (j - k) i ω_{0} w^{j} {\overset{ˉ}{w}}^{k}$ ; substitution therefore changes that coefficient by $- (j - k - 1) i ω_{0} c_{j k}$ . This divisor is nonzero for every $j + k = 2$ , so choose $c_{j k}$ to remove all quadratic terms. Use conjugate corrections in the conjugate equation to preserve the real system. A cubic change with the same divisor removes every cubic term except $(j, k) = (2, 1)$ , whose divisor is zero. These changes are local diffeomorphisms because their derivative at zero is the identity; [F3] applies to their inverse equations. The resulting equation is $\dot{w} = i ω_{0} w + \frac{1}{2} G_{21} w^{2} \overset{ˉ}{w} + O (∣ w ∣^{4})$ . Composing the graph embedding with the changes gives a full-space center-manifold parameterization $H (w, \overset{ˉ}{w})$ .

3.1F1F2F5step 2.1givenalgebra

Write $H (w, \overset{ˉ}{w}) = w q + \overset{ˉ}{w} \overset{ˉ}{q} + \frac{1}{2} h_{20} w^{2} + h_{11} w \overset{ˉ}{w} + \frac{1}{2} h_{02} {\overset{ˉ}{w}}^{2} + H_{3} (w, \overset{ˉ}{w}) + O (∣ w ∣^{4})$ , where $H_{3}$ is homogeneous cubic. The invariance equation is $D H \dot{w} = f (H)$ . With $f (x, 0) = A x + \frac{1}{2} B (x, x) + \frac{1}{6} C (x, x, x) + O (∥ x ∥^{4})$ and no quadratic terms in $\dot{w}$ , comparison of degree-two coefficients gives $(2 i ω_{0} I - A) h_{20} = B (q, q)$ and $A h_{11} = - B (q, \overset{ˉ}{q})$ . Zero and $2 i ω_{0}$ are not eigenvalues of $A$ : its only imaginary-axis eigenvalues are $\pm i ω_{0}$ . Thus both operators are invertible and $h_{20} = (2 i ω_{0} I - A)^{- 1} B (q, q)$ , $h_{11} = - A^{- 1} B (q, \overset{ˉ}{q})$ .

4.1F1F2step 3.1algebra

Let $h_{21}$ be the coefficient of $w^{2} \overset{ˉ}{w}$ in $H_{3}$ . Comparing that monomial in $D H \dot{w} = f (H)$ gives $(i ω_{0} I - A) h_{21} + \frac{1}{2} q G_{21} = \frac{1}{2} C (q, q, \overset{ˉ}{q}) + B (q, h_{11}) + \frac{1}{2} B (\overset{ˉ}{q}, h_{20})$ . The derivative term on the left has factor $i ω_{0}$ because $w^{2} \overset{ˉ}{w}$ evolves with linear frequency $(2 - 1) i ω_{0}$ . Left multiplication by $p^{*}$ annihilates $(i ω_{0} I - A) h_{21}$ and uses $p^{*} q = 1$ , yielding $G_{21} = p^{*} ⁣ (C (q, q, \overset{ˉ}{q}) + 2 B (q, h_{11}) + B (\overset{ˉ}{q}, h_{20}))$ . Substituting step 3.1's formulas gives exactly the expression in [F1].

5.1F2F4F5step 4.1givenalgebra

By [F2], the tangent plane of the graph is spanned by $q (β), \overset{ˉ}{q} (β)$ from [F4]. The coordinate $z = p (β)^{*} x$ is valid there because $p (β)^{*} q (β) = 1$ and $p (β)^{*} \overset{ˉ}{q} (β) = 0$ ; the latter follows from $p^{*} A = ζ p^{*}$ , $A \overset{ˉ}{q} = \overset{ˉ}{ζ} \overset{ˉ}{q}$ , and $ζ \neq \overset{ˉ}{ζ}$ . Hence the linear center equation is exactly $\dot{z} = (β + i ω (β)) z$ . The center graph is $C^{5}$ and the normalized left and right eigenpair are $C^{4}$ in the parameter. The coordinate changes are obtained by solving finite-dimensional homological equations whose divisors stay nonzero for small $β$ , so their coefficients have at least $C^{2}$ parameter dependence. The resonant coefficient is $G_{21} + O (∣ β ∣)$ ; its change contributes $O (∣ β ∣ ∣ z ∣^{3})$ and its $z$ -derivative contributes $O (∣ β ∣ ∣ z ∣^{2})$ . Taylor's theorem for the $C^{5}$ reduced vector field gives an $O (∣ z ∣^{4})$ remainder with derivative $O (∣ z ∣^{3})$ . Combining these terms yields $R = O (∣ z ∣^{4} + ∣ β ∣ ∣ z ∣^{3})$ and $D_{z} R = O (∣ z ∣^{3} + ∣ β ∣ ∣ z ∣^{2})$ .

6.1F1step 5.1algebra∎

Finally $Re (G_{21} / 2) = ω_{0} ℓ_{1}$ by [F1]. Thus the real radial cubic coefficient is the stated value; step 5.1 establishes the normal form and its bounds.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passOpen item page →

Scalar fold, transcritical, and symmetric pitchfork equilibrium branches

Statement

Let $F (x, λ)$ be a real $C^{5}$ scalar function near $(0, 0)$ , with equilibria defined by $F (x, λ) = 0$ .

A fold occurs if $F (0, 0) = F_{x} (0, 0) = 0$ and $F_{λ} (0, 0) F_{x x} (0, 0) \neq 0$ . Its local equilibrium set is a unique curve $λ = ϕ (x)$ with $ϕ^{'} (0) = 0, ϕ^{''} (0) = - \frac{F_{x x} (0, 0)}{F_{λ} (0, 0)} \neq 0.$ For $λ$ sufficiently close to zero, there are exactly two nearby equilibria on the side where $λ ϕ^{''} (0) > 0$ , one at $λ = 0$ , and none on the opposite side.
A transcritical bifurcation occurs if $F (0, λ) = 0$ for all small $λ$ , $F_{x} (0, 0) = 0$ , and $F_{x λ} (0, 0) F_{x x} (0, 0) \neq 0$ . The local equilibria are exactly the trivial branch $x = 0$ and a second branch $x = ψ (λ)$ with $ψ (0) = 0, ψ^{'} (0) = - \frac{2 F_{x λ} (0, 0)}{F_{x x} (0, 0)} \neq 0.$ The two branches cross transversely.
A pitchfork bifurcation occurs if $F (- x, λ) = - F (x, λ)$ for all nearby $(x, λ)$ , $F_{x} (0, 0) = F_{x x} (0, 0) = 0$ , and $F_{x λ} (0, 0) F_{x x x} (0, 0) \neq 0$ . The trivial equilibrium $x = 0$ persists. A pair of nontrivial equilibria $x = \pm r (λ)$ exists on exactly the side where $λ ϕ^{''} (0) > 0$ , with $ϕ^{''} (0) = - \frac{F_{x x x} (0, 0)}{3 F_{x λ} (0, 0)} \neq 0,$ and there are no nontrivial equilibria on the opposite side.

Facts & Assumptions

Given: A scalar $C^{5}$ function $F$ and the relevant hypotheses in the Statement.

[F1]

The parametrized implicit function theorem with $C^{k}$ regularity: for a $C^{k}$ scalar equation with $k \geq 1$ , a nonzero derivative in the solved scalar variable gives a unique local $C^{k}$ solution branch containing every nearby zero.

[F2]

A simple fold has a unique local Lyapunov–Schmidt chart and nonzero parameter curvature: in the scalar case $n = 1$ , if $F = F_{x} = 0$ , $F_{λ} \neq 0$ , and $F_{x x} \neq 0$ , there is a unique local $C^{3}$ solution curve $(x (s), λ (s))$ with $x^{'} (0) = 1$ , $λ^{'} (0) = 0$ , and $λ^{''} (0) = - F_{x x} / F_{λ}$ .

[F3]

Newton–Leibniz needs only continuity on $[a, b]$ , differentiability on $(a, b)$ , and a Riemann-integrable extension of the interior derivative: for $C^{1}$ scalar $g$ , $g (x) - g (0) = \int_{0}^{x} g^{'} (s) d s$ .

[F4]

The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ : derivatives of compositions are computed by the chain rule.

[F5]

Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on $[a, b]$ takes every value between $f (a)$ and $f (b)$ : a continuous real function on a closed interval attains every value between its endpoint values.

Proof

Given: $F$ and the hypotheses for the case being proved.

1.1F2given

In the fold case choose $n = 1$ , $v = w = 1$ in [F2]. Its hypotheses are exactly $F (0, 0) = F_{x} (0, 0) = 0$ and $F_{λ} F_{x x} \neq 0$ . Thus all nearby equilibria lie on a unique curve $λ = ϕ (x)$ with the stated first and second derivatives.

1.2F3givenconstruct

For the transcritical and pitchfork cases define $G (x, λ) : = \int_{0}^{1} F_{x} (t x, λ) d t$ . Because $F (0, λ) = 0$ in both cases, [F3] and the change of variable $s = t x$ give $F (x, λ) = x G (x, λ)$ . Since $F \in C^{5}$ , the derivatives of $F_{x} (t x, λ)$ through order four are continuous jointly in $(t, x, λ)$ ; on compact parameter neighborhoods their difference quotients converge uniformly in $t \in [0, 1]$ , so they may be integrated termwise. Thus $G \in C^{4}$ , with $G_{x} = \int_{0}^{1} t F_{x x} (t x, λ) d t$ , $G_{λ} = \int_{0}^{1} F_{x λ} (t x, λ) d t$ , and $G_{x x} = \int_{0}^{1} t^{2} F_{x x x} (t x, λ) d t$ .

2.1F2F3F5step 1.1givenalgebra

In the fold case, since $ϕ^{''} (0) \neq 0$ and $ϕ^{''}$ is continuous, shrink $δ > 0$ so $ϕ^{''}$ has the constant sign of $c : = ϕ^{''} (0)$ on $[- δ, δ]$ . By [F3], $ϕ^{'} (x) = \int_{0}^{x} ϕ^{''} (s) d s$ , so $ϕ^{'} (x)$ has the sign of $c x$ ; hence $ϕ$ is strictly monotone on each half-interval. Also $ϕ (x) = \int_{0}^{x} ϕ^{'} (s) d s$ has the sign of $c$ for every $x \neq 0$ . Thus $ϕ (- δ)$ and $ϕ (δ)$ are nonzero and have sign $c$ . Every sufficiently small nonzero level with $λ c > 0$ lies strictly between zero and each endpoint value, so [F5] and strict monotonicity give exactly one solution on each half-interval; no level of the opposite sign is attained.

2.2F1F4step 1.2givenalgebra

In the transcritical case, the derivative formulas from step 1.2 give $G (0, 0) = F_{x} (0, 0) = 0$ , $G_{x} (0, 0) = F_{x x} (0, 0) / 2 \neq 0$ , and $G_{λ} (0, 0) = F_{x λ} (0, 0) \neq 0$ . Apply [F1] with $k = 4$ , solving $G = 0$ for $x = ψ (λ)$ ; differentiating gives $ψ^{'} (0) = - G_{λ} / G_{x} = - 2 F_{x λ} / F_{x x}$ . Since $F = x G$ , every nearby zero lies on at least one of the branches $x = 0$ or $x = ψ (λ)$ ; at their common point $(0, 0)$ they coincide, and elsewhere sufficiently near zero they are distinct. Their distinct tangent slopes make them transverse.

2.3F1F4step 1.2givenalgebra

In the pitchfork case, oddness of $F$ makes $G$ even in $x$ . The derivative formulas from step 1.2 give $G (0, 0) = 0$ , $G_{x} (0, 0) = 0$ , $G_{λ} (0, 0) = F_{x λ} (0, 0) \neq 0$ , and $G_{x x} (0, 0) = F_{x x x} (0, 0) / 3 \neq 0$ . By [F1] with $k = 4$ , $G = 0$ is a unique local curve $λ = ϕ (x)$ , with $ϕ^{'} (0) = 0$ and $ϕ^{''} (0) = - G_{x x} / G_{λ} = - F_{x x x} / (3 F_{x λ})$ . Evenness of $G$ and uniqueness imply $ϕ (- x) = ϕ (x)$ .

3.1step 2.3givenalgebra∎

Shrink the interval so $ϕ^{''}$ has the sign of $ϕ^{''} (0)$ . Then $ϕ$ is strictly monotone for $x > 0$ , and by evenness it has exactly one positive and one negative solution of $ϕ (x) = λ$ on the side $λ ϕ^{''} (0) > 0$ , and no nonzero solution on the other side. Since $F = x G$ , these are exactly the two nontrivial equilibria in addition to the persistent branch $x = 0$ .

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passOpen item page →

A simple nondegenerate Hopf point creates a local periodic branch

Statement

Let $f (x, λ)$ be a real $C^{5}$ vector field near an equilibrium $(x_{0}, 0)$ in $R^{d} \times R$ . Put $A_{0} = D_{x} f (x_{0}, 0)$ . Assume:

$A_{0}$ has a simple pair $\pm i ω_{0}$ , $ω_{0} > 0$ ;
every other eigenvalue $ν_{j}$ of $A_{0}$ has $Re ν_{j} \neq 0$ ;
by the parameterized implicit-function theorem, $ξ (λ)$ is the unique local equilibrium branch through $x_{0}$ and $A_{λ} : = D_{x} f (ξ (λ), λ)$ is a $C^{4}$ matrix path; for its $C^{4}$ simple critical eigenvalue branch $ζ (λ) = β (λ) + i ω (λ)$ , $β (0) = 0$ and $β^{'} (0) \neq 0$ ;
the first Lyapunov coefficient $ℓ_{1}$ in Hopf spectral and multilinear normal-form data is nonzero.

There is a local branch of nonconstant periodic orbits, unique up to phase on a fixed local Poincare section. Writing $r > 0$ for amplitude in the normal-form center coordinate and $β$ for the real part of the critical eigenvalue, its period and parameter satisfy

$r^{2} = - \frac{β}{ω_{0} ℓ_{1}} + O (∣ β ∣^{3 / 2}), T = \frac{2 π}{ω_{0}} + O (∣ β ∣) .$

Thus the branch exists precisely on the side $β ℓ_{1} < 0$ ; there are no sufficiently small nonconstant periodic orbits on the opposite side. Its phase Floquet multiplier is $1$ , its radial multiplier is

$μ_{r a d} = 1 - \frac{4 π}{ω_{0}} β + O (∣ β ∣^{3 / 2}),$

and the other Floquet multipliers converge, with algebraic multiplicity, to $e^{2 π ν_{j} / ω_{0}}$ . If any $Re ν_{j} > 0$ , the periodic orbit is unstable. If all $Re ν_{j} < 0$ , the orbit is orbitally asymptotically stable for $β > 0$ and unstable for $β < 0$ . These are local conclusions only; no global branch completeness or global dynamics is asserted.

Facts & Assumptions

Given: $f$ , $(x_{0}, 0)$ , $A_{0}$ , $ω_{0}$ , the critical eigenvalue branch, $β^{'} (0)$ , and $ℓ_{1}$ as in the Statement.

[F1]

The parametrized implicit function theorem with $C^{k}$ regularity: since $D_{x} f (x_{0}, 0) = A_{0}$ is invertible, the equilibrium equation has a unique local $C^{5}$ branch $x = ξ (λ)$ ; applying the same theorem with $k = 4$ to the $C^{4}$ critical eigenvalue path gives its local parameter inverse.

[F2]

A simple eigenpair has a regularity-matched gauge-fixed parameter branch: the simple critical eigenvalue and normalized left and right eigenvectors have the regularity of the matrix path; here the path is $C^{4}$ because $f$ is $C^{5}$ , with $ζ (λ) = β (λ) + i ω (λ)$ and $β^{'} (0) = Re (p^{*} A^{'} (0) q)$ .

[F3]

A parameterized C5 center manifold exists at a simple Hopf spectral split: after adjoining $\dot{λ} = 0$ , there is a $C^{5}$ invariant center graph with the stated invariance equation, and every sufficiently small periodic orbit in the neighborhood lies on it.

[F4]

The first Lyapunov coefficient is the frequency-normalized radial cubic Hopf coefficient: on that graph, a near-identity coordinate change with at least $C^{2}$ parameter dependence gives $\dot{z} = (β + i ω (β)) z + \frac{1}{2} G_{21} z ∣ z ∣^{2} + R, Re (G_{21} / 2) = ω_{0} ℓ_{1}, R = O (∣ z ∣^{4} + ∣ β ∣ ∣ z ∣^{3}), D_{z} R = O (∣ z ∣^{3} + ∣ β ∣ ∣ z ∣^{2}) .$

[F5]

Characteristic roots preserve separated cluster counts under matrix perturbation: under a small matrix perturbation, characteristic roots remain in the same separated neighborhoods with the same algebraic multiplicities.

[F6]

C¹ Euclidean maximal flows, variational dependence and the finite C² upgrade: a $C^{1}$ autonomous vector field has a jointly $C^{1}$ local flow, unique trajectories, and a continuous first state derivative satisfying its variational equation. For the $C^{1}$ nonautonomous radial equation on $r > 0$ , adjoining $θ^{'} = 1$ and $β^{'} = 0$ gives the same joint $C^{1}$ dependence on radius and parameter; no fifth derivative of a flow is used.

[F7]

Local periodic-orbit, Poincare-return, and Floquet data: the monodromy matrix gives the Floquet multipliers, and a local transverse section defines its return map.

[F8]

Hyperbolic return-map stability is orbital stability: a hyperbolic Poincare return map with all multipliers inside the unit circle gives an orbitally asymptotically stable periodic orbit; a multiplier outside gives orbital instability.

[F9]

Proof

Given: The hypotheses and facts above.

1.1F1F2givenalgebra

Because $\pm i ω_{0}$ and every other eigenvalue of $A_{0}$ are nonzero, $A_{0}$ is invertible. First set $y = x - x_{0}$ and $\hat{f} (y, λ) = f (x_{0} + y, λ)$ , so $\hat{f} (0, 0) = 0$ . The data in Hopf spectral and multilinear normal-form data are those of this field: $A = A_{0}$ , $B = D_{x}^{2} f (x_{0}, 0)$ , $C = D_{x}^{3} f (x_{0}, 0)$ , and $p, q$ are eigenvectors of this same $A_{0}$ with both declared normalizations. Apply [F1] to obtain the unique nearby equilibrium $ξ (λ)$ of the original field. In the parameter-dependent translated state $v = x - ξ (λ)$ , the field is $f (v + ξ (λ), λ)$ and vanishes at $v = 0$ for each fixed parameter; its critical spatial jets agree with the preceding data, since $ξ (0) = x_{0}$ and $\dot{λ} = 0$ . Apply [F2] to obtain $ζ (λ)$ with $β^{'} (0) \neq 0$ , and apply [F1] to $Re ζ (λ) - \hat{β} = 0$ in solved variable $λ$ . This makes $\hat{β}$ a valid local parameter, which we relabel $β$ .

1.2F3F4givenalgebra

By [F3], every sufficiently small periodic orbit is on the parameterized center graph. Restricting to a fixed parameter and using [F4], its reduced dynamics have $\dot{r} = r (β + ω_{0} ℓ_{1} r^{2}) + O (r^{4} + ∣ β ∣ r^{3})$ and $\dot{θ} = ω_{0} + O (∣ β ∣ + r^{2})$ , with the first-derivative bounds supplied by [F4]. In particular $\dot{θ} > 0$ after shrinking the neighborhood.

2.1step 1.2F4F6algebra

Reparameterize by the strictly increasing angle from step 1.2 and write $d r / d θ = ρ (r, θ, β) : = \dot{r} / \dot{θ}$ . The bounds in [F4] give uniformly in $θ$ that $ρ = (r / ω_{0}) (β + ω_{0} ℓ_{1} r^{2}) + O (β^{2} r + ∣ β ∣ r^{3} + r^{4})$ and $\partial_{r} ρ = (β + 3 ω_{0} ℓ_{1} r^{2}) / ω_{0} + O (β^{2} + ∣ β ∣ r^{2} + r^{3})$ . On $r > 0$ the radial field is jointly $C^{1}$ in $(θ, r, β)$ by the finite-regularity coordinate construction in [F4]. Applying [F6] to $(θ, r, β)^{'} = (1, ρ (θ, r, β), 0)$ gives the required common local solution and first variations, with finite composition over $[0, 2 π]$ . For small $r_{0} > 0$ and $∣ β ∣$ , while $r \in [r_{0} / 2, 2 r_{0}]$ the bound $∣ ρ / r ∣ \leq C (∣ β ∣ + 4 r_{0}^{2})$ makes the change in $\log r$ over $[0, 2 π]$ smaller than $\log 2$ . Thus no first exit from that interval occurs; compact continuation in [F6] supplies the full angular interval and positivity, and $\partial_{θ} \log r = ρ / r = O (∣ β ∣ + r^{2})$ ; integrating over the bounded interval $[0, 2 π]$ gives $r (θ; r_{0}) = r_{0} + O (∣ β ∣ r_{0} + r_{0}^{3})$ . Substituting this bound into $P_{β} (r_{0}) - r_{0} = \int_{0}^{2 π} ρ (r (θ; r_{0}), θ, β) d θ$ gives $P_{β} (r_{0}) - r_{0} = \frac{2 π}{ω_{0}} r_{0} (β + ω_{0} ℓ_{1} r_{0}^{2}) + O (β^{2} r_{0} + ∣ β ∣ r_{0}^{3} + r_{0}^{4})$ . The variational derivative $Q = \partial r / \partial r_{0}$ solves $\partial_{θ} Q = (\partial_{r} ρ) Q$ , $Q (0) = 1$ , so $Q (2 π) = \exp (\int_{0}^{2 π} \partial_{r} ρ d θ)$ . The same bound on $r (θ; r_{0})$ in the derivative expansion yields $P_{β}^{'} (r_{0}) = 1 + \frac{2 π}{ω_{0}} (β + 3 ω_{0} ℓ_{1} r_{0}^{2}) + O (β^{2} + ∣ β ∣ r_{0}^{2} + r_{0}^{3})$ . The factor $r_{0}$ is the persistent equilibrium.

3.1F1F9step 2.1givenalgebra

For $r > 0$ , divide step 2.1 by $(2 π / ω_{0}) r$ and call the result $H (r, β)$ . Then $H (r, β) = β + ω_{0} ℓ_{1} r^{2} + O (β^{2} + ∣ β ∣ r^{2} + r^{3})$ . Differentiating this quotient using both expansions in step 2.1 gives $\partial_{r} H (r, β) = 2 ω_{0} ℓ_{1} r + O (β^{2} / r + ∣ β ∣ r + r^{2})$ . If $β ℓ_{1} > 0$ , then $∣ β + ω_{0} ℓ_{1} r^{2} ∣ = ∣ β ∣ + ω_{0} ∣ ℓ_{1} ∣ r^{2}$ ; the error is bounded by $C (β^{2} + ∣ β ∣ r^{2} + r^{3})$ , which is at most an arbitrarily small multiple of $∣ β ∣ + r^{2}$ after shrinking $r, ∣ β ∣$ . Thus there is no positive root. If $β = 0$ , then $H (r, 0) = ω_{0} ℓ_{1} r^{2} + O (r^{3})$ , whose leading term dominates for all sufficiently small $r > 0$ , so there is no nonconstant periodic orbit at the threshold either. If $β ℓ_{1} < 0$ , choose $0 < c_{-} < 1 / \sqrt{ω_{0} ∣ ℓ_{1} ∣} < c_{+}$ . At $r = c_{-} \sqrt{∣ β ∣}$ and $r = c_{+} \sqrt{∣ β ∣}$ the leading terms have opposite signs and the error is $O (∣ β ∣^{3 / 2})$ , so [F9] gives a root between them. Every root lies between fixed such multiples of $\sqrt{∣ β ∣}$ : below a sufficiently small multiple, $∣ β ∣$ dominates the error; above a sufficiently large multiple, $ω_{0} ∣ ℓ_{1} ∣ r^{2}$ dominates both $∣ β ∣$ and the error. On this annulus, $β^{2} / r + ∣ β ∣ r + r^{2} = o (r)$ uniformly as $β \to 0$ , so $\partial_{r} H$ has the sign of $ℓ_{1}$ and the root is unique. Since this derivative is nonzero, [F1] with $k = 1$ makes the radius a $C^{1}$ function of $β$ on the punctured existence side, using the joint $C^{1}$ return map from [F6].

4.1F3F4F6step 3.1givenalgebra

Every sufficiently small periodic trajectory lies on the center graph by [F3], and [F4] gives $\dot{θ} > 0$ , so it meets the ray $θ = 0$ and returns after some positive integer number of turns. Reparameterize the radial equation by $θ$ ; $d r / d θ = \dot{r} / \dot{θ}$ is a $C^{1}$ scalar nonautonomous ODE on $r > 0$ , so two solutions cannot cross by uniqueness from the augmented $C^{1}$ flow [F6]. Therefore the one-turn radius map is strictly increasing. If a periodic trajectory met the section in a $k$ -cycle with $P_{β}^{k} (r) = r$ , strict increase forces $P_{β} (r) = r$ ; indeed $P_{β} (r) > r$ would imply $P_{β}^{k} (r) > r$ , and $P_{β} (r) < r$ would imply $P_{β}^{k} (r) < r$ . Thus the unique positive fixed point from step 3.1 describes the unique local periodic orbit up to phase, and none exists on the opposite side.

4.2step 1.2step 2.1step 3.1givenalgebra

At the root, step 3.1 gives $r^{2} = - β / (ω_{0} ℓ_{1}) + O (∣ β ∣^{3 / 2})$ . The angular speed in step 1.2 is $ω_{0} + O (∣ β ∣ + r^{2})$ , so the return period is $2 π / ω_{0} + O (∣ β ∣)$ . Differentiating the return map at this fixed radius yields $P_{β}^{'} (r) = 1 + \frac{2 π}{ω_{0}} (β + 3 ω_{0} ℓ_{1} r^{2}) + O (∣ β ∣^{3 / 2}) = 1 - \frac{4 π}{ω_{0}} β + O (∣ β ∣^{3 / 2})$ . Thus this nontrivial radial multiplier is inside the unit circle for $β > 0$ and outside it for $β < 0$ , when $β$ is sufficiently small.

5.1F3F5F6step 4.2givenalgebra

The full monodromy matrix along the periodic orbit converges to $e^{(2 π / ω_{0}) A_{0}}$ . Indeed its variational coefficient $D_{x} f (x (t), λ)$ converges uniformly to $A_{0}$ ; subtracting the two fundamental-matrix integral equations and iterating the resulting bound gives uniform convergence on the bounded period interval. The limiting matrix has the critical multiplier $1$ of algebraic multiplicity two, and all remaining multipliers $e^{2 π ν_{j} / ω_{0}}$ have modulus different from one. By [F5], exactly two multipliers remain near $1$ and the others converge with multiplicity to the hyperbolic multipliers. One of the two is exactly $1$ because ${\dot{x}}_{*} (t)$ solves the variational equation and is periodic; the other is the radial multiplier of step 4.2. For a section $Σ$ transverse to $v = {\dot{x}}_{*} (0)$ , differentiating $P (y) = ϕ_{τ (y)} (y)$ gives $D P = π M ∣_{T Σ}$ , where $M$ is the monodromy matrix and $π$ is projection along $v$ onto $T Σ$ . Thus $D P$ represents the induced map on the quotient by $span {v}$ , so its eigenvalues are exactly the non-phase Floquet multipliers.

6.1F7F8step 3.1step 4.1step 4.2step 5.1given∎

On the branch $β \neq 0$ , step 4.2 makes the radial multiplier different from one, and the other multipliers are off the unit circle by step 5.1. The return-map derivative has exactly the non-phase multipliers: if $v = {\dot{x}}_{*} (0)$ and $π$ projects onto the section tangent along $v$ , differentiating $P (y) = ϕ_{τ (y)} (y)$ gives $D P = π M ∣_{T Σ}$ , which represents the map induced by $M$ on the quotient by $span {v}$ . Thus the return map is hyperbolic. If all $Re ν_{j} < 0$ and $β > 0$ , every return multiplier is inside the unit circle, so [F8] gives orbital asymptotic stability. If $β < 0$ , the radial multiplier is outside; if any $Re ν_{j} > 0$ , a transverse multiplier is outside. In either case [F8] gives orbital instability. Steps 3.1–4.1 prove local existence, side, and uniqueness up to phase; the arguments use only the local center graph and return section, so assert no global completeness.

Remarks

When $β$ increases through zero, $ℓ_{1} < 0$ gives the supercritical stable branch if the transverse spectrum is stable; $ℓ_{1} > 0$ gives the subcritical unstable branch. If the transverse spectrum contains an unstable eigenvalue, the branch exists with the same side but is unstable in the full system.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passOpen item page →

A certified interval Hopf record verifies only the local Hopf hypotheses

Statement

For any admissible proof-carrying record, if Validate a proof-carrying local Hopf certificate returns certified-local-hopf, then the represented equilibrium has a simple pair $\pm i ω$ , $ω > 0$ , no other eigenvalues on the imaginary axis, nonzero critical eigenvalue crossing derivative, and nonzero first Lyapunov coefficient. Therefore A simple nondegenerate Hopf point creates a local periodic branch supplies the local periodic branch and its local stability classification on the stated side. The certificate proves no global dynamical claim.

Facts & Assumptions

Given: A proof-carrying input record satisfying the input type of Validate a proof-carrying local Hopf certificate.

[F1]

Validate a proof-carrying local Hopf certificate: a certified-local-hopf output occurs only after the exact equilibrium/root witness, the Jacobian/jet/branch-derivative/inverse witnesses tied to that root, simple-pair and multiplicity-cover evidence, positive frequency interval, and strict nonzero intervals for $β^{'}$ and $ℓ_{1}$ pass.

[F2]

A bounded residual and derivative error give a local root certificate: a record satisfying its residual, derivative, inverse, Lipschitz, and contraction inequalities contains exactly one zero in its specified ball.

[F3]

A simple nondegenerate Hopf point creates a local periodic branch: a simple imaginary pair with positive frequency, no other imaginary eigenvalues, nonzero crossing derivative, and nonzero first Lyapunov coefficient has the stated local periodic branch and stability classification.

Proof

Given: A record for which the algorithm returns certified-local-hopf.

1.1F1F2given

By [F1], the root field has either an exact zero or a root-isolation record satisfying the hypotheses of [F2]; in the latter case [F2] proves the unique represented equilibrium exists in the specified ball.

2.1F1step 1.1givenalgebra

By [F1], the accepted Jacobian and derivative data are proved to be those of the exact represented equilibrium (or the unique isolated branch), and the eigenpair and multiplicity-cover witnesses enclose its exact spectrum. Their strict conditions give a simple conjugate pair with positive frequency and put every other eigenvalue strictly off the imaginary axis. Write the represented exact point as $(x_{*}, λ_{0})$ and translate by $\hat{f} (y, μ) = f (x_{*} + y, λ_{0} + μ)$ . Its origin jets are precisely the accepted $A, B, C$ , its critical eigenpair is the accepted normalized pair, and its equilibrium-branch derivative is the accepted derivative with respect to $μ$ . This identifies the record with the base-point convention of Hopf spectral and multilinear normal-form data and the equilibrium $(x_{*}, 0)$ after parameter translation in [F3].

3.1F1step 2.1givenalgebra

The exact values $β^{'}$ and $ℓ_{1}$ lie in their certified intervals by the input-witness condition. Since the algorithm accepts only intervals disjoint from zero, both exact values are nonzero. The eigenvalue branch derivative is the one in A simple eigenpair has a regularity-matched gauge-fixed parameter branch, and the coefficient is the normalization in Hopf spectral and multilinear normal-form data.

4.1F3step 1.1step 2.1step 3.1given∎

Steps 1.1–2.1 establish every hypothesis of [F3]. Applying [F3] gives the local branch, its parameter side, and the stated local Floquet classification. None of these local hypotheses or conclusions asserts a global orbit or a global continuation trace, so the certificate carries no such implication.

5 · Examples, counterexamples and false statements

None yet.

Local bifurcation normal forms and numerical certificates

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

Hopf spectral and multilinear normal-form data

Definition

Weighted trajectory space for a local center-manifold construction

Definition

Characteristic roots preserve separated cluster counts under matrix perturbation

Statement

Facts & Assumptions

Proof

A simple eigenpair has a regularity-matched gauge-fixed parameter branch

Statement

Facts & Assumptions

Proof

Local periodic-orbit, Poincare-return, and Floquet data

Definition

A hyperbolic fixed point of a local map is stable exactly when all multipliers contract

Statement

Facts & Assumptions

Proof

The weighted trajectory space is complete

Statement

Facts & Assumptions

Proof

Remarks

Validate a proof-carrying local Hopf certificate

Definition

Remarks

Hyperbolic return-map stability is orbital stability

Statement

Facts & Assumptions

Proof

A parameterized C5 center manifold exists at a simple Hopf spectral split

Statement

Facts & Assumptions

Proof

Remarks

The first Lyapunov coefficient is the frequency-normalized radial cubic Hopf coefficient

Statement

Facts & Assumptions

Proof

Scalar fold, transcritical, and symmetric pitchfork equilibrium branches

Statement

Facts & Assumptions

Proof

A simple nondegenerate Hopf point creates a local periodic branch

Statement

Facts & Assumptions

Proof

Remarks

A certified interval Hopf record verifies only the local Hopf hypotheses

Statement

Facts & Assumptions

Proof

5 · Examples, counterexamples and false statements

Sources