ExistenceUniquenessCert
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not establish the explicit algebraic form of the J-cost function.
- Does not connect uniqueness to the phi fixed point or eight-tick octave.
- Does not extend the analysis beyond the positive real line.
- Does not quantify isolation for arbitrary neighborhoods around 1.
formal statement (Lean)
59structure ExistenceUniquenessCert where
60 zero_iff_one : ∀ {x : ℝ}, 0 < x → (Jcost x = 0 ↔ x = 1)
61 unique_member : ∀ {x y : ℝ}, 0 < x → 0 < y →
62 Jcost x = 0 → Jcost y = 0 → x = y
63 log_symmetric : ∀ {x : ℝ}, 0 < x → Jcost x = Jcost x⁻¹
64 isolated : ∀ {x : ℝ}, 0 < x → x ≠ 1 → 0 < Jcost x
65
66/-- Existence uniqueness certificate. -/