Pith. sign in
theorem

PRCSignedAdmissibleRatioCharacter_global_orientation

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

plain-language theorem explainer

Any signed-admissible ratio character is globally cost-oriented: on every rational orbit it acts as the identity or as reciprocal inversion. Cost-uniqueness and rigidity arguments cite this to move from prime-level sign calibration to full orbit orientation. The proof is a short term composition: admissibility yields coherent prime orientation, which then propagates to the global target.

Claim. Let $\chi$ map ratio orbits to ratio orbits. If $\chi$ is a signed-admissible ratio character (prime and prime-pair admissibility together with signed-unit calibration), then $\chi$ has global cost orientation: for every ratio orbit $q$, either $\chi(q)$ is cross-equal to $q$ or $\chi(q)$ is cross-equal to the reciprocal of $q$.

background

In the Primitive Recognition Calculus, a ratio character $\chi$ is a map on ratio orbits that encodes how multiplicative directions are recognized. Admissibility constrains $\chi$ on primes and prime pairs so that the induced cost matches the native J-cost structure on those generators. The signed repair adds explicit preservation of the signed unit; without it, unsigned admissibility can erase orientation and still look admissible at primes.

Global cost orientation means that on every rational orbit, $\chi$ either fixes the direction or sends it to its reciprocal. Because the J-cost is reciprocal-symmetric ($J(x)=J(1/x)$), that binary choice is exactly the orientation data needed to propagate costs from primes to composites. The module develops native-cost uniqueness: characters that generate the native cost must be rigid once signs are controlled.

Upstream scaffolding includes the doubled-trace and d'Alembert side of the native cost, and the signed-unit calibration field that blocks independent prime inversions from preserving prime costs while breaking composite costs.

proof idea

Term-mode composition of two already-proved targets. First apply the lemma that every admissible character has coherent prime orientation, using the admissible projection of the signed hypothesis. Then feed that coherence, together with the underlying ratio character and the signed-unit field, into the propagation theorem that lifts coherent prime orientation to global cost orientation on all ratio orbits. No extra case splits appear at this layer.

why it matters

This is the orientation bridge inside signed native-cost uniqueness. The sole direct consumer is the signed-admissible character rigidity target: once global orientation is known, that theorem cases on same-orbit versus reciprocal and concludes that the character-generated cost is canonical on every rational direction.

In framework terms it repairs a real gap in unsigned admissible rigidity. Sign erasure can keep prime costs while scrambling composites; the signed unit plus this global orientation step closes that hole. It sits under the PRC native-cost uniqueness program that feeds the J-uniqueness landmark (T5) and the Recognition Composition Law: orientation-correct characters are what make the cost functional well-defined on the full multiplicative group of positive ratios, not merely on prime generators.

The doc-comment on the rigidity parent states the payoff directly: once sign erasure is excluded, the character-generated cost is canonical everywhere.

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