PRCPrimeCalibrationForcesNonunitIdentityWitnessGlobalizesTarget
plain-language theorem explainer
Names the open target that prime-direction J-calibration of a ratio character forces identity-branch witness globalization: any single identity-oriented nonunit direction, if present, locks the identity branch on every nonzero orbit. Cited by the native-cost uniqueness blocker certificate and by the iff bridges to branch-transport and local-exclusion forms. The body is a pure Prop abbreviation, not a proof.
Claim. The following proposition is the target: for every map $\chi$ on rational orbits that is a ratio character and is prime-direction calibrated (generated cost matches canonical $J$-cost on every prime orbit), the identity-oriented nonunit witness globalizes: existence of one identity-oriented nonunit direction implies the identity branch is fixed for every nonzero orbit direction.
background
In the primitive recognition calculus, a RatioOrbit is a rational display: signed numerator over a nonzero distinction-nat denominator. A ratio character $\chi$ is a structure-preserving self-map of these orbits; cost is recovered from $\chi$ via costFromCharacter and compared to the canonical $J$-cost on orbits.
Prime-direction calibration means that on every native prime orbit the character-generated cost agrees with $J$ under the orbit cross-equality. Separately, identity-witness globalization is the statement that a single identity-oriented nonunit direction (a non-unit distinction with identity orientation under $\chi$) forces the identity branch on all nonzero directions. Reciprocal and identity events from the ledger/observer layer supply the two orientations being coupled.
This module packages native-cost uniqueness as a stack of exact Lean targets rather than a closed theorem. The present definition is the witness-globalization packaging of the branch-coupling blocker under prime calibration.
proof idea
Definition only: the body is the universal quantification $\forall,\chi,;\mathrm{RatioCharacter}(\chi)\to\mathrm{PrimeCalibrated}(\chi)\to\mathrm{WitnessGlobalizes}(\chi)$. No tactics or lemmas are applied. Downstream bridges discharge or transport this Prop by applying the pointwise lemmas that convert between witness globalization, branch transport, and local exclusion once $\chi$ is fixed.
why it matters
Native cost uniqueness (forcing the recognition cost to the unique $J$ of the T5 step) is not yet closed; the Pass-25 blocker certificate splits the gap into named targets. This target is the witness-globalization form of the prime-calibration branch-coupling blocker: prime $J$-agreement should leave no room for mixed identity/reciprocal nonunit witnesses.
It feeds PRCNativeCostUniquenessBlockerCertificate and is interderivable with the branch-transport and local-exclusion targets via the _iff_ and _of_ theorems in the same module. Closing it (or an equivalent form) is one of the exact mathematical obligations still open on the path from PRC characters to uniqueness of the native cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.