PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget_iff_two_prime_reciprocal_excludes
plain-language theorem explainer
The one-sided target (prime calibration forces identity on the orbit-2 axis once any calibrated prime is identity) is equivalent to the two-reciprocal exclusion target (if orbit-2 is reciprocal, no native prime stays on identity). Native-cost uniqueness and universal-foundation certificates cite this bridge. Proof is a pure Iff pair of the two already-proved one-direction implications.
Claim. The following are equivalent for ratio-orbit characters that are prime-direction calibrated: (i) identity on any calibrated prime axis forces identity on the orbit-$2$ prime axis; (ii) if the orbit-$2$ prime axis lies on the reciprocal branch, then no native prime axis remains on the identity branch.
background
In the Primitive Recognition Calculus, a ratio character $\chi$ is a map on ratio orbits obeying the multiplicative character laws of the PRC kernel. Prime-direction calibration means every native prime axis is fixed to one of the two admissible orientations: identity or reciprocal.
Two global targets package how calibration interacts with the distinguished orbit-$2$ axis. The first says identity anywhere on a calibrated prime forces identity at orbit $2$. The second is the contrapositive-style exclusion: reciprocal orientation at orbit $2$ forbids any residual identity-oriented native prime.
Both targets are quantified over the same class of characters (ratio character plus prime-direction calibration). The module develops them as intermediate blockers toward uniqueness of the native cost functional built from doubled-trace d'Alembert data.
proof idea
Term-mode Iff constructor. The forward direction applies the already-proved implication from the identity-forces-two target to the two-reciprocal exclusion target. The reverse applies the converse implication. Each of those lemmas reduces, after introducing a calibrated character, to a local character-level lemma relating the two pointwise properties. No new arithmetic is done here.
why it matters
This equivalence lets the native-cost uniqueness development treat the distinguished-axis forcing statement and the reciprocal-exclusion statement as interchangeable blockers. Downstream, prc_native_cost_uniqueness_blocker_certificate assembles factorization and signed-admissible refutation targets that sit on the same calibration spine; the universal-foundation conditional certificate likewise consumes the uniqueness stack. In the broader RS forcing chain, native-cost uniqueness is the PRC-side route toward the unique $J$-cost of T5 and the Recognition Composition Law, so collapsing two calibration targets into one logical unit removes a bookkeeping fork before those certificates close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.