omega_tau_classifier (theorem)

/-- [I.T25] The subobject classifier for PSh(Cat_τ) is Ω_τ = Truth4. In a Grothendieck topos, the subobject classifier Ω is characterized by: for every mono m: S ↪ X, there exists a unique χ: X → Ω such that the pullback of true: 1 → Ω along χ recovers S. In our four-valued setting: - T: the element is in S (both sectors confirm membership) - F: the element is not in S (both sectors deny) - B: overdetermined (B-sector confirms, C-sector denies) - N: underdetermined (neither sector confirms) The key theorem: Ω_τ has exactly four elements, matching Truth4. -/