Pith. sign in
theorem

PRCAdmissibleCharacterGlobalOrientationTarget_of_signed_global_propagation

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

plain-language theorem explainer

If every admissible ratio character is signed-unit calibrated, and signed coherent prime orientation propagates to global cost orientation, then every admissible character is globally identity- or reciprocal-oriented. Native-cost uniqueness arguments cite this to reduce global orientation rigidity to those two interface hypotheses. The proof is a four-line wiring: feed the character, its ratio-character field, signed calibration, and the already-proved prime-coherence lemma into the propagation hypothesis.

Claim. Assume (i) every admissible ratio character $\chi$ is signed-unit calibrated, and (ii) whenever a ratio character is signed-unit calibrated and prime-orientation coherent, it is globally cost-oriented (pointwise identity or reciprocal). Then every admissible ratio character is globally cost-oriented.

background

In the Primitive Recognition Calculus native-cost uniqueness module, characters act on ratio orbits. Admissibility packages the repaired interface fields that a character must satisfy to be a candidate native cost. Global cost orientation means that at every orbit the character acts either as the identity branch or the reciprocal branch, consistently with the cost reading.

After an absolute-value countermodel, coherent prime orientation alone is not enough: the repaired target requires signed-unit calibration before one may conclude pointwise global identity-or-reciprocal orientation. The propagation hypothesis states exactly that repaired implication: ratio character + signed-unit calibration + prime-orientation coherence $\Rightarrow$ global cost orientation.

Prime-orientation coherence under admissibility is already closed: the proved lemma supplies it from any admissible character. Signed-unit calibration under admissibility remains an explicit interface hypothesis (Pass 279 notes that repaired prime-pair fields still do not force it).

proof idea

Term-mode wiring, not a new calculation. Introduce an admissible character $\chi$. Apply the propagation hypothesis to $\chi$, using four ingredients: the ratio-character projection of admissibility; signed-unit calibration from the first hypothesis at $(\chi,\mathrm{hadm})$; and prime-orientation coherence from the already-proved admissible prime-coherence theorem at $(\chi,\mathrm{hadm})$. The conclusion is exactly global cost orientation for $\chi$, which is the global orientation target.

why it matters

This is the composition step that turns the repaired orientation stack into the admissible global-orientation target used by native-cost uniqueness. Downstream, PRCAdmissibleCharacterGlobalOrientationTarget_of_signed_unit_calibration specializes it by plugging in the proved propagation theorem, leaving only signed-unit calibration as the remaining interface obligation.

In the Recognition forcing picture this sits under J-uniqueness (T5) and the Recognition Composition Law: characters that survive admissibility must collapse to the two global orientations that reproduce the unique native cost $J(x)=(x+x^{-1})/2-1$. The declaration does not itself force calibration; it isolates that remaining gap so later passes can discharge or refute it cleanly.

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