module module

`IndisputableMonolith.Theology.SubstrateIndependentMonotheism`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (16)

structure Substrate L46
def isDivine L55
abbrev Theology L67
def divine L72
def isMonotheistic L77
def isPolytheistic L82
def isAtheistic L86
theorem trichotomy L91
def totalSigma L106
theorem polytheistic_two_violates_canonical L110
theorem monotheistic_canonical_sigma L118
theorem unique_occupant_is_monotheistic L125
theorem one_god_with_creatures_is_monotheistic L133
structure SubstrateIndependentMonotheismCert L141
def substrateIndependentMonotheismCert L154
theorem substrate_monotheism_one_statement L165