Registry · Proposition III.P01 tau-effective formalized

III.P01 — E₁ Strictness Witness

The bipolar Hom decomposition Hom(A,B) = e₊·Hom₊ + e₋·Hom₋ is a genuine E₁ structure: no E₀ object carries this decomposition. The split-complex scalar action on morphism spaces is the strictness witness separating E₁ from E₀.

Book III Part 1 Ch. 6

Dependency Graph

Depends on (2)

Depended on by (1)

Lean Formalization

Module: TauLib.BookIII.Enrichment.CanonicalLadder

Symbol: e1_strictness_8_3