PRCCharacterPrimeIdentityRespectsCanonicalAddTrace
plain-language theorem explainer
Identity orientation of a ratio character transports between prime axes that share the canonical finite δ-orbit merger of their sum. Anyone proving native-cost uniqueness or character branch-uniformity cites this as the witness-free form of prime-identity transport. The declaration is a Prop packaging: for primes p,r, if both orbit-position traces extend into the sum trace and χ fixes p's prime direction, then χ fixes r's.
Claim. For a map $\chi$ on ratio orbits, whenever $p$ and $r$ are prime distinction-naturals whose orbit-position traces both extend into the orbit-position trace of $p+r$, if $\chi$ fixes the prime direction of $p$ up to cross-equality, then $\chi$ also fixes the prime direction of $r$ up to cross-equality.
background
In the Primitive Recognition Calculus, a finite trace is built by successive distinction acts (empty, or extend by one act). Trace extension means the longer trace is the shorter one followed by a suffix. Each distinction-natural carries an orbit-position trace recording its finite δ-orbit history; for primes p and r the sum p+r supplies a canonical common finite merger of those histories.
A ratio character χ is a self-map on ratio orbits. Cross-equality of χ(d) with d means the character leaves the direction d in the identity orientation (the orientation tied to the J-cost minimum at the identity event). The local module develops native-cost uniqueness: which structural conditions on χ force the cost extracted from the character to match the unique J-cost of the forcing chain.
Upstream, Extends is the K2.5 suffix relation on traces. The present Prop specializes common-trace transport to the single canonical witness orbitPositionTrace(p+r), stripping arbitrary intermediate traces.
proof idea
Pure Prop definition, not a proved theorem. The body is the universal quantification itself: for all prime orbits p,r, the two Extends hypotheses into orbitPositionTrace(p+r), plus cross-equality of χ on p's prime direction, imply cross-equality of χ on r's prime direction. No tactics or lemmas are applied; downstream theorems treat the name as the packaged hypothesis.
why it matters
This is the canonical-add-trace form of prime-identity transport inside PRC native-cost uniqueness. Downstream it is shown equivalent to branch-uniformity, to common-trace-extension respect, and to trace-connected respect (the three iff theorems in the same module). Those equivalences let later arguments drop arbitrary witnesses and work only with the finite δ-merger p+r.
In the broader Recognition framework the package feeds the uniqueness path toward the native cost matching J (T5 J-uniqueness: J(x)=(x+x^{-1})/2-1). The doc-comment states the intent: remove the arbitrary witness from common-trace transport so the only remaining content is that the character respects the canonical finite δ-trace merger of two prime axes. Closing this interface is a step toward forcing the cost functional equation (RCL) from PRC structure alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.