PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget_of_two_prime_reciprocal_excludes
plain-language theorem explainer
If prime calibration excludes identity on every native prime axis whenever the orbit-2 axis sits on the reciprocal branch, then identity on any calibrated prime axis forces identity on the orbit-2 axis. Cost-uniqueness and distinguished-axis arguments cite this implication. The proof feeds the proved local orientation target and the exclusion hypothesis into the character-level forcing lemma.
Claim. Assume: whenever a ratio character is prime-direction calibrated and the orbit-$2$ prime axis is reciprocal-oriented, no native prime axis remains identity-oriented. Then, for every such calibrated character, identity orientation on any native prime axis forces identity orientation on the orbit-$2$ prime axis.
background
In the Primitive Recognition Calculus, ratio characters $\chi$ act on ratio orbits and encode orientation of prime axes (identity versus reciprocal). Prime-direction calibration restricts how $\chi$ may assign those orientations. The orbit-$2$ axis is the distinguished two-prime axis used as a global reference for native cost uniqueness.
Two target propositions package the global claims. The exclusion target says that if calibration leaves orbit-$2$ on the reciprocal branch, then no native prime axis may stay on identity. The one-sided distinguished-axis target says the converse forcing direction: identity at any calibrated prime axis forces identity at orbit-$2$.
Upstream, local orientation under prime calibration is already proved, and a character-level lemma converts local orientation plus two-prime reciprocal exclusion into the identity-forces-two-identity property for a single $\chi$.
proof idea
Short tactic proof. Introduce a ratio character $\chi$ with the ratio-character and prime-calibration hypotheses. Apply the character-level lemma that local prime orientation together with two-prime reciprocal exclusion of prime identity yields prime-identity-forces-two-prime-identity. Discharge local orientation by the already-proved local prime-orientation target at $\chi$, and discharge exclusion by specializing the assumed global exclusion target at the same $\chi$.
why it matters
Closes one direction of the equivalence between the distinguished-axis identity-forcing target and the two-reciprocal exclusion target, used immediately by the corresponding iff theorem and by witness and forces variants that reduce stronger reciprocal hypotheses to this implication.
Downstream it feeds the native-cost uniqueness blocker certificate and, through that chain, the conditional universal-foundation certificate. In the Recognition framework this is bookkeeping on the prime-axis orientation side of native cost uniqueness for the J-cost (T5), not a new physical constant derivation; it keeps the orbit-$2$ axis from drifting off the identity branch once any calibrated prime is fixed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.