ExistenceMode
plain-language theorem explainer
The inductive enumeration defines five modes of existence as physical, biological, conscious, mathematical, and ethical. Foundational researchers in Recognition Science cite this to anchor the claim that existence equals the J-cost zero condition across domains. The definition is a direct inductive construction that derives Fintype, enabling immediate cardinality computation via the decide tactic.
Claim. Let $E$ be the set of existence modes. Then $E$ consists of the five elements physical, biological, conscious, mathematical, ethical and carries decidable equality together with finite type structure.
background
The module develops the pre-Big-Bang claim that existence itself equals the cost-zero condition under the J-function. Specifically, J(1) = 0 marks the unique state of existence while J(x) > 0 for x ≠ 1 and J(x) → ∞ as x → 0. The five modes listed here correspond to configuration dimension D = 5 in this setting.
proof idea
Direct inductive definition of the five constructors followed by automatic derivation of DecidableEq, Repr, BEq, and Fintype instances. No lemmas are applied; the Fintype derivation supplies the cardinality fact used downstream.
why it matters
This supplies the five-mode enumeration required by the ExistenceCert structure, which pairs Fintype.card = 5 with the statements Jcost 1 = 0 and positivity of Jcost for x ≠ 1. It implements the configDim D = 5 asserted in the module doc-comment and feeds the explicit cardinality theorem existenceModeCount. The definition therefore grounds the extension of the J-cost framework to multiple domains while remaining within the T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.