PRCPrimeCalibrationForcesMixedNonunitWitnessesReflectPrimeWitnessesTarget_iff_split
plain-language theorem explainer
The composite reflection target for mixed nonunit witnesses is equivalent to its split into identity and reciprocal halves. Native-cost uniqueness and universal-foundation certificate work cite this bridge. The proof is a pure Iff constructor from the two one-way lemmas already proved in-module.
Claim. The following are equivalent: (i) every prime-direction-calibrated ratio character has the property that mixed nonunit witnesses reflect down to mixed prime-axis witnesses; (ii) the same holds separately for the identity-witness half and the reciprocal-witness half (their conjunction).
background
In the Primitive Recognition Calculus, a ratio character $\chi$ is a map on ratio orbits obeying the multiplicative character laws of the PRC kernel. Prime-direction calibration means $\chi$ is already fixed on the prime axes used for native-cost comparison.
The reflection target asserts that any mixed nonunit witness for such a $\chi$ must reflect down to a mixed prime-axis witness. That is the composite bridge form used when arguing that nonunit composite structure cannot create new cost witnesses beyond the primes.
The split target factors the same claim into two independent halves: identity-witness reflection and reciprocal-witness reflection. The module treats the split as the operational form of the current no-mixed-witness blocker (rule out mixed primes first, then lift control to nonunit composites).
proof idea
Term-mode Iff introduction. The forward direction is the already-proved lemma that the composite reflection target implies the split (constructor on the two halves). The reverse direction is the already-proved lemma that the split implies the composite (introduce $\chi$, apply the split-to-composite character lemma). No new arithmetic or case analysis appears here.
why it matters
This equivalence lets the native-cost uniqueness pipeline switch freely between the compact reflection form and the split form used in blocker certificates. Downstream it is consumed by prc_native_cost_uniqueness_blocker_certificate, which packages zero-calibrated factorization targets and signed-admissible refutations, and by prc_universal_foundation_conditional_certificate in UniversalFoundation.
In the broader RS forcing picture this sits inside the PRC native-cost uniqueness layer that underwrites uniqueness of the J-cost (T5) once characters are prime-calibrated. It does not itself force $\phi$ or the eight-tick structure; it only keeps the mixed-witness bridge interchangeable across certificate styles.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.