twoPrimeDirection
plain-language theorem explainer
The distinguished ratio-orbit direction along the native prime orbit for 2. Anyone calibrating a ratio character, or reducing prime-axis identity to the two-axis, cites this constant. It is a one-line specialization of the general prime-direction constructor to the two-orbit and its primality certificate.
Claim. Let $2$ be the two-step distinction orbit (successor of one). The two-prime direction is the ratio orbit associated to that native prime: the orbit-direction of $2$, using that $2$ is a prime orbit.
background
In the primitive recognition calculus, a ratio orbit packages a signed integer orbit numerator over a nonzero distinction-nat denominator (K4.7). Native primes are distinction orbits whose underlying naturals have no nontrivial factors; the two-orbit is the successor of one, and is proved prime.
The general prime-direction map sends a native prime orbit $p$ to the ratio orbit given by the orbit-direction of $p$. That construction is the only input here: the two-prime direction is that map evaluated at the two-orbit.
The surrounding module develops uniqueness of native cost from ratio characters. Characters are maps on ratio orbits; calibration and identity normal forms are stated relative to prime directions, with the two-axis singled out as the distinguished reference.
proof idea
One-line definitional wrapper. Apply the general prime-direction constructor to the two-orbit, discharging the primality hypothesis by the existing theorem that the two-orbit is a prime orbit. No further rewriting.
why it matters
This constant is the reference axis for the identity-iff-two normal forms: identity of a character on any calibrated prime direction is equivalent (for admissible characters) to identity on the two-prime direction, and one-sided forcing lemmas reduce prime-axis identity to the two-axis. Downstream calibration theorems (absolute-value character cost-calibrated on two; prime-direction calibration from two-adic axis twist) unfold this definition and rewrite through the general prime-direction constructor.
In the Recognition forcing chain, native cost uniqueness feeds the J-cost story (T5: $J(x)=(x+x^{-1})/2-1$). Pinning the two-axis as the distinguished prime direction is the bookkeeping step that lets character hypotheses on all primes collapse to a single check at orbit-2, which is where the absolute-value and reciprocal-twist arguments land.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.