PRCNativeCostCharacterRigidityTarget_of_prime_targets
plain-language theorem explainer
If two-point calibration at orbit 2 forces prime-direction calibration, and prime calibration propagates to every rational direction, then a ratio character calibrated at 2 is the canonical identity cost on all rational orbits. Native-cost uniqueness proofs cite this as the A-then-B composition that discharges character rigidity. The proof is a three-line term that feeds the two-calibration hypothesis through the prime-forcing target into the propagation target.
Claim. Assume (A) that any ratio character $\chi$ whose cost matches the canonical cost at orbit $2$ is calibrated on every prime direction, and (B) that any such prime-calibrated character has cost matching the canonical cost on every rational orbit. Then any ratio character calibrated at $2$ has cost equal to the canonical identity-character cost on every rational orbit $q$.
background
In the primitive recognition calculus, ratio orbits carry a native cost. A ratio character $\chi$ is a map on orbits; costFromCharacter rebuilds a cost from $\chi$, and crossEq asserts that this rebuilt cost agrees with the canonical cost onRatioOrbit at a given orbit. Calibration at the distinguished orbit $2$ is the two-point anchor.
The rigidity target says that two-point calibration already forces full agreement on every rational orbit: no free prime-direction twisting can survive. The module splits that demand into two sharper targets. Target A (two-calibration forces prime calibration) is where independent prime axes must be killed. Target B (prime calibration propagates) is the unique-factorization half: once primes match, every rational direction matches.
This declaration is the pure logical glue: A and B together are exactly the rigidity target. It does not prove A or B; it only records the composition.
proof idea
Term-mode composition, no algebra. Introduce a character $\chi$, the character hypothesis, the two-point calibration hypothesis at orbit $2$, and an arbitrary rational orbit $q$. Apply target A to $\chi$ to obtain prime-direction calibration from the two-point data. Feed that prime-calibrated character into target B to conclude cost agreement at $q$. The whole body is one exact of hprop applied to the result of htwo.
why it matters
Character rigidity is the second exact blocker on the native-cost uniqueness path: a calibrated rational character cost must be the canonical identity-character cost, eliminating prime-direction freedom. This theorem packages the two sharper prime targets into that blocker so downstream uniqueness can assume a single rigidity hypothesis.
It is used by PRCNativeCostUniquenessTarget_of_prime_character_targets, which builds full native-cost uniqueness from factorization plus the same two prime targets, and it appears in the uniqueness blocker certificate assembly. In the broader Recognition forcing chain this sits under J-uniqueness (T5) and the Recognition Composition Law: native cost must be forced to the unique J-shape, and character rigidity is the rational-orbit half of that forcing. The open work remains proving targets A and B themselves; this result only closes the composition step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.