PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget_of_two_prime_reciprocal_excludes
plain-language theorem explainer
Under prime-direction calibration, if every ratio character that puts the orbit-2 axis on the reciprocal branch forbids any native prime axis from staying on identity, then the same data also forbid any identity-oriented native prime witness. Native-cost uniqueness certificates and the universal-foundation conditional certificate cite this lift. The proof is a one-line reduction through the pointwise character-to-witness exclusion lemma.
Claim. Assume that for every ratio character $\chi$ that is prime-direction calibrated, if the orbit-$2$ prime axis lies on the reciprocal branch then no native prime axis remains on the identity branch. Then for every such $\chi$, if the orbit-$2$ prime axis is reciprocal-oriented, no identity-oriented native prime witness exists.
background
In the Primitive Recognition Calculus, a ratio character is a map $\chi$ on ratio orbits that encodes how each orbit is oriented (identity versus reciprocal branch) relative to the native cost. Prime-direction calibration restricts how prime axes may be oriented once the cost is fixed. The orbit-$2$ axis is the distinguished two-prime direction that appears in the mixed-branch rigidity analysis.
Two target propositions package the global claims. The two-reciprocal exclusion target asserts: under calibration, reciprocal orientation of orbit $2$ forces every native prime axis off the identity branch. The mixed-witness exclusion target is the witness-level strengthening: reciprocal orientation of orbit $2$ forbids existence of any identity-oriented native prime witness.
Upstream, the pointwise lemma already converts a character-level two-reciprocal exclusion into the corresponding witness exclusion for a fixed $\chi$. The present declaration only quantifies that conversion over calibrated characters.
proof idea
One-line wrapper. Introduce a ratio character $\chi$ together with the ratio-character and prime-direction-calibration hypotheses. Apply the given two-reciprocal exclusion target at $(\chi,h_\chi,h_{\mathrm{prime}})$ to obtain the character-level exclusion, then feed that into the upstream pointwise theorem that turns character-level two-reciprocal exclusion into mixed-witness exclusion. No further case analysis.
why it matters
This is one direction of the equivalence between the two-reciprocal exclusion target and the mixed-witness exclusion target; the sibling converse closes the iff. Downstream, the identity-forces-two route reuses this lift to obtain the witness target from a stronger identity-forcing hypothesis. Both the native-cost uniqueness blocker certificate and the universal-foundation conditional certificate depend on the witness-shaped form, so the lift is the bridge from axis-level rigidity to the certificate interface.
In the Recognition forcing chain this sits inside native-cost uniqueness for the J-cost (T5), which underwrites the unique self-similar fixed point $\varphi$ (T6) and the later dimensional and octave steps. The mixed-witness exclusion is exactly the obstruction that would be refuted by a calibrated mixed-character model; closing it keeps the character-rigidity route intact.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.