Lean 4 / Mathlib companion · release v0.1.1
Chemotaxis III in Lean
A Lean 4 / Mathlib companion formalizing coefficient calculations, stationary estimates, compactness and conditional bifurcation deductions for Chemotaxis III.
What is proved
The library supplies finite coefficient and modal identities, classical stationary mass and regularity estimates, weak limits and spike subsequences under stated inputs, bounded-sensitivity compactness, actual weak-H2 cosine coordinates and complement splitting, and conditional local/global branch deductions. The latest additions also derive the critical modal signal response from an actual elliptic solution family and a supplied population jet, and a quadratic coefficient from conserved mass.
The scope ledger retains 47 verified scopes, 23 conditional scopes, and 3 exclusions across 73 overlapping manuscript-facing scopes. These counts are not a percentage of whole-paper correctness. The library has 1,525 indexed declarations, including definitions; compiler-generated auxiliaries are not counted as new mathematical theorems.
Not proved here: whole-paper correctness, actual stationary operator/Fredholm identification, construction/exhaustion of the local PDE branch, a center manifold with dynamical invariance, global bifurcation alternatives and correspondence, or PDE stability. Supplied families, phase-norm jets, chart/exhaustion data, critical-parameter identifications and other named inputs remain explicit where used. A geometric Fourier complement is not identification with an operator’s range or stable spectrum.
Find your way
Results
What is proved
Result families, the sign-off boundary and selected statement cards.
Results by paper section
Every formalized result, grouped under the manuscript section that states it.
All Lean statements
Generated page: each result's Lean statement, hypotheses and the checks that ran.
Scope ledger
All 73 primary scopes with manuscript numbering and pages.
Trust and reproduction
Trust and axioms
Allowed axioms, comparator coverage and how the public source relates to the accepted source.
Reproduce
Beginner guide to ./verify.sh, the pinned toolchain and troubleshooting.
Release evidence
Phase-composite manifest, recovery summary and logs.
Acknowledgments and citation
Authors and AI disclosure, lean-pkg, the Auburn University Easley Cluster, and how to cite.
Paper
Le Chen, Ian Ruau and Wenxian Shen, Chemotaxis models with signal-dependent sensitivity and a logistic-type source, III: Bifurcation and spike-like solutions. Manuscript source and PDF · arXiv:2610.20976v2, the version the scope ledger maps (manuscript versions).
Use it
git clone https://github.com/chenle02/chemotaxis-paper-iii-lean.git
cd chemotaxis-paper-iii-lean
./verify.sh
[[require]]
name = "chemotaxis-bifurcation-lean"
git = "https://github.com/chenle02/chemotaxis-paper-iii-lean"
rev = "v0.1.1"
Developed and verified with lean-pkg (doi:10.5281/zenodo.23272098). This work was completed in part with resources provided by the Auburn University Easley Cluster; what ran there. Coding agents: start from llms.txt.