existenceModeCount
plain-language theorem explainer
The theorem establishes that the inductive type ExistenceMode has exactly five elements, corresponding to the physical, biological, conscious, mathematical, and ethical modes. A researcher assembling the existence certificate in the pre-Big-Bang philosophy module would reference this result to confirm the configuration dimension equals five. The proof proceeds via a single decision tactic that enumerates the constructors of the inductive definition.
Claim. The finite type of existence modes has cardinality five: $|$physical, biological, conscious, mathematical, ethical$| = 5$.
background
In the Existence from J-Cost module, the Recognition Science framework posits that existence corresponds to the zero-cost state of the J-functional, where J(1) = 0 while J(x) > 0 for x ≠ 1 and J(x) → ∞ as x → 0. The module defines ExistenceMode as an inductive type with five constructors: physical, biological, conscious, mathematical, and ethical. This enumeration aligns with the configuration dimension D = 5 in the RS philosophy section, which treats these as the distinct domains of existence.
proof idea
The proof is a one-line wrapper that invokes the decide tactic on the Fintype.card expression. This tactic leverages the automatically derived Fintype instance for the inductive type ExistenceMode, which has exactly five constructors, to compute the cardinality as 5.
why it matters
This cardinality result supplies the five_modes field in the existenceCert definition, which certifies the zero-cost nature of existence across the five modes. It fills the structural claim in the module documentation that five modes of existence correspond to configDim D = 5. Within the broader framework, it supports the pre-Big-Bang philosophy by grounding the distinction between existence (J=0) and non-existence (J>0) in a finite enumeration of domains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.