cost_zero_set_singleton
plain-language theorem explainer
The J-cost functional vanishes on the positive reals precisely at unity. Pre-Big-Bang uniqueness arguments cite this to show the cost minimum cannot be plural. The proof splits the biconditional, applies positivity away from one on the forward leg, and substitutes the explicit zero on the reverse leg.
Claim. For every real $x > 0$, the cost $J(x) = 0$ if and only if $x = 1$.
background
The module establishes the uniqueness half of the pre-Big-Bang claim that existence is not plural: the set of positive reals with zero J-cost is a singleton. Jcost is the squared-ratio cost $J(x) = (x-1)^2/(2x)$ induced by the multiplicative recognizer. Upstream lemmas supply the two directions: Jcost is strictly positive for every $x > 0$ with $x ≠ 1$, and Jcost(1) = 0 exactly.
proof idea
Term-mode biconditional. Forward direction: assume Jcost x = 0, derive contradiction from Jcost_pos_of_ne_one when x ≠ 1. Reverse direction: substitute x = 1 into Jcost_unit0.
why it matters
Supplies the singleton property used by cost_zero_set_has_one_member and by the ExistenceUniquenessCert record. It closes the uniqueness half of the pre-Big-Bang claim that no two distinct cost minima exist on ℝ⁺, consistent with the Recognition Composition Law and the T5 J-uniqueness step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.