Registry · Definition III.D52 tau-effective formalized

III.D52 — Observable Transition

δ_M^obs operates on K_M-bit configurations (machine constant). Cook-Levin tableau for TTM has constant width W = 1+m. Bounded observation window drives the collapse.

Book III Part 9 Ch. 55

Dependency Graph

Depends on (1)

Depended on by (1)

Lean Formalization

Module: TauLib.BookIII.Computation.TowerMachine

Symbol: observable_transition_check