Registry · Theorem VII.T35 tau-effective formalized

VII.T35 — CI as j-Closed Fixed Point

The categorical imperative is a minimal j-closed fixed point in the presheaf topos; CI is not postulated but derived from kernel structure.

Book VII Part 7 Ch. 88

Dependency Graph

Depends on (2)

VII.L08 VII.T31

Depended on by (4)

VII.L29 VII.L42 VII.P25 VII.R53

Lean Formalization

Module: TauLib.BookVII.Ethics.CIProof

Symbol: Tau.BookVII.Ethics.CIProof.ci_j_closed_fixed_point