Pith. sign in
theorem

PRCAdmissibleCharacterGlobalOrientationTarget_of_global_propagation

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

plain-language theorem explainer

Under the remaining hypothesis that coherent prime orientation propagates to every ratio direction, every admissible ratio character is globally identity- or reciprocal-oriented pointwise. Cost-uniqueness arguments cite this to collapse admissible-character rigidity to a single propagation assumption. The proof is a one-line term application of the two-hypothesis reduction, inserting the already-proved prime-coherence target.

Claim. Assume that whenever a multiplicative ratio character has coherent prime orientation, that orientation propagates to every ratio direction (via the character law and native rational factorization). Then every admissible ratio character $\chi$ is globally cost-oriented: at each ratio orbit it agrees with either the identity branch or the reciprocal branch.

background

In the primitive recognition calculus, ratio characters are multiplicative maps on ratio orbits. Admissibility packages the native cost hypotheses that make a character a candidate for the unique cost functional. Global cost orientation means the character is pointwise either the identity or the reciprocal on every orbit; that is the repaired orientation target after the absolute-value countermodel.

Prime-orientation coherence is the intermediate claim that all prime axes choose one branch consistently. That subtarget is already discharged for admissible characters. The remaining blocker is propagation: once primes are coherent, the multiplicative law and native rational factorization must force the same orientation on every composite ratio direction.

The local module builds native-cost uniqueness by reducing rigidity of admissible characters to orientation, then splitting orientation into prime coherence plus global propagation.

proof idea

One-line term wrapper. Apply the two-hypothesis reduction that turns prime-coherence plus global-propagation into the full admissible global-orientation target. Supply the already-proved prime-coherence theorem as the first argument and the assumed propagation hypothesis as the second. No further case analysis.

why it matters

This is the last packaging step before native-cost admissible-character rigidity under the propagation hypothesis. The immediate parent is the rigidity theorem that, given the same propagation assumption, concludes the full native-cost admissible-character rigidity target by composing this result with the admissible-global-orientation-to-rigidity bridge.

In the Recognition forcing picture, unique native cost is the analytic face of J-uniqueness (T5) and the Recognition Composition Law: characters that survive admissibility must be the identity or reciprocal orientation of the cost, not exotic multiplicative twists. Closing the propagation hypothesis would finish this branch of the uniqueness argument; until then the result isolates exactly what remains open.

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