existenceCert
plain-language theorem explainer
existenceCert assembles the zero-cost property of J at unity, the positivity of J elsewhere, and the count of five existence modes into a single certificate. Recognition Science researchers cite it to formalize the pre-Big-Bang identification of existence with J-cost zero. The construction directly references three sibling theorems without further proof steps.
Claim. Let $J$ be the J-cost function. There exists a certificate $C$ such that the cardinality of the set of existence modes equals five, $J(1)=0$, and $J(x)>0$ for all $x>0$ with $x≠1$.
background
The module establishes existence as the cost-zero condition in Recognition Science. Per the module documentation, existence itself equals the cost-zero condition, with nothing corresponding to J(x) tending to infinity as x tends to zero, and something to J(x) equaling zero at x equals one. Five modes of existence are posited across domains, matching dimension five.
proof idea
existenceCert is defined by direct field assignment in the structure ExistenceCert. The five_modes component receives the value from existenceModeCount. The existence_zero component receives existence_zero_cost. The non_existence_positive component receives non_existence_costs. This constitutes a one-line wrapper construction with no additional logical steps.
why it matters
The declaration provides the concrete witness for the Recognition Science claim that existence is the unique zero of the J-cost function. It fulfills the key structural requirements outlined in the module documentation for the five-mode ontology. No downstream uses appear in the current dependency graph, yet it anchors the philosophical foundation linking J-cost to pre-Big-Bang existence. It connects to the framework's emphasis on J-uniqueness and the cost functional as the origin of ontology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.