Registry · Definition I.D20 tau-effective formalized

I.D20 — Split-Complex Scalars

Split-complex unit j with j^2 = +1 (not i^2 = -1). Earned from boundary ring structure. The foundational scalar field for tau-holomorphy.

Book I Part 10 Ch. 40

Dependency Graph

Depends on (1)

I.D19

Depended on by (20)

I.D105 I.D22 I.D34 I.D37 I.D42 I.D83 I.R43 II.D01 II.D21 II.D32 II.D33 II.D35 II.D36 II.D39 II.D42 II.D53 II.D54 II.L07 II.T26 II.T27

Lean Formalization

Module: TauLib.BookI.Boundary.SplitComplex

Symbol: Tau.Boundary.SplitComplex