Decode a paired product-machine state

Proved

CookLevin.productState_decode

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

cook-levinproduct-constructionturing-machine

If $0\le q_2<Q_2+1$ , quotient and remainder by the radix $Q_2+1$ recover both components of the product-state encoding $q_1(Q_2+1)+q_2$ .

This decoding identity is used in exact command lookup and product-machine simulation.

Formal statement

import Definitions.Def_CookLevin_ProductState
open CookLevin

theorem CookLevin.productState_decode (Q2 q1 q2 : Nat) (hq2 : q2 < Q2 + 1) :
    productState Q2 q1 q2 / (Q2 + 1) = q1 ∧
    productState Q2 q1 q2 % (Q2 + 1) = q2 := by sorry

Source

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

View graph