Registry · Theorem VII.T04 tau-effective formalized

VII.T04 — Rigidity Corollary

Each sector internally consistent; normalizer is rigid with respect to sector structure; retyping between sectors changes verdict.

Book VII Part 1 Ch. 6

Dependency Graph

Depends on (3)

VII.D11 VII.T01 VII.T03

Lean Formalization

Module: TauLib.BookVII.Meta.Registers

Symbol: Tau.BookVII.Meta.Registers.RigidityCorollary