jcost_eq_zero_iff
J-cost vanishes for positive reals precisely at unity. F1 paper authors cite the result when they need the unique minimizer of the reciprocal cost. The argument rewrites via the squared-ratio identity, uses positivity to conclude the difference is zero, and recovers the unit case by substitution.
claimFor every real number $x > 0$, $J(x) = 0$ if and only if $x = 1$, where $J(x) := 1/2 (x + x^{-1}) - 1$.
background
The module develops the log-domain geometry of the canonical reciprocal cost J(x) = 1/2 (x + x^{-1}) - 1. This cost serves as the basic deviation measure in multiplicative settings for the F1 foundation paper, which also treats geometric-mean optimality and simultaneous versus sequential descent.
proof idea
The forward direction assumes Jcost x = 0 with x > 0. It invokes the squared-form lemma Jcost_eq_sq to replace the cost by (x - 1)^2 / (2x). Positivity of the denominator then forces (x - 1)^2 = 0, hence x = 1. The converse direction substitutes x = 1 into the unit lemma Jcost_unit0.
why it matters in Recognition Science
F1.1.3 supplies the uniqueness of the zero of J, which is invoked directly by the ratio form F1.2.1 (jcost_ratio_zero_iff) that equates vanishing cost on a ratio to equality of numerator and denominator. In the Recognition framework this pins the fixed point of the J map, consistent with T5 J-uniqueness in the forcing chain.
scope and limits
- Does not apply when x ≤ 0.
- Does not address complex or vector-valued arguments.
- Does not derive the result from the Recognition Composition Law.
- Does not quantify growth of J away from unity.
Lean usage
theorem jcost_ratio_zero_iff {v n : ℝ} (hv : 0 < v) (hn : 0 < n) : Jcost (v / n) = 0 ↔ v = n := by have hvn : 0 < v / n := div_pos hv hn; rw [jcost_eq_zero_iff hvn]; exact div_eq_one_iff_eq (ne_of_gt hn)formal statement (Lean)
42theorem jcost_eq_zero_iff {x : ℝ} (hx : 0 < x) : Jcost x = 0 ↔ x = 1 := by
proof body
Tactic-mode proof.
43 constructor
44 · intro h
45 have hne : x ≠ 0 := ne_of_gt hx
46 rw [Jcost_eq_sq hne] at h
47 have hden : 0 < 2 * x := by positivity
48 have hsq : (x - 1) ^ 2 = 0 := by
49 by_contra hne'
50 have : 0 < (x - 1) ^ 2 := by positivity
51 have := div_pos this hden
52 linarith
53 have := sq_eq_zero_iff.mp hsq
54 linarith
55 · intro h; subst h; exact Jcost_unit0
56
57/-- **F1.1.4**: J(x) = J(1/x) for x > 0 -/