Skip to content

Chemotaxis III in Lean Partial Lean 4 formalization · release v0.1.1

Menu

Results by paper section

Each entry opens the result on the verification page, which shows the Lean statement, its hypotheses, the checks that ran and, where it is quoted, the paper’s statement. The class in brackets repeats that page’s own wording. Section titles follow the arXiv v2 manuscript; results are grouped by the section whose number they carry.

Listed here: 70 results (47 with the paper’s own hypotheses, 23 with extra hypotheses) and 3 not formalized.

1. Introduction

22 results

Proposition 1.1: Linear stability/instability (paper’s own hypotheses)
Theorem 1.1 (reduced scalar equation): Local pitchfork bifurcation: equilibria of the reduced scalar equation (extra hypotheses)
Theorem 1.2(1): beta_n0 is a quadratic in beta with negative leading coefficient (extra hypotheses)
Theorem 1.2(2): beta_n0 as a rational function of lambda_n0; sign changes and domain-size limits (extra hypotheses)
Remark 1.1(1): Reduction to the scalar ODE for u_n0 (extra hypotheses)
Theorem 1.4: Spike-like stationary solutions (paper’s own hypotheses)
Remark 1.3(2): No Dirac mass in the non-minimal model (paper’s own hypotheses)
Proposition 1.2: Consistency of thresholds (paper’s own hypotheses)
Equation (1.24): Eigenvalues of the discrete Neumann Laplacian (corrected: of -Delta_h) (paper’s own hypotheses)
Equation (1.15): beta_n0 = P(lambda_n0)/Q(lambda_n0) (paper’s own hypotheses)
Theorem 1.2(2), eigenvalue intervals: Interval of lambda_n0 for an admissible length (paper’s own hypotheses)
Theorem 1.2: Degree-three numerator and denominator of beta_n0 in the minimal model (paper’s own hypotheses)
Theorem 1.3(1): Relative component construction of the global branch (extra hypotheses)
Theorem 1.3(3): Fixed mass and vanishing tails give a Dirac limit (paper’s own hypotheses)
Remark 1.3(2) (local-mass): Uniformly small local mass (paper’s own hypotheses)
Theorem 1.3(3) (part-3-concentration): Concentration at an endpoint along the global branch (paper’s own hypotheses)
Theorem 1.1: Two continuous branch curves of the reduced equation (extra hypotheses)
Remark 1.3(2) (no-atom-limit): No atom in the limit measure (paper’s own hypotheses)
Theorem 1.4 (deductions): Deductions of the spike theorem (paper’s own hypotheses)
Theorem 1.3(1)-(3): Logical deductions of the global extension theorem (extra hypotheses)
Theorem 1.3(2)-(3), ambient-limit proof paragraphs: Ambient closure of the admissible set (extra hypotheses)
Theorem 1.3(3), Equation 4.18, full range 1 <= m <= 2: ODE content of the monotone-locus argument (extra hypotheses)

2. Local bifurcation of constant solutions

23 results

Lemma 2.1, Equations 2.1-2.4: Integrals of products of cosine series (paper’s own hypotheses)
Equation (2.8): Mobility coefficients B_0, B_u, B_v (paper’s own hypotheses)
Equation (2.9): Mobility coefficients B_uu, B_uv, B_vv (paper’s own hypotheses)
Equation (2.10): Logistic coefficients A’, A’’, A’’’ (paper’s own hypotheses)
Equation (2.11): Signal-source coefficients C’, C’’, C’’’ (paper’s own hypotheses)
Equation (2.20): Signal coefficients C_k^(1), C_k^(2), C_k^(3) (paper’s own hypotheses)
Equation (2.32): Quadratic coefficient Gamma_{2 n0} (extra hypotheses)
Equation (2.33): Constant-mode coefficients a_{0,1}, a_{0,2} (extra hypotheses)
Equation (2.36b): Higher-mode coefficients a_{k,1} (extra hypotheses)
Equation (2.42): Auxiliary quantities F, G, H (extra hypotheses)
Equation (2.41): Cubic coefficient Gamma_{n0}^(3) (extra hypotheses)
Equation (2.44): Crossing coefficient alpha_n0 (paper’s own hypotheses)
Equation (2.45): Cubic coefficient beta_n0 (extra hypotheses)
Equation (2.43): Reduced equation on the centre manifold (extra hypotheses)
Equation (2.49): beta_n0 in the minimal model (extra hypotheses)
Lemma 2.1, Equations 2.1-2.4 (infinite-fourier-convolution): Infinite Fourier series: summability, exchange of sums and integrals, convolution (paper’s own hypotheses)
Equation (2.43) (current-remainder-consumer): Mixed remainder and derivative interface of the reduced equation (extra hypotheses)
Lemma 2.1 and Equation 2.17: Cosine-series bridge for the Neumann phase space (paper’s own hypotheses)
Equation (2.43) (remainder-from-jet): Remainder bounds from the point jet (extra hypotheses)
Lemma 2.1 and Equation 2.17 (phase-space-H2): Neumann H^2 phase space as cosine series (paper’s own hypotheses)
Equation (2.43) (axis-condition): Axis condition for the remainder (jet conditions alone do not suffice) (extra hypotheses)
Equation (2.22) (projected-remainder): Projection of the fourth-order remainder onto a cosine mode (paper’s own hypotheses)
Equations 2.18-2.19: Normalized signal Taylor remainder (paper’s own hypotheses)

3. Effects of β and L on the bifurcation

7 results

Equation (3.1): beta_n0 in terms of p(beta) and q(beta) (extra hypotheses)
Equation (3.3): Coefficients A, B, C of the quadratic in beta (paper’s own hypotheses)
Equation (3.4): Closed form of the leading coefficient A (paper’s own hypotheses)
Equation (3.6): Unique minimizing mode on each admissible interval (paper’s own hypotheses)
Equation (3.7): Large-lambda asymptotics of beta_n0 in Example 3.1 (paper’s own hypotheses)
Equation (3.8): Large-domain limit beta_infinity in Example 3.1 (extra hypotheses)
Table 3.2: Real roots of P(lambda, beta) for selected beta (extra hypotheses)

4. Extension of the local bifurcation branches

13 results

Lemma 4.1: Bounds for stationary solutions of the non-minimal model (paper’s own hypotheses)
Lemma 4.2: Bounds for stationary solutions of the minimal model (paper’s own hypotheses)
Lemma 4.1 and Lemma 4.2, bounded-sensitivity proof context: Compactness at bounded sensitivity (dissolved into Lemmas 4.1-4.2 in v1) (paper’s own hypotheses)
Lemma 4.1(1), Equation 4.1: Mass and moment bounds for stationary solutions of the non-minimal model (paper’s own hypotheses)
Lemma 4.1(2), Equation 4.6: Moment step for 0 < gamma <= 1 + alpha (paper’s own hypotheses)
Equation 4.14 (proof of Lemma 4.2(2)): Flux identity of the minimal model (paper’s own hypotheses)
Lemma 4.2(1): Mass and moment bounds for stationary solutions of the minimal model (paper’s own hypotheses)
Proof of Lemma 4.2(2) (applies Equation 4.6, p. 28, TeX line 2687): Fixed-mass Jensen step (paper’s own hypotheses)
Proof of Lemma 4.2(2), m=1 case of the variation-of-constants display: Exponential representation for m = 1 (paper’s own hypotheses)
Proof of Lemma 4.2(2), Equations 4.7-4.8: Signal bounds in the minimal model (paper’s own hypotheses)
Proof of Lemma 4.2(2): the uniform bounds on u and u_x from the flux identity (4.14), before the elliptic step to (4.13) (alternative estimate for 1<=m<2): Sup bound for 0 < m < 2 in the minimal model (paper’s own hypotheses)
Proof of Lemma 4.2(2), m=1 case: Sup bound for m = 1 in the minimal model (paper’s own hypotheses)
Lemma 4.1(2), Equation 4.11 (alternative route for 1<=m<(alpha+2)/2): Gradient bound chain in the non-minimal model (paper’s own hypotheses)

5. Spike-like stationary solutions

3 results

Lemma 5.1: Constant limits at large sensitivity (paper’s own hypotheses)
Proof of Lemma 5.1, W^{2,q} step with r=1+alpha: W^{2,q} bound for the signal (step in the proof of Lemma 5.1) (paper’s own hypotheses)
Lemma 5.1 (deductions): Deductions of the constant-limit lemma (paper’s own hypotheses)

6. Numerical analysis of the bifurcation and spike-like solutions

2 results

Equation (6.1): Semidiscrete scheme for the non-minimal model (paper’s own hypotheses)
Equation (6.2): Conservative semidiscrete scheme for the minimal model (paper’s own hypotheses)

Not formalized

Listed with their reasons on the verification page:

Theorem 1.1 (PDE branches and stability) (Local pitchfork bifurcation
Theorem 1.3 (Extension of the local bifurcation branches)
Equation (2.16) (Centre manifold as a graph over the critical mode)