Registry · Definition III.D113 established formalized

III.D113 — Forbidden Move Mapping

All three gaps map to exponential_quantification (K4 violation). Finite→infinite passage requires exponential quantification.

Book III Part 10 Ch. 81

Dependency Graph

Depends on (2)

III.D112 III.D69

Depended on by (2)

III.D111 III.T80

Lean Formalization

Module: TauLib.BookIII.Bridge.ConjectureGaps

Symbol: gap_forbidden_move