Concatenation law for the multiplication model's MSB-first bit encoding

For the exact IntMul.val defined by a left fold in base two on MSB-first Boolean words, concatenating two bit strings obeys val(x++y)=2^(length y)·val(x)+val(y). This identity is foundational for correctly reading split input records, proving output padding, converting between binary string conventions and verifying the tape-level arithmetic implementation. The result uses no multiplication speedup assumptions and is valid for empty strings and leading zeros.