Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Unary outer-length prefixes

Abstract

Unary outer-length prefixes.

This live slice retains only the unary natural-prefix writer, reader, exact reconstruction and length law. It contains no supplied SAT language or Cook-Levin classification. A prefix consists of the stated number of ones followed by zero.

Theorem 1.1 (SAT.readNat_eq_some).

Lean statement: D5/S0/Computability/BinaryMachine/UnaryWords.readNat_eq_some

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

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

Commentary.

This declaration and its proof are attributed immutable source supply. The mathematical namespace and proof body are preserved. Full license, source correspondence and the finite retirement contract are recorded in docs/reports/licenses/RBarishBinaryMachine.md. This port supplies no new classification or independent mathematical escape content.

References