Scalar Pitchfork Lean 4 library · release v0.1.0
Menu

Lean 4 / Mathlib library · release v0.1.0 · Apache-2.0

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.

What is proved All Lean statements Get started

Not proved here.

  • No Crandall–Rabinowitz theorem and no center-manifold reduction: the scalar normal form $\alpha\tau z-\beta z^3+R$ is the starting point, not derived from an operator equation.
  • No Lyapunov–Schmidt reduction.
  • No degree theory: no Leray–Schauder degree and no Rabinowitz global alternative. The global part is the topological skeleton only; the alternatives are hypotheses, not derived from degree theory.
  • No certified-root tools: no interval arithmetic or root isolation for specific polynomials.
  • No PDE: no existence, uniqueness or regularity theorem for any differential equation.

Find your way

Results

What is proved

Each result with its exact compared Lean statement.

All Lean statements

Generated page: every result, its hypotheses, receipts and the checks that ran.

Coverage table

Every coverage row, its claims, inputs and notes.

Modules

What each Lean module contains.

Use and trust

Get started

Build, verify, and depend on the library from your own Lake project.

Trust and axioms

Permitted axioms and what the comparator checks.

Acknowledgments and citation

Authors and AI disclosure, lean-pkg, the Auburn University Easley Cluster, what it builds on, related work, and how to cite.

This library was first developed for the Chemotaxis III Lean companion. Its sibling library is neumann-cosine-lean. The two libraries are independent.