prc_cost_joint_stratification
plain-language theorem explainer
The honest cost-joint stratification holds as one Prop: every positive scale of the native cost family obeys reciprocity, normalization, the composition law, and continuity; the gauge orbit is power-rescaling of J; calibration selects exactly J; without calibration J is not forced. Cite this when arguing what the δ-program does and does not force at the cost joint. Term-mode assembly of four already-proved pass theorems into the structure fields.
Claim. The recognition cost joint admits an honest stratification: for every scale $\lambda>0$, the scaled cost $C_\lambda$ is reciprocal, normalized, continuous on $(0,\infty)$, and satisfies the Recognition Composition Law; the gauge orbit is $C_\lambda(x)=J(x^\lambda)$ with $(xy)^\lambda=x^\lambda y^\lambda$; calibration holds iff $\lambda=1$, selecting the native $J$; and the composition law without calibration does not force $J$.
background
In the Primitive Recognition Calculus the native cost is the unique continuous solution of the Recognition Composition Law
$J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$
with reciprocity and normalization; classically $J(x)=(x+x^{-1})/2-1$ (T5). The one-parameter family costLambda rescales the argument, $C_\lambda(x)=J(x^\lambda)$, and is the algebraic gauge orbit of that solution.
PRCCostJointStratification packages four claims as a single Prop: the full scale family satisfies the algebraic and continuity laws (form_forced); the orbit identity and multiplicative powering hold (gauge_orbit); a calibration condition holds exactly at $\lambda=1$, selecting $J$ (calibration_selects_jcost); and dropping calibration leaves a genuine free orbit (gauge_not_forced). The module assembles these from the pass 331/331b/332/333 theorems rather than restating them in prose.
Upstream, the composition-law and calibration lemmas live in the PRC J-cost and monotone d'Alembert layers; the functional-equation package supplies the reciprocal/normalized/composition predicates used in the fields.
proof idea
Pure term-mode structure construction. form_forced is filled by composition_law_admits_full_scale_family (every $\lambda>0$ yields a reciprocal, normalized, composition-law, continuous-on-$(0,\infty)$ cost). gauge_orbit is the pair of projections from calibration_is_mul_automorphism_gauge (orbit identity $C_\lambda(x)=J(x^\lambda)$ and multiplicative powering). calibration_selects_jcost pairs isCalibrated_costLambda_pos_iff with costLambda_one_eq_jcost (calibration iff $\lambda=1$, and $\lambda=1$ recovers $J$). gauge_not_forced is composition_law_without_calibration_does_not_force_jcost. No new algebra is proved here; the object only bundles the four discharges.
why it matters
This is the load-bearing cost joint of the δ-program: it states, as checked Lean rather than documentation, exactly what the composition law forces and what remains gauge. Downstream it is consumed by prc_full_stratification, which lifts the cost joint into the full carrier/completion stratification (δ-only floor, trace-closure boundary, and the strict order between them).
In framework terms this is the local face of T5 J-uniqueness and the RCL: the continuous calibrated completion selects $J$, while the uncalibrated algebraic laws alone leave the positive scale orbit free. The companion strength-separation object in the same module then records that δ-only does not force $J$ and that trace-closure strictly exceeds δ-only in the commitment order. Without this joint package, full stratification would have to re-prove or re-assert the cost side field-by-field.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.