PRCPrimeCalibrationForcesNonunitOrbitOrientationCoherentSharpenedTarget
plain-language theorem explainer
Defines the sharpened nonunit-orientation-coherence target as the conjunction of local nonunit orbit orientation and prime-floor successor transport under prime calibration. Anyone tracking native-cost uniqueness blockers cites this as the exact split of the older coherence demand. The body is a two-conjunct Prop abbreviation, not a proof.
Claim. The sharpened target asserts both: (i) every ratio-orbit character that is prime-direction calibrated orients every nonunit orbit locally, and (ii) every such character forces identity-successor transport on orbits above the self-reciprocal unit floor. Together these are meant to pin every nonunit orbit direction to one coherent identity/reciprocal branch.
background
In the Primitive Recognition Calculus, ratio-orbit characters are maps on ratio orbits that encode multiplicative recognition structure. Prime-direction calibration is the hypothesis that the character is already fixed on prime axes. Native cost uniqueness work then asks whether that calibration forces global orientation of nonunit orbits onto a single identity-versus-reciprocal branch.
The first conjunct is the local-orientation target: prime calibration should orient every nonunit orbit direction, not only prime axes. The second is the corrected successor-transport target: prime calibration should force successor transport above the self-reciprocal unit floor, rather than additive transport out of the unit orbit itself.
This module packages open uniqueness obligations as named Prop targets so blockers and certificates can point at exact missing mathematics rather than informal gaps.
proof idea
No proof: the declaration is a definitional abbreviation. It is literally the conjunction of the local nonunit-orientation target and the prime-floor successor-transport target. Downstream lemmas treat a hypothesis of this sharpened target by projecting the two conjuncts and feeding them to the coherence reconstruction lemma.
why it matters
This is the sharpened source used to equate the older nonunit-orientation-coherence target with a pair of more local obligations. Downstream, the iff theorem identifies the unsharpened coherence target with this conjunction; one direction rebuilds coherence from the two conjuncts, the other factors coherence back into them. A later theorem refutes the sharpened target, and that refutation feeds the native-cost uniqueness blocker certificate and the universal-foundation open-target ledger.
In the Recognition Science forcing picture, native cost is the J-cost side of the uniqueness story (T5 J-uniqueness and the Recognition Composition Law). This definition does not close uniqueness; it records the precise split of one failed forcing route so the certificate can mark that route as refuted rather than merely open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.