Registry · Lemma VII.L36 tau-effective formalized

VII.L36 — Recognition Topology Generation

J_rec is a valid Grothendieck topology generated by recognition morphisms, inheriting pullback stability from J_τ.

Book VII Part 8 Ch. 94

Dependency Graph

Depends on (1)

VII.D76

Lean Formalization

Module: TauLib.BookVII.Social.Ontology

Symbol: Tau.BookVII.Social.Ontology.recognition_topology_generation