PRCJCostCertificate
plain-language theorem explainer
Bundles the Primitive Recognition Calculus cost pass into one Prop: rational J-cost on ratio orbits, bridge to real J-cost, reciprocal and normalization invariance, canonical RCL, and the existing continuous-real uniqueness theorem, plus a named native-uniqueness target. Kernel and cost-pass constructors cite it as the cost-stage certificate. As a structure of hypotheses, there is no proof body; inhabitants discharge each field separately.
Claim. A certificate asserting: (i) on every ratio orbit $q$, the PRC cost equals $(q+q^{-1})/2-1$ in $\mathbb{Q}$; (ii) that rational value equals $J(q)$ in $\mathbb{R}$; (iii) cost is reciprocal-symmetric and normalization-invariant under cross-equality of orbits; (iv) the Recognition Composition Law holds on nonzero ratio orbits; (v) any continuous positive-real $F$ satisfying Aczél smoothness, reciprocity, normalization, composition, and calibration equals $J$; (vi) the named native uniqueness target is self-identified for a later pass.
background
Primitive Recognition Calculus (PRC) works on discrete ratio orbits before continuous reals. The cost on an orbit is the classical recognition cost $J(x)=(x+x^{-1})/2-1$ (also $\cosh(\log x)-1$), forced uniquely in the continuous setting by the Recognition Composition Law together with reciprocity, normalization, calibration, and regularity (Aczél smoothness: continuous d'Alembert solutions are $C^\infty$).
Sibling lemmas in this module already establish the rational formula (onRatioOrbit_toRat), the real bridge (onRatioOrbit_toReal_jcost), reciprocal symmetry, and normalization invariance. The native uniqueness target is the missing discrete theorem: every admissible PRC cost on normalized ratio orbits equals the canonical orbit cost, with continuous uniqueness only as a corollary.
This structure packages those obligations into one Prop so the first-pass kernel can point at a single cost-stage certificate rather than a scatter of lemmas.
proof idea
No proof body: this is a structure (definition of a Prop). An inhabitant is assembled fieldwise. The companion theorem prc_jcost_certificate fills the fields by naming the sibling lemmas: rational formula from onRatioOrbit_toRat, real bridge from onRatioOrbit_toReal_jcost, reciprocal from reciprocal_symmetric, normalization from normalized_invariant, and canonical RCL by a short tactic proof on the orbit cross-equality. The continuous uniqueness field reuses the existing real-domain theorem under AczelSmoothnessPackage and the standard cost hypotheses. The last field is definitional self-equality of PRCNativeCostUniquenessTarget.
why it matters
Closes the cost stage of the first PRC theorem chain. Downstream, prc_jcost_certificate inhabits this structure, and KernelFirstPassCertificate bundles it among the concrete Lean objects for each first-pass stage ("bundling certificate, not yet the final inevitability theorem").
In the Recognition framework this is the discrete face of T5 J-uniqueness and the RCL: $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$, with $J$ forced as $(x+x^{-1})/2-1$. The certificate bridges the rational orbit surface honestly to continuous uniqueness while explicitly naming the open native target: classify admissible PRC costs on orbits first, then transport to reals as a corollary, rather than taking the real theorem as premise.
Until that native uniqueness is proved, the cost pass is closed only relative to the continuous theorem and the listed orbit identities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.