Registry · Theorem VI.T02 tau-effective planned

VI.T02 — Distinction Well-Definedness

τ-finiteness bounds stabilization N ≤ dim_τ(X); evaluation terminates in dim_τ(X) steps; distinction is unique given character χ. Computability corollary follows.

Book VI Part 1 Ch. 4

Dependency Graph

Depends on (1)

VI.D04

Lean Formalization

Module: TauLib.BookVI.LifeCore.Distinction

Symbol: Tau.BookVI.Distinction.DistinctionWelldefinedness