PRCPrimeCalibrationForcesPrimeIdentityIffTwoPrimeIdentityTarget
plain-language theorem explainer
Prime calibration of a ratio character forces the identity-iff-two normal form: identity orientation on any native prime axis holds exactly when it holds on the distinguished orbit-2 axis. Native-cost uniqueness work cites this Prop as the exact open target tying prime-axis calibration to uniform identity orientation. Pure Prop definition: a universal package over calibrated characters, not a proof.
Claim. For every map $\chi$ on ratio orbits that is a ratio character and is calibrated on every native prime direction (its generated cost matches canonical $J$-cost on each prime orbit), identity orientation of $\chi$ on an arbitrary native prime axis is equivalent to identity orientation of $\chi$ on the distinguished orbit-$2$ prime axis.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer numerator over a nonzero distinction-nat denominator. A ratio character $\chi$ is a structure-preserving self-map of these orbits. Cost generated from $\chi$ is compared to the canonical $J$-cost $J(x)=(x+x^{-1})/2-1$ by cross-equality of orbits.
Prime-direction calibration means: on every native prime orbit direction, the cost induced by $\chi$ agrees with canonical $J$ on that prime. The identity-iff-two normal form then says $\chi$ fixes a prime direction (cross-equals the identity orientation on that axis) if and only if it fixes the distinguished orbit-$2$ prime direction.
This module factors native-cost uniqueness into exact Lean targets. The present definition is one such target obligation: every prime-calibrated ratio character must satisfy identity-iff-two.
proof idea
Prop definition, not a proved theorem. The body is a single universal quantifier: every ratio character that is prime-direction calibrated must satisfy the identity-iff-two normal form on prime axes. No tactics or lemmas fire; the declaration only names the open obligation that downstream equivalence theorems rearrange into branch-uniformity and one-sided identity-forces-two forms.
why it matters
Native cost uniqueness aims to force the unique $J$-cost (forcing-chain T5, and the Recognition Composition Law) from primitive recognition structure alone. This target is consumed by the Pass-25 blocker certificate, which records that uniqueness is not closed but splits the gap into exact Lean obligations.
Downstream equivalences identify it with the branch-uniformity target and with the one-sided identity-forces-two target (mutual implications via the corresponding _of_ and _iff_ lemmas). Those reductions let the uniqueness program collapse several formulations to one open Prop. Discharging it would clear a named blocker on the path from prime calibration to full character uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.