PRCCharacterTraceMatchesCost_of_cost_crossEq
plain-language theorem explainer
If a cost map F agrees on every ratio orbit with the cost built from a character χ (under cross-multiplication equality), then the doubled trace of χ matches the native doubled-trace cost of F. Used when lifting character factorization of a native cost to d'Alembert/trace form. Proof rewrites both sides to rational displays and closes by linear arithmetic on the verifier values.
Claim. Let $F$ and $\chi$ be maps on ratio orbits. Suppose that for every ratio orbit $q$, $F(q)$ is cross-equivalent to the cost derived from the character $\chi$ at $q$. Then for every $q$, $\chi(q)+\chi(q)^{-1}$ is cross-equivalent to the native doubled-trace cost of $F$ at $q$ (i.e. the trace form of character factorization holds).
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): cross-multiplication balance of numerator/denominator orbits, which agrees with ordinary rational equality of the verifier maps toRat.
The target predicate PRCCharacterTraceMatchesCost is the trace form of character factorization. Its doc states it is "the d'Alembert lift hidden inside $F = J \circ \chi$: the generated trace of $\chi q$ must be $2(F q + 1)$". Concretely it asserts that $\chi(q)+\chi(q)^{-1}$ is cross-equivalent to nativeCostDoubledTrace F q for every $q$.
The hypothesis packages pointwise agreement of $F$ with costFromCharacter χ under crossEq. That character cost is the PRC-native avatar of the J-cost $J(x)=(x+x^{-1})/2-1$ from the forcing chain (T5), so the doubled-trace identity is the algebraic rearrangement $x+x^{-1}=2(J(x)+1)$.
proof idea
Term/tactic hybrid, one goal per orbit $q$. Instantiate the hypothesis at $q$, then convert both the hypothesis and the goal from crossEq to rational equality via crossEq_iff_toRat_eq. Rewrite the hypothesis through costFromCharacter_toRat. Expand the goal's native doubled-trace side by unfolding nativeCostDoubledTrace and doubledTraceValue, then push toRat through add, recip, mul, the constant two, and one using the IntegerRational lemmas add_toRat, recip_toRat, mul_toRat, two_toRat, one_toRat. The resulting rational identity is closed by linarith.
why it matters
This is the bridge from pointwise cost-character agreement to the d'Alembert/trace matching predicate used in native-cost uniqueness. The sole downstream consumer is PRCNativeCostCharacterTraceLiftTarget_of_factorization, which, given a full character factorization of a native cost, packages a character together with this trace-matching fact to discharge the trace-lift target.
In framework terms it realises the T5 J-uniqueness geometry inside PRC: once $F$ factors as $J\circ\chi$ on ratio orbits, the Recognition Composition Law / d'Alembert structure is recovered as the doubled-trace identity $\chi+\chi^{-1}=2(F+1)$. It does not itself prove uniqueness of $F$; it only converts the factorization witness into the form the uniqueness pipeline consumes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.