jcost_isCostRequirements
plain-language theorem explainer
The canonical recognition cost J(x)=(x+x^{-1})/2-1 meets the two CostRequirements axioms: unit vanishing J(1)=0 and reciprocal symmetry on positives. Anyone citing the PRC completeness-independence theorems needs this certificate so the premise is a genuine cost model, not mere functional closure. The proof is a one-line structure constructor from the existing symmetry and unit lemmas.
Claim. The map $J:\mathbb{R}_{>0}\to\mathbb{R}$ given by $J(x)=\frac{x+x^{-1}}{2}-1$ satisfies the recognition-cost requirements: $J(1)=0$, and $J(x)=J(x^{-1})$ whenever $x>0$.
background
In the Cost module, a recognition cost is any real function F on positives that obeys two structural laws packaged as CostRequirements: reciprocal symmetry F(x)=F(x^{-1}) for x>0, and the unit law F(1)=0. The canonical candidate is the J-cost J(x)=(x+x^{-1})/2-1, equivalently cosh(log x)-1, which is the unique continuous solution forced by the Recognition Composition Law (T5 in the forcing chain).
This module (PRCCompletenessIndependence) separates order-completeness of the ambient field from those cost laws. Upstream lemmas already establish Jcost_symm (symmetry via the squared form and field simplification) and Jcost_unit0 (direct evaluation at 1). The present theorem simply records that those two facts assemble into the CostRequirements structure, so later independence statements can quantify over genuine cost models rather than ad-hoc closed sets.
proof idea
One-line structure introduction. The proof supplies the two fields of CostRequirements by applying the existing lemmas Jcost_symm (for the symmetric component, under the hypothesis 0<x) and Jcost_unit0 (for the unit0 component). No new algebra is performed.
why it matters
This certificate upgrades the completeness-independence story from "closed under a function" to "models the genuine cost axioms." Downstream, completeness_not_forced_by_genuine_cost_laws and the sibling completeness_is_exactly_the_continuum rely on J being a bona fide cost so a skeptic cannot dismiss the independence as an artifact of a weak premise. It is also consumed by costLambda_symm in PRCCalibrationIndependence, which lifts reciprocal symmetry to the calibrated family. In the forcing chain this sits under T5 (J-uniqueness): once J is fixed, the only remaining commitments (continuum completeness, D=3, eight-tick) are independent of the cost laws themselves.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.