ExistenceUniquenessCert
plain-language theorem explainer
ExistenceUniquenessCert bundles four properties of the J-cost function on positive reals: zero only at unity, uniqueness of that point, invariance under inversion, and strict positivity away from one. Researchers citing the Recognition Science pre-Big-Bang foundation would reference this to certify a unique cost minimum. The structure is assembled from four sibling lemmas each handling one property.
Claim. Let $J$ be the J-cost function. Then the certificate states that for every $x > 0$, $J(x) = 0$ if and only if $x = 1$; moreover if $J(x) = 0 = J(y)$ for $x, y > 0$ then $x = y$; $J(x) = J(1/x)$ holds for all $x > 0$; and $J(x) > 0$ whenever $x > 0$ and $x ≠ 1$.
background
The module provides a pre-Big-Bang complement to the earlier result that recognition existence RSExists(x) is equivalent to J(x) = 0 and to x = 1. The present development extracts uniqueness directly from the J-cost functional form without additional assumptions. J-cost here refers to the cost associated with the J function, whose zero set on the positive reals is shown to be the singleton {1}.
proof idea
The declaration defines a structure whose fields are populated by four lemmas from the same module: cost_zero_set_singleton supplies the zero_iff_one property, cost_zero_set_has_one_member the unique_member property, jcost_log_symmetric the log_symmetric property, and jcost_isolated_from_zero the isolated property. It functions as a direct bundling with no further reasoning steps.
why it matters
This certificate is instantiated in the existenceUniquenessCert definition, which provides the explicit uniqueness witness required by the pre-Big-Bang complement. It supports the paper proposition that existence is not plural by establishing that the cost zero set contains only one element. Within the Recognition Science framework it strengthens the J-uniqueness aspect by certifying that the fixed point at 1 is the sole location where cost vanishes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.