PRCCharacterMixedNonunitWitnessesReflectPrimeWitnesses_of_split
plain-language theorem explainer
If a ratio-orbit character satisfies the split mixed-nonunit reflection property (identity and reciprocal branches each pull back to the prime axis under one shared antecedent), then it satisfies the composite reflection form: mixed nonunit witnesses imply mixed prime-axis witnesses. Cited by the split/composite equivalence and by prime-calibration forcing. Proof is a one-line unpacking of the conjunction.
Claim. Let $\chi$ be a map on ratio orbits. Suppose $\chi$ satisfies the split mixed-nonunit reflection property: the identity branch and the reciprocal branch each separately send mixed nonunit witnesses to prime-axis witnesses under the same mixed-context antecedent. Then $\chi$ satisfies the composite mixed-nonunit reflection property: if both a mixed nonunit identity witness and a mixed nonunit reciprocal witness exist, then mixed prime-axis witnesses with cross-equality already exist.
background
In the Primitive Recognition Calculus, a ratio orbit is a rational display: signed-orbit numerator over a nonzero distinction-natural denominator. Characters $\chi$ act on these orbits. Native-cost uniqueness tracks how orbit directions (identity versus reciprocal) behave on nonunit loci versus the prime axis.
The composite reflection property is the reverse bridge not supplied by product propagation: existence of mixed nonunit witnesses in both directions forces existence of mixed prime-axis witnesses with cross-equality. Its split packaging factors that single implication into two branch reflections that share one mixed-context antecedent: identity nonunit witnesses pull back to prime-axis identity witnesses, and reciprocal nonunit witnesses pull back to prime-axis reciprocal witnesses.
This module develops uniqueness of the native cost character on ratio orbits; the reflection lemmas close the nonunit-to-prime direction of the composite bridge.
proof idea
One-line wrapper. The split hypothesis is the conjunction of the identity-branch and reciprocal-branch reflection properties. Introduce the mixed-nonunit antecedent of the composite implication, apply each conjunct of the split to that same antecedent, and pair the two conclusions to obtain the composite consequent.
why it matters
This is one direction of the equivalence between composite and split mixed-nonunit reflection, so later proofs may use whichever packaging is convenient. Downstream, the prime-calibration forcing target is recovered from its split packaging by applying this conversion: once calibration forces the two branch reflections, the composite reflection target follows at once.
In the native-cost uniqueness chain, reflection closes the bridge from mixed nonunit witnesses back onto the prime axis, complementing forward product-propagation. The result sits in the foundation layer that pins the unique native cost character before mass-ladder and constant extraction; it does not itself invoke J-uniqueness (T5) or the Recognition Composition Law, but supplies a structural step those later uniqueness arguments rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.