Registry · Lemma VII.L04 tau-effective formalized

VII.L04 — Strictness Between Layers

E₀ ⊂ E₁ ⊂ E₂ ⊂ E₃ strictly; separation witnesses: sector admissibility, internal code evaluation, self-model consistency.

Book VII Part 1 Ch. 7

Dependency Graph

Depends on (1)

VII.D05

Depended on by (1)

VII.T05

Lean Formalization

Module: TauLib.BookVII.Meta.Registers

Symbol: Tau.BookVII.Meta.Registers.StrictnessBetweenLayers