Scalar Pitchfork

The scalar pitchfork $f(\tau,z)=\alpha\tau z-\beta z^3+R(\tau,z)$ with a remainder bounded by explicit weights or by jets at the origin: for small $\tau$ with $\tau\beta>0$, exactly one small zero of each sign, $|z|=\sqrt{\alpha\tau/\beta}+O(|\tau|)$, with the stability sign, lying on two branches continuous in $\tau$ when $R$ is continuous in $\tau$ (automatic under the jet hypotheses); no small nonzero zero when $\tau\beta\le0$; and the topological skeleton of global branches, with the global alternatives as hypotheses. Formalized in Lean 4 with Mathlib.

Documentation site · What is proved · Verification page · Build · Cite

What is proved

Here $f(\tau,z)=\alpha\tau z-\beta z^3+R(\tau,z)$ with parameter $\tau$ and amplitude $z$. Items 1–5 assume $\alpha>0$, $\beta\ne0$, $C\ge0$, $0<r\le1$ and the remainder bounds on the box $|\tau|,|z|\le r$:

|R(\tau,z)|\le C\big(|z|\tau^2+|z|^3|\tau|+z^4\big),\qquad
\partial_zR(\tau,z)=R_z(\tau,z)\ \text{exists},\qquad
|R_z(\tau,z)|\le C\big(\tau^2+z^2|\tau|+|z|^3\big).

"For small $\tau$" means for all $\tau$ in some neighbourhood of $0$. Items 6–12 state their own hypotheses. The results are classical bifurcation theory in quantitative form; no new mathematics is claimed.

This is the beginning of the README. Read the rest at the original. Read the full README ↗