PRCCostJointStratification
plain-language theorem explainer
Packages the honest terminal statement of the recognition-cost joint: algebraic laws force the one-parameter family F_λ(x)=J(x^λ) for λ>0, calibration selects λ=1 (hence J itself), and the multiplicative gauge is not fixed by algebra alone. Cite this when stating exactly what the δ-program forces versus leaves free at the cost joint. It is a Prop-structure whose four fields are the named pass-331–333 theorems, not prose.
Claim. A proposition with four conjuncts on the scaled cost family $F_\lambda$ ($\lambda>0$): (1) each $F_\lambda$ is reciprocal ($F(x)=F(1/x)$), normalized ($F(1)=0$), satisfies the recognition composition law, and is continuous on $(0,\infty)$; (2) $F_\lambda(x)=J(x^\lambda)$ with $x\mapsto x^\lambda$ multiplicative on positives; (3) calibration (second derivative of $t\mapsto F(e^t)$ at $0$ equals $1$) holds iff $\lambda=1$, and $F_1=J$ on positives; (4) some continuous reciprocal normalized composition-law cost differs from $J$.
background
Recognition cost on positive ratios is the classical $J(x)=(x+x^{-1})/2-1$. The functional-equation package isolates four properties: reciprocal symmetry $F(x)=F(1/x)$, normalization $F(1)=0$, the Recognition Composition Law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$ (here stated for a general $F$), and continuity on $(0,\infty)$. Calibration is the curvature condition $\frac{d^2}{dt^2}F(e^t)|{t=0}=1$, equivalently $\lim{t\to 0}2F(e^t)/t^2=1$.
The local setting is Primitive Recognition Calculus cost uniqueness: the δ-program forces algebraic structure on cost, but must separate form from gauge. The one-parameter family is $F_\lambda(x)=J(x^\lambda)$ for $\lambda>0$, the orbit of $J$ under the continuous automorphisms of $(\mathbb{R}_{>0},\times)$.
Upstream, IsReciprocalCost, IsNormalized, SatisfiesCompositionLaw, and IsCalibrated are the named predicates; $J$ itself is the RS-native cost used throughout the monolith (T5 J-uniqueness in the forcing chain).
proof idea
No proof body: this is a structure (a bundled Prop). The four fields are pure interfaces. Instantiation is the sibling theorem prc_cost_joint_stratification, which fills them by named results: form_forced from composition_law_admits_full_scale_family; gauge_orbit from the two halves of calibration_is_mul_automorphism_gauge; calibration_selects_jcost from isCalibrated_costLambda_pos_iff and costLambda_one_eq_jcost; gauge_not_forced from composition_law_without_calibration_does_not_force_jcost (witness $\lambda=2$). Read the structure as the exact claim surface those theorems discharge.
why it matters
This is the single exact Lean object for what is forced versus free at the load-bearing cost joint. Downstream, prc_cost_joint_stratification proves the structure holds, and PRCFullStratification embeds the cost joint into the top-level honest stratification (δ-only floor, completion boundary, carrier strictly below completion). Framework landmark: T5 forces the J-form via the composition law (RCL); calibration $\lambda^2=1$ is the within-form selector; the residual multiplicative-automorphism gauge is explicitly not pinned by δ. The doc-comment states the terminal reading: algebra forces form, calibration selects $J$, gauge value remains free. Anyone auditing whether RS overclaims uniqueness of $J$ from algebra alone should start here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.