Paired-state encoding for product Turing machines

Definition

CookLevin_ProductState

by junyihjy · Sep 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

cook-levinproduct-constructionturing-machine

The product-machine state encoding maps a pair $(q_1,q_2)$ to $q_1(Q_2+1)+q_2$ . The pair of local halting states is the unique joint-halting state.

Definition code

import Definitions.Def_CookLevin_Basic
set_option autoImplicit false
namespace CookLevin

/-- Encode a pair of local states using radix Q2+1. -/
def productState (Q2 q1 q2 : Nat) : Nat := q1 * (Q2 + 1) + q2

/-- The unique joint-halting state of the product encoding. -/
def productStateCount (Q1 Q2 : Nat) : Nat := productState Q2 Q1 Q2

end CookLevin

Source

Product-machine construction supporting https://prove2.me/theorems/6e7f5aa7-4e76-407b-a196-af95907e3fcc

View graph