PRCAdmissibleCharacterSignedUnitCalibratedTarget
plain-language theorem explainer
Names the open target that every admissible ratio character must fix the signed unit orbit −1. Native-cost uniqueness work cites it when chaining calibration into global orientation and rigidity. The body is a pure Prop abbreviation: universal quantification over characters with the repaired admissibility package implying signed-unit calibration.
Claim. For every map $\chi$ from ratio orbits to ratio orbits, if $\chi$ is an admissible ratio character (ratio-character laws, prime-direction calibration, and prime-pair product cost consistency), then $\chi$ is signed-unit calibrated: $\chi(-1)$ equals the orbit of $-1$.
background
In the primitive recognition calculus, a ratio orbit is an integer numerator over a nonzero distinction-nat denominator: the display of a rational scale factor. Characters are maps $\chi$ on those orbits meant to encode multiplicative cost data.
After a two-adic countermodel, admissibility was repaired: an admissible ratio character must obey the ratio-character laws, be prime-direction calibrated, and keep prime-pair product costs consistent. That package preserves two global orientations and kills valuation twists, but does not by itself pin the sign of the unit.
Signed-unit calibration is the separate demand that $\chi$ fix the orbit of $-1$. The module doc line for that predicate states that prime-direction data alone cannot force it. This definition packages the missing implication as a named Prop target.
proof idea
Definitional Prop, not a proved theorem. The body is the single universal statement: for all $\chi$, admissibility of $\chi$ implies signed-unit calibration of $\chi$. No tactics, no lemmas applied at the definition site.
why it matters
Pass 279 isolates that repaired prime-pair admissibility still fails to force signed-unit calibration. Downstream, the target is an explicit hypothesis in the bridges from signed calibration to global orientation and then to admissible-character rigidity and the strengthened native-cost uniqueness target.
It is also the subject of a direct refutation: the absolute-value character is admissible yet not signed-unit calibrated, so the target is false. That refutation feeds the pass-25 blocker certificate, which records that native cost uniqueness is not closed and splits the missing mathematics into exact Lean targets. In the Recognition forcing picture this sits upstream of J-uniqueness and native cost rigidity: without signed-unit control, character factorization cannot pin the physical cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.