Swap Operator sigma

sigma (swap): first derived operator from rho. Exchanges positions within orbit rays via rank transfer composition.

Swap Operator sigma

Summary

sigma (swap): first derived operator from rho. Exchanges positions within orbit rays via rank transfer composition.

Statement

%
\label{def:swap}
The \textbf{swap operator} $\sigma_{s,t}$ for generators
$s, t \in \{\alpha, \pi, \gamma, \eta\}$
is the map
\[
    \sigma_{s,t} := \mathrm{RT}_t \circ \mathrm{RT}_s^{-1}
    : O_s \to O_t
\]
that transfers an element from the $s$-orbit to the $t$-orbit
at the same depth.
Explicitly: $\sigma_{s,t}(\rho^n(s)) = \rho^n(t)$.

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-01.jsonl line 23
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part03/ch11-swap-add-mul.tex lines 45-58

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookI.Denotation.TauIdx
• Name: Tau.Denotation.sigma

Dependencies

• Canonical: I.D08, I.D02

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.