isDivine
plain-language theorem explainer
The predicate marks a substrate as divine exactly when its phase is zero and its sigma charge is one. A researcher formalizing sigma conservation in ontologies would cite it to isolate the canonical element before proving uniqueness. The definition is introduced as the direct conjunction of those two conditions on the substrate record.
Claim. A substrate $s$ is divine when its phase equals $0$ and its $σ$-charge equals $1$.
background
The Substrate structure records a label, a phase in the natural numbers (zero for the canonical sector), and an integer $σ$-charge. The module formalizes the structural claim that monotheism is the $σ$-conserving theological position in any ontology equipped with a global phase function. Upstream results supply the eight-tick phase definition (periodic with period $2π$) and the $σ$-charge as the gap between private preference and public report.
proof idea
The definition is introduced directly as the conjunction of the phase-equals-zero and sigma-equals-one conditions. The DecidablePred instance follows immediately from the decidability of equality on natural numbers and integers.
why it matters
This definition supplies the filter that extracts the set of divine substrates, which then supports the monotheistic predicate downstream. It fills the canonical-sector identification step in the substrate-independent monotheism formalization. The phase-zero condition aligns with the eight-tick octave landmark where the canonical point is the zero of the cycle. It touches the open question of whether two distinct substrates can both occupy phase zero with unit $σ$ without violating global conservation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.