Pith. sign in
theorem

PRCPrimeCalibrationForcesPrimeReciprocalForcesTwoPrimeReciprocalTarget_of_reciprocal_witness_globalizes

proved
show as:
module
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostUniqueness
domain
Foundation
line
9205 · github
papers citing
none yet

plain-language theorem explainer

Assuming reciprocal-witness globalization under prime calibration, any reciprocal-oriented native prime axis forces the orbit-2 prime axis onto the reciprocal branch. Cited by the split-target packaging of reciprocal globalization and by the native-cost uniqueness blocker chain. Proof is a short specialization: apply the character-level forcing lemma after instantiating the global target on a calibrated ratio character.

Claim. If, for every ratio-orbit character $\chi$ that is prime-direction calibrated, a single reciprocal-oriented native prime witness forces reciprocal orientation on every native prime axis, then for every such $\chi$ any reciprocal-oriented native prime axis forces the orbit-$2$ prime axis onto the reciprocal branch.

background

In the Primitive Recognition Calculus, a ratio character $\chi$ is a map on ratio orbits encoding how multiplicative structure is read by the native cost. Prime-direction calibration fixes how $\chi$ orients each native prime axis (forward versus reciprocal). Reciprocal orientation means the character places that prime on the inverse branch of the cost, the branch compatible with the Recognition Composition Law and the $J$-cost $J(x)=(x+x^{-1})/2-1$.

The reciprocal-witness globalization target asserts: once calibration admits even one reciprocal-oriented native prime witness, every native prime axis must sit on the reciprocal branch. The distinguished-axis converse half is weaker and local: any reciprocal-oriented native prime must force the orbit-$2$ prime axis onto that same reciprocal branch. Orbit $2$ is the distinguished dyadic axis in the eight-tick / power-of-two scaffolding of the foundation.

Upstream, the character-level lemma already shows that full reciprocal-witness globalization on a fixed $\chi$ implies the orbit-$2$ forcing property for that $\chi$, by feeding the witness triple into globalization at twoOrbit.

proof idea

One-line target lift. Introduce a calibrated ratio character $\chi$. Specialize the assumed globalization target at $\chi$ to obtain character-level reciprocal-witness globalization. Hand that hypothesis to the upstream lemma PRCCharacterPrimeReciprocalForcesTwoPrimeReciprocal_of_reciprocal_witness_globalizes, which itself only unpacks a reciprocal prime witness and applies globalization at the orbit-$2$ prime. No new arithmetic is done at this layer.

why it matters

This is the converse half of the reciprocal-globalization split used to pin native cost uniqueness. Downstream it is packaged into the split target theorem that pairs orbit-$2$ forcing with the complementary branch-forcing half, and that split feeds the native-cost uniqueness blocker certificate. The same chain is referenced by the conditional universal-foundation certificate, so the result sits on the path from PRC kernel hypotheses to a unique native cost character.

In framework terms it protects the reciprocal branch of the $J$-cost on the distinguished dyadic axis (orbit $2$), which is the axis tied to the eight-tick octave and to self-similar scaling by $\varphi$. Without forcing orbit $2$ onto the reciprocal branch once any prime is reciprocal, signed or mixed factorizations could survive calibration and block uniqueness.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.