Registry · Lemma VII.L30 tau-effective formalized

VII.L30 — CI Uniqueness Derivation

Full chain: lattice completeness + Kernel Theorem non-emptiness + Knaster-Tarski → CI uniqueness up to natural isomorphism.

Book VII Part 7 Ch. 89

Dependency Graph

Depends on (3)

VII.P21 VII.T36 VII.L12

Lean Formalization

Module: TauLib.BookVII.Ethics.CIProof

Symbol: Tau.BookVII.Ethics.CIProof.ci_uniqueness_derivation