feat(MultiTapeTM): loglogn_equals_no_space

Cslib.lean

@@ -99,6 +99,8 @@ public import Cslib.Computability.Machines.Turing.MultiTape.Combinators.Id
 public import Cslib.Computability.Machines.Turing.MultiTape.ConfigBound
 public import Cslib.Computability.Machines.Turing.MultiTape.Configuration
 public import Cslib.Computability.Machines.Turing.MultiTape.Deterministic
+public import Cslib.Computability.Machines.Turing.MultiTape.InputShortening
+public import Cslib.Computability.Machines.Turing.MultiTape.LoglognEqualsNoSpace
 public import Cslib.Computability.Machines.Turing.MultiTape.Nondeterministic
 public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.ClearWork
 public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.ExtendTapes
@@ -140,6 +142,7 @@ public import Cslib.Crypto.Protocols.SecretSharing.Defs
 public import Cslib.Crypto.Protocols.SecretSharing.Scheme
 public import Cslib.Crypto.Protocols.SecretSharing.Shamir
 public import Cslib.Crypto.Protocols.SecretSharing.Shamir.Polynomial
+public import Cslib.Foundations.Analysis.Asymptotics
 public import Cslib.Foundations.Combinatorics.InfiniteGraphRamsey
 public import Cslib.Foundations.Control.Monad.Free
 public import Cslib.Foundations.Control.Monad.Free.Effects

Cslib/Computability/Machines/Turing/MultiTape/ConfigBound.lean

@@ -232,6 +232,33 @@ lemma storageBound_le_pow [Fintype Symbol] [Fintype State] :
     ∃ a c : ℕ, ∀ s : ℕ, storageBound Symbol State k s ≤ a * 2 ^ (c * s) :=
   ⟨_, _, storageBound_le_base_mul_pow⟩
 
+/-- A fixed multiple of `(storageBound + 1) ^ storageBound` grows at most doubly exponentially
+in the space. -/
+lemma storageBound_pow_le_pow_pow [Fintype Symbol] [Fintype State] (m : ℕ) :
+    ∃ a c : ℕ, ∀ s : ℕ,
+      m * (storageBound Symbol State k s + 1) ^ storageBound Symbol State k s
+        ≤ 2 ^ (2 ^ (a + c * s)) := by
+  obtain ⟨a, c, hbound⟩ := storageBound_le_pow (Symbol := Symbol) (State := State) (k := k)
+  refine ⟨m + 2 * a + 1, 2 * c, fun s ↦ ?_⟩
+  let B := storageBound Symbol State k s
+  let E := m + 2 * a + 2 * c * s
+  have hB : B ≤ 2 ^ (a + c * s) := by
+    rw [pow_add]
+    exact (hbound s).trans (by gcongr; exact Nat.lt_two_pow_self.le)
+  have hsum : m + B * B ≤ 2 ^ (E + 1) := by
+    calc m + B * B
+      _ ≤ 2 ^ m + 2 ^ (a + c * s) * 2 ^ (a + c * s) := by
+        gcongr; exact Nat.lt_two_pow_self.le
+      _ = 2 ^ m + 2 ^ (2 * a + 2 * c * s) := by ring
+      _ ≤ 2 ^ E + 2 ^ E := by gcongr <;> omega
+      _ = 2 ^ (E + 1) := by ring
+  calc m * (B + 1) ^ B
+    _ ≤ 2 ^ m * (2 ^ B) ^ B := by
+      exact Nat.mul_le_mul Nat.lt_two_pow_self.le (Nat.pow_le_pow_left Nat.lt_two_pow_self B)
+    _ = 2 ^ (m + B * B) := by ring
+    _ ≤ 2 ^ (2 ^ (E + 1)) := by gcongr; omega
+    _ = _ := by dsimp [E]; ring
+
 /-! ## The storage and the core of a configuration
 
 Now we relate `Cfg` and `Storage` by giving the projection.

Cslib/Computability/Machines/Turing/MultiTape/Configuration.lean

@@ -60,6 +60,7 @@ the sub-linear space modifications from chapter 2.5 with the following changes:
     output tape
 * `Action`: what a machine does in one step
 * `Action.apply`: the effect of one action on a configuration
+* `HeadSymbols`, `Cfg.headSymbols`: the symbols under the heads, which a transition reads
 * `Cfg.Halted`, `Cfg.init`: halting, and the configuration a machine starts in
 
 ## References
@@ -198,6 +199,19 @@ lemma inputSymbolInner {cfg : Cfg k Symbol State input} (p : ℕ)
 def Cfg.workTapeSymbols (cfg : Cfg k Symbol State input) (i : Fin k) : Option Symbol :=
   cfg.workTapes i (cfg.workTapePos i)
 
+/-- The symbols under the heads of a machine with `k` work tapes, which its transitions read. -/
+@[ext]
+structure HeadSymbols (k : ℕ) (Symbol : Type*) where
+  /-- the symbol under the input head -/
+  inputSymbol : Option Symbol
+  /-- the symbols under the work-tape heads -/
+  workTapeSymbols : Fin k → Option Symbol
+
+/-- The symbols under the heads of a configuration. -/
+@[simps]
+def Cfg.headSymbols (cfg : Cfg k Symbol State input) : HeadSymbols k Symbol :=
+  ⟨cfg.inputSymbol, cfg.workTapeSymbols⟩
+
 /-- A configuration is halted when it has no state to continue from. -/
 abbrev Cfg.Halted (cfg : Cfg k Symbol State input) : Prop := cfg.state = none
 
@@ -212,19 +226,18 @@ output, so prepending to it preserves steps: cf. `Turing.MultiTapeNTM.prependOut
     {State' : Type*} (q : Option State') : Cfg k Symbol State' input :=
   ⟨q, cfg.inputPos, cfg.workTapes, cfg.workTapePos, cfg.output⟩
 
-/-- Forget the control state of a configuration, keeping the input head, the work tapes, the
-work-tape heads and the output. A property of this part of a configuration makes sense for every
-machine, whatever its state type. -/
-@[simps] def Cfg.forgetState (cfg : Cfg k Symbol State input) : Cfg k Symbol Unit input :=
-  ⟨some (), cfg.inputPos, cfg.workTapes, cfg.workTapePos, cfg.output⟩
-
 /-- Remap the (optional) state of a configuration through `φ`, leaving the input head, the work
 tapes, the work-tape heads and the output alone. Control-flow combinators such as `seq` embed a
 sub-machine's configurations into the combined machine by exactly such a state remap. -/
 @[simps] def Cfg.mapState {State' : Type*} (φ : Option State → Option State')
     (c : Cfg k Symbol State input) : Cfg k Symbol State' input :=
   ⟨φ c.state, c.inputPos, c.workTapes, c.workTapePos, c.output⟩
 
+/-- Remap the successor state of an action through `φ`, leaving its effect on the tapes alone. -/
+@[simps] def Action.mapState {State' : Type*} (φ : Option State → Option State')
+    (action : Action k Symbol State) : Action k Symbol State' :=
+  { action with state := φ action.state }
+
 /-- The initial configuration for a starting state and an input string. -/
 @[simp]
 def Cfg.init (q₀ : State) (input : List Symbol) : Cfg k Symbol State input :=