Registry · Theorem I.T19 tau-effective formalized

I.T19 — Diagonal-Free Protection

The zero-divisor product e_plus * e_minus = 0 cannot arise as T(t1) * T(t2) for any T in HolFun and compatible omega-tails t1, t2. Sector-pure outputs cannot combine nontrivially.

Book I Part 13 Ch. 51

Dependency Graph

Depends on (3)

I.P23 I.D47 I.T05

Lean Formalization

Module: TauLib.BookI.Holomorphy.DiagonalProtection

Symbol: Tau.Holomorphy.diagonal_free_protection