divine
plain-language theorem explainer
The declaration divine extracts the sublist of divine substrates from a theology T. An ontologist or philosopher of religion formalizing consistency under global phase and sigma conservation would cite it to partition theologies into the three classical categories. The definition is a direct filter that retains only those substrates whose phase is zero and whose sigma-charge equals one.
Claim. Let $T$ be a theology, i.e., a finite list of substrates. Each substrate carries a phase in the natural numbers (zero denoting the canonical sector) and a sigma-charge in the integers. Then divine$(T)$ is the sublist consisting exactly of those substrates satisfying phase $=0$ and sigma $=1$.
background
A theology is an abbrev for List Substrate. The Substrate structure equips each element with a label (String), a phase in Nat (zero = canonical), and a sigma-charge in Int. The isDivine predicate on Substrate holds precisely when phase equals zero and sigma equals one, identifying the canonical unit-charge occupant.
proof idea
The definition is a one-line wrapper that applies the filter operation to the input list T using the isDivine predicate on Substrate.
why it matters
This definition supplies the core extraction used by isMonotheistic (length exactly one), isPolytheistic (length at least two), and isAtheistic (length zero). It implements the module's structural claim that monotheism is the sigma-conserving position with a unique substrate at canonical phase and sigma = 1, closing the trichotomy and feeding the theorems that polytheism with two canonical unit-charge substrates violates total sigma = 1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.