PRCPrimeCalibrationForcesMixedNonunitWitnessesReflectPrimeWitnessesSplitTarget
plain-language theorem explainer
Packages the mixed-nonunit reflection obligation as the conjunction of its identity and reciprocal halves. Anyone tracking the no-mixed-witness blocker in native-cost uniqueness cites this split form. The body is pure definitional conjunction of the two half-targets; no mathematics is proved here.
Claim. The split mixed-nonunit reflection target is the conjunction of: (i) every ratio character that is prime-direction calibrated reflects mixed nonunit identity witnesses from prime witnesses, and (ii) every such character likewise reflects mixed nonunit reciprocal witnesses from prime witnesses.
background
In the Primitive Recognition Calculus, a ratio character is a map on ratio orbits obeying the multiplicative character laws used to build native cost. Prime-direction calibration forces the character on prime generators; the remaining obstruction is whether that control extends to mixed nonunit composites (products involving both a nonunit and a unit-direction factor).
The identity half requires that mixed nonunit identity witnesses are already controlled by the prime-witness data. The reciprocal half does the same for reciprocal witnesses. Upstream, each half is itself a bare Prop target: for all characters $\chi$ that are ratio characters and prime-direction calibrated, the corresponding mixed-nonunit reflection property holds.
Locally this module is closing native-cost uniqueness by splitting blockers into exact Lean targets rather than a single opaque gap.
proof idea
Definitional abbreviation only: the split target is literally the conjunction of the identity-half target and the reciprocal-half target. No tactics, no lemmas, no proof obligations are discharged at this declaration.
why it matters
This is the bookkeeping hinge for the no-mixed-witness blocker inside native-cost uniqueness. Downstream, an iff theorem equates the unsplit mixed-nonunit reflection target with this split form, and constructor/destructor lemmas move between them. A proved inhabitant is assembled by pairing the two half-target proofs. The native-cost uniqueness blocker certificate and the universal-foundation open-target ledger both hang off this split, so the missing mathematics is named as two independent half-obligations rather than one opaque Prop. In the broader forcing picture this sits under native J-cost uniqueness (the T5 lineage), not under dimension or period forcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.