existenceUniquenessCert
The declaration packages a certificate that the J-cost on positive reals vanishes if and only if the argument equals 1, that this zero is unique, that the cost is symmetric under inversion, and that it is strictly positive away from 1. A physicist working on the pre-Big-Bang sector would cite it to invoke uniqueness of the cost minimum when building the forcing chain from T5 onward. The construction is a direct record that wires four upstream theorems into the four fields of the certificate structure.
claimThe certificate asserts that for every $x > 0$, $J(x) = 0$ if and only if $x = 1$, that any two positive reals with $J(x) = J(y) = 0$ satisfy $x = y$, that $J(x) = J(x^{-1})$, and that $J(x) > 0$ whenever $x > 0$ and $x ≠ 1$.
background
The module ExistenceUniquenessFromCost supplies the uniqueness half of the statement that RSExists(x) holds precisely when J-cost vanishes. Module documentation states: “there is exactly one point in ℝ+ with J-cost zero, and this uniqueness is derivable from the J-cost functional form alone.” It also notes that the result addresses the pre-BB claim that “existence is not plural.” J-cost is the functional J(x) = (x + x^{-1})/2 − 1 (equivalently cosh(log x) − 1) whose only zero on the positive reals is at unity.
proof idea
The definition constructs the ExistenceUniquenessCert structure by direct field assignment. It sets zero_iff_one to cost_zero_set_singleton, unique_member to cost_zero_set_has_one_member, log_symmetric to jcost_log_symmetric, and isolated to jcost_isolated_from_zero. The proof is therefore a one-line wrapper that assembles the four component theorems into a single certificate object.
why it matters in Recognition Science
The certificate supplies the explicit uniqueness statement required for the pre-Big-Bang complement and reinforces T5 J-uniqueness in the forcing chain. It shows there cannot be two distinct cost minima on ℝ+, a fact used to derive the phi-ladder and the eight-tick octave. No downstream theorems are yet recorded, but the object is the canonical interface for any later derivation that needs the singleton property of the cost-zero set.
scope and limits
- Does not derive the explicit algebraic form of J.
- Does not address existence statements outside the cost-zero set.
- Does not connect to numerical constants such as alpha or G.
- Does not extend isolation or symmetry to complex arguments.
formal statement (Lean)
67def existenceUniquenessCert : ExistenceUniquenessCert where
68 zero_iff_one := @cost_zero_set_singleton
proof body
Definition body.
69 unique_member := @cost_zero_set_has_one_member
70 log_symmetric := @jcost_log_symmetric
71 isolated := @jcost_isolated_from_zero
72
73end
74end ExistenceUniquenessFromCost
75end Foundation
76end IndisputableMonolith