Registry · Lemma VII.L12 tau-effective formalized

VII.L12 — CI Minimality Lemma

The CI is the minimal j-closed fixed point with universalizability property; uniqueness among ethical operators.

Book VII Part 7 Ch. 88

Dependency Graph

Depends on (2)

VII.L08 VII.T31

Depended on by (1)

VII.L30

Lean Formalization

Module: TauLib.BookVII.Ethics.CIProof

Symbol: Tau.BookVII.Ethics.CIProof.ci_minimality