Jcost_is_reciprocal
plain-language theorem explainer
Jcost obeys the reciprocal symmetry axiom of the functional equation framework. Workers on cost uniqueness in Recognition Science cite this to confirm the candidate J satisfies the required F(x) = F(1/x) property before invoking the full T5 theorem. The proof is a one-line term that feeds the positivity hypothesis directly into the Jcost_symm lemma.
Claim. The function $J : (0,∞) → ℝ$ satisfies $J(x) = J(x^{-1})$ for all $x > 0$.
background
The CostUniqueness module consolidates results toward the main T5 uniqueness theorem: any cost functional obeying symmetry, unit normalization, strict convexity and calibration equals Jcost on the positive reals. Jcost itself is the explicit function built from the Recognition Composition Law and the phi-ladder. The upstream lemma Jcost_symm states that Jcost x equals Jcost of its reciprocal whenever x > 0; the IsReciprocalCost definition packages this symmetry as the predicate ∀ x > 0, F x = F x^{-1}.
proof idea
Term-mode one-liner. The proof constructs the required function by applying the Jcost_symm lemma to the supplied positivity witness hx, returning the equality Jcost x = Jcost x^{-1} directly.
why it matters
The declaration verifies that Jcost meets the reciprocal-cost axiom needed for the T5 uniqueness theorem stated in the module doc. It sits inside the J-uniqueness step of the forcing chain and supplies one of the four required properties (symmetry, normalization, convexity, calibration) before the main uniqueness result is assembled. No downstream uses appear in the current graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.