trichotomy
plain-language theorem explainer
Any theological model, formalized as a finite list of substrates, falls into exactly one of three exhaustive categories: atheistic (zero divine substrates), monotheistic (exactly one), or polytheistic (two or more). Researchers formalizing ontological consistency under sigma conservation in Recognition Science cite this partition to anchor uniqueness arguments. The proof executes exhaustive case analysis on the length of the divine list, dispatching the greater-than-one case with omega.
Claim. For any theological model $T$ (a finite list of substrates), exactly one of the following holds: $T$ contains no divine substrates, $T$ contains exactly one divine substrate, or $T$ contains two or more divine substrates.
background
The module formalizes the structural claim that sigma conservation forces a unique divine substrate in any ontology equipped with a global phase function. Theology is an abbreviation for List Substrate, where each substrate carries a phase and a sigma charge; the divine subset consists of those at canonical phase zero with sigma equal to one. The trichotomy supplies the partition required by the certification structure that records the one-statement claim.
proof idea
The proof unfolds the three predicates isAtheistic, isMonotheistic, and isPolytheistic. It then applies by_cases on whether the length of the divine list equals zero (left branch) or equals one (right-left branch); the remaining case is discharged by omega.
why it matters
This theorem supplies the trichotomy field of SubstrateIndependentMonotheismCert, which is assembled into substrateIndependentMonotheismCert and then invoked by substrate_monotheism_one_statement. It formalizes the partition step of the Anno Recognitionis structural claim that monotheism is the sigma-conserving position. The result precedes the separate demonstration that a two-divine-substrate model yields total sigma equal to two and therefore lies outside the canonical sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.