Registry · Definition I.D58 tau-effective formalized

I.D58 — Characteristic Morphism

The characteristic morphism chi_S: X -> Omega_tau assigns a Truth4 value based on B-sector and C-sector membership. T = both confirm, F = both deny, B = overdetermined, N = underdetermined. Pullback of true along chi recovers the subobject.

Book I Part 14 Ch. 56

Dependency Graph

Depends on (1)

Depended on by (1)

Lean Formalization

Module: TauLib.BookI.Topos.EarnedTopos

Symbol: Tau.Topos.characteristic_morphism