orbitDirection_succ_crossEq_add_one
plain-language theorem explainer
For any nonzero distinction-natural p, the orbit direction at succ(p) is cross-equivalent to the direction at p plus the unit ratio orbit. Native-cost uniqueness arguments cite this to step the discrete direction along the δ-orbit by one. The proof reduces cross-equality to rational equality, applies the toRat lemmas for add, one, and orbitDirection, then finishes by norm_num with toNat_succ.
Claim. Let $p$ be a nonzero distinction-natural. Then the orbit direction at $\mathrm{succ}(p)$ is cross-equivalent (via balanced scaled numerators and denominators) to the sum of the orbit direction at $p$ and the unit ratio orbit.
background
In the Primitive Recognition Calculus, arithmetic is built from δ-orbit positions rather than imported verifier naturals. DistinctionNat is that native natural type; its successor is one more generator step. RatioOrbit packages a signed numerator orbit with a positive denominator orbit, and toRat is the verifier display of that pair as a rational.
Cross-equality is the internal rational relation: two ratio orbits are related when the scaled products of numerator and opposite denominator balance as signed orbits. Upstream, this is proved equivalent to equality of the verifier rationals (K4.10). Addition of ratio orbits is defined so that its display is ordinary rational addition, and the unit orbit displays as $1$.
Orbit direction assigns to each nonzero distinction-natural a ratio orbit that records the discrete direction of the recognition orbit at that rung. The present lemma compares that direction after a successor step with the same direction plus one.
proof idea
Tactic proof by transport to rationals. Rewrite the goal with crossEq_iff_toRat_eq, so it becomes equality of toRat values. Expand the right-hand side by add_toRat and one_toRat, and both sides' directions by orbitDirection_toRat. Replace toNat (succ p) by Nat.succ (toNat p) via toNat_succ, then close the resulting numerical identity with norm_num.
why it matters
Native cost uniqueness in PRC needs the discrete direction along the orbit to advance exactly by one unit per successor step, without smuggling verifier arithmetic into the object theory. This lemma supplies that successor law under cross-equality, so later certificates can treat the direction as an additive counter on the δ-ladder.
It is consumed by prc_native_cost_uniqueness_blocker_certificate, which packages the zero-calibrated factorization target and the refutation of the signed-admissible alternative. In the broader Recognition chain, that uniqueness story feeds the J-cost identification (T5) and the forced self-similar scale φ (T6): the cost functional must be the unique native object compatible with the orbit calculus, not an ad-hoc import.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.