Registry · Theorem VII.T08 tau-effective formalized

VII.T08 — Archetype Existence

For every structural invariant I with j-closed exhibitor, unique archetype A_I exists as minimal j-closed fixed point exhibiting I.

Book VII Part 1 Ch. 10

Dependency Graph

Depends on (1)

VII.L08

Depended on by (1)

VII.L25

Lean Formalization

Module: TauLib.BookVII.Meta.Archetypes

Symbol: Tau.BookVII.Meta.Archetypes.archetype_existence