PRCPrimeCalibrationForcesTwoPrimeBranchControlsPrimesTarget
plain-language theorem explainer
Distinguished-prime normal form of a native-cost uniqueness blocker: every prime-direction-calibrated ratio character must have the branch chosen at orbit 2 control every native prime branch. Cited by the uniqueness blocker certificate and by equivalence theorems linking coherent prime orientation to identity-iff-two forms. Pure Prop packaging; no proof content beyond the quantified implication.
Claim. For every map $\chi$ from ratio orbits to ratio orbits, if $\chi$ is a ratio character and is prime-direction calibrated, then the branch chosen at the distinguished orbit $2$ controls every native prime branch.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer numerator over a nonzero orbit denominator (K4.7). The distinguished orbit $2$ is the ratio orbit with numerator the signed orbit of two and denominator one. A ratio character $\chi$ is a structure-preserving map on these orbits used to build native cost from multiplicative data.
Prime-direction calibration means the character's orientation on prime axes has been fixed by the calibration data. The two-prime branch-control property then says that whatever branch $\chi$ selects at orbit $2$ already determines the branch on every native prime. This sits inside the native-cost uniqueness module, which isolates exact Lean targets for what still blocks uniqueness of the native cost functional.
Upstream identity and mismatch machinery (zero self-comparison cost, reciprocal symmetry) supply the ambient comparison language; the local work is about how prime axes orient once calibration is imposed.
proof idea
Definitional Prop only: the body is the universal quantification over ratio-orbit maps $\chi$, assuming the ratio-character and prime-direction-calibration hypotheses, and concluding the two-prime branch-controls-primes property. No tactics, no lemmas applied at this site; downstream theorems discharge or refute instances of this target.
why it matters
This is the distinguished-prime normal form of the same blocker that appears in the Pass-25 native cost uniqueness certificate: uniqueness is not closed, but the missing mathematics is split into exact Lean targets. It is definitionally interchangeable (via proved iff theorems) with the coherent-prime-orientation target and with the prime-identity-iff-two-identity target, so any of the three forms can be used as the working statement.
Downstream, the blocker certificate records this (and sibling) targets; one-direction lemmas turn a proof of this target into coherent orientation or identity-iff-two, and conversely. In the broader RS forcing picture this is bookkeeping toward T5 J-uniqueness: native cost must be forced to the unique J-cost once prime branches cannot freeload independent orientations after calibration at $2$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.