PRCPrimeCalibrationForcesTwoPrimeReciprocalForcesPrimeReciprocalTarget_iff_identity_forces_two
plain-language theorem explainer
Equates two distinguished-axis calibration targets for ratio characters: reciprocal globalization from the orbit-2 prime axis, and identity forcing from any calibrated prime axis onto orbit-2. Native-cost uniqueness proofs cite it to move blockers between the reciprocal and identity branches. The proof is the pair of already-established one-way implications.
Claim. For ratio characters with prime-direction calibration, the following are equivalent: (i) if the orbit-$2$ prime axis lies on the reciprocal branch, then every native prime axis is reciprocal; (ii) if any calibrated prime axis is identity, then the orbit-$2$ prime axis is identity.
background
In the Primitive Recognition Calculus, a ratio character $\chi$ assigns to each ratio orbit a transformed orbit, subject to multiplicative and calibration constraints. Prime-direction calibration fixes how $\chi$ acts on the distinguished prime axes of the ratio lattice. Each such axis may sit on the identity branch or the reciprocal branch.
Two Prop-level targets package the desired forcing statements. The reciprocal target says: once calibration places the orbit-$2$ prime axis on the reciprocal branch, every native prime axis must follow. The identity target says the dual one-sided claim: identity at any calibrated prime axis forces identity at orbit-$2$.
Both targets live in the native-cost uniqueness module, which aims to pin the cost functional on calibrated characters before the broader J-uniqueness and forcing chain (T5 onward) are invoked.
proof idea
Term-mode biconditional: the forward direction is the existing lemma that derives the identity target from the reciprocal target (via the intermediate reciprocal-excludes-identity form); the reverse direction is the dual lemma that derives the reciprocal target from the identity target. The proof is exactly the pair of those two arrows, with no extra tactics.
why it matters
Collapses two branch-selection blockers into one logical package. Downstream, the reciprocal target is refuted by transporting the already-refuted identity target across this equivalence (...Target_refuted). That refutation feeds prc_native_cost_uniqueness_blocker_certificate, which records which factorization and calibration targets are proved versus eliminated. The same certificate surface is consumed by the conditional universal-foundation certificate.
In framework terms this is bookkeeping inside the PRC layer that precedes T5 J-uniqueness: it ensures the native cost cannot hide on a mixed identity/reciprocal prime configuration once calibration is fixed. No new physics constant is forced here; the gain is a clean equivalence for the uniqueness ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.