PRCPrimeCalibrationForcesPrimeIdentityCommonTraceExtensionTarget_of_canonical_add_trace
plain-language theorem explainer
If prime calibration forces identity orientation through the canonical additive orbit-position trace, then it also forces identity orientation on any explicitly witnessed common finite δ-trace extension. Anyone equating the two trace-transport targets cites this implication. The proof is a one-line pointwise application of the character-level transport lemma.
Claim. Assume that every ratio-orbit character that is prime-direction calibrated has identity orientation transporting through the canonical finite common extension given by the orbit-position trace of $p+r$. Then every such character also has identity orientation respecting any explicitly witnessed common finite $\delta$-trace extension.
background
In the Primitive Recognition Calculus, ratio-orbit characters are maps on ratio orbits that encode orientation and cost data. Prime-direction calibration pins how those characters behave on prime generators. Two related targets ask whether that calibration forces identity orientation to survive finite trace transport.
The canonical-add-trace target requires transport through the concrete common extension orbitPositionTrace(p+r). The common-trace-extension target is the sharper form: identity orientation must respect any explicitly witnessed common finite δ-orbit trace extension, not only the canonical additive one.
Upstream, the character-level lemma already shows that respecting the canonical additive trace implies respecting a witnessed common extension (the extra witness hypotheses are unused). This declaration lifts that implication from a single character to the quantified calibration targets.
proof idea
Term-mode wrapper. Introduce a character χ together with the ratio-character and prime-calibration hypotheses. Apply the assumed canonical-add-trace target at χ to obtain the character-level canonical property, then feed that into the upstream lemma PRCCharacterPrimeIdentityRespectsCommonTraceExtension_of_canonical_add_trace, which drops the unused common-extension witnesses and yields the common-trace-extension property for χ.
why it matters
This is one direction of the equivalence between the canonical-add-trace and common-trace-extension calibration targets. The sibling iff theorem packages both directions so the two Prop targets may be used interchangeably in uniqueness arguments.
Downstream it feeds the native-cost uniqueness blocker certificate and, through the foundation stack, the conditional universal-foundation certificate. In the Recognition forcing chain this sits inside the PRC native-cost uniqueness layer that constrains admissible cost characters before J-uniqueness (T5) and the self-similar fixed point φ (T6) are invoked at higher levels. It closes no open scaffold by itself; it only collapses two equivalent formulations of the same prime-identity transport demand.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.