Sparse unbounded TM configurations in RAM registers

This is the fixed-layout representation used for the uniform TM-to-RAM simulation. Unlike the bounded dense layout, its addresses do not depend on an input length or running-time bound.

theorem Complexity.RAM.TMConfig.Sparse.fieldReg_injective {n : ℕ} : Function.Injective fieldReg

Distinct sparse fields occupy distinct RAM registers.

theorem Complexity.RAM.TMConfig.Sparse.encodeRegs_represents {n : ℕ} (tm : TM n) (cfg : Complexity.Cfg n tm.Q) : Represents tm cfg (encodeRegs tm cfg)

The canonical sparse encoding represents every state, head, and cell.

theorem Complexity.RAM.TMConfig.Sparse.decode_of_represents {n : ℕ} (tm : TM n) (cfg : Complexity.Cfg n tm.Q) (store : Structured.Store) (hrepresents : Represents tm cfg store) : decode tm store = cfg

Any representing sparse store decodes to its complete configuration; no external cell-window premise is needed.

theorem Complexity.RAM.TMConfig.Sparse.decode_encode {n : ℕ} (tm : TM n) (cfg : Complexity.Cfg n tm.Q) : decode tm (encodeRegs tm cfg) = cfg

Sparse encoding followed by decoding is exact for every configuration.