Read-back: Def_IntMul_MultitapeModel (namespace IntMul)

The file depends only on Mathlib. It defines a model of deterministic multitape Turing machines, together with what it means for one of them to multiply $n$-bit integers within a step budget. The declarations are described below in source order.

---

1. Move

There are three possible head movements: left, stay and right. Equality between them is decidable.

---

2. MultitapeTM: a deterministic $k$-tape machine

A machine $M$ consists of the following data and conditions.

• Alphabet. A type $\Sigma$, assumed finite (a Fintype instance), with five named symbols: the blank $\square$, the start symbol $\triangleright$, the bit symbols $\mathtt{0}$ and $\mathtt{1}$, and the separator $\#$. The only condition is that these five are pairwise distinct. $\Sigma$ may contain any finite number of further symbols, which can serve as work symbols.
• States. A finite type $K$ with a start state $q_{\mathrm{start}}$ and a halting state $q_{\mathrm{halt}}$, where $q_{\mathrm{start}} \ne q_{\mathrm{halt}}$. No other states are named, and nothing else is required of $K$.
• Tapes. A natural number $k$ with $k \ge 2$. Each machine has its own fixed $k$. Tapes are indexed by $\{0,\dots,k-1\}$.
• Transition function. A total function

$$\delta : K \times \Sigma^{k} \to K \times (\Sigma \times \{\mathrm{left},\mathrm{stay},\mathrm{right}\})^{k}.$$

For $\delta(q,a) = (q', (\sigma_i, d_i)_{i<k})$, the value $\sigma_i$ is the symbol written on tape $i$ and $d_i$ is the move of head $i$.

The following conditions are imposed for every state $q$ (including $q_{\mathrm{halt}}$), every scanned tuple $a \in \Sigma^k$ and every tape $i$:

1. (start symbol preserved) If $a_i = \triangleright$, then $\sigma_i = \triangleright$ and $d_i \ne \mathrm{left}$.
2. (start symbol never newly written) If $a_i \ne \triangleright$, then $\sigma_i \ne \triangleright$.
3. (halt is frozen) For every $a$, $\delta(q_{\mathrm{halt}}, a) = (q_{\mathrm{halt}}, (a_i, \mathrm{stay})_{i<k})$. In the halting state the machine rewrites every scanned symbol unchanged and does not move any head.
4. (input tape read-only) For every $q$ and $a$, $\sigma_0 = a_0$: tape $0$ always gets back the symbol it scanned. The head on tape $0$ may still move freely.

Conditions 1 and 2 together say that $\delta$ writes $\triangleright$ on a tape exactly when that tape scans $\triangleright$. No condition restricts the output tape (for example, it is not write-only), the work tapes, the symbols written on tapes $1,\dots,k-1$ other than $\triangleright$, or the moves of the heads, apart from the ban on moving left from a $\triangleright$. Conditions 1–4 are mutually consistent, so such machines exist.

---

3. inTape and outTape

The input tape is tape $0$ and the output tape is tape $1$. Both exist because $k \ge 2$. Tapes $2,\dots,k-1$ have no designated role.

---

4. Cfg: configurations

A configuration of $M$ is a triple $(q, C, h)$:

• $q \in K$ is the current state;
• $C : \{0,\dots,k-1\} \times \mathbb{N} \to \Sigma$ gives the contents, with $C_i(p)$ the symbol in cell $p$ of tape $i$;
• $h : \{0,\dots,k-1\} \to \mathbb{N}$ gives the head positions.

Each tape is one-way infinite, with cells $0,1,2,\dots$. A configuration as such is completely unconstrained: tape contents are arbitrary functions, need not be blank from some point on, and may hold $\triangleright$ anywhere. The constraints below come only from reachability from the initial configuration.

---

5. step: one computation step

From $(q, C, h)$, let $a_i = C_i(h_i)$ be the scanned symbols and let $\delta(q, a) = (q', (\sigma_i, d_i)_i)$. The next configuration is $(q', C', h')$, where

$$C'_i(p) = \begin{cases} \sigma_i & p = h_i \\ C_i(p) & p \ne h_i \end{cases} \qquad h'_i = \begin{cases} h_i \dot- 1 & d_i = \mathrm{left} \\ h_i & d_i = \mathrm{stay} \\ h_i + 1 & d_i = \mathrm{right}. \end{cases}$$

Here $\dot-$ is truncated subtraction on $\mathbb{N}$. So a head at cell $0$ that is told to move left stays at cell $0$; this is not an error. In configurations reachable from an initial configuration (see items 8 and 9) this case never arises. There, cell $0$ of every tape always holds $\triangleright$, and condition 1 forbids moving left from $\triangleright$.

step is a total function. It is applied the same way in every state. Because of condition 3, a configuration in state $q_{\mathrm{halt}}$ is a fixed point of step: the scanned cells are rewritten with their own contents and no head moves.

---

6. bitSym

Booleans are encoded as symbols: $\mathrm{true} \mapsto \mathtt{1}$ and $\mathrm{false} \mapsto \mathtt{0}$. For a bit list $u$, write $\overline{u}$ for its symbol list.

---

7. tapeOf

For a finite symbol list $w = (w_1,\dots,w_m)$, the tape contents $\mathrm{tape}(w) : \mathbb{N} \to \Sigma$ are

$$\mathrm{tape}(w)(0) = \triangleright,\qquad \mathrm{tape}(w)(p) = w_p \ (1 \le p \le m),\qquad \mathrm{tape}(w)(p) = \square \ (p > m).$$

So $\mathrm{tape}(w) = \triangleright\, w_1 \cdots w_m\, \square\,\square \cdots$. The empty list gives $\mathrm{tape}(\,) = \triangleright\,\square\,\square\cdots$.

---

8. initCfg: the initial configuration on $(x, y)$

For bit lists $x$ and $y$ of any lengths, possibly different and possibly empty, the initial configuration has:

• state $q_{\mathrm{start}}$;
• input tape $\mathrm{tape}(\overline{x}\,\#\,\overline{y}) = \triangleright\, x_1\cdots x_{|x|}\, \#\, y_1 \cdots y_{|y|}\, \square\,\square\cdots$;
• every other tape (the output tape and all work tapes) equal to $\triangleright\,\square\,\square\cdots$;
• every head at cell $0$.

For $x = y = ()$ the input tape is $\triangleright\,\#\,\square\cdots$.

Where $\triangleright$ can appear. In the initial configuration, $\triangleright$ is in cell $0$ of every tape and nowhere else, because $\square, \mathtt{0}, \mathtt{1}, \#$ are all distinct from $\triangleright$. A step changes only the scanned cells. By conditions 1–2, a scanned $\triangleright$ is rewritten as $\triangleright$ and a scanned non-$\triangleright$ is never turned into $\triangleright$. Hence every configuration reachable from initCfg has $\triangleright$ in exactly cell $0$ of each tape. This is a consequence of the definitions; the file does not state it as a lemma. In arbitrary, non-reachable configurations, $\triangleright$ can appear anywhere.

---

9. HaltsWithOutput

For bit lists $x, y, w$ and $t \in \mathbb{N}$, let $\mathrm{step}^{t}$ denote $t$ applications of step, with $\mathrm{step}^0$ the identity. The predicate holds iff the configuration

$$\mathrm{step}^{t}(\mathrm{init}(x,y))$$

satisfies both of the following:

• its state is $q_{\mathrm{halt}}$; and
• its entire output tape (tape $1$) equals $\mathrm{tape}(\overline{w})$. That is, cell $0$ holds $\triangleright$, cells $1,\dots,|w|$ hold the bits of $w$ as $\mathtt{0}/\mathtt{1}$ symbols, and every later cell holds $\square$. No leftover non-blank symbols are allowed anywhere on tape $1$.

The predicate does not constrain:

• the position of the output head or of any other head;
• the contents of the input tape or of the work tapes;
• whether $t$ is the first time the state is $q_{\mathrm{halt}}$.

Because halted configurations are fixed points, if the predicate holds at $t$ it also holds at every $t' \ge t$. Hence "it holds for some $t \le T$" is the same as "the machine reaches $q_{\mathrm{halt}}$ within $T$ steps with this output tape". Here $t$ counts applications of the step function, and the step that enters $q_{\mathrm{halt}}$ is counted. Since $q_{\mathrm{start}} \ne q_{\mathrm{halt}}$, the predicate fails at $t = 0$, so $t \ge 1$ is necessary.

---

10. val

For a bit list $x = (x_1,\dots,x_m)$, the value is

$$\mathrm{val}(x) = \sum_{j=1}^{m} x_j\, 2^{m-j},$$

with the most significant bit first. It is computed by folding $a \mapsto 2a + x_j$ from $a = 0$. Leading zeros are allowed and $\mathrm{val}(\,) = 0$. Every $x$ of length $n$ has $0 \le \mathrm{val}(x) < 2^n$.

---

11. bin

For $k, z \in \mathbb{N}$, $\mathrm{bin}_k(z)$ is the length-$k$ bit list whose $i$-th entry ($i = 0,\dots,k-1$) is bit number $k-1-i$ of $z$, where bit $0$ is the least significant. It is therefore the binary representation of

$$z \bmod 2^k$$

padded with leading zeros to exactly $k$ bits, most significant bit first. If $z \ge 2^k$, the higher bits are silently dropped. $\mathrm{bin}_0(z)$ is the empty list.

---

12. lg

For $n \in \mathbb{N}$,

$$\mathrm{lg}(n) = \max\bigl(\lceil \log_2 n \rceil, 1\bigr).$$

Here $\lceil\log_2 n\rceil$ is Mathlib's Nat.clog 2 n, the least $m \in \mathbb{N}$ with $n \le 2^m$, which is $0$ for $n \in \{0,1\}$. So $\mathrm{lg}(0) = \mathrm{lg}(1) = \mathrm{lg}(2) = 1$, $\mathrm{lg}(3) = \mathrm{lg}(4) = 2$, $\mathrm{lg}(5) = 3$, and so on. In every case $\mathrm{lg}(n) \ge 1$.

---

13. MultipliesAt

For a machine $M$, $n \in \mathbb{N}$ and a real number $T$, the predicate holds iff:

$$\forall\, x, y \in \{0,1\}^n\ \ \exists\, t \in \mathbb{N}:\ \ t \le T\ \ \wedge\ \ \mathrm{HaltsWithOutput}_M\bigl(x, y, t, \mathrm{bin}_{2n}(\mathrm{val}(x)\cdot \mathrm{val}(y))\bigr).$$

Since $\mathrm{val}(x)\,\mathrm{val}(y) < 2^{2n}$, the required output is exactly the product written with exactly $2n$ bits, including leading zeros, and no truncation occurs.

• The predicate quantifies only over inputs where both $x$ and $y$ have length exactly $n$. Behaviour on unequal lengths is unconstrained.
• The bound $t \le T$ is a comparison of the natural number $t$ with a real, so it is equivalent to $t \le \lfloor T \rfloor$.
• If $T < 1$, the predicate is false for $n \ge 0$, because $t \ge 1$ is needed and there is at least one input.
• For $n = 0$ the only input is $x = y = ()$, and the required output is $\mathrm{bin}_0(0) = ()$, so the output tape must be $\triangleright\,\square\,\square\cdots$.

---

14. MulTimeBound

For $g : \mathbb{N} \to \mathbb{R}$, $\mathrm{MulTimeBound}(g)$ holds iff:

$$\exists\, M \;\Bigl[\ \bigl(\forall n \in \mathbb{N},\ n \ge 1 \Rightarrow \exists\, T \in \mathbb{R}:\ \mathrm{MultipliesAt}(M, n, T)\bigr)\ \ \wedge\ \ \exists\, c \in \mathbb{R},\ c > 0,\ \exists\, n_0 \in \mathbb{N},\ \forall n \in \mathbb{N},\ n \ge n_0 \Rightarrow n \ge 1 \Rightarrow \mathrm{MultipliesAt}\bigl(M, n, c\cdot g(n)\bigr)\ \Bigr].$$

The machine. One single machine $M$, with fixed alphabet, state set and tape count $k$, must work for all $n$.

First conjunct. For every $n \ge 1$, $M$ correctly multiplies all pairs of $n$-bit inputs and halts within some finite real bound $T$ that may depend on $n$. Since there are finitely many inputs of length $n$, this amounts to: $M$ halts on every $x\#y$ with $|x| = |y| = n \ge 1$, and its output tape is then exactly $\mathrm{tape}(\overline{\mathrm{bin}_{2n}(\mathrm{val}(x)\mathrm{val}(y))})$. This conjunct is what forces correctness for $1 \le n < n_0$, which the second conjunct does not cover. It imposes no time bound.

Second conjunct. There are a real constant $c > 0$ and a threshold $n_0 \in \mathbb{N}$. Both are chosen after $M$, and neither depends on $n$. For every $n \ge \max(n_0, 1)$ and every pair $x, y$ of length $n$, $M$ reaches $q_{\mathrm{halt}}$ with the correct output tape within at most $\lfloor c\, g(n) \rfloor$ steps.

What is not constrained. Inputs with $n = 0$ are never constrained. Inputs with $|x| \ne |y|$ are never constrained. Nothing is required of $g$ itself. If $c\,g(n) < 1$ for infinitely many $n$ (for example, if $g(n) \le 0$ infinitely often), the second conjunct is unsatisfiable.

---

15. KappaBound

For a real $\kappa$, with no restriction on its sign or size,

$$\mathrm{KappaBound}(\kappa) \iff \mathrm{MulTimeBound}\Bigl(n \mapsto n \cdot \mathrm{lg}(n)^{\,1-\kappa}\Bigr).$$

The power is the real power. Since $\mathrm{lg}(n) \ge 1$, the base is a positive real and $\mathrm{lg}(n)^{1-\kappa} > 0$ for all $n$. At $n = 1$ the function equals $1$.

• $\kappa = 0$ gives $n\,\mathrm{lg}(n)$.
• $\kappa = 1$ gives $n$.
• $\kappa > 1$ gives $n\,\mathrm{lg}(n)^{-(\kappa-1)}$, which grows more slowly than $n$.
• $\kappa < 0$ gives exponents larger than $1$.

Unfolded, the statement is: there exist one machine $M$, a constant $c > 0$ and an $n_0$ as in item 14. $M$ correctly multiplies all pairs of $n$-bit inputs for every $n \ge 1$. For every $n \ge \max(n_0,1)$ it does so within $c \cdot n \cdot \mathrm{lg}(n)^{1-\kappa}$ steps on every such pair.