PRCNativeCostCharacterRigidityTarget_refuted
plain-language theorem explainer
The rigidity target for native cost characters is false: two-calibration of a rational ratio character does not force the induced cost to match the canonical native cost on every ratio orbit. The absolute-value character is the counterexample; it is a ratio character calibrated at 2 yet mismatches at the orbit of -1 because it erases sign. Native-cost uniqueness and universal-foundation certificates cite this refutation. The proof applies the assumed rigidity map to that character and invokes the known non-canonicity at -1.
Claim. It is not true that every map $\chi$ on ratio orbits that is a ratio character and whose induced character-cost is cross-equal to the canonical native cost at $2$ must have character-cost cross-equal to the canonical native cost at every ratio orbit $q$. In short, two-calibration of a rational character cost does not force global identity with the canonical cost.
background
In the primitive recognition calculus, ratio orbits are the quotient displays of nonzero rationals used as verifier coordinates. A ratio character $\chi$ is a structure-preserving self-map of those orbits (unit-preserving and compatible with the ratio product law). From any such $\chi$ one builds an induced cost costFromCharacter, and compares it to the canonical native cost onRatioOrbit via the cross-equality relation on orbits (equality of underlying rational representatives).
The rigidity target asserts that if $\chi$ is a ratio character and the induced cost matches the canonical cost at the orbit of $2$, then the match extends to every orbit. The module treats this as the second exact blocker for native-cost uniqueness: the place where residual prime-direction (and signed-unit) freedom must be killed if uniqueness is to hold.
Upstream, the absolute-value character sends each orbit to the orbit of the absolute value of its rational representative. It is proved to be a ratio character and to be calibrated at $2$, yet its induced cost fails cross-equality at the orbit of $-1$, which is the signed unit used to expose missing orientation calibration.
proof idea
Term-mode contradiction. Assume the rigidity proposition. Instantiate it at the absolute-value character, feeding the three already-proved facts that (i) absolute value is a ratio character, (ii) its induced cost is cross-equal to the canonical cost at $2$, and (iii) the orbit of $-1$ is a legitimate test point. Rigidity then yields cross-equality of the absolute-value cost with the canonical cost at $-1$. That conclusion is exactly the negation of the upstream lemma that the absolute-value cost is not canonical at $-1$, giving the contradiction.
why it matters
This refutation is one of the explicit blockers packaged into the native-cost uniqueness blocker certificate, and it is consumed by the conditional universal-foundation certificate. In the Recognition forcing chain the native cost is meant to be the unique J-type cost on rational displays (the discrete shadow of T5 J-uniqueness and the Recognition Composition Law). The rigidity target was the natural route from two-calibration to global uniqueness; showing it false forces the development to track signed units and prime-direction orientation separately rather than hoping calibration at $2$ alone erases all character freedom.
Downstream certificates therefore record both what has been proved (factorization under stronger zero-calibration hypotheses) and what has been refuted (naive character rigidity and certain signed-admissible factorizations). The open path is a tighter uniqueness theorem that adds the missing signed-unit or orientation axioms the absolute-value counterexample exploits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.