Functionals of T rounds (EPI-4)

The COBRA–BIPS duality reverses the sampled rounds: time reversal of i.i.d. uniform rounds is the core's Dynamics.expList_comp_reverse (FND-6). Its pathwise form only holds on lists of the right length, so the comparison uses that expList α T only evaluates its functional on lists of length T.

theorem Epidemics.expList_congr_length {α : Type u_1} [Fintype α] (T : ℕ) {F G : List α → ℝ} (h : ∀ (l : List α), l.length = T → F l = G l) : Dynamics.expList α T F = Dynamics.expList α T G

expList α T only evaluates its functional on lists of length T.