PRCPrimeCalibrationForcesPrimeIdentityIffTwoPrimeIdentityTarget_iff_identity_forces_two
plain-language theorem explainer
The two-sided identity-iff-two prime-calibration target is equivalent to the one-sided target that identity on any calibrated prime axis forces identity on the distinguished orbit-2 axis. Native-cost uniqueness and branch-uniformity arguments cite this to collapse those targets. Proof is a pure Iff packing of the two already-proved directed implications.
Claim. The following are equivalent. (A) For every ratio character $\chi$ that is prime-direction calibrated, identity orientation holds on a prime axis if and only if it holds on the distinguished orbit-$2$ prime axis. (B) For every such $\chi$, identity on any calibrated prime axis forces identity on the orbit-$2$ prime axis.
background
In the primitive recognition calculus, a ratio character is a map $\chi$ on ratio orbits that encodes orientation (identity versus reciprocal) along each axis. Prime-direction calibration restricts how $\chi$ may sit on prime axes. The distinguished orbit-$2$ axis is the reference prime axis against which other primes are compared.
Two Prop-level targets package the desired forcing statements. The identity-iff-two target asks that, under prime calibration, identity on any prime axis holds exactly when identity holds on orbit $2$. The one-sided target asks only the forward half: identity anywhere among calibrated primes forces identity at orbit $2$.
This module develops native-cost uniqueness via character and doubled-trace constraints. Equating the two targets lets later arguments reduce two-sided branch conditions to the simpler one-sided distinguished-axis claim (or the reverse).
proof idea
Term-mode Iff introduction. The forward direction applies the already-proved implication from the identity-iff-two target to the one-sided forces-two target (specialize the universal quantifiers and invoke the character-level one-way lemma). The reverse direction applies the converse implication, which rebuilds the biconditional at each prime from the one-sided forcing hypothesis. No new arithmetic or calibration reasoning appears here; the declaration only packages those two directed theorems.
why it matters
This equivalence is the hinge that collapses identity-iff-two language into identity-forces-two language inside native-cost uniqueness. Downstream, the branch-uniformity target is chained through this Iff to the one-sided target, and the identity-iff-two target is refuted by transporting the one-sided refutation across the equivalence. Both feed the native-cost uniqueness blocker certificate and, further out, the conditional universal-foundation certificate.
In the Recognition forcing picture this sits under native J-cost uniqueness (the T5 J-uniqueness landmark): orientation of prime axes must be rigid enough that cost characters cannot freeload on mixed identity/reciprocal branches. The declaration itself does not settle uniqueness; it only identifies which target statements are interchangeable before the refutation and certificate layers fire.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.