Jcost_is_reciprocal
Jcost satisfies the reciprocal symmetry axiom F(x) = F(1/x) for all x > 0. Researchers citing the T5 uniqueness theorem in CostUniqueness would reference this to verify that the candidate cost meets the symmetry requirement before invoking convexity and calibration. The proof is a one-line term that applies the Jcost symmetry lemma directly to the IsReciprocalCost definition.
claimThe function $Jcost : (0,∞) → ℝ$ satisfies $Jcost(x) = Jcost(x^{-1})$ for every $x > 0$.
background
The CostUniqueness module consolidates results to prove that any cost functional obeying symmetry, unit normalization, strict convexity, and calibration equals Jcost on the positive reals; this is the main T5 uniqueness theorem. IsReciprocalCost is the predicate requiring F(x) = F(1/x) for all x > 0, introduced in the FunctionalEquation submodule as Definition 2.1. Jcost itself is the explicit cost (x + x^{-1})/2 - 1, whose symmetry Jcost(x) = Jcost(x^{-1}) for x > 0 is already established by the lemma Jcost_symm in both the Cost and JcostCore files.
proof idea
The declaration is a term-mode one-liner. It constructs the required function by applying the lemma Jcost_symm (which states Jcost x = Jcost x^{-1} under the hypothesis 0 < x) pointwise to the universal quantifier in the definition of IsReciprocalCost.
why it matters in Recognition Science
This result discharges the reciprocal-symmetry half of the axioms needed for the main uniqueness theorem T5 in the same module. It sits inside the forcing chain at T5 J-uniqueness and confirms that the explicit Jcost candidate satisfies the symmetry leg of the Recognition Composition Law before convexity and calibration are applied. No open questions are left at this step; the declaration is fully proved and used only internally to close the uniqueness argument.
scope and limits
- Does not establish uniqueness of Jcost by itself.
- Does not address normalization, convexity, or calibration axioms.
- Applies only to the explicit Jcost; does not quantify over other candidate functionals.
- Restricted to positive reals; says nothing about zero or negative arguments.
formal statement (Lean)
145theorem Jcost_is_reciprocal : FunctionalEquation.IsReciprocalCost Jcost :=
proof body
Term-mode proof.
146 fun x hx => Jcost_symm hx
147
148/-- `Jcost` is normalized at `1`. -/