Registry · Theorem I.T07 established formalized

I.T07 — Rigidity of tau

Aut(tau) = {id}. Every automorphism fixes all generators (named constants) and all orbit elements (by induction on depth).

Book I Part 2 Ch. 9

Dependency Graph

Depends on (8)

I.T01 I.K1 I.K2 I.K3 I.K4 I.K5 I.K6 I.P01

Depended on by (3)

I.T11 I.T11a IV.T34p

Lean Formalization

Module: TauLib.BookI.Orbit.Rigidity

Symbol: Tau.Orbit.rigidity