PRCCharacterPrimeIdentityRespectsCanonicalAddTrace_iff_trace_connected
plain-language theorem explainer
For a map χ on rational orbits, preserving identity orientation under the canonical add-trace merger of two prime axes is equivalent to preserving it along any finite δ-trace connection between those axes. Native-cost uniqueness and universal-foundation certificates cite the equivalence when collapsing transport hypotheses. The proof is a pure biconditional packaging of the two already-proved directions.
Claim. Let $\chi$ be a map on rational orbits. Then $\chi$ preserves identity orientation through the canonical finite common extension given by the position trace of $p+r$ (for prime axes $p,r$) if and only if $\chi$ preserves identity orientation whenever those prime axes are related by a finite $\delta$-trace connection.
background
In the Primitive Recognition Calculus, a rational orbit is an integer numerator over a nonzero distinction-nat denominator. Characters are maps $\chi$ on such orbits. Prime axes carry preferred directions; identity orientation means $\chi$ fixes that direction up to the cross-equality relation on orbits.
Two formulations of "identity transports between prime axes" appear. The trace-connected form says: whenever two prime axes lie in the same finite $\delta$-trace component, identity on one forces identity on the other. The canonical-add-trace form specializes the witness: identity transports through the concrete common extension given by the position trace of the sum $p+r$, provided both axes extend into that sum trace. The latter removes an arbitrary common-extension witness; only the canonical merger remains.
Both properties live in the native-cost uniqueness development, which aims to force the recognition cost character from algebraic and trace axioms alone.
proof idea
Term-mode biconditional: the forward direction is the existing lemma that canonical-add-trace respect implies trace-connected respect (via the common-trace-extension intermediate); the reverse is the existing lemma that trace-connected respect implies canonical-add-trace respect (by instantiating the connection hypothesis with the proved fact that every pair of prime axes is trace-connected, then discarding the extension premises). No new arithmetic is done here.
why it matters
The equivalence lets downstream certificates treat the cleaner canonical-add form and the more semantic trace-connected form interchangeably when stating character hypotheses. It is consumed by the native-cost uniqueness blocker certificate and by the universal-foundation conditional certificate, both of which assemble the PRC stack toward a unique native cost. In the broader Recognition Science chain this sits under the drive to J-uniqueness (T5): characters that respect prime-axis identity transport are the candidates that can match the doubled-trace d'Alembert cost and thereby force $J(x)=(x+x^{-1})/2-1$. The lemma itself closes no open gap; it only collapses two equivalent interfaces so uniqueness proofs need not carry both.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.