Registry · Theorem VII.T10 tau-effective formalized

VII.T10 — Readout Functor Faithfulness

Readout functor faithful on archetypes iff it preserves j-closure structure; distinct j-closed patterns produce distinct expressions iff R is faithful.

Book VII Part 1 Ch. 15

Dependency Graph

Depends on (1)

VII.D22

Depended on by (1)

VII.T12

Lean Formalization

Module: TauLib.BookVII.Meta.Registers

Symbol: Tau.BookVII.Meta.Registers.readout_functor_faithfulness