twoOrbit
plain-language theorem explainer
Names the two-step position in the base-neutral distinction orbit: one successor past the unit orbit. Anyone building ratio orbits, the native cost on 2, or two-point calibration cites it as the canonical integer-2 seed. The body is a one-line constructor application of successor to the unit orbit.
Claim. Let $\mathrm{DistinctionNat}$ be the inductive orbit of repeated distinction (zero and successor). Define the two-step orbit position by $\mathrm{twoOrbit} := \mathrm{succ}(1)$, i.e. one successor applied to the unit orbit element.
background
In the Primitive Recognition Calculus, finite counting is not imported from Peano arithmetic as an axiom package. DistinctionNat (K2.12) is the base-neutral finite orbit of repeated distinction: an inductive type with zero and succ. Successor means one more application of the generator, matching the ArithmeticFromLogic reading that successor is one more generator step.
The local module builds the J-cost side of PRC: ratio orbits, the native cost functional, and calibration at the integer two. Integer positions on the distinction orbit are the numerators and denominators of those ratio orbits. The unit orbit is already present; the next constructive seed needed everywhere is the two-step position.
Upstream, the only content is the inductive structure and successor. No metric or cost is attached yet; that comes when the orbit is mapped to naturals or embedded into ratio orbits.
proof idea
Definition, not a proof. The body is the term DistinctionNat.succ DistinctionNat.one: apply the inductive successor once to the unit orbit element. No tactics, no lemmas. The companion simp fact twoOrbit_toNat then reduces toNat of this term to the numeral 2 by rfl.
why it matters
This is the canonical seed for the integer two inside PRC. Downstream it builds the ratio orbit two (numerator the signed two-orbit, denominator one) and the reciprocal ratio orbit half (numerator one, denominator twoOrbit). Those feed the two-point cost calibration that uniqueness and minimality theorems transport across prime axes.
In particular, character_pair_two_calibration_forces_prime_calibration treats cross-equality of character cost at two with the native cost on two as the base ledger entry that, with prime-pair product consistency, forces prime-direction calibration on every native axis. Absolute-value character theorems likewise calibrate cost at two via twoOrbit and its primality-as-orbit fact. Without a named two-step orbit, the two-calibration premise of the native-cost uniqueness chain has no carrier.
Framework-wise this sits under the forcing chain's cost side (T5 J-uniqueness and the Recognition Composition Law): the discrete orbit must supply the integer 2 before J can be evaluated on the ratio 2 and 1/2.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.