TauLib.Orbit.Generation

Orbit rays, iterated ρ, and the generative act.

Registry Cross-References

• [I.X01] The Generative Act — generative_act

• [I.D05] Orbit Rays — OrbitRay

• [I.P03] Pairwise Disjointness — orbit_disjoint

Mathematical Content

The generative act applies ρ to each non-omega generator g, producing the orbit ray O_g = {g, ρ(g), ρ²(g), …}. The four orbit rays are pairwise disjoint (different seeds), and ω sits alone as a fixed point.

NOTE: We use predicates (TauObj → Prop) rather than Mathlib’s Set, since we import Mathlib for tactics only.

Tau.Orbit.iter_rho

source def Tau.Orbit.iter_rho :Nat → Kernel.TauObj → Kernel.TauObj

Iterated application of ρ: ρⁿ(x). Equations

• Tau.Orbit.iter_rho 0 x✝ = x✝
• Tau.Orbit.iter_rho n.succ x✝ = Tau.Kernel.rho (Tau.Orbit.iter_rho n x✝) Instances For

Tau.Orbit.iter_rho_zero

source@[simp]

theorem Tau.Orbit.iter_rho_zero (x : Kernel.TauObj) :iter_rho 0 x = x

Tau.Orbit.iter_rho_succ

source@[simp]

**theorem Tau.Orbit.iter_rho_succ (n : Nat)

(x : Kernel.TauObj) :iter_rho (n + 1) x = Kernel.rho (iter_rho n x)**

Tau.Orbit.iter_rho_depth

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

(hg : g ≠ Kernel.Generator.omega)

(d n : Nat) :iter_rho n { seed := g, depth := d } = { seed := g, depth := d + n }**

iter_rho on a non-omega object increments depth.

Tau.Orbit.iter_rho_omega

source@[simp]

theorem Tau.Orbit.iter_rho_omega (n d : Nat) :iter_rho n { seed := Kernel.Generator.omega, depth := d } = { seed := Kernel.Generator.omega, depth := d }

iter_rho on omega is the identity.

Tau.Orbit.iter_rho_seed

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

(hg : g ≠ Kernel.Generator.omega)

(d n : Nat) :(iter_rho n { seed := g, depth := d }).seed = g**

iter_rho preserves the seed for non-omega generators.

Tau.Orbit.iter_rho_add

source **theorem Tau.Orbit.iter_rho_add (n m : Nat)

(x : Kernel.TauObj) :iter_rho (n + m) x = iter_rho n (iter_rho m x)**

iter_rho composes: ρⁿ⁺ᵐ(x) = ρⁿ(ρᵐ(x)).

Tau.Orbit.OrbitRay

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

(x : Kernel.TauObj) :Prop**

[I.D05] Orbit ray membership predicate: x ∈ O_g iff x has seed g and g is not omega. Equations

• Tau.Orbit.OrbitRay g x = (x.seed = g ∧ g ≠ Tau.Kernel.Generator.omega) Instances For

Tau.Orbit.OmegaFiber

source def Tau.Orbit.OmegaFiber (x : Kernel.TauObj) :Prop

The omega fiber: all TauObj with seed omega. Equations

• Tau.Orbit.OmegaFiber x = (x.seed = Tau.Kernel.Generator.omega) Instances For

Tau.Orbit.orbit_ray_contains_gen

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

(hg : g ≠ Kernel.Generator.omega) :OrbitRay g (Kernel.TauObj.ofGen g)**

Each non-omega generator belongs to its own orbit ray.

Tau.Orbit.orbit_ray_rho_closed

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

(hg : g ≠ Kernel.Generator.omega)

(x : Kernel.TauObj)

(hx : OrbitRay g x) :OrbitRay g (Kernel.rho x)**

Orbit rays are closed under ρ.

Tau.Orbit.orbit_ray_characterize

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

(hg : g ≠ Kernel.Generator.omega)

(x : Kernel.TauObj) :OrbitRay g x ↔ ∃ (n : Nat), x = { seed := g, depth := n }**

Every element of an orbit ray is ⟨g, n⟩ for some n.

Tau.Orbit.orbit_disjoint

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

(hgh : g ≠ h)

(x : Kernel.TauObj) :¬(OrbitRay g x ∧ OrbitRay h x)**

[I.P03] Orbit rays are pairwise disjoint: if g ≠ h, no object belongs to both O_g and O_h.

Tau.Orbit.omega_not_in_orbit

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

(hg : g ≠ Kernel.Generator.omega)

(n : Nat) :¬OrbitRay g { seed := Kernel.Generator.omega, depth := n }**

Omega is not in any orbit ray.

Tau.Orbit.orbit_ray_seed

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

(x : Kernel.TauObj)

(hx : OrbitRay g x) :x.seed = g**

Orbit ray elements have seed equal to the generator.

Tau.Orbit.generative_act

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

(hx : x.seed ≠ Kernel.Generator.omega) :∃ (g : Kernel.Generator), ∃ (n : Nat), g ≠ Kernel.Generator.omega ∧ iter_rho n (Kernel.TauObj.ofGen g) = x**

[I.X01] The generative act: every non-omega TauObj is reachable by iterated ρ from a generator.