PRCTwoCalibrationForcesPrimeCalibrationTarget
plain-language theorem explainer
Names the open target that two-point calibration of a ratio character at the orbit of 2 forces calibration on every prime direction. Anyone chasing native-cost uniqueness or character rigidity cites this as the missing prime-axis control step. It is a pure proposition definition, not a proved theorem.
Claim. The following assertion is recorded as a named target: for every map $\chi$ from ratio orbits to ratio orbits that is a PRC ratio character, if the character-induced cost at the orbit of $2$ is cross-equivalent to the native cost on that same orbit, then $\chi$ is calibrated on every prime direction.
background
In the Primitive Recognition Calculus, rational comparisons live on RatioOrbit displays (signed numerator over a nonzero distinction-nat denominator). Two such orbits are identified by cross-multiplication balance (crossEq), the internal stand-in for rational equality.
A PRC ratio character $\chi$ is a structure-preserving map on those orbits. From it one builds an induced cost costFromCharacter; the native reference cost on orbits is onRatioOrbit. The special orbit of the integer $2$ is the two-point calibration site used throughout the native-cost uniqueness program.
The surrounding module isolates uniqueness of the native cost functional. This definition packages the first half of the sharpened rigidity problem: control of independent prime axes after calibration only at $2$.
proof idea
No proof: the declaration is a bare Prop abbreviation. It quantifies over characters, assumes the PRC ratio-character axioms and cross-equality of character cost with native cost at the orbit of $2$, and concludes prime-direction calibration. Downstream theorems treat the whole statement as a named hypothesis to be discharged later.
why it matters
This is Sharper Target A in the native-cost uniqueness campaign: the exact gap where the present surface lacks control of independent prime axes. It is conjoined with prime-calibration propagation to form the sharpened character-rigidity target, and is an explicit hypothesis in the reduction theorems that rebuild full rigidity and uniqueness from factorization plus two-calibration.
Those reductions feed the blocker certificate that splits unfinished uniqueness work into exact Lean targets, and the signed/strengthened uniqueness packages that route through character factorization. In the broader Recognition chain this sits under J-uniqueness (T5) and the Recognition Composition Law: without prime-axis forcing, the character cost need not coincide with the forced $J$-cost on all rational directions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.