Registry · Proposition I.P23 tau-effective formalized

I.P23 — No Simultaneous Projection

No Simultaneous Projection: the diagonal-free discipline prevents any omega-tail from projecting nontrivially onto BOTH idempotent sectors e_plus and e_minus simultaneously.

Book I Part 13 Ch. 51

Dependency Graph

Depends on (3)

I.D03 I.T05 I.D47

Depended on by (1)

I.T19

Lean Formalization

Module: TauLib.BookI.Holomorphy.DiagonalProtection

Symbol: Tau.Holomorphy.no_simul_projection_b