PRCNativeCostCharacterRigiditySharpenedTarget
plain-language theorem explainer
The Pass-26 sharpened rigidity target for native cost uniqueness is the conjunction of two subgoals: two-point calibration at the orbit of 2 forces prime-direction calibration of any ratio character, and prime calibration then propagates character-cost agreement to every rational orbit. Uniqueness-blocker and universal-foundation ledgers cite it as the exact rigidity surface. It is a pure Prop abbreviation, not a proved statement.
Claim. The following two claims hold simultaneously: (A) every ratio character $\chi$ that matches native cost at the orbit of $2$ is calibrated on every prime direction; (B) every ratio character calibrated on all prime directions satisfies $\mathrm{cost}_\chi(q)=J(q)$ (cross-equality) for every rational orbit $q$.
background
In the Primitive Recognition Calculus, ratio orbits carry the multiplicative skeleton on which the native J-cost lives. A ratio character $\chi$ is a map on orbits preserving the character axioms; costFromCharacter rebuilds a cost functional from $\chi$, and cross-equality compares that rebuild to the native cost on a given orbit.
The uniqueness program asks when matching native cost at sparse calibration points forces $\chi$ to reproduce native cost everywhere. Upstream target A isolates the missing control of independent prime axes: calibration only at the orbit of 2 should force prime-direction calibration. Upstream target B is the unique-factorization half: once primes are calibrated, the character cost must agree on every rational orbit.
This module packages those two sharper surfaces as a single Pass-26 rigidity target, refining earlier coarser formulations of native-cost character rigidity.
proof idea
Definitional abbreviation only: the target is the propositional conjunction of the two upstream targets (two-calibration forces prime calibration, and prime calibration propagates to all rationals). No tactics, no lemmas applied.
why it matters
Native cost uniqueness is the PRC-side counterpart of J-uniqueness in the forcing chain (T5: $J(x)=(x+x^{-1})/2-1$). This sharpened target names the exact rigidity surface the program tried to close.
Downstream it is immediately refuted: the companion theorem shows the conjunction fails because the first conjunct already fails. That refutation feeds PRCNativeCostUniquenessBlockerCertificate (Pass-25 split of missing mathematics into exact Lean targets) and the historical open-target ledger in PRCUniversalFoundationOpenTargets, which records negative entries for routes that cannot force the final surface. The declaration therefore earns its place as a precise, citable blocker rather than as a proved uniqueness step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.