Registry · Lemma VII.L02 tau-effective formalized

VII.L02 — Shadow Soundness Lemma

Shadow functors (VM/ZFC-PA and epistemic/pragmatic) are sound: accepted τ-content projects to coherent content in target formalism.

Book VII Part 1 Ch. 6

Dependency Graph

Depends on (2)

VII.D12 VII.D13

Lean Formalization

Module: TauLib.BookVII.Meta.Registers

Symbol: Tau.BookVII.Meta.Registers.ShadowSoundnessLemma