PRCPrimeCalibrationForcesPrimeIdentityBranchUniformityTarget_of_canonical_add_trace
plain-language theorem explainer
If prime calibration forces identity orientation to transport along the canonical add-trace (the finite common extension orbitPositionTrace of p+r), then it also forces branch uniformity: every identity-oriented native prime axis puts all native prime axes on the identity branch. Cited when equating the two calibration targets and when assembling native-cost uniqueness certificates. Proof is a pointwise reduction through the character-level implication.
Claim. Assume that for every ratio-orbit character $\chi$ that is a PRC ratio character and is prime-direction calibrated, identity orientation transports through the concrete finite common extension $\mathrm{orbitPositionTrace}(p+r)$. Then every such $\chi$ is branch-uniform: every identity-oriented native prime axis places all native prime axes on the identity branch.
background
In the Primitive Recognition Calculus, a ratio-orbit character $\chi$ is a map on ratio orbits used to build native cost. Prime-direction calibration fixes how $\chi$ orients native prime axes. Two related targets package what calibration should force at the identity orientation.
The canonical-add-trace target asks that identity orientation transport through the concrete finite common extension $\mathrm{orbitPositionTrace}(p+r)$. The branch-uniformity target is trace-free: it asks that every identity-oriented native prime axis put all native prime axes on the identity branch.
Upstream, the character-level lemma already shows that respecting canonical add-trace implies branch uniformity for a fixed $\chi$. This declaration lifts that implication from characters to the quantified calibration targets.
proof idea
Term-style tactic proof. Introduce a ratio-orbit character $\chi$ together with the hypotheses that it is a PRC ratio character and is prime-direction calibrated. Apply the assumed canonical-add-trace target at $(\chi,h_\chi,h_{\mathrm{prime}})$ to obtain that $\chi$ respects canonical add-trace. Feed that fact into PRCCharacterPrimeIdentityBranchUniform_of_canonical_add_trace, which is the character-level one-line reduction (itself just applying the add-trace hypothesis at primes $p,r$). The result is branch uniformity of $\chi$, which is exactly the branch-uniformity target.
why it matters
Closes one direction of the equivalence between the branch-uniformity target and the canonical-add-trace target (...BranchUniformityTarget_iff_canonical_add_trace). That equivalence lets the native-cost uniqueness development treat the two formulations interchangeably when discharging calibration obligations.
Downstream it appears in prc_native_cost_uniqueness_blocker_certificate and in prc_universal_foundation_conditional_certificate, so it sits on the path that packages PRC uniqueness and the conditional universal-foundation certificate. In the broader Recognition chain this is foundation scaffolding under native cost uniqueness (the J-cost / T5 layer), not a direct T6–T8 forcing step; it tightens how prime calibration forces identity-branch coherence before cost uniqueness is certified.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.