PRCCharacterMixedNonunitWitnessesReflectPrimeWitnesses_iff_split
plain-language theorem explainer
The composite reflection property for a ratio-orbit character (mixed nonunit witnesses force mixed prime-axis witnesses) is equivalent to its split form, which separates identity and reciprocal branches. Anyone working the PRC native-cost uniqueness bridge between nonunit and prime-axis orientation will cite this. The proof is a two-line term packaging the two already-proved one-direction lemmas.
Claim. For any map $\chi$ on rational orbits, the following are equivalent: (i) whenever mixed nonunit identity and reciprocal witnesses both exist for $\chi$, mixed prime-axis witnesses already exist; (ii) the same antecedent forces the identity branch and the reciprocal branch each to pull back separately to the prime axis.
background
In the Primitive Recognition Calculus, a RatioOrbit is a rational display: signed-orbit numerator over a nonzero distinction-nat denominator. Characters act as maps $\chi$ on these orbits and can orient orbit directions as identity-type or reciprocal-type relative to a cost or doubled-trace reading.
The composite reflection property says: if there are mixed nonunit witnesses (some nonunit orbit identity-oriented and some reciprocal-oriented), then mixed prime-axis witnesses must already exist. Its doc calls this "the exact reverse direction not supplied by product propagation." The split form factors that implication into two independent pullbacks: identity nonunit witnesses reflect to prime-axis identity, and reciprocal nonunit witnesses reflect to prime-axis reciprocal, under the same mixed antecedent.
This sits in the native-cost uniqueness module, where character/trace matching and d'Alembert-type constraints force the cost functional toward the unique $J$-shape used later in the forcing chain.
proof idea
Pure term-mode packaging of an already-established biconditional. The left-to-right arrow is PRCCharacterMixedNonunitWitnessesReflectPrimeWitnessesSplit_of_reflects (from the composite reflection hypothesis, construct the pair of branch-wise reflection props). The right-to-left arrow is PRCCharacterMixedNonunitWitnessesReflectPrimeWitnesses_of_split (from the split pair, feed the mixed antecedent into each conjunct and reassemble the composite conclusion). No new arithmetic or case analysis appears here.
why it matters
Native-cost uniqueness needs a clean interface between "composite" and "split" formulations of mixed-witness reflection so later arguments can switch forms without re-proving orientation transport. The composite form matches the global bridge language (nonunit mixed data force prime-axis mixed data); the split form is what branch-wise coherence lemmas actually discharge.
No downstream users are recorded yet on this declaration, so it is presently a local API glue step inside PRC native-cost uniqueness rather than a cited parent theorem. In the broader Recognition picture it supports the path that isolates the unique cost compatible with recognition composition (the $J$-cost of T5 and the RCL), by ensuring character orientation data on nonunits cannot appear without corresponding prime-axis structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.