Coherent feed-forward loop

DefinitionVariation-of-constants solution of a linear relaxation equation#✓fully proved

The variation-of-constants solution of z' = P(t) - α z, z(0) = z₀: z(t) = z₀ e^{-α t} + ∫₀ᵗ e^{-α (t - s)} P(s) ds. Used for t ≥ 0.

noncomputable def relaxation (α : ℝ) (P : ℝ → ℝ) (z₀ t : ℝ) : ℝ :=
  z₀ * exp (-α * t) + ∫ s in (0)..t, exp (-α * (t - s)) * P s

Used by 8

Used byFeed-forward loop target after an OFF step · Feed-forward loop target after an ON step · Delayed rise · ON delay · Relaxation solution satisfies its differential equation · Simple-regulation target after an OFF step · Simple-regulation target after an ON step · Simple regulation responds without delay

TheoremRelaxation solution satisfies its differential equation#✓fully proved

The relaxation solves z' = P - α z at every time where the (locally integrable) production rate P is continuous.

theorem hasDerivAt_relaxation {α : ℝ} {P : ℝ → ℝ} (z₀ : ℝ)
    (hP : ∀ a b, IntervalIntegrable P volume a b) {t : ℝ} (ht : ContinuousAt P t) :
    HasDerivAt (relaxation α P z₀) (P t - α * relaxation α P z₀ t) t

Uses 1

Statement usesVariation-of-constants solution of a linear relaxation equation

DefinitionAND-gate production rate in the logic approximation#✓fully proved

AND-gate production in the logic approximation: rate β when K_x < x and K_y < y, else 0.

noncomputable def andGate (Kx Ky β x y : ℝ) : ℝ :=
  if Kx < x ∧ Ky < y then β else 0

Used by 5

Used byFeed-forward loop target after an OFF step · No OFF delay · Feed-forward loop target after an ON step · Delayed rise · ON delay

DefinitionSingle-input production rate in the logic approximation#✓fully proved

Single-input production in the logic approximation: rate β when K_x < x, else 0.

noncomputable def simpleGate (Kx β x : ℝ) : ℝ :=
  if Kx < x then β else 0

Used by 4

Used byNo OFF delay · Simple-regulation target after an OFF step · Simple-regulation target after an ON step · Simple regulation responds without delay

DefinitionIntermediate factor after an ON step#✓fully proved

Y after an ON step of Sx from Y(0) = 0: Y(t) = (β_y/α_y)(1 - e^{-α_y t}).

noncomputable def yOn (αy βy t : ℝ) : ℝ :=
  βy / αy * (1 - exp (-αy * t))

Used by 5

Used byFeed-forward loop target after an ON step · Delayed rise · ON delay · Intermediate factor solves its production–decay equation · Intermediate factor exceeds the threshold exactly after the ON delay

DefinitionON-step delay of the feed-forward loop#✓fully proved

The ON-step delay T_on = (1/α_y) log(1 / (1 - K_yz / Y_st)), Y_st = β_y/α_y: the time at which Y crosses the activation threshold K_yz of Z. Meaningful for 0 < K_yz < Y_st.

noncomputable def onDelay (αy βy Kyz : ℝ) : ℝ :=
  1 / αy * log (1 / (1 - Kyz / (βy / αy)))

Used by 4

Used byDelayed rise · ON delay · Positivity of the ON delay · Intermediate factor exceeds the threshold exactly after the ON delay

TheoremIntermediate factor solves its production–decay equation#✓fully proved

yOn solves Y' = β_y - α_y Y with Y(0) = 0 (for α_y ≠ 0; at α_y = 0 Lean's β_y / 0 = 0 makes yOn identically 0, which is not a solution).

theorem hasDerivAt_yOn {αy : ℝ} (hα : αy ≠ 0) (βy t : ℝ) :
    HasDerivAt (yOn αy βy) (βy - αy * yOn αy βy t) t ∧ yOn αy βy 0 = 0

Uses 1

Statement usesIntermediate factor after an ON step

TheoremPositivity of the ON delay#✓fully proved

The ON delay is positive.

theorem onDelay_pos {αy βy Kyz : ℝ} (hα : 0 < αy) (hβ : 0 < βy) (hK : 0 < Kyz)
    (hKs : Kyz < βy / αy) : 0 < onDelay αy βy Kyz

Uses 1 · Used by 1

Statement usesON-step delay of the feed-forward loop

Used byDelayed rise

TheoremIntermediate factor exceeds the threshold exactly after the ON delay#✓fully proved

Y exceeds K_yz exactly after the ON delay: K_yz < Y(t) ↔ T_on < t.

theorem yOn_gt_iff {αy βy Kyz : ℝ} (hα : 0 < αy) (hβ : 0 < βy)
    (hKs : Kyz < βy / αy) (t : ℝ) : Kyz < yOn αy βy t ↔ onDelay αy βy Kyz < t

Uses 2 · Used by 2

Statement usesON-step delay of the feed-forward loop · Intermediate factor after an ON step

Used byDelayed rise · ON delay

DefinitionFeed-forward loop target after an ON step#✓fully proved

The FFL target after an ON step of Sx at t = 0 from Y(0) = Z(0) = 0, with X* = 1 and K_xz < 1.

noncomputable def fflOn (αy βy αz βz Kxz Kyz t : ℝ) : ℝ :=
  relaxation αz (fun s ↦ andGate Kxz Kyz βz 1 (yOn αy βy s)) 0 t

Uses 3 · Used by 2

Statement usesAND-gate production rate in the logic approximation · Variation-of-constants solution of a linear relaxation equation · Intermediate factor after an ON step

Used byDelayed rise · ON delay

DefinitionSimple-regulation target after an ON step#✓fully proved

The simple-regulation target after an ON step of Sx at t = 0 from Z(0) = 0.

noncomputable def simpleOn (αz βz Kxz t : ℝ) : ℝ :=
  relaxation αz (fun _ ↦ simpleGate Kxz βz 1) 0 t

Uses 2 · Used by 1

Statement usesVariation-of-constants solution of a linear relaxation equation · Single-input production rate in the logic approximation

Used bySimple regulation responds without delay

TheoremON delay#✓fully proved

The FFL target stays at 0 until T_on.

theorem ffl_on_eq_zero {αy βy αz βz Kxz Kyz : ℝ} (hα : 0 < αy) (hβ : 0 < βy)
    (hKs : Kyz < βy / αy) {t : ℝ} (ht0 : 0 ≤ t) (ht : t ≤ onDelay αy βy Kyz) :
    fflOn αy βy αz βz Kxz Kyz t = 0

Uses 6

Statement usesFeed-forward loop target after an ON step · ON-step delay of the feed-forward loop

Proof usesAND-gate production rate in the logic approximation · Variation-of-constants solution of a linear relaxation equation · Intermediate factor after an ON step · Intermediate factor exceeds the threshold exactly after the ON delay

TheoremDelayed rise#✓fully proved

After T_on the FFL target relaxes from 0 towards β_z/α_z: Z(t) = (β_z/α_z)(1 - e^{-α_z (t - T_on)}) (for α_z > 0, K_xz < 1).

theorem ffl_on_eq {αy βy αz βz Kxz Kyz : ℝ} (hα : 0 < αy) (hβ : 0 < βy) (hK : 0 < Kyz)
    (hKs : Kyz < βy / αy) (hαz : 0 < αz) (hKxz : Kxz < 1) {t : ℝ}
    (ht : onDelay αy βy Kyz ≤ t) :
    fflOn αy βy αz βz Kxz Kyz t =
      βz / αz * (1 - exp (-αz * (t - onDelay αy βy Kyz)))

Uses 7

Statement usesFeed-forward loop target after an ON step · ON-step delay of the feed-forward loop

Proof usesAND-gate production rate in the logic approximation · Positivity of the ON delay · Variation-of-constants solution of a linear relaxation equation · Intermediate factor after an ON step · Intermediate factor exceeds the threshold exactly after the ON delay

TheoremSimple regulation responds without delay#✓fully proved

Simple regulation responds without delay: Z(t) = (β_z/α_z)(1 - e^{-α_z t}) > 0 for all t > 0.

theorem simple_on_pos {αz βz Kxz : ℝ} (hαz : 0 < αz) (hβz : 0 < βz) (hKxz : Kxz < 1) {t : ℝ}
    (ht : 0 < t) : 0 < simpleOn αz βz Kxz t

Uses 3

Statement usesSimple-regulation target after an ON step

Proof usesVariation-of-constants solution of a linear relaxation equation · Single-input production rate in the logic approximation

DefinitionFeed-forward loop target after an OFF step#✓fully proved

The FFL target after Sx is removed at t = 0 (X* = 0), starting from Z(0) = z₀, for an arbitrary trajectory Y of the intermediate factor.

noncomputable def fflOff (αz βz Kxz Kyz z₀ : ℝ) (Y : ℝ → ℝ) (t : ℝ) : ℝ :=
  relaxation αz (fun s ↦ andGate Kxz Kyz βz 0 (Y s)) z₀ t

Uses 2 · Used by 1

Statement usesAND-gate production rate in the logic approximation · Variation-of-constants solution of a linear relaxation equation

Used byNo OFF delay

DefinitionSimple-regulation target after an OFF step#✓fully proved

The simple-regulation target after Sx is removed at t = 0, from Z(0) = z₀.

noncomputable def simpleOff (αz βz Kxz z₀ t : ℝ) : ℝ :=
  relaxation αz (fun _ ↦ simpleGate Kxz βz 0) z₀ t

Uses 2 · Used by 1

Statement usesVariation-of-constants solution of a linear relaxation equation · Single-input production rate in the logic approximation

Used byNo OFF delay

TheoremNo OFF delay#✓fully proved

For a nonnegative threshold K_xz, whatever Y does, the FFL and simple regulation decay identically after an OFF step: Z(t) = z₀ e^{-α_z t}.

theorem ffl_off_eq_simple_off {αz βz Kxz Kyz z₀ : ℝ} (hKxz : 0 ≤ Kxz) (Y : ℝ → ℝ) (t : ℝ) :
    fflOff αz βz Kxz Kyz z₀ Y t = simpleOff αz βz Kxz z₀ t ∧
      simpleOff αz βz Kxz z₀ t = z₀ * exp (-αz * t)

Uses 4

Statement usesFeed-forward loop target after an OFF step · Simple-regulation target after an OFF step

Proof usesAND-gate production rate in the logic approximation · Single-input production rate in the logic approximation

17 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.