theorem proved term proof

`substrate_monotheism_one_statement`

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

formal statement (Lean)

 165theorem substrate_monotheism_one_statement :
 166    (∀ T : Theology, Theology.isAtheistic T ∨ Theology.isMonotheistic T ∨
 167       Theology.isPolytheistic T) ∧
 168    totalSigma [⟨"god1", 0, 1⟩, ⟨"god2", 0, 1⟩] = 2 ∧
 169    totalSigma [⟨"GOD", 0, 1⟩] = 1 ∧
 170    Theology.isMonotheistic [⟨"GOD", 0, 1⟩] :=

proof body

Term-mode proof.

 171  ⟨Theology.trichotomy, polytheistic_two_violates_canonical,
 172   monotheistic_canonical_sigma, unique_occupant_is_monotheistic⟩
 173
 174end SubstrateIndependentMonotheism
 175end Theology
 176end IndisputableMonolith

depends on (12)

Lean names referenced from this declaration's body.

T in IndisputableMonolith.Foundation.Breath1024 decl_use
T in IndisputableMonolith.Gap45.SyncMinimization decl_use
totalSigma in IndisputableMonolith.Jurisprudence.PrecedentStabilityFromSigma decl_use
isAtheistic in IndisputableMonolith.Theology.SubstrateIndependentMonotheism decl_use
isMonotheistic in IndisputableMonolith.Theology.SubstrateIndependentMonotheism decl_use
isPolytheistic in IndisputableMonolith.Theology.SubstrateIndependentMonotheism decl_use
monotheistic_canonical_sigma in IndisputableMonolith.Theology.SubstrateIndependentMonotheism decl_use
polytheistic_two_violates_canonical in IndisputableMonolith.Theology.SubstrateIndependentMonotheism decl_use
Theology in IndisputableMonolith.Theology.SubstrateIndependentMonotheism decl_use
totalSigma in IndisputableMonolith.Theology.SubstrateIndependentMonotheism decl_use
trichotomy in IndisputableMonolith.Theology.SubstrateIndependentMonotheism decl_use
unique_occupant_is_monotheistic in IndisputableMonolith.Theology.SubstrateIndependentMonotheism decl_use