1.2. Messages🔗

Messages are typed by engine index. The total message type MailboxActors.TotalMsg is the dependent sum Σ (i : 𝕀). Msg_i, collecting all payloads across engine types into a single universe.

A MailboxActors.Message is a packet in transit, carrying a sender address, a target address, and a TotalMsg payload.

The MailboxActors.Append wrapper distinguishes mailbox-level messages from processing-level messages: a mailbox engine for type i receives Append(Msg_i), making the indirection explicit in the type.