Registry · Theorem III.T31 tau-effective formalized

III.T31 — Interface Width Principle

τ-admissible functions are determined by a single finite quotient ℤ/Prim(k₀)ℤ. If computation stabilizes, the infinite tower collapses to one level. Proof via tower coherence and Global Hartogs.

Book III Part 9 Ch. 56

Dependency Graph

Depends on (3)

III.D54 III.D53 III.T09

Depended on by (4)

III.D56 III.P21 III.T32 III.T33

Lean Formalization

Module: TauLib.BookIII.Computation.Admissibility

Symbol: width_principle_check