Fixed tuples of radix registers

The number of registers and their enumeration are fixed independently of the input. Packing and reading a fixed digit therefore require only finitely many binary additions, multiplications, divisions and remainders. The radix itself remains an ordinary binary argument.

The pure operations and their recovery/capacity results live in Cslib.Radix, in the module CslibFrontier.Foundations.Data.Nat.Radix.

Main results

• Turing.MultiTapeNTM.ConfigurationGraph.digit_inSpace: fixed-position digit extraction.
• Turing.MultiTapeNTM.ConfigurationGraph.component_inSpace: finite-tuple component extraction.
• Turing.MultiTapeNTM.ConfigurationGraph.pack_inSpace: finite-tuple packing.

theorem Turing.MultiTapeNTM.ConfigurationGraph.digit_inSpace (i : ℕ) : MultiTapeTM.ComputableInSpace (fun (p : ℕ × ℕ) => Cslib.Radix.digit p.1 p.2 i) (MultiTapeTM.encPair MultiTapeTM.encNat MultiTapeTM.encNat) MultiTapeTM.encNat fun (p : ℕ × ℕ) => ((MultiTapeTM.encPair MultiTapeTM.encNat MultiTapeTM.encNat) p).length

Reading a fixed digit uses linear space in the binary radix and packed value.

theorem Turing.MultiTapeNTM.ConfigurationGraph.component_inSpace {ι : Type} [Fintype ι] (i : ι) : MultiTapeTM.ComputableInSpace (fun (p : ℕ × ℕ) => Cslib.Radix.component p.1 p.2 i) (MultiTapeTM.encPair MultiTapeTM.encNat MultiTapeTM.encNat) MultiTapeTM.encNat fun (p : ℕ × ℕ) => ((MultiTapeTM.encPair MultiTapeTM.encNat MultiTapeTM.encNat) p).length

Reading any one fixed component is a native deterministic linear-space routine.

theorem Turing.MultiTapeNTM.ConfigurationGraph.pack_inSpace {ι : Type} [Fintype ι] {α : Type} {enc : α ↪ List Bool} {S B : α → ℕ} {f : α → ι → ℕ} (hB : MultiTapeTM.ComputableInSpace B enc MultiTapeTM.encNat S) (hf : ∀ (i : ι), MultiTapeTM.ComputableInSpace (fun (a : α) => f a i) enc MultiTapeTM.encNat S) (hin : MultiTapeTM.BigOLe (fun (a : α) => (enc a).length) S) : MultiTapeTM.ComputableInSpace (fun (a : α) => Cslib.Radix.pack (B a) (f a)) enc MultiTapeTM.encNat S

Packing a fixed tuple of computed components preserves a common space budget.