Goldbeter–Koshland ultrasensitivity

DefinitionRate ratio at a given steady-state modified fraction#✓fully proved

The value of V₁ / V₂ for which the mole fraction W of modified protein is at steady state (Goldbeter–Koshland 1981, Eq. 8): W (1 - W + K₁) / ((1 - W) (W + K₂)). Meaningful for 0 < W < 1 and K₁, K₂ > 0; at W = 1 Lean's a / 0 = 0 gives the junk value 0.

noncomputable def rateRatio (K₁ K₂ W : ℝ) : ℝ :=
  W * (1 - W + K₁) / ((1 - W) * (W + K₂))

Used by 7

Used byUniqueness of the steady state · Equal maximal rates · The Goldbeter–Koshland function is a steady state · Response coefficient of a covalent modification cycle · The response coefficient · Steady state of the modification cycle · Rate ratio is strictly increasing in the modified fraction

DefinitionGoldbeter–Koshland function#✓fully proved

The Goldbeter–Koshland function: the steady-state mole fraction of modified protein when V₁ / V₂ = v (Goldbeter–Koshland 1981, Eq. 7, rationalized so that it also covers v = 1, Eq. 9). Meaningful for v, K₁, K₂ > 0.

noncomputable def goldbeterKoshland (v K₁ K₂ : ℝ) : ℝ :=
  2 * v * K₂ / (√((v - 1 - K₁ - K₂ * v) ^ 2 + 4 * (v - 1) * v * K₂) - (v - 1 - K₁ - K₂ * v))

Used by 4

Used byUniqueness of the steady state · Goldbeter–Koshland function lies strictly between 0 and 1 · Equal maximal rates · The Goldbeter–Koshland function is a steady state

DefinitionResponse coefficient of a covalent modification cycle#✓fully proved

The response coefficient R_v: the ratio of the values of V₁ / V₂ giving 90% and 10% modified protein at steady state (Goldbeter–Koshland 1981).

noncomputable def responseCoefficient (K₁ K₂ : ℝ) : ℝ :=
  rateRatio K₁ K₂ 0.9 / rateRatio K₁ K₂ 0.1

Uses 1 · Used by 5

Statement usesRate ratio at a given steady-state modified fraction

Used byResponse coefficient exceeds 1 · The response coefficient · Response coefficient is below the Michaelis–Menten value 81 · First-order limit · Zero-order ultrasensitivity

DefinitionHill response function#✓fully proved

The fraction of a Hill response Sⁿ / (Kⁿ + Sⁿ) with half-saturation constant K and Hill coefficient n (meaningful for S, K > 0, n > 0).

noncomputable def hill (n K S : ℝ) : ℝ :=
  S ^ n / (K ^ n + S ^ n)

Used by 2

Used byHill response coefficient · Michaelis–Menten response

TheoremSteady state of the modification cycle#✓fully proved

Steady state of the modification cycle (Goldbeter–Koshland 1981, Eq. 8). For V₂ > 0, K₁, K₂ > 0 and 0 < W < 1, modification and demodification balance, V₁ (1 - W) / (K₁ + 1 - W) = V₂ W / (K₂ + W), iff V₁ / V₂ = rateRatio K₁ K₂ W.

theorem steadyState_iff {V₁ V₂ K₁ K₂ W : ℝ} (hV₂ : 0 < V₂) (hK₁ : 0 < K₁) (hK₂ : 0 < K₂)
    (hW0 : 0 < W) (hW1 : W < 1) :
    V₁ * (1 - W) / (K₁ + (1 - W)) = V₂ * W / (K₂ + W) ↔ V₁ / V₂ = rateRatio K₁ K₂ W

Uses 1

Statement usesRate ratio at a given steady-state modified fraction

TheoremRate ratio is strictly increasing in the modified fraction#✓fully proved

rateRatio K₁ K₂ is strictly increasing on (0, 1) for K₁, K₂ > 0: it is the product of the positive increasing functions W / (W + K₂) and 1 + K₁ / (1 - W).

theorem strictMonoOn_rateRatio {K₁ K₂ : ℝ} (hK₁ : 0 < K₁) (hK₂ : 0 < K₂) :
    StrictMonoOn (rateRatio K₁ K₂) (Ioo 0 1)

Uses 1 · Used by 1

Statement usesRate ratio at a given steady-state modified fraction

Used byUniqueness of the steady state

TheoremGoldbeter–Koshland function lies strictly between 0 and 1#✓fully proved

For v, K₁, K₂ > 0 the Goldbeter–Koshland function lies in (0, 1).

theorem goldbeterKoshland_mem_Ioo {v K₁ K₂ : ℝ} (hv : 0 < v) (hK₁ : 0 < K₁) (hK₂ : 0 < K₂) :
    goldbeterKoshland v K₁ K₂ ∈ Ioo 0 1

Uses 1 · Used by 2

Statement usesGoldbeter–Koshland function

Used byUniqueness of the steady state · The Goldbeter–Koshland function is a steady state

TheoremThe Goldbeter–Koshland function is a steady state#✓fully proved

The Goldbeter–Koshland function is a steady state (Goldbeter–Koshland 1981, Eq. 7): for v, K₁, K₂ > 0, rateRatio K₁ K₂ (goldbeterKoshland v K₁ K₂) = v.

theorem rateRatio_goldbeterKoshland {v K₁ K₂ : ℝ} (hv : 0 < v) (hK₁ : 0 < K₁) (hK₂ : 0 < K₂) :
    rateRatio K₁ K₂ (goldbeterKoshland v K₁ K₂) = v

Uses 3 · Used by 1

Statement usesGoldbeter–Koshland function · Rate ratio at a given steady-state modified fraction

Proof usesGoldbeter–Koshland function lies strictly between 0 and 1

Used byUniqueness of the steady state

TheoremUniqueness of the steady state#✓fully proved

Uniqueness of the steady state (Goldbeter–Koshland 1981, Eq. 7). For K₁, K₂ > 0, if 0 < W < 1 and rateRatio K₁ K₂ W = v with v > 0, then W is the Goldbeter–Koshland function.

theorem eq_goldbeterKoshland {v K₁ K₂ W : ℝ} (hv : 0 < v) (hK₁ : 0 < K₁) (hK₂ : 0 < K₂)
    (hW : W ∈ Ioo 0 1) (h : rateRatio K₁ K₂ W = v) : W = goldbeterKoshland v K₁ K₂

Uses 5 · Used by 1

Statement usesGoldbeter–Koshland function · Rate ratio at a given steady-state modified fraction

Proof usesGoldbeter–Koshland function lies strictly between 0 and 1 · The Goldbeter–Koshland function is a steady state · Rate ratio is strictly increasing in the modified fraction

Used byEqual maximal rates

TheoremEqual maximal rates#✓fully proved

Equal maximal rates (Goldbeter–Koshland 1981, Eq. 9): for V₁ = V₂ and K₁, K₂ > 0 the steady-state modified fraction is K₂ / (K₁ + K₂).

theorem goldbeterKoshland_one {K₁ K₂ : ℝ} (hK₁ : 0 < K₁) (hK₂ : 0 < K₂) :
    goldbeterKoshland 1 K₁ K₂ = K₂ / (K₁ + K₂)

Uses 3

Statement usesGoldbeter–Koshland function

Proof usesUniqueness of the steady state · Rate ratio at a given steady-state modified fraction

TheoremThe response coefficient#✓fully proved

The response coefficient (Goldbeter–Koshland 1981, Eq. 10): for K₁, K₂ > -0.1, R_v = 81 (K₁ + 0.1)(K₂ + 0.1) / ((K₁ + 0.9)(K₂ + 0.9)).

theorem responseCoefficient_eq {K₁ K₂ : ℝ} (hK₁ : -0.1 < K₁) (hK₂ : -0.1 < K₂) :
    responseCoefficient K₁ K₂ = 81 * (K₁ + 0.1) * (K₂ + 0.1) / ((K₁ + 0.9) * (K₂ + 0.9))

Uses 2 · Used by 4

Statement usesResponse coefficient of a covalent modification cycle

Proof usesRate ratio at a given steady-state modified fraction

Used byResponse coefficient exceeds 1 · Response coefficient is below the Michaelis–Menten value 81 · First-order limit · Zero-order ultrasensitivity

TheoremResponse coefficient exceeds 1#✓fully proved

For K₁, K₂ > 0 the response coefficient exceeds 1: the switch is never infinitely sharp.

theorem one_lt_responseCoefficient {K₁ K₂ : ℝ} (hK₁ : 0 < K₁) (hK₂ : 0 < K₂) :
    1 < responseCoefficient K₁ K₂

Uses 2

Statement usesResponse coefficient of a covalent modification cycle

Proof usesThe response coefficient

TheoremResponse coefficient is below the Michaelis–Menten value 81#✓fully proved

For K₁, K₂ > 0 the response coefficient is below the Michaelis–Menten value 81.

theorem responseCoefficient_lt_81 {K₁ K₂ : ℝ} (hK₁ : 0 < K₁) (hK₂ : 0 < K₂) :
    responseCoefficient K₁ K₂ < 81

Uses 2

Statement usesResponse coefficient of a covalent modification cycle

Proof usesThe response coefficient

TheoremFirst-order limit#✓fully proved

As both K₁, K₂ → ∞ the response coefficient tends to 81, the value of a Michaelis–Menten response.

theorem tendsto_responseCoefficient_atTop :
    Tendsto (fun p : ℝ × ℝ => responseCoefficient p.1 p.2) (atTop ×ˢ atTop) (𝓝 81)

Uses 2

Statement usesResponse coefficient of a covalent modification cycle

Proof usesThe response coefficient

TheoremZero-order ultrasensitivity#✓fully proved

As both K₁, K₂ → 0 the response coefficient tends to 1.

theorem tendsto_responseCoefficient_zero :
    Tendsto (fun p : ℝ × ℝ => responseCoefficient p.1 p.2) (𝓝 (0, 0)) (𝓝 1)

Uses 2

Statement usesResponse coefficient of a covalent modification cycle

Proof usesThe response coefficient

TheoremHill response coefficient#✓fully proved

Hill response coefficient (Goldbeter–Koshland 1981, Eq. 11). For a Hill response with n > 0 and K > 0, if S₉, S₁ > 0 give 90% and 10% response, then S₉ / S₁ = 81 ^ (1 / n).

theorem hill_ratio_eq {n K S₉ S₁ : ℝ} (hn : 0 < n) (hK : 0 < K) (hS₉ : 0 < S₉) (hS₁ : 0 < S₁)
    (h₉ : hill n K S₉ = 0.9) (h₁ : hill n K S₁ = 0.1) : S₉ / S₁ = 81 ^ (1 / n)

Uses 1 · Used by 1

Statement usesHill response function

Used byMichaelis–Menten response

TheoremMichaelis–Menten response#✓fully proved

Michaelis–Menten response (n = 1): going from 10% to 90% of the response takes an 81-fold increase of the stimulus.

theorem michaelisMenten_ratio_eq {K S₉ S₁ : ℝ} (hK : 0 < K) (hS₉ : 0 < S₉) (hS₁ : 0 < S₁)
    (h₉ : hill 1 K S₉ = 0.9) (h₁ : hill 1 K S₁ = 0.1) : S₉ / S₁ = 81

Uses 2

Statement usesHill response function

Proof usesHill response coefficient

17 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.