Pith. sign in
theorem

PRCPrimeCalibrationForcesTwoPrimeReciprocalTraceConnectedTarget_of_forces

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

plain-language theorem explainer

If prime calibration forces reciprocal orientation at the orbit-2 axis to put every native prime on the reciprocal branch, then it also forces that orientation to transport along any finite δ-trace to a native prime. Native-cost uniqueness and universal-foundation certificates cite this implication. The argument is a one-line lift of the character-level specialization that global force implies trace-connected force.

Claim. Assume that whenever a ratio character is prime-direction calibrated, reciprocal orientation at the orbit-$2$ prime axis forces reciprocal orientation at every native prime axis. Then, for every such calibrated character, reciprocal orientation at orbit-$2$ transports along any finite $\delta$-trace connection to a native prime axis.

background

In the Primitive Recognition Calculus, a ratio character $\chi$ is a map on ratio orbits that encodes orientation choices (identity versus reciprocal branch) along prime axes. Prime-direction calibration fixes how the distinguished orbit-$2$ axis sits relative to the reciprocal branch. The native-cost uniqueness program needs to know that this local choice cannot stay isolated: it must propagate to other native primes.

Two target propositions package that demand. The stronger one says calibration forces a global rule: if orbit-$2$ is reciprocal, every native prime is reciprocal. The weaker one only asks for transport along finite $\delta$-trace connections from orbit-$2$ to a native prime. Upstream, the character-level lemma already records that the global force property implies the trace-connected respect property, by discarding the connection data and applying the universal quantifier over primes.

This declaration lifts that character-level fact to the quantified target level used by the uniqueness certificates.

proof idea

Term-mode proof. Introduce a ratio character $\chi$ together with the ratio-character and prime-calibration hypotheses. Apply the assumed target hypothesis to obtain the character-level global force property. Feed that property into the upstream lemma that global two-prime reciprocal force implies trace-connected reciprocal respect. The connection hypothesis is unused, as expected: force-for-all-primes is strictly stronger than force-along-connected-primes.

why it matters

This is one direction of the equivalence between the global reciprocal-force target and the trace-connected reciprocal target. Downstream, that equivalence is assembled as an iff, so either formulation may be used as the uniqueness blocker. The native-cost uniqueness blocker certificate and the conditional universal-foundation certificate both depend on this packaging: they need a clean statement that prime calibration cannot leave reciprocal orientation stranded at orbit-$2$ while other primes remain free.

In the broader Recognition forcing chain, native cost uniqueness is the PRC-side route toward J-uniqueness (T5) and the Recognition Composition Law. Closing the reciprocal-transport blocker is a concrete step toward a single admissible cost character, rather than a family of signed or misoriented alternatives.

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