PRCPrimeCalibrationForcesPrimeWitnessesControlNonunitWitnessesTarget_iff_mixed_reflects
plain-language theorem explainer
Under prime-direction calibration of a ratio character, the composite bridge that prime no-mixing controls arbitrary nonunit no-mixing is equivalent to its reflection form: mixed nonunit witnesses reflect down to mixed prime-axis witnesses. Native-cost uniqueness and universal-foundation certificates cite this equivalence to swap bridge orientations freely. The proof is a two-constructor Iff term from the two one-way implications already proved in-module.
Claim. The following are equivalent. (A) For every ratio-orbit map $\chi$ that is a ratio character and is prime-direction calibrated, prime witnesses control nonunit witnesses for $\chi$. (B) For every such $\chi$, mixed nonunit witnesses reflect down to mixed prime-axis witnesses for $\chi$.
background
In the Primitive Recognition Calculus, a ratio character is a map $\chi$ on ratio orbits preserving the multiplicative structure used to build native cost. Prime-direction calibration means $\chi$ is aligned on the prime axes of the orbit lattice, so mixing phenomena can be reduced to prime generators.
Two Prop targets package the same composite bridge under that calibration. The control form asserts that prime no-mixing already forces arbitrary nonunit no-mixing. The reflection form asserts the dual: any mixed nonunit witness must reflect down to a mixed witness on a prime axis. Both sit inside the native-cost uniqueness development, which aims to force the J-cost shape from recognition axioms (cf. T5 J-uniqueness and the Recognition Composition Law).
Upstream, each direction is already a short theorem: control implies reflection by applying the character-level reflection-of-control lemma, and reflection implies control by the dual character-level lemma.
proof idea
Term-mode Iff introduction. The forward arrow is the existing theorem that the control target implies the mixed-reflection target (introduces $\chi$, character, and prime-calibration hypotheses, then applies the character-level reflection-from-control lemma). The reverse arrow is the dual theorem that mixed reflection implies the control target (same intro pattern, then the character-level control-from-reflection lemma). No new algebra is done at this layer; the declaration only packages the two one-way bridges as a single equivalence.
why it matters
The native-cost uniqueness blocker certificate and the universal-foundation conditional certificate both consume this bridge layer. Equivalence lets downstream proofs choose whichever orientation matches the local witness geometry: control when arguing from prime generators outward, reflection when reducing mixed nonunit data back to primes.
In the Recognition forcing chain this sits under the uniqueness of the J-cost (T5) and the composition law that pins $J(x)=(x+x^{-1})/2-1$. Closing the witness-split bridge is part of showing that calibrated characters cannot smuggle non-native cost shapes past the prime axes. The declaration itself is only the iff glue; the substantive content lives in the two one-way theorems and the character-level lemmas they call.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.