PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget_of_identity_iff_two
plain-language theorem explainer
If prime calibration forces identity orientation on every prime axis exactly when it does so on the distinguished orbit-2 axis, then the one-sided implication also holds: identity at any calibrated prime axis forces identity at orbit 2. Native-cost uniqueness and PRC calibration arguments cite this reduction. The proof is a pointwise unwrap: apply the character-level one-direction extraction to the biconditional hypothesis.
Claim. Assume that for every ratio-orbit map $\chi$ that is a PRC ratio character and is prime-direction calibrated, identity orientation holds on an arbitrary prime axis if and only if it holds on the distinguished orbit-$2$ prime axis. Then, for every such $\chi$, identity on any calibrated prime axis forces identity on the orbit-$2$ axis.
background
In the Primitive Recognition Calculus, a ratio character is a map $\chi$ on ratio orbits that encodes orientation (identity versus reciprocal branch) along prime axes. Prime-direction calibration restricts which orientations are admissible once a native cost is fixed. The distinguished orbit-$2$ axis is the reference prime axis against which other prime axes are compared.
Two target propositions package the global calibration demand. The identity-iff-two target asserts that, under prime calibration, identity on any prime axis is equivalent to identity on orbit $2$. The one-sided distinguished-axis target asserts only the forward force: identity at any calibrated prime axis implies identity at orbit $2$.
At the single-character level, the biconditional already yields the one-sided force by taking the forward half of the equivalence. The present declaration lifts that character-level fact to the quantified target propositions used in the native-cost uniqueness certificate chain.
proof idea
Term-mode wrapper. Introduce a ratio character $\chi$ together with the ratio-character and prime-direction-calibration hypotheses. Instantiate the assumed identity-iff-two target at $\chi$ to obtain the character-level biconditional. Feed that biconditional into the upstream lemma that extracts the one-sided force from the iff at fixed $\chi$. The resulting one-sided statement is exactly the body of the distinguished-axis target.
why it matters
This is one direction of the equivalence between the identity-iff-two target and the one-sided distinguished-axis target; the sibling converse closes the other direction, and together they give the iff used downstream. The native-cost uniqueness blocker certificate and the universal-foundation conditional certificate both depend on this calibration ladder being coherent: forcing identity at orbit $2$ from any calibrated prime axis is the distinguished-axis half of the uniqueness story for the native cost (the $J$-cost side of the Recognition Composition Law and the T5 uniqueness landmark). Without the reduction, the quantified targets would not interchange, and the certificate assembly would stall on mismatched hypothesis shapes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.