Registry · Lemma VII.L37 tau-effective formalized

VII.L37 — Social Sheaf Construction

F_soc is a valid sheaf on (Ω_soc, J_rec): presheaf + gluing + locality + dignity constraint.

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.social_sheaf_construction