cost_zero_set_singleton
For positive real x the J-cost vanishes precisely when x equals 1. Researchers tracing the Recognition Science pre-Big-Bang uniqueness claims cite this result to establish that the cost minimum on R+ is a singleton. The term proof splits the biconditional, deriving a contradiction from the positivity lemma when x differs from 1 and substituting the unit value to recover zero cost.
claimFor every $x > 0$, $J(x) = 0$ if and only if $x = 1$, where $J(x) = (x-1)^2/(2x)$ is the cost function.
background
The module ExistenceUniquenessFromCost supplies the uniqueness half of the claim that RSExists(x) is equivalent to J(x) = 0 and to x = 1. Jcost is the explicit cost J(x) = (x-1)^2/(2x) for x > 0, obtained as the squared ratio that measures multiplicative deviation from unity. Upstream lemmas Jcost_pos_of_ne_one and Jcost_unit0 establish strict positivity away from 1 and exact vanishing at the unit point.
proof idea
The term proof introduces positive x and splits the biconditional. The forward direction assumes Jcost x = 0 together with x ≠ 1, then applies Jcost_pos_of_ne_one to reach a contradiction. The reverse direction substitutes x = 1 and invokes Jcost_unit0 to obtain zero cost directly.
why it matters in Recognition Science
The theorem feeds cost_zero_set_has_one_member, which equates any two cost-zero points, and existenceUniquenessCert, which packages the full certificate including isolation and log-symmetry. It closes the pre-Big-Bang uniqueness step in the Recognition framework, confirming that the sole cost minimum lies at the self-similar fixed point and is consistent with the eight-tick octave structure.
scope and limits
- Does not extend the statement to non-positive reals.
- Does not derive the explicit algebraic form of Jcost.
- Does not address multiplicity questions in discrete or higher-dimensional settings.
- Does not prove existence of a global minimum, only uniqueness of the zero.
formal statement (Lean)
33theorem cost_zero_set_singleton :
34 ∀ x : ℝ, 0 < x → (Jcost x = 0 ↔ x = 1) := by
proof body
Term-mode proof.
35 intro x hx
36 constructor
37 · intro h
38 by_contra hne
39 exact absurd h (ne_of_gt (Jcost_pos_of_ne_one x hx hne))
40 · rintro rfl; exact Jcost_unit0
41
42/-- The cost-zero set in ℝ+ has cardinality 1 (in the sense that any two
43 members are equal). -/