PRCPrimeCalibrationForcesMixedNonunitWitnessesReflectPrimeWitnessesTarget
plain-language theorem explainer
Names the reflection target: every prime-calibrated ratio character must send mixed nonunit witnesses down to mixed prime-axis witnesses. Native-cost uniqueness and the blocker certificate cite it as the identity half of the composite bridge. The body is a pure Prop abbreviation packing three character hypotheses into one universal statement.
Claim. The following proposition holds: for every map $\chi$ from ratio orbits to ratio orbits, if $\chi$ is a ratio character (unit at $1$, multiplicative up to cross-equivalence) and is calibrated on every native prime direction (generated cost matches canonical $J$-cost on each prime orbit), then mixed nonunit witnesses for $\chi$ reflect to mixed prime-axis witnesses.
background
In the Primitive Recognition Calculus, costs live on ratio orbits: integer numerators over nonzero orbit denominators. A ratio character $\chi$ is a quotient-native candidate for the d'Alembert factorization of a PRC cost: it fixes the unit orbit up to cross-equivalence and is multiplicative under orbit multiplication.
Prime-direction calibration means that the cost generated from $\chi$ agrees with the canonical $J$-cost on every prime orbit direction. The mixed-nonunit reflection property is the reverse bridge: existence of mixed nonunit witnesses forces existence of mixed prime-axis witnesses (the direction product propagation does not supply).
This module packages native-cost uniqueness into exact Lean targets. The present definition is the universal closure of that reflection property under the two standing hypotheses on $\chi$.
proof idea
No proof body: the declaration is a definitional abbreviation of a proposition. It quantifies over maps $\chi : \mathrm{RatioOrbit} \to \mathrm{RatioOrbit}$, assumes the ratio-character structure and prime-direction calibration, and concludes the mixed-nonunit-reflects-prime-witnesses predicate on $\chi$. Downstream theorems discharge or split this target rather than unfold a tactic script here.
why it matters
This is the identity half of the mixed-context reflection target inside the native-cost uniqueness program. It feeds the blocker certificate that records which uniqueness subgoals remain open, and it is the left-hand side of the iff with the split target. Downstream lemmas prove the target from prime-control, from the split form, and finally as a proved theorem via the split path. In the Recognition forcing chain this sits under T5 $J$-uniqueness and the Recognition Composition Law: characters calibrated on primes must not invent mixed nonunit defects that lack prime-axis support. Closing or citing this target keeps the uniqueness blockers exact rather than diffuse.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.