Registry · Theorem IV.T128 tau-effective formalized

IV.T128 — Readout Preserves Identities

R_mu preserves internal identities: equal Layer 1 objects yield equal SI readouts.

Book IV Part 8 Ch. 68

Dependency Graph

Depends on (2)

IV.D326 IV.D323

Lean Formalization

Module: TauLib.BookIV.Physics.ReadoutFunctor

Symbol: Tau.BookIV.Physics.readout_preserves_identities