Registry · Theorem I.T39 established formalized

I.T39 — K5 Structural Exclusion

K5 diagonal discipline places tau on star-autonomous side; Lawvere FPT does not apply. Necessary but not sufficient for self-hosting.

Book I Part 18 Ch. 72

Dependency Graph

Depends on (3)

I.D81 I.T37 I.D03

Depended on by (4)

I.D82 I.R21 I.T46 II.R16

Lean Formalization

Module: TauLib.BookI.MetaLogic.StructuralExclusion

Symbol: k5_structural_exclusion