Definition A.2Bounded-unrolling recurrence: at most T updates in total from an input-independent initial state

79/-- WINDOW SIMULATION THEOREM.  For a valid L-layer cell with fan-ins/widths ≤ M reading80    the input block and the w most recent states, the state after T updates is computed by81    formulas with depth ≤ 3·L·T, size ≤ rnnSize W M L T, reading only the T input blocks. -/82theorem window_ac0 {W M : Nat} (cell : List Layer) (hv : NetValid W cell) (hb : NetBounded M cell)83    (n m w : Nat) (h0 : Nat → Bool) : ∀ T i,84    (∀ x : Nat → Bool, eval x (wCirc W cell n m w h0 T i) = wState cell n m w h0 x T i) ∧85    size (wCirc W cell n m w h0 T i) ≤ rnnSize W M cell.length T ∧86    depth (wCirc W cell n m w h0 T i) ≤ 3 * cell.length * T ∧87    maxInput (wCirc W cell n m w h0 T i) ≤ T * n := by88  intro T89  induction T using Nat.strongRecOn with90  | ind T ih =>91    intro i92    cases T with93    | zero => simp [wCirc.eq_1, wState.eq_1, rnnSize]94    | succ t =>95      -- the leaves of the last update96      let prev : Nat → Circ := fun j => if j < n then input (t * n + j) else if j < n + w * m then97        (if (j - n) / m ≤ t then wCirc W cell n m w h0 (t - (j - n) / m) ((j - n) % m) else const (h0 ((j - n) % m)))98        else const false99      have hprev : ∀ j, size (prev j) ≤ rnnSize W M cell.length t ∧ depth (prev j) ≤ 3 * cell.length * t ∧100          maxInput (prev j) ≤ (t + 1) * n := by101        intro j102        simp only [prev]103        split104        · simp; refine ⟨rnnSize_pos _ _ _ _, ?_⟩; rw [Nat.succ_mul]; omega105        · split106          · split107            · next hδ =>108              have hlt : t - (j - n) / m < t + 1 := Nat.lt_succ_of_le (Nat.sub_le _ _)109              have hle : t - (j - n) / m ≤ t := Nat.sub_le _ _110              obtain ⟨_, h2, h3, h4⟩ := ih (t - (j - n) / m) hlt ((j - n) % m)111              refine ⟨Nat.le_trans h2 (rnnSize_mono W M _ hle), Nat.le_trans h3 (Nat.mul_le_mul_left _ hle),112                Nat.le_trans h4 ?_⟩113              rw [Nat.succ_mul]; exact Nat.le_trans (Nat.mul_le_mul_right n hle) (Nat.le_add_right _ _)114            · simp; exact rnnSize_pos _ _ _ _115          · simp; exact rnnSize_pos _ _ _ _116      have hsd := compileNet_sd (W := W) cell hb prev (rnnSize W M cell.length t) (3 * cell.length * t)117        (fun j => (hprev j).1) (fun j => (hprev j).2.1) i118      have hmx := compileNet_max (W := W) cell prev ((t + 1) * n) (fun j => (hprev j).2.2) i119      refine ⟨fun x => ?_, ?_, ?_, ?_⟩120      · rw [wCirc_succ, wState_succ, eval_compileNet cell hv]121        congr 1122        funext j123        unfold winIn124        split125        · simp126        · split127          · split128            · next hδ => simp only [if_pos hδ]; exact (ih (t - (j - n) / m) (Nat.lt_succ_of_le (Nat.sub_le _ _)) ((j - n) % m)).1 x129            · next hδ => simp [hδ]130          · simp131      · rw [wCirc_succ]; simp only [rnnSize]; exact hsd.1132      · rw [wCirc_succ]; have := hsd.2; rw [Nat.mul_succ]; omega133      · rw [wCirc_succ]; exact hmx

135/-- Closed polynomial size bound for a fixed number T of updates. -/136theorem window_size_closed (W M L T : Nat) :137    rnnSize W M L T + 1 ≤ 2 * ((2 * W + 3) ^ L * (M + 1) ^ (W * L)) ^ T := rnnSize_closed W M L T

1006/-- BOUNDED-UNROLLING RECURRENCE (paper Definition RNN-formal with total unrolling T):1007    the state after T updates of a valid L-layer cell with fan-ins/widths ≤ M is1008    computed by formulas of depth ≤ 3 L T and size ≤ rnnSize W M L T, reading only1009    the inputs of the T blocks (indices < T n). -/1010theorem rnn_ac0 {W M : Nat} (cell : List Layer) (hv : NetValid W cell) (hb : NetBounded M cell)1011    (n : Nat) (h0 : Nat → Bool) : ∀ T i,1012    (∀ x : Nat → Bool, eval x (rnnCirc W cell n h0 T i) = rnnState cell n h0 x T i) ∧1013    size (rnnCirc W cell n h0 T i) ≤ rnnSize W M cell.length T ∧1014    depth (rnnCirc W cell n h0 T i) ≤ 3 * cell.length * T ∧1015    maxInput (rnnCirc W cell n h0 T i) ≤ T * n1016  | 0, i => ⟨fun x => eval_rnnCirc cell hv n h0 x 0 i, by simp [rnnCirc, rnnSize],1017      by simp [rnnCirc], by simp [rnnCirc]⟩1018  | T + 1, i => by1019    have ih := fun j => rnn_ac0 cell hv hb n h0 T j1020    have hp_size : ∀ j, size ((fun j => if j < n then input (T * n + j)1021        else rnnCirc W cell n h0 T (j - n)) j) ≤ rnnSize W M cell.length T := by1022      intro j; simp only; split1023      · simp; exact rnnSize_pos W M cell.length T1024      · exact (ih (j - n)).2.11025    have hp_depth : ∀ j, depth ((fun j => if j < n then input (T * n + j)1026        else rnnCirc W cell n h0 T (j - n)) j) ≤ 3 * cell.length * T := by1027      intro j; simp only; split1028      · simp1029      · exact (ih (j - n)).2.2.11030    have hp_max : ∀ j, maxInput ((fun j => if j < n then input (T * n + j)1031        else rnnCirc W cell n h0 T (j - n)) j) ≤ (T + 1) * n := by1032      intro j; simp only; split1033      · simp; rw [Nat.succ_mul]; omega1034      · have := (ih (j - n)).2.2.2; rw [Nat.succ_mul]; omega1035    have hb' := compileNet_sd (W := W) cell hb _ _ _ hp_size hp_depth i1036    have hm' := compileNet_max (W := W) cell _ _ hp_max i1037    refine ⟨fun x => eval_rnnCirc cell hv n h0 x (T + 1) i, ?_, ?_, ?_⟩1038    · simp only [rnnCirc, rnnSize]; exact hb'.11039    · simp only [rnnCirc]; have := hb'.2; rw [Nat.mul_succ]; omega1040    · simp only [rnnCirc]; exact hm'