PRCPrimeCalibrationForcesPrimeIdentityBranchUniformityTarget_iff_identity_forces_two
plain-language theorem explainer
Prime-calibration branch uniformity is equivalent to the one-sided rule that identity on any calibrated prime axis forces identity on the orbit-2 axis. Anyone chaining native-cost uniqueness or the universal foundation certificate cites this bridge. The proof is a two-step Iff.trans through the intermediate identity-iff-two target.
Claim. The following are equivalent for ratio characters that are prime-direction calibrated: (i) every identity-oriented native prime axis forces all native prime axes onto the identity branch; (ii) identity at any calibrated prime axis forces identity at the distinguished orbit-$2$ prime axis.
background
In the Primitive Recognition Calculus, a ratio character $\chi$ assigns to each ratio orbit another orbit and is required to obey the PRC ratio-character axioms. Prime-direction calibration means $\chi$ is aligned on the native prime axes. Each such axis may sit on the identity branch or the reciprocal branch.
The branch-uniformity target asserts that if any native prime axis is identity-oriented under a calibrated character, then every native prime axis is identity-oriented. The one-sided forces-two target is weaker in appearance: identity anywhere among calibrated primes forces identity specifically at the orbit-$2$ axis (the distinguished generator of the prime-axis trace graph).
An intermediate target, identity-iff-two, equates identity on an arbitrary calibrated prime with identity on orbit $2$. Prior lemmas already show branch uniformity $\leftrightarrow$ identity-iff-two and identity-iff-two $\leftrightarrow$ forces-two; this declaration closes the remaining edge.
proof idea
Pure term-mode composition of two already-proved equivalences. First apply the lemma equating branch uniformity with the identity-iff-two target; then apply the lemma equating identity-iff-two with the one-sided forces-two target. The result is the direct Iff by trans. No new case analysis or character arithmetic is introduced.
why it matters
This bridge lets downstream arguments treat branch uniformity and the orbit-$2$ forcing rule as interchangeable. It is used immediately to equate prime-pair product cost consistency with forces-two, and to rewrite the negation of forces-two as existence of a distinct-prime mixed-pair witness character. The universal foundation conditional certificate consumes the same uniqueness spine, so the equivalence sits on the path that packages native-cost uniqueness into the PRC foundation certificate. In the broader Recognition chain this is bookkeeping inside native J-cost uniqueness (the T5 uniqueness of $J(x)=(x+x^{-1})/2-1$), not a new forcing step, but it collapses several target formulations into one reusable Prop.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.