Theology
plain-language theorem explainer
A theological model is formalized as a list of substrates, each carrying a string label, phase in natural numbers, and integer sigma charge. Researchers formalizing substrate-independent monotheism cite this as the carrier type for classifying theologies by number of divine elements. The declaration is a direct type abbreviation with no proof obligations or computational reduction.
Claim. A theology is a list of substrates, where each substrate is a structure with label in strings, phase in natural numbers (0 canonical), and sigma charge in integers.
background
The module formalizes the structural claim that monotheism is the sigma-conserving theological position in any ontology with a global phase function. A substrate is the structure with label : String, phase : Nat, sigma : Int, deriving DecidableEq. The local setting treats a theology as any finite list of such substrates, with the divine predicate selecting those at phase 0 and sigma 1. Upstream structures supply the phase and sigma conventions via the ILG substrate definition and phi-forcing derivations, but the abbreviation itself introduces no new axioms.
proof idea
Direct abbreviation equating Theology to List Substrate. No tactics or lemmas are applied; the definition inherits the structure fields and decidable equality from the sibling Substrate declaration.
why it matters
This supplies the base type for the downstream predicates divine, isMonotheistic, isPolytheistic, and isAtheistic that partition theologies by count of canonical sigma=1 substrates. It fills the module's structural side of the AR-essay claim that sigma-conservation forces at most one divine substrate. The definition touches the open falsifier of a consistent ontology admitting two distinct phase-0, sigma=1 substrates without conservation violation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.