PRCPrimeCalibrationForcesPrimeIdentityWitnessGlobalizesNonunitTarget_of_prime_floor_successor_transport
plain-language theorem explainer
Prime calibration that forces successor transport above the unit floor also forces the witness-globalized identity rule on every nonunit orbit. Anyone tracking the native-cost uniqueness blockers cites this implication. The proof is a one-line lift: instantiate the target hypothesis on a character and apply the character-level globalization lemma.
Claim. If every prime-direction-calibrated ratio character $\chi$ satisfies prime-floor orbit-identity successor transport, then every such $\chi$ also satisfies the witness-globalized nonunit identity rule: whenever any calibrated prime axis is sent to the identity orbit, every nonunit orbit direction is sent to the identity.
background
In the Primitive Recognition Calculus, ratio characters $\chi$ are maps on ratio orbits that encode admissible cost-compatible transport. Prime-direction calibration restricts how $\chi$ acts on prime axes. The corrected successor target says calibration should force successor transport above the self-reciprocal unit floor, not additive escape from the unit orbit itself.
The witness-globalized nonunit target is the corresponding blocker form: if any calibrated prime axis lands on the identity orbit, then every nonunit orbit direction must also land on identity. Both targets quantify the same character-level properties over all ratio characters that are prime-direction calibrated.
Upstream, the character-level lemma already shows that prime-floor identity successor transport on a fixed $\chi$ implies the witness-globalized nonunit identity property for that $\chi$. This declaration only packages that implication at the universal (target) level used by the uniqueness certificates.
proof idea
One-line wrapper. Introduce a ratio character $\chi$ together with the ratio-character and prime-calibration hypotheses. Apply the target hypothesis to obtain prime-floor orbit-identity successor transport for $\chi$. Feed that into the character-level lemma PRCCharacterPrimeIdentityWitnessGlobalizesNonunit_of_prime_floor_successor_transport, which returns the witness-globalized nonunit identity property for $\chi$.
why it matters
Closes the forward half of the equivalence between the corrected prime-floor successor target and the witness-globalized nonunit identity target. That equivalence is recorded as PRCPrimeCalibrationForcesPrimeFloorSuccessorTransportTarget_iff_prime_identity_witness_globalizes.
Downstream, the native-cost uniqueness blocker certificate and the universal-foundation conditional certificate both depend on this prime-floor package. In the Recognition forcing chain the native cost is the unique $J$ solving the Recognition Composition Law (T5), so locking the prime-axis identity blockers is part of showing no rival cost character survives calibration. The result does not itself prove uniqueness of $J$; it only advances the prime-floor half of the blocker stack that uniqueness certificates consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.