isAtheistic
plain-language theorem explainer
A theology is atheistic precisely when its list of divine substrates is empty. Researchers formalizing the Recognition Science claim that monotheism conserves global σ-charge would cite this predicate when partitioning ontologies. The definition reduces to a direct length check on the divine list extracted from the input theology.
Claim. A theology $T$ is atheistic if and only if the number of divine substrates in $T$ is zero.
background
Theology is an abbrev for List Substrate, where each substrate carries a phase and a σ-charge. The divine list collects those substrates at canonical phase zero with σ equal to one. The module formalizes the AR-essay structural claim that any ontology with a global phase function and σ-conservation admits at most one divine substrate, partitioning models into atheistic, monotheistic, and polytheistic cases.
proof idea
One-line definition that applies the length check to the divine list of the input theology.
why it matters
This definition supplies the base case for the trichotomy theorem that every theology is exactly one of atheistic, monotheistic, or polytheistic. It feeds the substrate-monotheism one-statement, which records that a two-divine model yields total σ = 2 while the unique-occupant model yields σ = 1. It directly implements the module's claim that monotheism is the σ-conserving position in any ontology with global phase.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.