PRCCharacterPrimeIdentityRespectsTraceConnected
plain-language theorem explainer
A character on ratio orbits respects prime-axis trace connection when identity orientation on one prime axis transports to every prime axis linked by a finite δ-trace component. Native-cost uniqueness arguments cite this Prop as the transport rule for the identity character along the prime lattice. The declaration is pure definitional packaging of that universal quantification; no proof is attached.
Claim. For a map $\chi$ from ratio orbits to ratio orbits: whenever $p$ and $r$ are prime distinction-orbits that are prime-axis trace-connected, if $\chi$ sends the prime direction of $p$ to a cross-multiplication equivalent of itself, then $\chi$ sends the prime direction of $r$ to a cross-multiplication equivalent of itself.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer numerator over a nonzero distinction-orbit denominator (the internal PRC display of a positive rational). Two ratio orbits are cross-equivalent when the signed cross-products of numerator and denominator balance as orbits; that is the native stand-in for rational equality.
Distinction orbits are the base-neutral finite iterates of repeated distinction. A prime orbit is a nonzero, non-unit position with no nontrivial factorization. The identity event of ObserverForcing sits at the J-cost minimum $x=1$; here "identity orientation" means the character $\chi$ fixes a prime direction up to cross-equivalence.
The local module develops native uniqueness of the recognition cost. The predicate packages the rule that identity orientation transports along any finite $\delta$-trace component that already relates two prime axes (the upstream prime-axis trace-connectedness witness).
proof idea
Definitional packaging only: the body is the Prop itself, a four-quantifier implication over prime orbits $p,r$, a prime-axis trace-connectedness hypothesis, and a cross-equivalence hypothesis on $\chi$ at the prime direction of $p$, concluding the same cross-equivalence at the prime direction of $r$. No tactics, no lemmas applied inside the definition.
why it matters
This Prop is the common interface for the identity-transport half of native cost uniqueness. Downstream it is shown equivalent to canonical-add-trace respect, to common finite $\delta$-trace extension respect, and to full prime-identity trace coherence; those equivalences let uniqueness proofs switch freely among the three formulations.
In the Recognition forcing chain this sits under T5 (J-uniqueness): characters that preserve the identity orientation on the prime lattice are forced toward the unique cost $J(x)=(x+x^{-1})/2-1$ once d'Alembert and cross-equation hypotheses are restored. Parent theorems include the iff with canonical-add-trace respect and the iff with trace coherence, both used to close the native-cost uniqueness argument without external analytic assumptions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.