TauLib.Denotation.RankTransfer

Rank transfer maps: canonical bijections TauIdx ↔ OrbitRay g.

Registry Cross-References

• [I.D08] Rank Transfer — RT, RT_inv

Mathematical Content

Since every orbit ray O_g has the form {⟨g, 0⟩, ⟨g, 1⟩, ⟨g, 2⟩, …}, there is a canonical bijection with TauIdx (= Nat) via depth. The rank transfer RT_g : TauIdx → O_g maps n ↦ ⟨g, n⟩.

This gives each orbit ray the same arithmetic structure as the alpha orbit: any operation on TauIdx can be “transferred” to any orbit ray.

Tau.Denotation.RT

source **def Tau.Denotation.RT (g : Kernel.Generator)

(n : TauIdx) :Kernel.TauObj**

[I.D08] Rank transfer: TauIdx → orbit ray O_g, mapping n ↦ ⟨g, n⟩. Equations

• Tau.Denotation.RT g n = { seed := g, depth := n } Instances For

Tau.Denotation.RT_inv

source def Tau.Denotation.RT_inv (x : Kernel.TauObj) :TauIdx

Rank transfer inverse: orbit ray element → TauIdx (extracts depth). Equations

• Tau.Denotation.RT_inv x = x.depth Instances For

Tau.Denotation.RT_injective

source **theorem Tau.Denotation.RT_injective (g : Kernel.Generator)

(n m : TauIdx)

(h : RT g n = RT g m) :n = m**

RT is injective.

Tau.Denotation.RT_surjective

source **theorem Tau.Denotation.RT_surjective (g : Kernel.Generator)

(_hg : g ≠ Kernel.Generator.omega)

(x : Kernel.TauObj)

(hx : Orbit.OrbitRay g x) :∃ (n : TauIdx), RT g n = x**

RT hits every orbit ray element.

Tau.Denotation.RT_inv_left

source **theorem Tau.Denotation.RT_inv_left (g : Kernel.Generator)

(n : TauIdx) :RT_inv (RT g n) = n**

Round-trip: RT_inv ∘ RT = id.

Tau.Denotation.RT_inv_right

source **theorem Tau.Denotation.RT_inv_right (g : Kernel.Generator)

(x : Kernel.TauObj)

(h : x.seed = g) :RT g (RT_inv x) = x**

Round-trip: RT ∘ RT_inv = id (on orbit ray elements).

Tau.Denotation.RT_rho_comm

source **theorem Tau.Denotation.RT_rho_comm (g : Kernel.Generator)

(hg : g ≠ Kernel.Generator.omega)

(n : TauIdx) :RT g (n + 1) = Kernel.rho (RT g n)**

RT commutes with ρ: RT_g(n+1) = ρ(RT_g(n)) for g ≠ ω.

Tau.Denotation.RT_in_orbit

source **theorem Tau.Denotation.RT_in_orbit (g : Kernel.Generator)

(hg : g ≠ Kernel.Generator.omega)

(n : TauIdx) :Orbit.OrbitRay g (RT g n)**

RT lands in the orbit ray.

Tau.Denotation.RT_alpha_eq

source theorem Tau.Denotation.RT_alpha_eq (n : TauIdx) :RT Kernel.Generator.alpha n = toAlphaOrbit n

RT for alpha is the same as toAlphaOrbit.

Tau.Denotation.RT_sigma

source **theorem Tau.Denotation.RT_sigma (g h : Kernel.Generator)

(_hg : g ≠ h)

(n : TauIdx) :sigma g h (RT g n) = RT h n**

Rank transfer is natural: σ_{g,h} ∘ RT_g = RT_h.