Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Uniform numerical clocks and output bounds

Abstract

Uniform numerical clocks and output bounds.

Polynomial clocks use natural coefficients and exponents independent of the input. A transducer output has a polynomial length bound because an executed instruction changes finite tape size by a bounded amount. Pair lengths and verifier clocks are numerical consequences of actual executions.

Theorem 1.1 (polyTime_output_length).

Lean statement: D5/S0/Computability/BinaryMachine/Clock.polyTime_output_length

Proof. Machine-checked in Lean as D5/S0/Computability/BinaryMachine/Clock.polyTime_output_length (✓ 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