isPolytheistic
plain-language theorem explainer
A definition classifying any theological model T as polytheistic exactly when its list of divine substrates has length at least two. Workers on the substrate-independent monotheism argument cite it to complete the exhaustive partition of ontologies. The definition is a direct length comparison on the divine sublist extracted from T.
Claim. Let $T$ be a theological model (a finite list of substrates). Let $D(T)$ be the sublist of substrates at canonical phase with unit $σ$-charge. Then $T$ is polytheistic if and only if $|D(T)| ≥ 2$.
background
The module formalizes the structural claim that monotheism is the σ-conserving theological position under a global phase function. Theology is an abbrev for List Substrate, where each substrate carries a phase and a σ-charge. The divine function (sibling definition) extracts the sublist of substrates whose phase is zero and whose σ equals one, corresponding to the canonical sector.
proof idea
One-line wrapper that applies the length comparison 2 ≤ (divine T).length directly to the input theology.
why it matters
This definition supplies one arm of the trichotomy theorem and is invoked by substrate_monotheism_one_statement to show that any two-divine-substrate model carries total σ = 2, off the canonical value of 1. It thereby supports the AR-essay claim that monotheism follows from global phase and σ-conservation (T0-T8 chain).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.