PRCPrimeCalibrationForcesPrimeReciprocalWitnessGlobalizesTarget_iff_identity_witness_excludes_reciprocal
plain-language theorem explainer
Under prime direction calibration of ratio characters, reciprocal-witness globalization is equivalent to identity-witness exclusion of reciprocal primes. Native-cost uniqueness arguments cite this bridge when collapsing orientation targets to a single obstruction. The proof is a pure Iff.trans through the shared “no mixed prime orientation” intermediate.
Claim. For ratio characters that are prime-direction calibrated, the following are equivalent: (i) if any native prime axis is reciprocal-oriented, then every native prime axis is reciprocal-oriented; (ii) if any native prime axis is identity-oriented, then no native prime axis is reciprocal-oriented.
background
In the Primitive Recognition Calculus, a ratio character is a map $\chi$ on ratio orbits that encodes how multiplicative structure is read by the native cost. Prime direction calibration restricts how $\chi$ may orient each native prime axis: either the identity branch or the reciprocal branch.
Two target propositions package the desired rigidity. Reciprocal-witness globalization says that a single reciprocal-oriented native prime forces the reciprocal branch on every native prime axis. Identity-witness exclusion says the opposite one-sided rule: once an identity-oriented prime witness exists, no reciprocal-oriented prime witness is allowed.
Both targets were already shown equivalent to the same intermediate, “no mixed prime orientation” (prime calibration forbids mixing identity and reciprocal orientations across native primes). This declaration closes the triangle by equating the two targets directly.
proof idea
Term-mode composition of two existing equivalences. First apply the theorem that reciprocal-witness globalization $\leftrightarrow$ no mixed prime orientation. Then compose with the symmetric form of the theorem that identity-witness exclusion $\leftrightarrow$ no mixed prime orientation. The common intermediate cancels, yielding the stated biconditional. No new case analysis on characters or primes is performed.
why it matters
Native cost uniqueness in PRC needs a single, non-redundant obstruction on prime orientations. Equating globalization of reciprocal witnesses with exclusion of reciprocal witnesses once an identity witness appears collapses two surface formulations into one logical package.
Downstream, the native-cost uniqueness blocker certificate and the universal-foundation conditional certificate consume this family of orientation targets. In the broader Recognition chain this sits under J-uniqueness (T5): the native cost is forced to the unique $J$-shape only after mixed prime orientations are ruled out. The declaration itself does not discharge the targets; it certifies that proving either form proves the other.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.