PRCCharacterTraceMatchesCost
plain-language theorem explainer
Packages the d'Alembert trace identity behind character factorization: for maps F and χ on ratio orbits, χ(q)+χ(q)⁻¹ equals 2(F(q)+1) under cross-multiplication, for every q. Anyone proving native-cost uniqueness or character-lift targets cites this Prop. It is a pure definitional packaging of that identity, not a proved statement.
Claim. For maps $F,\chi$ on ratio orbits, the character-trace match holds when, for every ratio orbit $q$, $$\chi(q)+\chi(q)^{-1}\;\sim\;2\bigl(F(q)+1\bigr)$$ under the internal cross-multiplication equality of ratio orbits (the PRC rational relation).
background
In the Primitive Recognition Calculus, costs and characters act on RatioOrbit: a signed-numerator / nonzero-denominator display of a rational, built entirely from δ-orbit positions. Equality of two such displays is crossEq, the K4.10 cross-multiplication balance of scaled numerators and denominators.
The classical J-cost satisfies $J(x)=(x+x^{-1})/2-1$, so the doubled d'Alembert trace is $x+x^{-1}=2(J(x)+1)$. On ratio orbits the same identity is written with the total reciprocal (sending zero to zero) and with nativeCostDoubledTrace F q := 2(F(q)+1). The present Prop asserts that the generated trace of χ matches that doubled cost trace pointwise under crossEq.
This is the exact trace form of the factorization $F=J\circ\chi$ used throughout the native-cost uniqueness module.
proof idea
Definitional Prop, not a theorem. The body is the single universal quantifier over ratio orbits q asserting crossEq between the orbit sum χ(q)+recip(χ(q)) and nativeCostDoubledTrace F q. No tactics, no lemmas applied; the meaning is entirely in the referenced orbit arithmetic and the doubled-trace abbreviation.
why it matters
This is the interface atom for character factorization in native-cost uniqueness. Two sibling theorems show it is equivalent to pointwise crossEq of F with costFromCharacter χ. The lift targets PRCNativeCostCharacterTraceLiftTarget and the zero-calibrated repair PRCZeroCalibratedNativeCostCharacterTraceLiftTarget quantify existence of a ratio character χ satisfying this Prop under native-cost hypotheses.
It also appears negatively: zeroFlatNativeCost_no_character_trace shows the zero-flat native cost admits no such χ, which is why the unqualified lift target fails and the zero-calibrated surface is the correct replacement. In the broader RS chain this is the discrete d'Alembert form of T5 J-uniqueness (J(x)=cosh(log x)-1) on ratio orbits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.