of_list (KIL4: literal-to-register simulation of register programs)

The following holds (Lean statement, in the scope of module Solutions.KIL4Sim):

theorem NLogN.KIL.PV.of_list {l : List (Fin HS × ℤ)} {s : IState HS}
    (h : ∀ p ∈ l, ∃ L, s.G p.1 = .int p.2 :: L) : PV (pmOf l) s

Context. The lemma belongs to the part KIL4: literal-to-register simulation of register programs: The KIL1–KIL3 programs carry the sizes of a configuration (field sizes, volumes, the modulus, pass counts, …) as literals Ex.lit v. A uniform program reads them from parameter stacks instead. RSim π p p' says that p' is p with some literal occurrences .lit v replaced by register reads .reg i, where the parameter map π says π i = some v.

Formalization Note. This lemma belongs to layer 5 of the Lean formalization (integer-multiplication-kappa campaign) of the OpenAI preprint Integer multiplication below $n\log n$: the uniform item-language machine (register programs over the NLogN multitape framework) assembling the Proposition 14 / Lemma 13 / Proposition 18 pieces, the resampling and chirp stages and the cost recurrences into one fixed machine, culminating in NLogN.KFTop.kappa_bound : IntMul.KappaBound (1 / 2 ^ 182) (the bound of Def_IntMul_MultitapeModel). All names refer to the definition bundles up to IntMul_Kappa_K_Defs33.