`Substrate`

definition

show as: view math explainer →

module: IndisputableMonolith.Theology.SubstrateIndependentMonotheism
domain: Theology
line: 46 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Theology.SubstrateIndependentMonotheism on GitHub at line 46.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  43
  44/-- A substrate has a phase ∈ ℕ (0 = canonical), a σ-charge ∈ ℤ,
  45and a label. -/
  46structure Substrate where
  47  label : String
  48  phase : ℕ
  49  sigma : ℤ
  50  deriving DecidableEq, Repr
  51
  52namespace Substrate
  53
  54/-- The "divine" substrate predicate: phase = 0 and σ = 1. -/
  55def isDivine (s : Substrate) : Prop :=
  56  s.phase = 0 ∧ s.sigma = 1
  57
  58/-- Decidability of `isDivine`. -/
  59instance : DecidablePred isDivine := fun s =>
  60  show Decidable (s.phase = 0 ∧ s.sigma = 1) from inferInstance
  61
  62end Substrate
  63
  64/-! ## §2. Monotheism vs. polytheism -/
  65
  66/-- A theological model is a list of substrates. -/
  67abbrev Theology := List Substrate
  68
  69namespace Theology
  70
  71/-- The set of divine substrates in a theology. -/
  72def divine (T : Theology) : List Substrate :=
  73  T.filter Substrate.isDivine
  74
  75/-- A theology is **monotheistic** iff it has exactly one divine
  76substrate. -/

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.