Registry · Definition III.D92 tau-effective formalized

III.D92 — Forbidden Move Obstruction Classes

Each of 5 forbidden moves obstructs arithmetic or topological translation. Arithmetic: 3 obstructions. Topology: 4 obstructions. Classification verified by native_decide.

Book III Part 10 Ch. 81

Dependency Graph

Depends on (1)

Depended on by (1)

Lean Formalization

Module: TauLib.BookIII.Bridge.TranslationObstruction

Symbol: move_obstructs_arith