PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalBranchAgreementTarget
plain-language theorem explainer
Defines the positive normal form of the nonunit branch-coupling blocker: local orbit orientation together with two-branch agreement under prime calibration. Anyone tracking PRC native-cost uniqueness or the open-target ledger cites it as the sharp local packaging of that blocker. The body is a pure conjunction of the two component target Props.
Claim. The local-branch-agreement target is the conjunction of (i) the local nonunit orbit-orientation target and (ii) the nonunit two-branch agreement target: for every ratio-orbit character that is prime-direction calibrated, local orientation holds and a nonunit branch choice in one direction agrees with every other nonunit direction on both the identity and reciprocal branches.
background
In the Primitive Recognition Calculus, ratio-orbit characters assign multiplicative data to positive ratio orbits. Prime-direction calibration pins the character on a distinguished prime orbit (classically the orbit of 2). Nonunit directions are those away from the identity event at ratio 1, where J-cost is minimized.
Two structural demands appear repeatedly. Local orientation asks that the character orient each nonunit orbit consistently in a neighborhood of the identity. Two-branch agreement asks that a nonunit branch choice forced in one direction transport to every other nonunit direction, for both the identity branch and the reciprocal branch (the automorphism sending a recognition event to its inverse-ratio reverse).
The module packages these demands as named target Props so that global coherence statements can be reduced to local normal forms. Upstream, the branch-agreement target is exactly the universal quantification over calibrated characters of the nonunit branch-agreement predicate; the local-orientation target is the matching local orientation predicate.
proof idea
Definitional abbreviation only: the Prop is the conjunction of the local nonunit orbit-orientation target and the nonunit two-branch agreement target. No tactics, no lemmas applied at the definition site. Downstream equivalences later identify this conjunction with the coherent target and with the local identity-transport target.
why it matters
This is the positive normal form of the global nonunit branch-coupling blocker inside PRC native-cost uniqueness. Downstream, it is proved equivalent to the coherent orientation target and to the local identity-transport target, so any of the three packages may be used interchangeably. It feeds the open-target registry in UniversalFoundation and the chain of of_/iff_ lemmas that move between coherent, local-branch-agreement, and local-identity-transport formulations.
A later theorem refutes the target outright: prime calibration does not force the conjunction. That refutation closes one scaffolding path in the uniqueness program and forces the framework to seek a different route from calibration to native J-cost uniqueness (T5 J-uniqueness and the Recognition Composition Law remain the intended landing points, but this particular forcing bridge is blocked).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.