cost_crossEq_of_PRCCharacterTraceMatchesCost
plain-language theorem explainer
If a ratio-orbit character χ has doubled trace matching the native cost of F (the d'Alembert form of F = J ∘ χ), then F equals the cost reconstructed from χ, pointwise up to cross-equivalence. Used when lifting a trace-match hypothesis to full character factorization of a native cost. Proof rewrites both sides to rational equality via toRat and closes by linear arithmetic.
Claim. Let $F$ and $\chi$ map ratio orbits to ratio orbits. Suppose that for every orbit $q$, $\chi(q)+\chi(q)^{-1}$ is cross-equivalent to the native doubled-trace $2\bigl(F(q)+1\bigr)$. Then for every $q$, $F(q)$ is cross-equivalent to the native cost reconstructed from the character $\chi$ at $q$.
background
In the Primitive Recognition Calculus, a RatioOrbit is a rational display: a signed-orbit numerator over a nonzero distinction-nat denominator. Equality of displays is internalised as crossEq (K4.10): two orbits are equivalent when cross-multiplication balances as signed orbits. By crossEq_iff_toRat_eq, this agrees with ordinary equality of the verifier rationals toRat.
The Recognition cost is the unique J-functional $J(x)=(x+x^{-1})/2-1$ (forcing step T5). Its doubled-trace form is $x+x^{-1}=2(J(x)+1)$, the d'Alembert identity hidden inside $F=J\circ\chi$. The hypothesis PRCCharacterTraceMatchesCost asserts exactly that: for every $q$, $\chi(q)+\chi(q)^{-1}$ is cross-equivalent to nativeCostDoubledTrace F q (i.e. $2(F(q)+1)$). The reconstructed cost costFromCharacter χ is the pointwise J applied to χ on ratio orbits.
This module develops native uniqueness of that cost character on the PRC integer/rational layer, before continuum or measure arguments enter.
proof idea
Fix an arbitrary ratio orbit $q$ and pull the pointwise trace-match hypothesis. Rewrite the goal and the hypothesis along crossEq_iff_toRat_eq, so both become equalities of rationals. Expand nativeCostDoubledTrace and doubledTraceValue on the hypothesis side, pushing toRat through addition, reciprocal, multiplication, the constant two, and the unit via the IntegerRational lemmas add_toRat, recip_toRat, mul_toRat, two_toRat, one_toRat. On the goal side, rewrite by costFromCharacter_toRat. The resulting rational identity is then discharged by linarith.
why it matters
This is the algebraic bridge from the d'Alembert/trace form of character factorization to the actual cost-equality form $F\sim J\circ\chi$ on ratio orbits. Downstream, PRCNativeCostCharacterFactorizationTarget_of_trace_lift applies it directly: given a trace-lift witness $\langle\chi,h_\chi,h_{\mathrm{trace}}\rangle$, it packages $\langle\chi,h_\chi,\texttt{cost_crossEq_of_PRCCharacterTraceMatchesCost},h_{\mathrm{trace}}\rangle$ as a full factorization target. The zero-calibrated uniqueness theorem PRCZeroCalibratedNativeCostCharacterFactorizationTarget_proved uses the same step after obtaining a calibrated trace lift.
In the broader Recognition chain this is local bookkeeping for T5 J-uniqueness on the native PRC layer: once the doubled trace of χ matches $2(F+1)$, the cost is forced to be J of that character, with no continuum hypotheses required. It does not itself prove existence of χ; it only converts a trace match into cost cross-equivalence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.