prc_jcost_strength_separation
plain-language theorem explainer
At δ-only carrier strength the native cost is not forced to be J; at trace-closure completion strength it is selected, and completion is strictly stronger in the ledger order. Anyone citing the PRC cost-forcing stratification or residual one-real gauge freedom needs this separation. The proof is a three-field structure instance wiring existing lemmas for free prime-axis orientation, calibrated costLambda selection, and the strength-tag inequality.
Claim. The strength-separation proposition for native $J$-forcing holds: (i) for every prime distinction orbit $p$ there is a ratio character that satisfies the cross-equation on every other prime axis yet fails on $p$ (so $\delta$-only does not force $J$); (ii) at trace-closure completion, positive calibration selects the $J$-cost family; (iii) trace-closure is strictly stronger than $\delta$-only in the K1 ledger order.
background
Primitive Recognition Calculus studies which algebraic cost laws force the unique native cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), the T5 landmark of the forcing chain. Two commitment strengths are compared. The $\delta$-only carrier works with discrete prime-orbit ratio data and cross-equation constraints on ratio characters. Trace-closure completion adds the continuous/trace hypotheses that pin the cost on the positives.
The structure being inhabited packages three claims as a single Prop: non-forcing at $\delta$-only, selection of $J$ at completion, and a strict inequality of strength tags. Ratio characters are maps on ratio orbits preserving the multiplicative recognizer structure; the cross-equation is the discrete stand-in for reciprocal/composition matching along a prime direction.
Local module setting is native-cost uniqueness inside PRC: stratify what the four algebraic laws (reciprocal symmetry, normalization, RCL composition, continuity) leave free before calibration, and prove $J$ appears only after the stronger completion commitment.
proof idea
Term-mode structure instance with three field assignments, no new reasoning.
delta_only_does_not_forceis exactlyprc_every_prime_axis_orientation_free: every prime axis still has an orientation-free character that breaks cross-equality only on that axis, so $\delta$-only never pins $J$.completion_selects_jcostis the lambdafun _ hl => isCalibrated_costLambda_pos_iff hl, reducing completion selection to the calibrated positive-costLambdacharacterization.strength_strictly_increasesis the existing inequalityStrengthTag.deltaOnly_lt_traceClosurein the K1 ledger order.
The whole proof is assembly of prior certificates into the single separation object.
why it matters
This is the type-level form of "J is forced only on the continuous completion": opposite answers at two strengths, with a genuine strengthening between them. Downstream, prc_full_stratification discharges its stratification fields from proven theorems and cites this separation as part of the no-axioms full stack; prc_cost_freedom_is_one_real then upgrades residual freedom after the four laws to a unique positive real (gauge as a torsor under $\mathrm{Aut}(\mathbb{R}_{>0},\times)$).
In the Recognition framework this sits under T5 J-uniqueness and the Recognition Composition Law: the discrete carrier alone does not force $J$, matching the program claim that forcing needs the completion/trace layer. It closes the strength-gap half of native-cost uniqueness without project-local axioms, so later completeness and calibration arguments can treat the separation as a checked Prop rather than narrative.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.