Registry · Definition I.D08 established formalized

I.D08 — Rank Transfer Maps

For each generator s in {pi, gamma, eta}, RT_s : tau-Idx -> O_s maps rho^n(alpha) to rho^n(s). Canonical bijection between counting scaffold and typed orbit ray.

Book I Part 3 Ch. 10

Dependency Graph

Depends on (3)

Depended on by (3)

Lean Formalization

Module: TauLib.BookI.Denotation.RankTransfer

Symbol: Tau.Denotation.rank_transfer