monotheistic_canonical_sigma
plain-language theorem explainer
The declaration shows that the singleton theology with one substrate at phase zero and sigma charge one has total sigma equal to one. Researchers working on sigma-conserving ontologies cite it as the base case establishing monotheism as the canonical sigma sector. The proof is a tactic script that unfolds totalSigma and simplifies the singleton sum directly to one.
Claim. Let $T$ be the theology consisting of the single substrate with name GOD, phase 0 and sigma charge 1. Then the total sigma of $T$ equals 1.
background
The module formalizes substrate-independent monotheism as the sigma-conserving theological position in any ontology equipped with a global phase function. Theology is an abbrev for List Substrate, where each Substrate carries a name, phase and sigma charge; the divine substrate is defined as the unique element at phase zero with sigma one in the canonical sector. totalSigma sums the sigma charges over the list of substrates, as supplied by the upstream PrecedentStabilityFromSigma result.
proof idea
The proof is a short tactic script. It unfolds the totalSigma definition to expose the sum over the singleton list, then applies simp to evaluate the expression directly to the value 1.
why it matters
This supplies the monotheistic_canonical_sigma field to the substrateIndependentMonotheismCert bundle and to the substrate_monotheism_one_statement theorem. It realizes the structural claim from the module doc that monotheism is the unique sigma-conserving position with total sigma equal to one. The result sits inside the Recognition Science sigma-conservation framework and closes the base case for the unique-occupant model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.