Registry · Definition III.D57 tau-effective formalized

III.D57 — Enrichment Functor Enr₀₁

Faithful functor Enr₀₁ : Cat_τ(E₀) → Cat_τ(E₁) enriching algebraic tower data with split-complex dynamics and sector structure

Book III Part 6 Ch. 44

Dependency Graph

Depends on (2)

III.T29 III.D48

Depended on by (7)

III.D58 III.D59 III.D61 III.D63 III.P24 III.T36 III.T37

Lean Formalization

Module: TauLib.BookIII.Arithmetic.EnrFunctor01

Symbol: enr_01_check