Skip to content

Turing patterns and diffusion-driven instability

DefinitionDiffusion matrix of a two-species system#✓fully proved

The diffusion matrix D = diag(d_u, d_v) of a two-species reaction-diffusion system.

def diffusionMatrix (du dv : ℝ) : Matrix (Fin 2) (Fin 2) ℝ :=
  Matrix.diagonal ![du, dv]
Used by 3
Used byDispersion relation · Classical solution of the linearized reaction-diffusion system · Mode matrix of a linearized reaction-diffusion system

DefinitionMode matrix of a linearized reaction-diffusion system#✓fully proved

The mode matrix J - k² D governing the Fourier mode of wavenumber k of the linearized system w_t = D w_xx + J w, where J is the Jacobian of the kinetics at the steady state (convention: J i j is the partial derivative of the i-th reaction term with respect to the j-th species, so J = [[f_u, f_v], [g_u, g_v]]).

def modeMatrix (J : Matrix (Fin 2) (Fin 2) ℝ) (du dv k : ℝ) : Matrix (Fin 2) (Fin 2) ℝ :=
  J - k ^ 2 • diffusionMatrix du dv
Uses 1 · Used by 10
Statement usesDiffusion matrix of a two-species system
Used byDeterminant of the mode matrix is the dispersion polynomial · Only finitely many Neumann modes are unstable · Dispersion relation · Linearly unstable Fourier mode · Instability criterion for a Fourier mode via trace and determinant · Mode instability iff the dispersion polynomial is negative · A Fourier mode grows iff J - k² D has an eigenvalue with positive real part · Homogeneous mode is stable for stable kinetics · Trace of the mode matrix · Diffusion-driven instability (Turing 1952)

DefinitionLinearly unstable Fourier mode#✓fully proved

The Fourier mode of wavenumber k is linearly unstable: the mode matrix J - k² D has a complex eigenvalue μ with 0 < Re μ.

def IsUnstableMode (J : Matrix (Fin 2) (Fin 2) ℝ) (du dv k : ℝ) : Prop :=
  ∃ μ : ℂ, 0 < μ.re ∧ ∃ v : Fin 2 → ℂ, v ≠ 0 ∧
    (modeMatrix J du dv k).map (↑) *ᵥ v = μ • v
Uses 1 · Used by 15
Statement usesMode matrix of a linearized reaction-diffusion system
Used byTuring's criterion · Large domains pattern · Only finitely many Neumann modes are unstable · Turing instability of the Gierer–Meinhardt kinetics · Instability criterion for a Fourier mode via trace and determinant · Mode instability iff the dispersion polynomial is negative · A Fourier mode grows iff J - k² D has an eigenvalue with positive real part · Finite domain · Critical wavenumber is unstable under Turing's criterion · The inhibitor diffuses faster · f_u and g_v have opposite signs · Small domains admit no pattern · Homogeneous mode is stable for stable kinetics · Turing instability of the Schnakenberg kinetics · Diffusion-driven instability (Turing 1952)

DefinitionComplex Fourier mode#✓fully proved

The complex Fourier mode w(t, x) = e^{μ t} cos(k x) v with growth rate μ, wavenumber k and amplitude vector v. (The real part of a complex solution of the real linear system is a real solution.)

noncomputable def fourierMode (μ : ℂ) (k : ℝ) (v : Fin 2 → ℂ) (t x : ℝ) : Fin 2 → ℂ :=
  (Complex.exp (μ * t) * (Real.cos (k * x) : ℂ)) • v
Used by 6
Used byDispersion relation · Neumann modes have zero flux at the boundary · A Fourier mode grows iff J - k² D has an eigenvalue with positive real part · Fourier mode is largest at the origin · Amplitude of a Fourier mode · Fourier mode grows unboundedly iff its growth rate is positive

DefinitionClassical solution of the linearized reaction-diffusion system#✓fully proved

w is a classical solution of the linearized reaction-diffusion system w_t = D w_xx + J w on ℝ × ℝ: w(t, ·) is twice differentiable with first and second derivatives wx, wxx, and w(·, x) is differentiable with the prescribed time derivative.

def IsLinearizedSolution (J : Matrix (Fin 2) (Fin 2) ℝ) (du dv : ℝ)
    (w : ℝ → ℝ → Fin 2 → ℂ) : Prop :=
  ∃ wx wxx : ℝ → ℝ → Fin 2 → ℂ, ∀ t x,
    HasDerivAt (w t) (wx t x) x ∧ HasDerivAt (wx t) (wxx t x) x ∧
    HasDerivAt (fun s => w s x)
      ((diffusionMatrix du dv).map (↑) *ᵥ wxx t x + J.map (↑) *ᵥ w t x) t
Uses 1 · Used by 2
Statement usesDiffusion matrix of a two-species system
Used byDispersion relation · A Fourier mode grows iff J - k² D has an eigenvalue with positive real part

DefinitionDispersion polynomial#✓fully proved

The dispersion polynomial h(q) = d_u d_v q² - (d_v f_u + d_u g_v) q + det J, so that det (J - k² D) = h(k²) (det_modeMatrix).

def dispersionDet (J : Matrix (Fin 2) (Fin 2) ℝ) (du dv q : ℝ) : ℝ :=
  du * dv * q ^ 2 - (dv * J 0 0 + du * J 1 1) * q + J.det
Used by 15
Used byCritical wavenumber at the Turing bifurcation threshold · Determinant of the mode matrix is the dispersion polynomial · Minimum value of the dispersion polynomial · Critical squared wavenumber minimizes the dispersion polynomial · Dispersion polynomial is negative exactly on the unstable band · Turing's criterion for diffusion-driven instability · Turing's criterion · Only finitely many Neumann modes are unstable · Mode instability iff the dispersion polynomial is negative · Finite domain · Critical wavenumber is unstable under Turing's criterion · The inhibitor diffuses faster · f_u and g_v have opposite signs · Homogeneous mode is stable for stable kinetics · Diffusion-driven instability (Turing 1952)

DefinitionSquared critical wavenumber#✓fully proved

The squared critical wavenumber k_c² = (d_v f_u + d_u g_v) / (2 d_u d_v), the minimizer of the dispersion polynomial (meaningful for d_u, d_v > 0; division by zero gives 0).

noncomputable def criticalWavenumberSq (J : Matrix (Fin 2) (Fin 2) ℝ) (du dv : ℝ) : ℝ :=
  (dv * J 0 0 + du * J 1 1) / (2 * du * dv)
Used by 4
Used byCritical wavenumber at the Turing bifurcation threshold · Minimum value of the dispersion polynomial · Critical squared wavenumber minimizes the dispersion polynomial · Critical wavenumber is unstable under Turing's criterion

DefinitionDiscriminant of the dispersion polynomial#✓fully proved

The discriminant (d_v f_u + d_u g_v)² - 4 d_u d_v det J of the dispersion polynomial.

def bandDiscriminant (J : Matrix (Fin 2) (Fin 2) ℝ) (du dv : ℝ) : ℝ :=
  (dv * J 0 0 + du * J 1 1) ^ 2 - 4 * du * dv * J.det
Used by 6
Used byLower end of the unstable wavenumber band · Upper end of the unstable wavenumber band · Dispersion polynomial is negative exactly on the unstable band · Large domains pattern · Finite domain · Small domains admit no pattern

DefinitionLower end of the unstable wavenumber band#✓fully proved

Lower end q₋ = (S - √Δ) / (2 d_u d_v) of the unstable band of squared wavenumbers, where S = d_v f_u + d_u g_v and Δ = bandDiscriminant (meaningful when 0 < Δ, d_u, d_v > 0).

noncomputable def bandLower (J : Matrix (Fin 2) (Fin 2) ℝ) (du dv : ℝ) : ℝ :=
  (dv * J 0 0 + du * J 1 1 - Real.sqrt (bandDiscriminant J du dv)) / (2 * du * dv)
Uses 1 · Used by 4
Statement usesDiscriminant of the dispersion polynomial
Used byDispersion polynomial is negative exactly on the unstable band · Large domains pattern · Finite domain · Small domains admit no pattern

DefinitionUpper end of the unstable wavenumber band#✓fully proved

Upper end q₊ = (S + √Δ) / (2 d_u d_v) of the unstable band of squared wavenumbers (meaningful when 0 < Δ, d_u, d_v > 0).

noncomputable def bandUpper (J : Matrix (Fin 2) (Fin 2) ℝ) (du dv : ℝ) : ℝ :=
  (dv * J 0 0 + du * J 1 1 + Real.sqrt (bandDiscriminant J du dv)) / (2 * du * dv)
Uses 1 · Used by 4
Statement usesDiscriminant of the dispersion polynomial
Used byDispersion polynomial is negative exactly on the unstable band · Large domains pattern · Finite domain · Small domains admit no pattern

DefinitionNeumann wavenumber on an interval#✓fully proved

The Neumann wavenumber k_n = n π / L of the mode cos(n π x / L) on [0, L]. Meaningful only for 0 < L; at L = 0 the totalized division gives 0, so every labeled Neumann mode collapses to the homogeneous mode.

noncomputable def neumannWavenumber (L : ℝ) (n : ℕ) : ℝ :=
  n * Real.pi / L
Used by 5
Used byLarge domains pattern · Only finitely many Neumann modes are unstable · Neumann modes have zero flux at the boundary · Finite domain · Small domains admit no pattern
55 fully proved

The dispersion relation

TheoremTrace of the mode matrix#✓fully proved

tr (J - k² D) = tr J - k² (d_u + d_v).

theorem trace_modeMatrix (J : Matrix (Fin 2) (Fin 2) ℝ) (du dv k : ℝ) :
    (modeMatrix J du dv k).trace = J.trace - k ^ 2 * (du + dv)
Uses 1 · Used by 3
Statement usesMode matrix of a linearized reaction-diffusion system
Used byOnly finitely many Neumann modes are unstable · Mode instability iff the dispersion polynomial is negative · Homogeneous mode is stable for stable kinetics

TheoremDeterminant of the mode matrix is the dispersion polynomial#✓fully proved

det (J - k² D) = h(k²).

theorem det_modeMatrix (J : Matrix (Fin 2) (Fin 2) ℝ) (du dv k : ℝ) :
    (modeMatrix J du dv k).det = dispersionDet J du dv (k ^ 2)
Uses 2 · Used by 4
Statement usesDispersion polynomial · Mode matrix of a linearized reaction-diffusion system
Used byOnly finitely many Neumann modes are unstable · Mode instability iff the dispersion polynomial is negative · Homogeneous mode is stable for stable kinetics · Diffusion-driven instability (Turing 1952)

TheoremRouth–Hurwitz for 2 × 2 matrices#✓fully proved

A real 2 × 2 matrix has a complex eigenvalue with positive real part iff its trace is positive or its determinant is negative.

theorem exists_eigenvalue_re_pos_iff (M : Matrix (Fin 2) (Fin 2) ℝ) :
    (∃ μ : ℂ, 0 < μ.re ∧ ∃ v : Fin 2 → ℂ, v ≠ 0 ∧ M.map (↑) *ᵥ v = μ • v) ↔
      0 < M.trace ∨ M.det < 0
Used by 1
Used byInstability criterion for a Fourier mode via trace and determinant

TheoremInstability criterion for a Fourier mode via trace and determinant#✓fully proved

Mode k is unstable iff 0 < tr (J - k² D) or det (J - k² D) < 0.

theorem isUnstableMode_iff {J : Matrix (Fin 2) (Fin 2) ℝ} {du dv k : ℝ} :
    IsUnstableMode J du dv k ↔
      0 < (modeMatrix J du dv k).trace ∨ (modeMatrix J du dv k).det < 0
Uses 3 · Used by 3
Statement usesLinearly unstable Fourier mode · Mode matrix of a linearized reaction-diffusion system
Proof usesRouth–Hurwitz for 2 × 2 matrices
Used byOnly finitely many Neumann modes are unstable · Mode instability iff the dispersion polynomial is negative · Homogeneous mode is stable for stable kinetics

TheoremDispersion relation#✓fully proved

The Fourier mode e^{μ t} cos(k x) v is a classical solution of the linearized system w_t = D w_xx + J w iff (J - k² D) v = μ v.

theorem fourierMode_isLinearizedSolution_iff (J : Matrix (Fin 2) (Fin 2) ℝ) (du dv k : ℝ)
    (μ : ℂ) (v : Fin 2 → ℂ) :
    IsLinearizedSolution J du dv (fourierMode μ k v) ↔
      (modeMatrix J du dv k).map (↑) *ᵥ v = μ • v
Uses 4 · Used by 1
Statement usesClassical solution of the linearized reaction-diffusion system · Complex Fourier mode · Mode matrix of a linearized reaction-diffusion system
Proof usesDiffusion matrix of a two-species system
Used byA Fourier mode grows iff J - k² D has an eigenvalue with positive real part

TheoremAmplitude of a Fourier mode#✓fully proved

The amplitude of a Fourier mode: ‖w(t, 0)‖ = e^{Re μ · t} ‖v‖.

theorem norm_fourierMode_zero (μ : ℂ) (k : ℝ) (v : Fin 2 → ℂ) (t : ℝ) :
    ‖fourierMode μ k v t 0‖ = Real.exp (μ.re * t) * ‖v‖
Uses 1 · Used by 2
Statement usesComplex Fourier mode
Used byFourier mode is largest at the origin · Fourier mode grows unboundedly iff its growth rate is positive

TheoremFourier mode is largest at the origin#✓fully proved

‖w(t, 0)‖ is the amplitude of the mode: ‖w(t, x)‖ ≤ ‖w(t, 0)‖ for every x.

theorem norm_fourierMode_le (μ : ℂ) (k : ℝ) (v : Fin 2 → ℂ) (t x : ℝ) :
    ‖fourierMode μ k v t x‖ ≤ ‖fourierMode μ k v t 0‖
Uses 2
Statement usesComplex Fourier mode
Proof usesAmplitude of a Fourier mode

TheoremFourier mode grows unboundedly iff its growth rate is positive#✓fully proved

A nonzero Fourier mode grows without bound iff its growth rate has positive real part.

theorem tendsto_norm_fourierMode_iff {v : Fin 2 → ℂ} (hv : v ≠ 0) (μ : ℂ) (k : ℝ) :
    Tendsto (fun t => ‖fourierMode μ k v t 0‖) atTop atTop ↔ 0 < μ.re
Uses 2 · Used by 1
Statement usesComplex Fourier mode
Proof usesAmplitude of a Fourier mode
Used byA Fourier mode grows iff J - k² D has an eigenvalue with positive real part

TheoremA Fourier mode grows iff J - k² D has an eigenvalue with positive real part#✓fully proved

A Fourier mode grows iff J - k² D has an eigenvalue with positive real part.

theorem isUnstableMode_iff_exists_growing {J : Matrix (Fin 2) (Fin 2) ℝ} {du dv k : ℝ} :
    IsUnstableMode J du dv k ↔ ∃ (μ : ℂ) (v : Fin 2 → ℂ), v ≠ 0 ∧
      IsLinearizedSolution J du dv (fourierMode μ k v) ∧
      Tendsto (fun t => ‖fourierMode μ k v t 0‖) atTop atTop
Uses 6
Statement usesClassical solution of the linearized reaction-diffusion system · Linearly unstable Fourier mode · Complex Fourier mode
Proof usesDispersion relation · Mode matrix of a linearized reaction-diffusion system · Fourier mode grows unboundedly iff its growth rate is positive

Diffusion-driven instability

TheoremHomogeneous mode is stable for stable kinetics#✓fully proved

The homogeneous mode k = 0 is stable when the kinetics are stable (tr J < 0, 0 < det J).

theorem not_isUnstableMode_zero {J : Matrix (Fin 2) (Fin 2) ℝ} (htr : J.trace < 0)
    (hdet : 0 < J.det) (du dv : ℝ) : ¬ IsUnstableMode J du dv 0
Uses 6 · Used by 2
Statement usesLinearly unstable Fourier mode
Proof usesDeterminant of the mode matrix is the dispersion polynomial · Dispersion polynomial · Instability criterion for a Fourier mode via trace and determinant · Mode matrix of a linearized reaction-diffusion system · Trace of the mode matrix
Used bySmall domains admit no pattern · Diffusion-driven instability (Turing 1952)

TheoremMode instability iff the dispersion polynomial is negative#✓fully proved

If tr J < 0 and d_u, d_v ≥ 0, mode k is unstable iff h(k²) < 0.

theorem isUnstableMode_iff_dispersionDet_neg {J : Matrix (Fin 2) (Fin 2) ℝ} {du dv : ℝ}
    (htr : J.trace < 0) (hdu : 0 ≤ du) (hdv : 0 ≤ dv) (k : ℝ) :
    IsUnstableMode J du dv k ↔ dispersionDet J du dv (k ^ 2) < 0
Uses 6 · Used by 6
Statement usesLinearly unstable Fourier mode · Dispersion polynomial
Proof usesDeterminant of the mode matrix is the dispersion polynomial · Instability criterion for a Fourier mode via trace and determinant · Mode matrix of a linearized reaction-diffusion system · Trace of the mode matrix
Used byTuring's criterion · Finite domain · Critical wavenumber is unstable under Turing's criterion · The inhibitor diffuses faster · f_u and g_v have opposite signs · Diffusion-driven instability (Turing 1952)

TheoremDiffusion-driven instability (Turing 1952)#✓fully proved

If the steady state is stable without diffusion (tr J < 0, 0 < det J), d_u, d_v ≥ 0, and det (J - k² D) < 0, then the homogeneous mode is stable while mode k is unstable.

theorem turing_instability {J : Matrix (Fin 2) (Fin 2) ℝ} {du dv k : ℝ} (htr : J.trace < 0)
    (hdet : 0 < J.det) (hdu : 0 ≤ du) (hdv : 0 ≤ dv) (hk : (modeMatrix J du dv k).det < 0) :
    ¬ IsUnstableMode J du dv 0 ∧ IsUnstableMode J du dv k
Uses 6
Statement usesLinearly unstable Fourier mode · Mode matrix of a linearized reaction-diffusion system
Proof usesDeterminant of the mode matrix is the dispersion polynomial · Dispersion polynomial · Mode instability iff the dispersion polynomial is negative · Homogeneous mode is stable for stable kinetics

TheoremMinimum value of the dispersion polynomial#✓fully proved

The value of the dispersion polynomial at its minimizer: h(k_c²) = det J - (d_v f_u + d_u g_v)² / (4 d_u d_v).

theorem dispersionDet_criticalWavenumberSq {J : Matrix (Fin 2) (Fin 2) ℝ} {du dv : ℝ}
    (hdu : 0 < du) (hdv : 0 < dv) :
    dispersionDet J du dv (criticalWavenumberSq J du dv) =
      J.det - (dv * J 0 0 + du * J 1 1) ^ 2 / (4 * du * dv)
Uses 2 · Used by 2
Statement usesSquared critical wavenumber · Dispersion polynomial
Used byCritical wavenumber at the Turing bifurcation threshold · Critical wavenumber is unstable under Turing's criterion

TheoremCritical squared wavenumber minimizes the dispersion polynomial#✓fully proved

The critical squared wavenumber minimizes the dispersion polynomial over all real q.

theorem dispersionDet_criticalWavenumberSq_le {J : Matrix (Fin 2) (Fin 2) ℝ} {du dv : ℝ}
    (hdu : 0 < du) (hdv : 0 < dv) (q : ℝ) :
    dispersionDet J du dv (criticalWavenumberSq J du dv) ≤ dispersionDet J du dv q
Uses 2
Statement usesSquared critical wavenumber · Dispersion polynomial

TheoremTuring condition in squared form#✓fully proved

The Turing condition in squared form: 2 √(d_u d_v det J) < S iff 0 < S and 4 d_u d_v det J < S², where S = d_v f_u + d_u g_v. This holds for all real inputs: when d_u d_v det J < 0, Real.sqrt returns 0 and both sides reduce to 0 < S.

theorem two_mul_sqrt_lt_iff {J : Matrix (Fin 2) (Fin 2) ℝ} {du dv : ℝ} :
    2 * Real.sqrt (du * dv * J.det) < dv * J 0 0 + du * J 1 1 ↔
      0 < dv * J 0 0 + du * J 1 1 ∧ 4 * du * dv * J.det < (dv * J 0 0 + du * J 1 1) ^ 2
Used by 3
Used byTuring's criterion for diffusion-driven instability · Large domains pattern · Critical wavenumber is unstable under Turing's criterion

TheoremTuring's criterion for diffusion-driven instability#✓fully proved

For d_u, d_v > 0 and 0 < det J, the dispersion polynomial is negative at some q ≥ 0 iff 2 √(d_u d_v det J) < d_v f_u + d_u g_v.

theorem exists_dispersionDet_neg_iff {J : Matrix (Fin 2) (Fin 2) ℝ} {du dv : ℝ}
    (hdu : 0 < du) (hdv : 0 < dv) (hdet : 0 < J.det) :
    (∃ q, 0 ≤ q ∧ dispersionDet J du dv q < 0) ↔
      2 * Real.sqrt (du * dv * J.det) < dv * J 0 0 + du * J 1 1
Uses 2 · Used by 1
Statement usesDispersion polynomial
Proof usesTuring condition in squared form
Used byTuring's criterion

TheoremTuring's criterion#✓fully proved

If the steady state is stable without diffusion (tr J < 0, 0 < det J) and d_u, d_v > 0, some Fourier mode is unstable iff d_v f_u + d_u g_v > 2 √(d_u d_v det J).

theorem exists_isUnstableMode_iff {J : Matrix (Fin 2) (Fin 2) ℝ} {du dv : ℝ} (hdu : 0 < du)
    (hdv : 0 < dv) (htr : J.trace < 0) (hdet : 0 < J.det) :
    (∃ k, IsUnstableMode J du dv k) ↔
      2 * Real.sqrt (du * dv * J.det) < dv * J 0 0 + du * J 1 1
Uses 4 · Used by 2
Statement usesLinearly unstable Fourier mode
Proof usesDispersion polynomial · Turing's criterion for diffusion-driven instability · Mode instability iff the dispersion polynomial is negative
Used byTuring instability of the Gierer–Meinhardt kinetics · Turing instability of the Schnakenberg kinetics

TheoremCritical wavenumber is unstable under Turing's criterion#✓fully proved

Under Turing's criterion the critical wavenumber k_c = √(k_c²) is itself unstable (and 0 < k_c²).

theorem isUnstableMode_sqrt_criticalWavenumberSq {J : Matrix (Fin 2) (Fin 2) ℝ} {du dv : ℝ}
    (hdu : 0 < du) (hdv : 0 < dv) (htr : J.trace < 0) (_hdet : 0 < J.det)
    (h : 2 * Real.sqrt (du * dv * J.det) < dv * J 0 0 + du * J 1 1) :
    0 < criticalWavenumberSq J du dv ∧
      IsUnstableMode J du dv (Real.sqrt (criticalWavenumberSq J du dv))
Uses 6
Statement usesLinearly unstable Fourier mode · Squared critical wavenumber
Proof usesDispersion polynomial · Minimum value of the dispersion polynomial · Mode instability iff the dispersion polynomial is negative · Turing condition in squared form

TheoremCritical wavenumber at the Turing bifurcation threshold#✓fully proved

At the bifurcation threshold d_v f_u + d_u g_v = 2 √(d_u d_v det J) the critical squared wavenumber is k_c² = √(det J / (d_u d_v)) and h(k_c²) = 0.

theorem criticalWavenumberSq_of_threshold {J : Matrix (Fin 2) (Fin 2) ℝ} {du dv : ℝ}
    (hdu : 0 < du) (hdv : 0 < dv) (hdet : 0 ≤ J.det)
    (h : dv * J 0 0 + du * J 1 1 = 2 * Real.sqrt (du * dv * J.det)) :
    criticalWavenumberSq J du dv = Real.sqrt (J.det / (du * dv)) ∧
      dispersionDet J du dv (criticalWavenumberSq J du dv) = 0
Uses 3
Statement usesSquared critical wavenumber · Dispersion polynomial
Proof usesMinimum value of the dispersion polynomial

Theoremf_u and g_v have opposite signs#✓fully proved

If the steady state is stable without diffusion and d_u, d_v ≥ 0, diffusion-driven instability forces f_u g_v < 0.

theorem mul_neg_of_exists_isUnstableMode {J : Matrix (Fin 2) (Fin 2) ℝ} {du dv : ℝ}
    (htr : J.trace < 0) (hdet : 0 < J.det) (hdu : 0 ≤ du) (hdv : 0 ≤ dv)
    (h : ∃ k, IsUnstableMode J du dv k) : J 0 0 * J 1 1 < 0
Uses 3
Statement usesLinearly unstable Fourier mode
Proof usesDispersion polynomial · Mode instability iff the dispersion polynomial is negative

TheoremThe inhibitor diffuses faster#✓fully proved

In the activator-inhibitor sign pattern (u is the activator, 0 < f_u; then g_v < 0 follows from tr J < 0), diffusion-driven instability of a kinetically stable state forces d_u < d_v.

theorem lt_of_exists_isUnstableMode {J : Matrix (Fin 2) (Fin 2) ℝ} {du dv : ℝ}
    (htr : J.trace < 0) (hdet : 0 < J.det) (hdu : 0 ≤ du) (hdv : 0 ≤ dv) (hfu : 0 < J 0 0)
    (h : ∃ k, IsUnstableMode J du dv k) : du < dv
Uses 3
Statement usesLinearly unstable Fourier mode
Proof usesDispersion polynomial · Mode instability iff the dispersion polynomial is negative

Unstable band and finite domains

TheoremDispersion polynomial is negative exactly on the unstable band#✓fully proved

For d_u, d_v > 0, the dispersion polynomial is negative exactly on the open band (q₋, q₊), which is nonempty iff the discriminant is positive.

theorem dispersionDet_neg_iff {J : Matrix (Fin 2) (Fin 2) ℝ} {du dv : ℝ} (hdu : 0 < du)
    (hdv : 0 < dv) (q : ℝ) :
    dispersionDet J du dv q < 0 ↔
      0 < bandDiscriminant J du dv ∧ bandLower J du dv < q ∧ q < bandUpper J du dv
Uses 4 · Used by 1
Statement usesDiscriminant of the dispersion polynomial · Lower end of the unstable wavenumber band · Upper end of the unstable wavenumber band · Dispersion polynomial
Used byFinite domain

TheoremNeumann modes have zero flux at the boundary#✓fully proved

The Neumann mode cos(k_n x) has zero flux at both ends of [0, L]: the x-derivative of the Fourier mode with wavenumber k_n = n π / L vanishes at x = 0 and x = L.

theorem hasDerivAt_fourierMode_neumannWavenumber {L : ℝ} (hL : L ≠ 0) (n : ℕ) (μ : ℂ)
    (v : Fin 2 → ℂ) (t : ℝ) :
    HasDerivAt (fourierMode μ (neumannWavenumber L n) v t) 0 0 ∧
      HasDerivAt (fourierMode μ (neumannWavenumber L n) v t) 0 L
Uses 2
Statement usesComplex Fourier mode · Neumann wavenumber on an interval

TheoremFinite domain#✓fully proved

On [0, L] with Neumann boundary conditions, if tr J < 0 and d_u, d_v > 0, mode n is unstable iff k_n² = (n π / L)² lies in the unstable band (q₋, q₊) (which requires a positive discriminant).

theorem isUnstableMode_neumannWavenumber_iff {J : Matrix (Fin 2) (Fin 2) ℝ} {du dv L : ℝ}
    (hdu : 0 < du) (hdv : 0 < dv) (htr : J.trace < 0) (_hL : 0 < L) (n : ℕ) :
    IsUnstableMode J du dv (neumannWavenumber L n) ↔
      0 < bandDiscriminant J du dv ∧ bandLower J du dv < (n * Real.pi / L) ^ 2 ∧
        (n * Real.pi / L) ^ 2 < bandUpper J du dv
Uses 8 · Used by 2
Statement usesLinearly unstable Fourier mode · Discriminant of the dispersion polynomial · Lower end of the unstable wavenumber band · Upper end of the unstable wavenumber band · Neumann wavenumber on an interval
Proof usesDispersion polynomial · Dispersion polynomial is negative exactly on the unstable band · Mode instability iff the dispersion polynomial is negative
Used byLarge domains pattern · Small domains admit no pattern

TheoremOnly finitely many Neumann modes are unstable#✓fully proved

Only finitely many Neumann modes are unstable on [0, L] (for d_u, d_v, L > 0, any J).

theorem finite_setOf_isUnstableMode_neumannWavenumber {J : Matrix (Fin 2) (Fin 2) ℝ}
    {du dv L : ℝ} (hdu : 0 < du) (hdv : 0 < dv) (hL : 0 < L) :
    {n : ℕ | IsUnstableMode J du dv (neumannWavenumber L n)}.Finite
Uses 7
Statement usesLinearly unstable Fourier mode · Neumann wavenumber on an interval
Proof usesDeterminant of the mode matrix is the dispersion polynomial · Dispersion polynomial · Instability criterion for a Fourier mode via trace and determinant · Mode matrix of a linearized reaction-diffusion system · Trace of the mode matrix

TheoremSmall domains admit no pattern#✓fully proved

If the first nonhomogeneous mode already lies beyond the band, q₊ ≤ (π / L)², then no Neumann mode is unstable on [0, L].

theorem not_isUnstableMode_neumannWavenumber_of_le {J : Matrix (Fin 2) (Fin 2) ℝ}
    {du dv L : ℝ} (hdu : 0 < du) (hdv : 0 < dv) (htr : J.trace < 0) (hdet : 0 < J.det)
    (hL : 0 < L) (hsmall : bandUpper J du dv ≤ (Real.pi / L) ^ 2) (n : ℕ) :
    ¬ IsUnstableMode J du dv (neumannWavenumber L n)
Uses 7
Statement usesLinearly unstable Fourier mode · Upper end of the unstable wavenumber band · Neumann wavenumber on an interval
Proof usesDiscriminant of the dispersion polynomial · Lower end of the unstable wavenumber band · Finite domain · Homogeneous mode is stable for stable kinetics

TheoremLong intervals have a squared Neumann wavenumber in any given band#✓fully proved

Every long enough interval has a squared Neumann wavenumber inside a given nonempty open band (qlo, qhi) with 0 < qhi: there is L₀ > 0 such that for all L ≥ L₀ some (n π / L)² lies in (qlo, qhi).

theorem exists_neumann_mem_band {qlo qhi : ℝ} (hlt : qlo < qhi) (hpos : 0 < qhi) :
    ∃ L₀ : ℝ, 0 < L₀ ∧ ∀ L, L₀ ≤ L → ∃ n : ℕ, qlo < (n * Real.pi / L) ^ 2 ∧
      (n * Real.pi / L) ^ 2 < qhi
Used by 1
Used byLarge domains pattern

TheoremLarge domains pattern#✓fully proved

Under Turing's criterion, every long enough interval [0, L] has an unstable Neumann mode.

theorem exists_isUnstableMode_neumannWavenumber {J : Matrix (Fin 2) (Fin 2) ℝ} {du dv : ℝ}
    (hdu : 0 < du) (hdv : 0 < dv) (htr : J.trace < 0) (_hdet : 0 < J.det)
    (h : 2 * Real.sqrt (du * dv * J.det) < dv * J 0 0 + du * J 1 1) :
    ∃ L₀ : ℝ, 0 < L₀ ∧ ∀ L, L₀ ≤ L → ∃ n : ℕ, IsUnstableMode J du dv (neumannWavenumber L n)
Uses 8
Statement usesLinearly unstable Fourier mode · Neumann wavenumber on an interval
Proof usesDiscriminant of the dispersion polynomial · Lower end of the unstable wavenumber band · Upper end of the unstable wavenumber band · Long intervals have a squared Neumann wavenumber in any given band · Finite domain · Turing condition in squared form

Schnakenberg kinetics

DefinitionSchnakenberg reaction kinetics#✓fully proved

Schnakenberg's reaction terms (f, g) = (a - u + u² v, b - u² v) as a map on x = (u, v) : Fin 2 → ℝ, with source rates a, b (biologically a, b > 0).

def schnakenberg (a b : ℝ) (x : Fin 2 → ℝ) : Fin 2 → ℝ :=
  ![a - x 0 + x 0 ^ 2 * x 1, b - x 0 ^ 2 * x 1]
Used by 2
Used byComputation of the Schnakenberg Jacobian at the steady state · Schnakenberg steady state is an equilibrium

DefinitionSteady state of the Schnakenberg kinetics#✓fully proved

The homogeneous steady state (u₀, v₀) = (a + b, b / (a + b)²) of the Schnakenberg kinetics (meaningful for a + b ≠ 0; at a + b = 0 the division gives the junk v₀ = 0).

noncomputable def schnakenbergSteadyState (a b : ℝ) : Fin 2 → ℝ :=
  ![a + b, b / (a + b) ^ 2]
Used by 2
Used byComputation of the Schnakenberg Jacobian at the steady state · Schnakenberg steady state is an equilibrium

DefinitionJacobian of the Schnakenberg kinetics at its steady state#✓fully proved

The Jacobian of the Schnakenberg kinetics at its steady state, [[(b - a) / (a + b), (a + b)²], [-2 b / (a + b), -(a + b)²]].

noncomputable def schnakenbergJacobian (a b : ℝ) : Matrix (Fin 2) (Fin 2) ℝ :=
  !![(b - a) / (a + b), (a + b) ^ 2; -(2 * b) / (a + b), -(a + b) ^ 2]
Used by 4
Used byDeterminant of the Schnakenberg Jacobian · Computation of the Schnakenberg Jacobian at the steady state · Turing instability of the Schnakenberg kinetics · Stability of the Schnakenberg steady state without diffusion

TheoremSchnakenberg steady state is an equilibrium#✓fully proved

(a + b, b / (a + b)²) is a steady state of the Schnakenberg kinetics when a + b ≠ 0.

theorem schnakenberg_steadyState {a b : ℝ} (hab : a + b ≠ 0) :
    schnakenberg a b (schnakenbergSteadyState a b) = 0
Uses 2
Statement usesSchnakenberg reaction kinetics · Steady state of the Schnakenberg kinetics

TheoremComputation of the Schnakenberg Jacobian at the steady state#✓fully proved

The Jacobian matrix of the Schnakenberg kinetics at the steady state is schnakenbergJacobian a b.

theorem jacobianMatrix_schnakenberg {a b : ℝ} (hab : a + b ≠ 0) :
    MetaMathlibExt.jacobianMatrix (schnakenberg a b) (schnakenbergSteadyState a b) =
      schnakenbergJacobian a b
Uses 4
Statement usesSchnakenberg reaction kinetics · Jacobian of the Schnakenberg kinetics at its steady state · Steady state of the Schnakenberg kinetics · Jacobian matrix

TheoremDeterminant of the Schnakenberg Jacobian#✓fully proved

det J = (a + b)² for the Schnakenberg Jacobian (a + b ≠ 0).

theorem det_schnakenbergJacobian {a b : ℝ} (hab : a + b ≠ 0) :
    (schnakenbergJacobian a b).det = (a + b) ^ 2
Uses 1 · Used by 1
Statement usesJacobian of the Schnakenberg kinetics at its steady state
Used byTuring instability of the Schnakenberg kinetics

TheoremStability of the Schnakenberg steady state without diffusion#✓fully proved

The Schnakenberg steady state is stable without diffusion iff b - a < (a + b)³ (for 0 < a + b; then 0 < det J automatically).

theorem trace_schnakenbergJacobian_neg_iff {a b : ℝ} (hab : 0 < a + b) :
    (schnakenbergJacobian a b).trace < 0 ↔ b - a < (a + b) ^ 3
Uses 1 · Used by 1
Statement usesJacobian of the Schnakenberg kinetics at its steady state
Used byTuring instability of the Schnakenberg kinetics

TheoremTuring instability of the Schnakenberg kinetics#✓fully proved

Turing instability of the Schnakenberg kinetics (Murray 2003, ch. 2). With d_u = 1, d_v = d > 0, 0 < a + b and b - a < (a + b)³ (stable without diffusion), some Fourier mode is unstable iff 2 √d (a + b)² < d (b - a) - (a + b)³.

theorem schnakenberg_turing_iff {a b d : ℝ} (hab : 0 < a + b) (hstab : b - a < (a + b) ^ 3)
    (hd : 0 < d) :
    (∃ k, IsUnstableMode (schnakenbergJacobian a b) 1 d k) ↔
      2 * Real.sqrt d * (a + b) ^ 2 < d * (b - a) - (a + b) ^ 3
Uses 5
Statement usesLinearly unstable Fourier mode · Jacobian of the Schnakenberg kinetics at its steady state
Proof usesDeterminant of the Schnakenberg Jacobian · Turing's criterion · Stability of the Schnakenberg steady state without diffusion

Gierer–Meinhardt kinetics

DefinitionGierer–Meinhardt activator-inhibitor kinetics#✓fully proved

Gierer–Meinhardt activator-inhibitor kinetics in Murray's nondimensional form (f, g) = (a - b u + u² / v, u² - v) on x = (u, v) (biologically a, b > 0 and u, v > 0; at v = 0 the division gives the junk u² / 0 = 0).

noncomputable def giererMeinhardt (a b : ℝ) (x : Fin 2 → ℝ) : Fin 2 → ℝ :=
  ![a - b * x 0 + x 0 ^ 2 / x 1, x 0 ^ 2 - x 1]
Used by 2
Used byGierer–Meinhardt steady state is an equilibrium · Computation of the Gierer–Meinhardt Jacobian at the steady state

DefinitionSteady state of the Gierer–Meinhardt kinetics#✓fully proved

The homogeneous steady state (u₀, v₀) = ((a + 1) / b, ((a + 1) / b)²) of the Gierer–Meinhardt kinetics (meaningful for b ≠ 0, a + 1 ≠ 0).

noncomputable def giererMeinhardtSteadyState (a b : ℝ) : Fin 2 → ℝ :=
  ![(a + 1) / b, ((a + 1) / b) ^ 2]
Used by 2
Used byGierer–Meinhardt steady state is an equilibrium · Computation of the Gierer–Meinhardt Jacobian at the steady state

DefinitionJacobian of the Gierer–Meinhardt kinetics at its steady state#✓fully proved

The Jacobian of the Gierer–Meinhardt kinetics at its steady state, [[b (1 - a) / (1 + a), -(b / (a + 1))²], [2 (a + 1) / b, -1]].

noncomputable def giererMeinhardtJacobian (a b : ℝ) : Matrix (Fin 2) (Fin 2) ℝ :=
  !![b * (1 - a) / (1 + a), -(b / (a + 1)) ^ 2; 2 * (a + 1) / b, -1]
Used by 4
Used byDeterminant of the Gierer–Meinhardt Jacobian · Turing instability of the Gierer–Meinhardt kinetics · Computation of the Gierer–Meinhardt Jacobian at the steady state · Stability of the Gierer–Meinhardt steady state without diffusion

TheoremGierer–Meinhardt steady state is an equilibrium#✓fully proved

((a + 1) / b, ((a + 1) / b)²) is a steady state of the Gierer–Meinhardt kinetics when a + 1 ≠ 0 and b ≠ 0.

theorem giererMeinhardt_steadyState {a b : ℝ} (ha : a + 1 ≠ 0) (hb : b ≠ 0) :
    giererMeinhardt a b (giererMeinhardtSteadyState a b) = 0
Uses 2
Statement usesGierer–Meinhardt activator-inhibitor kinetics · Steady state of the Gierer–Meinhardt kinetics

TheoremComputation of the Gierer–Meinhardt Jacobian at the steady state#✓fully proved

The Jacobian matrix of the Gierer–Meinhardt kinetics at the steady state is giererMeinhardtJacobian a b.

theorem jacobianMatrix_giererMeinhardt {a b : ℝ} (ha : a + 1 ≠ 0) (hb : b ≠ 0) :
    MetaMathlibExt.jacobianMatrix (giererMeinhardt a b) (giererMeinhardtSteadyState a b) =
      giererMeinhardtJacobian a b
Uses 4
Statement usesGierer–Meinhardt activator-inhibitor kinetics · Jacobian of the Gierer–Meinhardt kinetics at its steady state · Steady state of the Gierer–Meinhardt kinetics · Jacobian matrix

TheoremDeterminant of the Gierer–Meinhardt Jacobian#✓fully proved

det J = b for the Gierer–Meinhardt Jacobian (a + 1 ≠ 0, b ≠ 0).

theorem det_giererMeinhardtJacobian {a b : ℝ} (ha : a + 1 ≠ 0) (hb : b ≠ 0) :
    (giererMeinhardtJacobian a b).det = b
Uses 1 · Used by 1
Statement usesJacobian of the Gierer–Meinhardt kinetics at its steady state
Used byTuring instability of the Gierer–Meinhardt kinetics

TheoremStability of the Gierer–Meinhardt steady state without diffusion#✓fully proved

The Gierer–Meinhardt steady state is stable without diffusion iff b (1 - a) < 1 + a (for 0 < a + 1; then 0 < det J = b for 0 < b).

theorem trace_giererMeinhardtJacobian_neg_iff {a b : ℝ} (ha : 0 < a + 1) :
    (giererMeinhardtJacobian a b).trace < 0 ↔ b * (1 - a) < 1 + a
Uses 1 · Used by 1
Statement usesJacobian of the Gierer–Meinhardt kinetics at its steady state
Used byTuring instability of the Gierer–Meinhardt kinetics

TheoremTuring instability of the Gierer–Meinhardt kinetics#✓fully proved

With d_u = 1, d_v = d > 0, 0 < a + 1, 0 < b and b (1 - a) < 1 + a (stable without diffusion), some Fourier mode is unstable iff 2 √(d b) < d b (1 - a) / (1 + a) - 1.

theorem giererMeinhardt_turing_iff {a b d : ℝ} (ha : 0 < a + 1) (hb : 0 < b)
    (hstab : b * (1 - a) < 1 + a) (hd : 0 < d) :
    (∃ k, IsUnstableMode (giererMeinhardtJacobian a b) 1 d k) ↔
      2 * Real.sqrt (d * b) < d * (b * (1 - a) / (1 + a)) - 1
Uses 5
Statement usesLinearly unstable Fourier mode · Jacobian of the Gierer–Meinhardt kinetics at its steady state
Proof usesDeterminant of the Gierer–Meinhardt Jacobian · Turing's criterion · Stability of the Gierer–Meinhardt steady state without diffusion

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.