PRCPrimeAxisTraceConnected_proved
plain-language theorem explainer
Any two prime-orbit axes in the distinction lattice have native orbit traces that admit a common finite δ-extension. Character and cost-uniqueness arguments cite this to discharge pairwise trace-connected hypotheses between primes. The proof is a one-line existential: the orbit-position trace of the sum extends both axes.
Claim. Let $p$ and $r$ be distinction naturals lying on prime orbits. Then there exists a finite trace $T$ such that $T$ extends the native orbit-position trace of $p$ and also extends the native orbit-position trace of $r$.
background
In the Primitive Recognition Calculus, each distinction natural carries a native orbit-position trace: the finite δ-path recording successive positions along its multiplicative orbit. Two prime axes are called trace-connected when those native traces admit a common finite extension $T$ (a single longer trace that continues both).
Prime-orbit hypotheses mark $p$ and $r$ as generators of prime multiplicative axes in the distinction lattice. Trace extension is the structural relation used throughout this module to move character and cost data from one axis to another without leaving the native calculus.
The local setting is native-cost uniqueness for PRC characters: once every pair of prime axes is known to be trace-connected, identity and reciprocal constraints on characters can be transported along shared extensions and forced to match the canonical J-cost orientation.
proof idea
Term-mode existential. Witness the common extension by the orbit-position trace of the sum $p+r$. Discharge the two Extends conjuncts by the left and right add-extension lemmas for orbit-position traces (orbitPositionTrace_add_extends_left and orbitPositionTrace_add_extends_right). No case split and no character hypotheses are required; connectivity is purely additive on the underlying distinction naturals.
why it matters
This is the universal connectivity fact for prime axes inside PRC native-cost uniqueness. Downstream wrappers apply it to drop explicit connectivity assumptions: prime-identity characters that respect trace-connected pairs automatically respect canonical add-trace and become trace-coherent; two-prime reciprocal constraints force full prime-reciprocal behavior; prime-calibration transport upgrades to prime-identity trace-coherence targets.
It is wired into the native-cost uniqueness blocker certificate and into the conditional universal-foundation certificate. In the broader RS chain it supports uniqueness of the native cost (the J-cost forced at T5) by ensuring every prime pair can share a finite δ-extension along which character orientation must match reciprocal-symmetric cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.