PRCCharacterPrimeIdentityRespectsCanonicalAddTrace_iff_common_trace_extension
plain-language theorem explainer
Equivalence of two formulations of prime-identity transport for a ratio-orbit character χ: the canonical-add form (common extension fixed as the position trace of p+r) and the common-trace form (arbitrary finite δ-trace witness). Cited by native-cost uniqueness and universal-foundation certificates. Proof is a term-mode packaging of the two already-proved directions.
Claim. For any map $\chi$ from ratio orbits to ratio orbits, the following are equivalent: (i) if identity orientation of $\chi$ holds on a prime axis $p$ and both prime-axis position traces extend into the canonical merger $\mathrm{orbitPositionTrace}(p+r)$, then identity orientation holds on the prime axis $r$; (ii) the same transport holds whenever both prime-axis traces extend into some common finite $\delta$-trace $T$.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer-numerator / nonzero-orbit-denominator display of a rational. Characters are maps $\chi$ on ratio orbits; the native-cost uniqueness program constrains which characters can arise from a cost.
Two Props encode a prime-identity transport rule. The common-trace form says: if $\chi$ is identity-oriented on prime axis $p$ and the position traces of primes $p$ and $r$ both extend into one finite $\delta$-trace $T$, then $\chi$ is identity-oriented on $r$. The canonical-add form specializes the witness to $\mathrm{orbitPositionTrace}(p+r)$, the finite merger of the two prime axes; as its doc states, this "removes the arbitrary witness from common-trace transport."
Both directions of the equivalence are already proved as separate lemmas in this module; the present declaration only identifies them.
proof idea
Term-mode Iff.intro via the anonymous constructor. Left-to-right applies PRCCharacterPrimeIdentityRespectsCommonTraceExtension_of_canonical_add_trace; right-to-left applies PRCCharacterPrimeIdentityRespectsCanonicalAddTrace_of_common_trace_extension. The latter is the specialization that instantiates the arbitrary common trace $T$ by orbitPositionTrace (p + r). No new arithmetic is done here.
why it matters
Native-cost uniqueness needs a clean, witness-free statement of how identity orientation moves between prime axes under δ-trace merger. This iff lets downstream code switch between the explicit common-extension form and the canonical-add form without proof obligation churn.
It is consumed by prc_native_cost_uniqueness_blocker_certificate (the blocker certificate assembling zero-calibrated factorization targets) and by prc_universal_foundation_conditional_certificate in UniversalFoundation (kernel, real-complete ordered field, and trace-logic bundle). In the broader RS forcing picture this sits under the PRC foundation layer that feeds cost uniqueness toward the J-cost and T5 uniqueness story, though the theorem itself is purely about character/trace transport, not about J or φ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.