TauLib.Orbit.Countability

Each orbit ray is countable (bijection with Nat), and Obj(τ) is countable.

Registry Cross-References

• [I.P04] Orbit Countability — orbit_countable, tauObj_countable

Mathematical Content

Each orbit ray O_g is in bijection with Nat via the map n ↦ ⟨g, n⟩. The full universe Obj(τ) is countable: we construct an injection TauObj → Nat.

Tau.Orbit.orbitEnumerate

source **def Tau.Orbit.orbitEnumerate (g : Kernel.Generator)

(_hg : g ≠ Kernel.Generator.omega)

(n : Nat) :Kernel.TauObj**

Canonical enumeration of orbit ray O_g: n ↦ ⟨g, n⟩. Equations

• Tau.Orbit.orbitEnumerate g _hg n = { seed := g, depth := n } Instances For

Tau.Orbit.orbit_enumerate_injective

source **theorem Tau.Orbit.orbit_enumerate_injective (g : Kernel.Generator)

(hg : g ≠ Kernel.Generator.omega)

(n m : Nat)

(h : orbitEnumerate g hg n = orbitEnumerate g hg m) :n = m**

[I.P04 part 1] Orbit enumeration is injective.

Tau.Orbit.orbit_enumerate_surjective

source **theorem Tau.Orbit.orbit_enumerate_surjective (g : Kernel.Generator)

(hg : g ≠ Kernel.Generator.omega)

(x : Kernel.TauObj)

(hx : OrbitRay g x) :∃ (n : Nat), orbitEnumerate g hg n = x**

[I.P04 part 2] Orbit enumeration hits every orbit ray element.

Tau.Orbit.orbit_enumerate_in_ray

source **theorem Tau.Orbit.orbit_enumerate_in_ray (g : Kernel.Generator)

(hg : g ≠ Kernel.Generator.omega)

(n : Nat) :OrbitRay g (orbitEnumerate g hg n)**

Orbit enumeration produces elements in the orbit ray.

Tau.Orbit.tauObj_encode

source def Tau.Orbit.tauObj_encode (x : Kernel.TauObj) :Nat

Encode a TauObj as a natural number: 5 * depth + seed_index. This gives a computable injection TauObj → Nat. Equations

• Tau.Orbit.tauObj_encode x = 5 * x.depth + x.seed.toNat Instances For

Tau.Orbit.tauObj_encode_injective

source **theorem Tau.Orbit.tauObj_encode_injective (x y : Kernel.TauObj)

(h : tauObj_encode x = tauObj_encode y) :x = y**

The encoding is injective: distinct TauObjs yield distinct codes.

Tau.Orbit.tauObj_countable

source theorem Tau.Orbit.tauObj_countable :∃ (f : Kernel.TauObj → Nat), Function.Injective f

[I.P04] Obj(τ) is countable: there exists an injection TauObj → Nat.