ExistenceCert
plain-language theorem explainer
ExistenceCert bundles three properties that identify existence with the zero of the J-cost function across five enumerated modes. A foundational physicist or philosopher working in Recognition Science would cite it to formalize that only the unit state incurs zero cost while all other positive states are costly. The structure is introduced by direct field specification that invokes the Fintype cardinality of ExistenceMode together with the stated equalities and inequalities on Jcost.
Claim. Let $J$ be the J-cost function. The structure ExistenceCert asserts that the set of existence modes has cardinality five, that $J(1)=0$, and that $J(x)>0$ whenever $x>0$ and $x≠1$.
background
The module develops a pre-Big-Bang philosophy in which existence is the unique cost-zero state of the J-cost functional. The inductive type ExistenceMode enumerates five modes (physical, biological, conscious, mathematical, ethical) and carries a Fintype instance so that its cardinality is exactly five. Jcost is imported from the Cost module; the module documentation states that J(1)=0 while J(x)→∞ as x→0, making absolute nothing infinitely costly.
proof idea
As a structure definition the object is introduced by naming its three fields directly: five_modes records Fintype.card ExistenceMode = 5, existence_zero records Jcost 1 = 0, and non_existence_positive records the universal quantification ∀ {x:ℝ}, 0<x → x≠1 → 0 < Jcost x. No tactics or lemmas are applied; the definition is accepted once the field types are well-formed.
why it matters
ExistenceCert supplies the data for the downstream definition existenceCert, which packages the three properties into a single certificate. It realizes the Recognition Science claim that existence equals the cost-zero condition and aligns with the five-dimensional configuration space (D=5) and the uniqueness of the J-function fixed point from the forcing chain. The construction touches the open mapping from the five abstract modes onto concrete physical or conscious realizations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.