unique_occupant_is_monotheistic
plain-language theorem explainer
The unique-occupant model with one substrate at phase zero and unit sigma satisfies the monotheism predicate. Researchers on the substrate-independent monotheism track cite it as the base case that anchors the trichotomy. The proof is a one-line tactic that unfolds the isMonotheistic and divine predicates then resolves the claim by decision.
Claim. Let $T$ be the theology consisting of the single substrate $⟨$GOD$, 0, 1⟩$. Then $T$ is monotheistic.
background
A Theology is defined as a list of Substrates. Each Substrate carries a name, a phase value, and a sigma-charge. The divine predicate selects those substrates whose phase is zero and whose sigma-charge equals one. The module places this construction inside an ontology that carries a global phase function together with sigma-conservation across all moves. Upstream results supply the unit element in the integers and rationals derived from logic, the active-edge count per tick, and the fundamental period abbreviation, none of which are invoked in the present argument.
proof idea
The tactic proof unfolds the definitions of isMonotheistic and divine on the concrete list. It then applies the decide tactic to discharge the resulting decidable proposition.
why it matters
This theorem supplies the unique_occupant_monotheistic field inside the SubstrateIndependentMonotheismCert structure. It completes the structural claim recorded in the one-statement theorem: theological models partition into atheistic, monotheistic or polytheistic, the two-divine case yields total sigma two, and the single-occupant case yields total sigma one while satisfying the monotheism predicate. The construction aligns with the Recognition Science emphasis on conservation laws applied here to sigma-charge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.