valid (Lemma 12 (arbitrary-width interchange), generic array-model lemmas)
ProvedAModelL12.ShapeLE.validThe following holds (Lean statement, in the scope of module Solutions.AModelL12Basic):
theorem AModelL12.ShapeLE.valid {S T : Shape} (h : ShapeLE S T) {a : List ℕ} (ha : AModel.Valid S a) :
AModel.Valid T a
Context. The lemma belongs to the part Lemma 12 (arbitrary-width interchange), generic array-model lemmas: 1. decode_append, encode_append_len; pull_prefix (a pull acting only after a prefix does
not see how the prefix is split into fields), pull_blockSwap_prefix.
2. Embedding a small shape into a pointwise larger one (embed, zero/default filled) and
extracting back (pull T S id): extract_pull_embed — for every address map preserving
the small-shape validity, embed → pull → extract = pull on the original.
This is both the row padding R → R' and the binary padding [2^u] → [q^e].
3. Adjacent block swaps compose (blockSwap_blockSwap_adj); a list of aligned pieces
(runPieces) composes to the swap of the whole chunks (runPieces_eq).
4. Block rotation rotIdx (the joining moves) on lists, validity, inverse.
Formalization Note. This lemma belongs to layer 5 of the Lean formalization (integer-multiplication-kappa campaign) of the OpenAI preprint Integer multiplication below : 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.
-- OpenAI-preprint / κ-improvement development (integer-multiplication-kappa), generated by skeleton subtraction.
import Definitions.Def_IntMul_Kappa_K_Defs33
set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000
open AModelL12
open AModel
variable {α : Type*}
theorem AModelL12.ShapeLE.valid {S T : Shape} (h : ShapeLE S T) {a : List ℕ} (ha : AModel.Valid S a) :
AModel.Valid T a := by sorry