PRCPrimeCalibrationForcesPrimeIdentityBranchUniformityTarget_iff_identity_iff_two
plain-language theorem explainer
Equates two prime-calibration targets on native ratio characters: full identity-branch uniformity across prime axes, and identity orientation on any prime axis exactly when the distinguished orbit-2 axis is identity-oriented. Anyone closing the native-cost uniqueness or universal-foundation certificate cites this bridge. The proof is a pure bidirectional term pairing the two one-way implication lemmas.
Claim. The following two statements are equivalent. (A) Branch uniformity: for every ratio character that is prime-direction calibrated, identity orientation on any native prime axis forces every native prime axis onto the identity branch. (B) Identity-iff-two: for every such calibrated character, a native prime axis is identity-oriented if and only if the distinguished orbit-$2$ prime axis is identity-oriented.
background
In the Primitive Recognition Calculus, a ratio character $\chi$ is a map on ratio orbits that encodes how recognition cost orients along multiplicative axes. Prime-direction calibration restricts $\chi$ so that native prime axes behave coherently under the cost law. Two residual targets remain after that calibration is imposed.
The branch-uniformity target asks that once any identity-oriented native prime axis appears, every native prime axis sits on the identity branch (a trace-free global locking condition). The identity-iff-two target is thinner: identity orientation on an arbitrary prime axis is equivalent to identity orientation on the distinguished orbit-$2$ prime axis. Orbit $2$ is the canonical reference axis in the prime-axis trace graph already shown to be structurally connected upstream.
Both targets are quantified over the same class of calibrated ratio characters; this declaration only compares the two Prop-level packages.
proof idea
Term-mode $\leftrightarrow$ constructor. The forward direction applies PRCPrimeCalibrationForcesPrimeIdentityIffTwoPrimeIdentityTarget_of_branch_uniformity, which, for a fixed calibrated character, reduces branch uniformity to the identity-iff-two predicate via the character-level lemma PRCCharacterPrimeIdentityIffTwoPrimeIdentity_of_branch_uniform. The reverse direction applies PRCPrimeCalibrationForcesPrimeIdentityBranchUniformityTarget_of_identity_iff_two, which lifts identity-iff-two back to branch uniformity by PRCCharacterPrimeIdentityBranchUniform_of_identity_iff_two. No extra hypotheses or rewriting are needed; the two one-way theorems are exactly the two halves of the biconditional.
why it matters
This is a packaging lemma inside native-cost uniqueness: it lets later steps treat branch uniformity and the orbit-2 identity criterion as interchangeable. Immediately downstream, PRCPrimeCalibrationForcesPrimeIdentityBranchUniformityTarget_iff_identity_forces_two composes this equivalence with a further reduction to the one-sided "identity forces two" target, tightening the calibration ladder. The same bridge is consumed by prc_universal_foundation_conditional_certificate in UniversalFoundation, which assembles kernel, real-complete ordered field, and trace-logic certificates into the conditional universal-foundation package. In the broader RS forcing chain this sits under cost uniqueness for the native $J$-cost (T5 landmark), ensuring prime-axis orientation cannot split once calibration is fixed. It does not itself prove either target; it only identifies them.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.