Proving Turing Machines Compute Successor

Setup
In[]:=
PacletInstall["https://www.wolframcloud.com/obj/nikm/LeanLink.paclet",ForceVersionInstall->True];​​PacletInstall["https://www.wolframcloud.com/obj/nikm/TuringMachine.paclet",ForceVersionInstall->True];
In[]:=
Get["LeanLink`"];​​Get["WolframInstitute`TuringMachine`"];
In[]:=
p="OneSidedTM.";​​proofDir=FileNameJoin[{NotebookDirectory[],"..","TuringMachine","Proofs"}];​​leanImport[mod_]:=LeanImport[mod,"ProjectDir"->proofDir,"Filter"->"OneSidedTM"]
A one-sided Turing machine reads a binary-encoded natural number on its tape (LSB at position 0), executes transitions, and halts when the head moves past position 0 to the left. We ask: which TMs compute the successor function? And can we prove it for ALL inputs?
Part 1: Formalizing the Machine
In[]:=
defsEnv=LeanImportString["inductive Dir where | L | R deriving Repr, DecidableEq, BEq​structure Rule where nextState : Nat write : Nat dir : Dir deriving Repr, DecidableEq, BEq​structure TM where numStates : Nat numSymbols : Nat transition : Nat -> Nat -> Rule"]
Out[]=
LeanEnvironment
Constants: 3
Kinds: 3 inductive

In[]:=
defsEnv["TM"]["TypeForm"]
Out[]=
Type
Part 2: The Successor Predicate
ComputesSucc
says: for every n >= 1 there exists enough fuel for the TM to halt with output n + 1.
In[]:=
succEnv=LeanImportString["def ComputesSucc (run : Nat -> Nat -> Option Nat) : Prop := forall n : Nat, n >= 1 -> Exists fun fuel => run n fuel = some (n + 1)"]
Out[]=
LeanEnvironment
Constants: 1
Kinds: 1 def

In[]:=
succEnv["ComputesSucc"]["TypeForm"]
Out[]=
∀ (run : ∀ (a : Nat) (a : Nat), Option Nat), Prop
Part 3: Rule 445 -- The Machine
Rule 445 is the canonical (2,2) successor-computing TM.
In[]:=
Grid[{{OneSidedTuringMachinePlot[{445,2,2},1,20,ImageSize->120,"LabelInput"->True],OneSidedTuringMachinePlot[{445,2,2},3,20,ImageSize->120,"LabelInput"->True],OneSidedTuringMachinePlot[{445,2,2},7,20,ImageSize->120,"LabelInput"->True],OneSidedTuringMachinePlot[{445,2,2},15,40,ImageSize->120,"LabelInput"->True]}},Spacings->2]
Out[]=
1
2
3
4
7
8
15
16
Part 4: The Universal Proof
In[]:=
plusOneEnv=leanImport["OneSidedTM.PlusOne"]
Out[]=
LeanEnvironment
Constants: 221
Kinds: 158 theorem38 def20 axiom3 constructor2 inductive


Machine-Checked Spot Checks via
native_decide

In[]:=
plusOneEnv[p<>"rule445_succ_7"]["TypeForm"]
Out[]=
OneSidedTM.run OneSidedTM.rule445 7 20 = Option.some Nat 8

rule445_computesSucc
-- Correctness for ALL inputs

Structural induction on the binary representation. No finite enumeration -- true for every natural number:
In[]:=
plusOneEnv[p<>"rule445_computesSucc"]["TypeForm"]
Out[]=
OneSidedTM.ComputesSucc OneSidedTM.rule445
In[]:=
plusOneEnv[p<>"rule445_computesSucc"]["ExprGraph"]
Out[]=
Part 5: All (2,2) Successor Rules by Class
17 rules compute binary successor in the (2,2) space, partitioned into 3 classes:
In[]:=
Grid[{{Labeled[OneSidedTuringMachinePlot[{445,2,2},7,20,ImageSize->180,"LabelInput"->True],Style["Rule 445 (Class A)",Bold,11],Top],Labeled[OneSidedTuringMachinePlot[{453,2,2},7,20,ImageSize->180,"LabelInput"->True],Style["Rule 453 (Class B)",Bold,11],Top],Labeled[OneSidedTuringMachinePlot[{1512,2,2},7,20,ImageSize->180,"LabelInput"->True],Style["Rule 1512 (Class C)",Bold,11],Top]}},Spacings->2]
Out[]=
Rule 445 (Class A)
7
8
Rule 453 (Class B)
7
8
Rule 1512 (Class C)
7
8

Class B: Bounce-Back Scanback (8 rules)

In[]:=
allEnv=leanImport["OneSidedTM.AllPlusOne"]
Out[]=
LeanEnvironment
Constants: 460
Kinds: 311 theorem63 def69 axiom8 inductive9 constructor


Class C: Skip + Absorb + Clear-on-Return (8 rules)

Part 6: 3-State (3,2) Proof Classes

ThreeState: Rule 146514

Class S: Self-Loop Clear

Class SX: Toggle + Drop + Self-Loop Variants

Class SB: Bouncing Clearback

Class D: Delegated Scan (DW + DS)

Class W: Walk Variants

Part 7: The Near-Miss -- Proving Incorrectness
Rule 156830 correctly computes successor for inputs 1 through 6, then fails at n = 7:
Summary: Proof Architecture

(2,2) Classes

(3,2) Classes