threeOrbit
plain-language theorem explainer
Names the three-step finite distinction orbit, the canonical non-2 prime witness in the primitive recognition calculus. Downstream uniqueness and calibration arguments cite it whenever a concrete odd prime direction is needed (especially 3-adic valuations and two–three mixed characters). The body is a one-line successor of the two-step orbit.
Claim. Let the finite distinction orbit be the inductive type generated by zero and successor. Write $O_2$ for the two-step orbit position. Define the three-step orbit by $O_3 := \mathrm{succ}(O_2)$. This $O_3$ is the canonical non-$2$ prime witness used throughout native-cost uniqueness.
background
In the primitive recognition calculus, finite orbits of repeated distinction are tracked by an inductive type DistinctionNat (K2.12): base-neutral positions built from zero by successor, not from a preferred numeral base. The two-step orbit is already fixed as the successor of the unit orbit; the three-step position is the next successor.
The surrounding module develops native cost uniqueness for ratio characters and doubled-trace d'Alembert structure. Odd primes enter as orbit positions that must be separated from the two-adic axis. The three-step orbit is the smallest concrete non-2 prime direction used as that witness.
Upstream, successor on the logic/distinction naturals is just one more application of the generator. Reachability lemmas for step-closure are available but not needed to form the constant itself.
proof idea
Pure definitional construction: apply the distinction-orbit successor once to the already-defined two-step orbit. No tactics, no lemmas beyond the inductive constructors and the prior two-orbit abbreviation.
why it matters
Native-cost uniqueness and two-adic axis-twist arguments need a fixed odd prime orbit to test mixed characters, 3-adic valuations, and prime-calibration side conditions. This constant supplies that witness.
It is consumed by many results in the same module: vanishing of the 3-adic valuation of prime directions other than three; two–three mixed images under two-adic axis twists; refutations of uniqueness and prime-calibration targets (nonunit orbit orientation, reciprocal branch transport, prime-floor successor contraction); and non-existence of admissible factors for twist-generated costs. In the broader Recognition chain it supports the uniqueness side of the native J-cost story (T5 J-uniqueness / RCL), by pinning prime directions away from pure two-adic generation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.