Prove2Me

Every non-joint-halted product state is running

Proved
CookLevin.productState_running_lt_halt

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

cook-levinproduct-constructionturing-machine

For local states within their respective ranges, the encoded product state lies strictly below the joint-halting state unless both components are already halted.

This establishes that every nonterminal local-state pair indexes a running product command.

Formal statement
import Definitions.Def_CookLevin_ProductState
open CookLevin

theorem CookLevin.productState_running_lt_halt
    (Q1 Q2 q1 q2 : Nat)
    (hq1 : q1 ≤ Q1) (hq2 : q2 ≤ Q2)
    (hnot : q1 ≠ Q1 ∨ q2 ≠ Q2) :
    productState Q2 q1 q2 < productStateCount Q1 Q2 := by sorry
Source
Product-state construction supporting https://prove2.me/theorems/6e7f5aa7-4e76-407b-a196-af95907e3fcc

View graph