Array blocks in ordinary initialized inputs

Main results

• WordRAM.Data.init_realizes_append: a list segment appears at its actual initialized address, including the machine's length header.

This is a representation lemma for the existing Data.init, with no alternate input convention. It lives in a narrow input-array module to keep the list getD dependency and initialization bridge out of Allocation. This avoids changing the allocation interface and rebuilding its unrelated importers when the input representation API changes.

theorem Cslib.WordRAM.Data.init_realizes_append {r : ℕ} (pre payload post : List ℕ) : { base := pre.length + 1, length := payload.length }.Realizes (init (pre ++ (payload ++ post))).mem payload.get

The payload between an arbitrary prefix and suffix occupies its corresponding actual input block. The extra address word is the standard unsigned input-length header.