isMonotheistic
plain-language theorem explainer
Monotheism is defined as the property that a theological model contains exactly one divine substrate. Researchers formalizing σ-conserving ontologies cite this predicate when partitioning models into atheistic, monotheistic, and polytheistic classes under global phase and charge conservation. The definition is realized by a direct length-equality check on the divine sublist extracted from the model list.
Claim. A theological model $T$ is monotheistic if and only if the number of divine substrates in $T$ equals one.
background
The module formalizes the structural claim that σ-conservation across moves in any ontology with a global phase forces at most one divine substrate. A theological model is an ordered list of substrates, each carrying a phase value and a σ-charge. The divine substrates are those occupying the canonical sector (phase ≡ 0) with σ = 1. Upstream results on phase functions and σ-conservation supply the predicates that isolate the divine sublist.
proof idea
The definition is a one-line abbreviation that applies the divine predicate to the input list and asserts that the resulting sublist has length exactly one.
why it matters
This predicate supplies the monotheistic case inside the trichotomy theorem that exhausts all theological models and inside the one-statement summary of substrate-independent monotheism. It is invoked by the unique-occupant certification and by the contrast with the two-divine case whose total σ equals 2. The definition closes the structural half of the argument that monotheism is the only σ-conserving theological position.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.