PRCPrimeCalibrationForcesTwoPrimeBranchControlsPrimesTarget_of_prime_identity_iff_two
plain-language theorem explainer
If prime calibration forces identity on every prime axis exactly when it forces identity on the orbit-2 axis, then the branch chosen at orbit 2 controls every native prime branch. Native-cost uniqueness and coherent-orientation arguments cite this one-way reduction. The proof feeds the already-proved local orientation target and the identity-iff-two hypothesis into the character-level branch-control lemma.
Claim. Assume that for every ratio-orbit character $\chi$ that is prime-direction calibrated, $\chi$ has identity orientation on an arbitrary prime axis if and only if it has identity orientation on the distinguished orbit-$2$ prime axis. Then every such $\chi$ has the property that the branch chosen at orbit $2$ controls every native prime branch.
background
In the Primitive Recognition Calculus native-cost uniqueness module, ratio-orbit characters $\chi : \mathrm{RatioOrbit} \to \mathrm{RatioOrbit}$ encode admissible orientations of multiplicative ratio data. Prime-direction calibration restricts $\chi$ on prime axes so that cost and orientation data stay compatible with the native $J$-cost structure.
Two blocker targets package the same obstruction in different normal forms. The identity-iff-two target says calibration forces identity orientation on any prime axis exactly when it forces identity on the distinguished orbit-$2$ axis. The two-prime-branch-controls target says the branch chosen at orbit $2$ controls every native prime branch.
Upstream, local prime orientation under calibration is already proved unconditionally. At character level, local orientation plus identity-iff-two yields two-prime branch control. This declaration lifts that character lemma to the calibration-target layer.
proof idea
Short tactic proof. Introduce a ratio character $\chi$ that is a PRC ratio character and prime-direction calibrated. Apply the character-level lemma that local prime orientation plus identity-iff-two implies two-prime branch control. Discharge local orientation by the already-proved calibration-forces-local-orientation target at $(\chi,h\chi,h\mathrm{prime})$. Discharge identity-iff-two by applying the hypothesis target at the same triple. No further case analysis.
why it matters
This is one direction of the equivalence between the identity-iff-two and two-prime-branch-controls calibration targets; the sibling iff theorem packages both directions. Downstream, coherent prime orientation is obtained from prime-pair product cost consistency by routing through this implication and the two-prime-branch-controls normal form.
It feeds the native-cost uniqueness blocker certificate and, via that stack, the conditional universal-foundation certificate. In the Recognition forcing picture this is bookkeeping inside native-cost uniqueness for ratio characters, not a T5–T8 landmark itself: it ensures the distinguished prime $2$ can serve as the normal-form axis for branch control before uniqueness of the native cost is certified.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.