Registry · Theorem I.T10 established formalized

I.T10 — Split-Complex Forced

The bipolar prime partition forces split-complex (j^2 = +1) over elliptic (i^2 = -1) scalars. Three arguments: bipolar encoding requirement, wave-type propagation, diagonal-discipline compatibility.

Book I Part 7 Ch. 30

Dependency Graph

Depends on (2)

I.D26 I.D28

Depended on by (34)

I.D27 I.R43 II.D21 II.D32 II.D35 II.D36 II.D42 II.D43 II.D48 II.D68 II.D70 II.D72 II.D73 II.L04 II.L07 II.L08 II.P07 II.P09 II.R02 II.R23 II.R26 II.R27 II.R28 II.T24 II.T26 II.T27 II.T28 II.T30 II.T41 II.T43 II.T44 II.T45 II.T46 IV.T34p

Lean Formalization

Module: TauLib.BookI.Polarity.BipolarAlgebra

Symbol: Tau.Polarity.split_complex_forced