Pith. sign in
theorem

PRCAdmissibleCharacterGlobalOrientationTarget_of_signed_unit_calibration

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

plain-language theorem explainer

Assuming every admissible ratio character is signed-unit calibrated, every such character is globally identity- or reciprocal-oriented pointwise. Native-cost uniqueness cites this to reduce admissible-character rigidity to orientation. The proof is a one-line term that feeds the calibration hypothesis into the signed-global-propagation lemma together with the already-proved prime-to-global orientation theorem.

Claim. If every admissible ratio character $\chi$ is signed-unit calibrated, then every admissible ratio character is globally cost-oriented: pointwise it is either the identity orientation or the reciprocal orientation.

background

In the Primitive Recognition Calculus, ratio characters are maps $\chi$ on ratio orbits that encode how multiplicative structure is read as cost. Admissibility packages the repaired interface constraints (cross-equation respect, normalization, and related fields). Global cost orientation means that, at every orbit, $\chi$ chooses either the identity branch or the reciprocal branch consistently with the native $J$-cost geometry.

Signed-unit calibration is a stronger local constraint: admissible characters must fix the signed unit in the calibrated way. The module records that repaired prime-pair admissibility alone does not force this (Pass 279); it is therefore carried as an explicit target hypothesis.

Upstream, global orientation is already reduced to a propagation statement: if signed-unit calibration holds and coherent prime orientation propagates to the global target, then every admissible character is globally oriented. The prime-to-global propagation step itself is proved in this module.

proof idea

One-line term proof. Apply PRCAdmissibleCharacterGlobalOrientationTarget_of_signed_global_propagation to the given signed-unit calibration hypothesis and to PRCSignedCoherentPrimeOrientationPropagatesToGlobalTarget_proved. That intermediate lemma unpacks admissibility, feeds calibration into the character, and invokes the propagation target; here the propagation target is discharged by the already-proved theorem, so no further tactics are needed.

why it matters

This closes the calibration-to-orientation bridge on the native-cost uniqueness spine. The immediate parent is PRCNativeCostAdmissibleCharacterRigidityTarget_of_signed_unit_calibration, which composes this result with the admissible-global-orientation rigidity reduction to obtain full admissible-character rigidity from signed-unit calibration alone.

In Recognition Science terms, character rigidity is the algebraic gate before the native cost is forced to the unique $J$-shape $J(x)=(x+x^{-1})/2-1$ (T5 / RCL). Orientation coherence is the discrete choice (identity vs reciprocal) that must be global before that uniqueness can be stated on ratio orbits. The declaration does not invent new physics; it packages a proved propagation theorem so the rigidity target can be cited under a single, named calibration hypothesis.

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