PRCPrimeCalibrationForcesPrimeIdentityWitnessGlobalizesNonunitTarget_iff_no_mixed_prime_witnesses
plain-language theorem explainer
Equivalence of two prime-floor blocker targets: the witness-globalized form (any identity-oriented calibrated prime forces identity on every nonunit orbit) is equivalent to the no-mixed-prime-witnesses form (prime calibration forbids a reciprocal-oriented prime witness once an identity-oriented one exists). Downstream refutations and native-cost uniqueness certificates cite this bridge. Proof is a term-mode Iff from the two one-sided implications.
Claim. The following are equivalent for the prime-calibration forcing targets on ratio-orbit characters: (i) whenever a character is prime-direction calibrated, an identity witness on any calibrated prime axis forces the identity choice on every nonunit orbit direction; (ii) whenever a character is prime-direction calibrated, it admits no mixed prime witnesses (no reciprocal-oriented prime witness once an identity-oriented prime witness exists).
background
In the Primitive Recognition Calculus, ratio-orbit characters assign to each ratio orbit a direction (identity or reciprocal). Prime-direction calibration restricts how those characters behave on prime axes. The native-cost uniqueness program isolates a prime-floor blocker: once calibration is in force, mixed prime orientations should be impossible.
Two Prop-level targets package that blocker. The witness-globalized target says: if any calibrated prime axis picks identity, then every nonunit orbit direction must pick identity. The no-mixed-witnesses target is the existential prime-witness form of the same idea: prime calibration forbids any reciprocal-oriented prime witness once an identity-oriented prime witness exists.
Both targets quantify over characters that are ratio characters and prime-direction calibrated. The module already proves each direction of implication between them; this declaration packages the biconditional.
proof idea
Term-mode Iff constructor. The forward arm is the already-proved implication from the globalized identity target to the no-mixed-witnesses target (introduces a calibrated character and applies the character-level no-mixed lemma). The reverse arm is the dual implication from no-mixed witnesses to the globalized identity target (same intro pattern, then the character-level globalization lemma). No extra tactics or algebraic work.
why it matters
Closes the logical gap between two blocker formulations used in native-cost uniqueness. The refutation of the globalized identity target routes through this Iff (mp into the no-mixed refutation). The native-cost uniqueness blocker certificate and the universal-foundation conditional certificate sit downstream of the same prime-floor package, so the equivalence keeps certificate statements interchangeable.
In the broader Recognition chain this is scaffolding hygiene inside the foundation layer that feeds J-uniqueness and the native cost, not a direct T5–T8 step. It lets later work refute or assume either packaging without re-proving transport.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.