primeDirection
plain-language theorem explainer
Associates to each native prime orbit its ratio direction on the multiplicative orbit space. Downstream uniqueness and minimality arguments cite it whenever a cost or character must be checked on every prime axis. The body is a one-line projection through the existing orbit-direction map.
Claim. Given a distinction natural $p$ that lies on a native prime orbit, return the corresponding ratio orbit (the multiplicative direction of that prime).
background
In the primitive recognition calculus, costs and characters live on ratio orbits: equivalence classes of positive ratios under the reciprocal identification used by the J-cost. Native primes appear first as distinction naturals carrying a prime-orbit witness; calibration statements then ask that a candidate cost agree with canonical J on each such prime axis.
The surrounding module develops native-cost uniqueness: which hypothesis ledgers force a cost (or the character that generates it) to match J everywhere. Prime directions are the discrete generators of that check. Related scaffolding includes ratio characters, cost-from-character, and doubled-trace D'Alembert data that transport base two-point calibration out to the primes.
Upstream cost notions (observer J-cost, multiplicative-recognizer derived cost, rung-coarsen weighted sums) all ultimately compare against the same canonical J on these directions.
proof idea
One-line definitional wrapper: apply the existing orbit-direction constructor to $p$, using the underlying orbit membership packed inside the prime-orbit hypothesis. No extra arithmetic or uniqueness work occurs here.
why it matters
This is the indexing map for "evaluate on every native prime axis." Downstream, the slim ledger's uniqueness target is applied at primeDirection p hp to prove the all-prime axis field is redundant once base, zero, pair, and sign data are present. The transport lemma that recovers per-prime calibration from prime-pair products plus two-point calibration also ranges over these directions.
Selection and certificate modules use the same points to show the frozen canonical native cost meets the full zero-calibrated prime-signed strengthened class, and to refute ledgers that drop the pair field (two-adic twists fail mixed prime-pair products). In the broader forcing picture this is bookkeeping for T5-style J-uniqueness on the discrete prime skeleton before continuum rigidity closes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.