Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Register injection and disjoint frames

Abstract

Register injection and disjoint frames.

Every counted accepting or rejecting run lifts through an injective register map with identical primitive count. Registers outside the image retain their full words. The seven-to-nine-register instance preserves two extra frame words while running the original finite control unchanged.

Theorem 1.1 (exec_lift).

Lean statement: D5/S0/Computability/BinaryMachine/StackFrame.exec_lift

Proof. Machine-checked in Lean as D5/S0/Computability/BinaryMachine/StackFrame.exec_lift (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. RBarish-UTokyo (2026). NPCompleteness-Lean4 finite binary machine and composition source. URL: https://github.com/RBarish-UTokyo/NPCompleteness-Lean4/tree/3e603e795b44fedcf7d6dd65b7d1e30547ead925.

Commentary.

Every counted accepting or rejecting run lifts through an injective register map with identical primitive count. Registers outside the image retain their full words. The seven-to-nine-register instance preserves two extra frame words while running the original finite control unchanged.

Theorem 1.2 (exec_extend).

Lean statement: D5/S0/Computability/BinaryMachine/StackFrame.exec_extend

Proof. Machine-checked in Lean as D5/S0/Computability/BinaryMachine/StackFrame.exec_extend (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. RBarish-UTokyo (2026). NPCompleteness-Lean4 finite binary machine and composition source. URL: https://github.com/RBarish-UTokyo/NPCompleteness-Lean4/tree/3e603e795b44fedcf7d6dd65b7d1e30547ead925.

Commentary.

Every counted accepting or rejecting run lifts through an injective register map with identical primitive count. Registers outside the image retain their full words. The seven-to-nine-register instance preserves two extra frame words while running the original finite control unchanged.

References