cost_zero_set_has_one_member
plain-language theorem explainer
Any two positive reals with vanishing J-cost must coincide. Researchers formalizing the pre-Big-Bang uniqueness claims in Recognition Science would cite this result. The proof is a one-line term wrapper that reduces both zero-cost assumptions to the singleton characterization of the zero set.
Claim. If $x > 0$, $y > 0$, $J(x) = 0$ and $J(y) = 0$, then $x = y$, where $J$ is the J-cost function on positive reals.
background
The J-cost function is the cost induced by a multiplicative recognizer comparator on positive ratios. The upstream theorem cost_zero_set_singleton states that the cost-zero set is exactly {1}: for all $x > 0$, Jcost $x = 0$ if and only if $x = 1$. This module supplies the uniqueness half of the pre-Big-Bang analysis, showing that the set of positive reals with J-cost zero has cardinality one.
proof idea
The proof is a one-line term-mode wrapper. It rewrites both hypotheses via the forward direction of cost_zero_set_singleton, reducing Jcost $x = 0$ to $x = 1$ and Jcost $y = 0$ to $y = 1$, then equates the two sides by reflexivity of equality.
why it matters
This theorem supplies the unique_member field inside existenceUniquenessCert, which bundles zero_iff_one, isolation, and log-symmetry. It directly addresses the pre-Big-Bang claim that existence is not plural. In the Recognition framework it confirms the single fixed point of the J-functional at T5, consistent with the self-similar phi fixed point at T6.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.