PRCPrimeAxisTraceConnected
plain-language theorem explainer
Two native prime orbit axes are trace-connected when their native orbit traces admit a common finite δ-extension. Character-transport lemmas and the native-cost uniqueness blocker certificate cite this connectivity predicate as a hypothesis. The body is an existential Prop: some finite trace extends both primes' native orbit traces. A companion theorem later proves the relation for every prime pair via the sum orbit.
Claim. Let $p$ and $r$ be prime orbit positions (nonzero, non-unit, and free of nontrivial factorization). The axes are trace-connected if there exists a finite trace $T$ that extends the native orbit-position trace of $p$ and the native orbit-position trace of $r$.
background
In the Primitive Recognition Calculus, a finite trace is empty or built by successive distinction acts. Trace extension means the second trace is the first followed by some suffix (K2.5). DistinctionNat is the base-neutral finite orbit of repeated distinction; a prime orbit is nonzero, non-unit, and without nontrivial factorization.
Each orbit position carries a native trace defined by recursion on the δ-orbit (zero maps to the empty trace; successor appends one step), rather than by importing verifier Nat as object theory. The local module develops native cost uniqueness for the PRC cost, isolating when ratio characters match doubled-trace costs along connected components.
This definition packages the geometric relation that two prime axes lie in a common finite δ-component of the trace poset under extension.
proof idea
Definitional, not a proved theorem. The body is the Prop that there exists a finite trace $T$ extending both native orbit-position traces (via the Extends relation: some suffix appends to recover $T$). No tactics or lemmas are applied here. The companion result PRCPrimeAxisTraceConnected_proved later discharges the Prop for every prime pair by taking $T$ to be the orbit-position trace of $p+r$ and quoting the left/right add-extends lemmas.
why it matters
Supplies the connectivity hypothesis for character-respect predicates: identity orientation transport along a finite δ-component relating two prime axes, and the two-prime identity and reciprocal branch transports from the orbit-2 prime axis to a target native prime. Downstream, it appears in the Pass-25 native cost uniqueness blocker certificate, which records that uniqueness is not closed but splits the missing mathematics into exact Lean targets, and in the Universal Foundation open-target ledger.
In framework terms this is infrastructure toward uniqueness of the native cost functional (the PRC route to J-uniqueness / T5). Characters that match cost on a connected component can be forced along prime axes only once this relation is available as a named Prop.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.