Registry · Definition III.D91 tau-effective formalized

III.D91 — Obstruction Cocycle

Obstruction value for each forbidden move at stage k. Mild moves (damage 1): bounded deviation. Breaking moves (damage 3): deviation grows with M_k. Classifies translation failure precisely.

Book III Part 10 Ch. 81

Dependency Graph

Depends on (2)

III.P36 III.P37

Depended on by (2)

III.D92 III.T61

Lean Formalization

Module: TauLib.BookIII.Bridge.TranslationObstruction

Symbol: obstruction_value