Registry · Theorem III.T79 tau-effective formalized

III.T79 — Tower Finite Decidable

All three conjectures have defined gap types, forbidden moves, and scope labels. Finite τ-effective, infinite conjectural.

Book III Part 10 Ch. 81

Dependency Graph

Depends on (2)

III.D111 III.D112

Lean Formalization

Module: TauLib.BookIII.Bridge.ConjectureGaps

Symbol: tower_finite_decidable