PRCPrimeCalibrationForcesMixedNonunitIdentityWitnessReflectsPrimeWitnessTarget
plain-language theorem explainer
Defines the identity-half target: every prime-calibrated ratio character must send mixed nonunit identity witnesses down to prime-axis identity witnesses. Cited by the mixed-witness split target, the native-cost uniqueness blocker certificate, and the universal-foundation open-target ledger. Pure Prop packaging; the companion `_proved` theorem discharges it.
Claim. For every map $\chi$ from ratio orbits to ratio 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 identity half of the mixed-context reflection law holds: whenever mixed nonunit witnesses exist, every identity-oriented nonunit witness reflects to an identity-oriented prime-axis witness.
background
In the Primitive Recognition Calculus, costs live on ratio orbits: pairs of a signed numerator orbit with a nonzero distinction-nat denominator (K4.7). A ratio character $\chi$ is a candidate d'Alembert factor at that level: it fixes the unit orbit and is multiplicative, both up to cross-equivalence rather than definitional equality, so the statement stays quotient-native.
Prime-direction calibration asks that the cost generated from $\chi$ agree with the canonical $J$-cost on every prime orbit. The mixed-context reflection law then splits into identity and reciprocal halves. The identity half asserts that if mixed nonunit witnesses are present, any identity-oriented nonunit witness must reflect down to an identity-oriented prime-axis witness.
This module packages native-cost uniqueness obstacles as exact Lean targets. The present definition is the identity half of the prime-calibration-forces-mixed-reflection package.
proof idea
No proof body: this is a bare Prop abbreviation. It universally quantifies over maps $\chi : \mathrm{RatioOrbit}\to\mathrm{RatioOrbit}$, assumes the ratio-character structure and prime-direction calibration, and concludes the already-named identity-half reflection predicate on $\chi$. Discharge is deferred to the companion theorem that applies the prime-local reflection lemma after establishing orbit-product display compatibility from calibration.
why it matters
Native cost uniqueness in PRC is not closed; Pass-25 splits the missing mathematics into exact targets. This definition is the identity conjunct of the split mixed-nonunit reflection target, which itself feeds the native-cost uniqueness blocker certificate and the historical open-target ledger in UniversalFoundation.
The companion _proved theorem already closes this half under prime calibration, so the remaining work sits on the reciprocal half and on zero-calibrated factorization routes. In the broader Recognition chain this sits upstream of J-uniqueness (T5) and the Recognition Composition Law: characters that match $J$ on primes must obey the mixed-witness reflection needed for a unique native cost factorization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.