PRCCharacterTwoPrimeBranchControlsPrimes
plain-language theorem explainer
Defines distinguished-prime branch control for a ratio-orbit character: if the character fixes (or reciprocates) the orbit-2 prime axis, it does the same on every native prime axis. Downstream uniqueness and coherence theorems cite this as the one-axis form of coherent prime orientation. It is a pure Prop abbreviation, not a proved statement.
Claim. For a map $\chi$ on ratio orbits, the following holds: if $\chi$ is cross-equivalent to the identity on the distinguished prime axis of orbit $2$, then $\chi$ is cross-equivalent to the identity on every native prime axis; and if $\chi$ is cross-equivalent to the reciprocal on the orbit-$2$ prime axis, then $\chi$ is cross-equivalent to the reciprocal on every native prime axis.
background
In the Primitive Recognition Calculus, ratio orbits package signed numerator orbits over nonzero distinction-natural denominators. Cross-equivalence is the internal rational relation: two ratio orbits match when scaled numerators balance under cross-multiplication on $\delta$-orbit positions. The reciprocal sends a nonzero ratio orbit to its inverse (and zero to zero), mirroring $\mathbb{Q}$.
Distinction-naturals are the base-neutral finite orbits of repeated distinction; prime orbits among them supply native prime axes. The distinguished orbit-$2$ prime axis is the calibration reference. A ratio character $\chi$ assigns to each ratio orbit another ratio orbit; orientation on a prime axis means $\chi$ lands either on that axis or on its reciprocal (cross-equivalence).
This module develops native cost uniqueness from character hypotheses. Branch control is the one-axis version of coherent prime orientation: the branch chosen at $2$ is required to propagate to every prime.
proof idea
No proof: this is a definitional Prop. The body is a conjunction of two implications. The first says identity orientation at the orbit-$2$ prime axis forces identity orientation at every prime axis. The second says reciprocal orientation at orbit $2$ forces reciprocal orientation at every prime. Both use cross-equivalence of ratio orbits and the reciprocal operation on the prime directions.
why it matters
Branch control is the hinge between local orientation at primes and global coherent prime orientation. Downstream, local orientation plus this control yields coherent prime orientation and the identity-iff-two normal form (identity on a native prime axis iff identity on the orbit-$2$ axis). The converse directions recover branch control from coherence or from the identity-iff-two form.
It appears in the native-cost uniqueness blocker certificate and in open universal-foundation targets, so it marks an exact interface the uniqueness program must discharge. In the broader Recognition chain this sits under character-level forcing toward the unique native cost (tied to J-uniqueness and the Recognition Composition Law), before constants and the mass ladder are read off.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.