threePrimeDirection
plain-language theorem explainer
The ratio-orbit direction attached to the native prime orbit at three. Cost-uniqueness and two-adic twist arguments cite it as the canonical non-two prime witness in the first mixed-composite tests. The body is a one-line specialization of the prime-direction constructor to the three-orbit and its primality certificate.
Claim. Let the three-orbit be the successor of the two-orbit in the distinction-natural hierarchy (the canonical non-$2$ prime witness). The three-prime direction is the ratio orbit obtained by placing that prime orbit in the numerator over a nonzero orbit denominator, i.e. the rational direction associated to the native prime $3$.
background
In the primitive recognition calculus, a ratio orbit is an integer numerator over a nonzero orbit denominator (K4.7). Native primes appear as distinction-natural orbits; each such prime orbit determines a ratio direction by the prime-direction constructor.
The three-orbit is defined as the successor of the two-orbit and is proved to be a prime orbit (no nontrivial factor in its underlying natural). The module studies uniqueness of native costs generated from ratio characters, with special attention to two-adic axis twists and mixed composites built from $2$ and a first odd prime.
Upstream, the prime-direction map sends a prime orbit $p$ to the corresponding ratio direction. This definition simply freezes $p$ at three.
proof idea
One-line wrapper: apply the prime-direction constructor to the three-orbit together with the theorem that the three-orbit is a prime orbit. No further rewriting or case analysis.
why it matters
This is the fixed odd-prime axis used throughout the native-cost uniqueness development. Downstream it appears in the two-three mixed-image identity for two-adic axis-twist characters, in the refutation of the native-cost uniqueness target, in the no-admissible-factor theorem for twist-generated costs, and in a family of refutations of prime-calibration forcing targets (local orientation, reciprocal branch transport, floor-identity successor steps).
In framework terms it supplies the first concrete non-two prime needed to stress-test whether a ratio character calibrated on primes can still deviate from canonical $J$-cost on mixed composites, tying into the T5 $J$-uniqueness and Recognition Composition Law story at the level of discrete orbit directions rather than real analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.