PRCPrimeCalibrationForcesMixedNonunitReciprocalWitnessReflectsPrimeWitnessTarget
plain-language theorem explainer
Names the reciprocal half of the mixed-context reflection obligation: every prime-calibrated ratio character must send mixed nonunit reciprocal witnesses down to prime-axis reciprocal witnesses. Cited by the native-cost uniqueness blocker certificate and the split mixed-witness target. The body is a pure Prop packaging of three named hypotheses; the companion `_proved` theorem discharges it.
Claim. For every map $\chi$ on rational orbits that is a ratio character (unit-preserving and multiplicative up to cross-equivalence) and is prime-direction calibrated (its induced cost matches canonical $J$-cost on every prime orbit), the reciprocal mixed-nonunit reflection law holds: whenever mixed nonunit witnesses exist, every reciprocal-oriented nonunit witness reflects to a reciprocal-oriented prime-axis witness.
background
In the Primitive Recognition Calculus, costs are reconstructed from ratio characters on RatioOrbit (signed numerator over a nonzero distinction-nat denominator). A PRCRatioCharacter is a quotient-native candidate for d'Alembert factorization: it fixes the unit orbit and is multiplicative up to cross-equivalence rather than definitional equality.
Prime-direction calibration requires that the cost generated from $\chi$ agree with the canonical $J$-cost on every prime orbit. The reciprocal mixed-nonunit reflection law then says that, once mixed nonunit witnesses are present, any reciprocal-oriented nonunit witness must collapse to a reciprocal-oriented witness on a prime axis.
This module packages uniqueness obligations for native PRC cost as exact Lean Prop targets. The present definition is the reciprocal half of that mixed-context reflection package.
proof idea
Definitional packaging only: the body is the universal quantification
$\forall,\chi,;\mathrm{PRCRatioCharacter},\chi\to\mathrm{PRCCharacterPrimeDirectionCalibrated},\chi\to\mathrm{PRCCharacterMixedNonunitReciprocalWitnessReflectsPrimeWitness},\chi$.
No tactics. Discharge is deferred to the companion theorem PRCPrimeCalibrationForcesMixedNonunitReciprocalWitnessReflectsPrimeWitnessTarget_proved, which introduces $\chi$ and the two hypotheses, then applies PRCCharacterMixedNonunitReciprocalWitnessReflectsPrimeWitness_of_prime_local after the orbit-product display compatibility target.
why it matters
Native cost uniqueness in PRC is not yet closed; the Pass-25 blocker certificate splits the missing mathematics into exact targets. This declaration is the reciprocal half of the mixed-nonunit reflection obligation and is conjoined with the identity half into PRCPrimeCalibrationForcesMixedNonunitWitnessesReflectPrimeWitnessesSplitTarget.
It feeds PRCNativeCostUniquenessBlockerCertificate and appears on the historical ledger PRCUniversalFoundationOpenTargets. The companion _proved theorem already closes this half, so the open work sits on sibling blockers (zero-calibrated factorization routes, signed-admissible refutations) rather than on reciprocal reflection itself. In the broader RS chain this sits under J-uniqueness (T5) and the Recognition Composition Law: characters that match $J$ on primes must not invent extra mixed reciprocal structure off the prime axes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.