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.

Rank Transfer Maps

Summary

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.

Statement

%
\label{def:rank-transfer}
For each solenoidal generator $s \in \{\pi, \gamma, \eta\}$,
the \textbf{rank transfer map}
$\mathrm{RT}_s : \tau\text{-Idx} \to O_s$
is defined by
\[
    \mathrm{RT}_s(\underline{n}) := \rho^n(s).
\]
That is, $\mathrm{RT}_s$ maps the element at depth~$n$
in the alpha-orbit to the element at depth~$n$
in the $s$-orbit.

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-01.jsonl line 22
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part03/ch10-tau-idx.tex lines 126-139

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookI.Denotation.RankTransfer
• Name: Tau.Denotation.rank_transfer

Dependencies

• Canonical: I.D07, I.D05, I.T01

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.