PRCJCostStrengthSeparation
plain-language theorem explainer
A single Prop packaging the claim that the cost J is not forced on the δ-only rational carrier, is selected by calibration on the continuous completion, and that completion strength strictly exceeds δ-only strength. Anyone citing J-uniqueness (T5) at the PRC level needs this object. It is a three-field structure discharged by orientation freedom, calibration uniqueness, and the StrengthTag order.
Claim. A strength-separation statement asserts three facts: (i) for every prime distinction orbit $p$ there is a ratio character $\chi$ (unital, multiplicative, reciprocal under cross-equivalence) that fixes every other prime axis and fails to fix the $p$-axis; (ii) for every $\lambda>0$, the scaled cost $\mathrm{cost}_\lambda$ is calibrated ($G''(0)=1$) iff $\lambda=1$; (iii) $\delta$-only strength is strictly below trace-closure strength in the commitment order.
background
Primitive Recognition Calculus (PRC) builds costs on a δ-native rational carrier before any real completion. The carrier uses distinction naturals (finite orbits of repeated distinction) and ratio orbits (signed numerator over nonzero distinction denominator). Equality of ratios is cross-equivalence: two ratio orbits match when cross-multiplied signed orbits balance.
A ratio character is a map on ratio orbits that is unital, multiplicative, and reciprocal up to cross-equivalence. Such characters factor d'Alembert-type cost identities on the rational carrier. Calibration of a real cost $F$ is the condition $G''(0)=1$ where $G(t)=F(e^t)$, equivalently $\lim_{t\to 0} 2F(e^t)/t^2=1$. The one-parameter family $\mathrm{cost}_\lambda$ is the forced cost shape scaled by $\lambda$; calibration picks a unique scale.
The module's local setting is native-cost uniqueness: which data force the J-cost $J(x)=(x+x^{-1})/2-1$ versus which leave orientation free. Strength tags order commitments from δ-only data up through trace closure on the completion.
proof idea
No proof body: this is a Prop structure with three fields. The inhabiting theorem fills them by direct appeal to three prior results: orientation freedom of every prime axis supplies the δ-only non-forcing field; the positive-scale calibration criterion for the λ-family supplies the completion-selects-J field; and the strict inequality of strength tags supplies the ordered gap. Each field is therefore a one-line wrapper onto an already-proved lemma, assembled into one checked object.
why it matters
This is the type-level form of "J is forced only on the continuous completion": the same forcing question gets opposite answers at two strengths, with a genuine strengthening between them. Downstream, the inhabiting theorem prc_jcost_strength_separation witnesses the structure with no project-local axioms, and the full stratification object consumes the same uniqueness story as its completion boundary. In the forcing chain this is the PRC-native face of T5 (J-uniqueness via the Recognition Composition Law): without the third field one would have two unrelated facts; with it the gap between failing strength and forcing strength is real and ordered. That is the non-bookkeeping content of native-cost uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.