PRCPrimeCalibrationForcesMixedNonunitWitnessesReflectPrimeWitnessesSplitTarget_proved
plain-language theorem explainer
Under prime calibration of a PRC ratio character, both identity-type and reciprocal-type mixed nonunit witnesses are forced to reflect prime witnesses. Anyone tracking the no-mixed-witness blocker in native cost uniqueness will cite this. The proof is a one-line And-pair of the two already-proved conjuncts.
Claim. The split mixed-nonunit reflection target holds: under prime calibration, every mixed nonunit identity witness of a PRC ratio character reflects a prime witness, and every mixed nonunit reciprocal witness likewise reflects a prime witness.
background
In the Primitive Recognition Calculus, ratio characters assign multiplicative data to recognition orbits. Native cost uniqueness asks that the cost functional recovered from such a character be uniquely the J-cost $J(x)=(x+x^{-1})/2-1$ forced at T5 of the unified forcing chain.
A recurring obstruction is mixed nonunit witnesses: composite nonunit data that could spoil uniqueness unless they are controlled by prime-level witnesses. The module splits that obstruction into identity-type and reciprocal-type reflection targets, then packages them as a single split Prop (the conjunction of the two).
Upstream, each conjunct is already proved by reducing to a prime-local reflection lemma after orbit-product display compatibility is forced by prime calibration. This declaration only records that both halves are available together.
proof idea
One-line term proof: inhabit the split target Prop by pairing the two proved conjuncts
PRCPrimeCalibrationForcesMixedNonunitIdentityWitnessReflectsPrimeWitnessTarget_proved and
PRCPrimeCalibrationForcesMixedNonunitReciprocalWitnessReflectsPrimeWitnessTarget_proved
as an And-introduction. No further tactics or algebraic work.
why it matters
Feeds the unsplit mixed-nonunit reflection theorem via the of_split constructor, which is the next line in the same module. That unsplit form is part of the native-cost-uniqueness blocker certificate and appears in the conditional universal-foundation certificate.
In framework terms this is bookkeeping on the path from prime calibration to uniqueness of the native cost (the J-cost of T5 / RCL). Closing the no-mixed-witness blocker is required before composite nonunits can be said to inherit prime-level control, a step toward ruling out exotic cost characters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.