Pith. sign in
theorem

PRCNativeCostAdmissibleCharacterRigidityTarget_of_signed_unit_calibration

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

plain-language theorem explainer

Signed-unit calibration of every admissible ratio character already forces native-cost rigidity: the cost built from that character matches canonical J-cost on every ratio orbit. Cite this when discharging the admissible-character rigidity target from the signed-unit calibration interface alone. The proof is a two-step term composition: calibration yields global orientation, then orientation yields cost rigidity.

Claim. If every admissible ratio character $\chi$ is signed-unit calibrated, then for every such $\chi$ and every ratio orbit $q$, the cost reconstructed from $\chi$ at $q$ is cross-equal to the canonical $J$-cost on $q$.

background

In the Primitive Recognition Calculus, ratio characters $\chi$ act on ratio orbits. Admissibility packages the structural constraints a character must satisfy to be a candidate generator of native cost. The cost-from-character construction turns such a $\chi$ into a cost functional on orbits; the canonical comparison object is the $J$-cost pulled back to ratio orbits (the unique cost forced by the Recognition Composition Law and T5 $J$-uniqueness).

Native-cost admissible character rigidity asks only that this reconstructed cost match canonical $J$ pointwise on orbits (via cross-equality), not that the character itself be identically oriented. That is the admissible replacement for raw character rigidity.

Signed-unit calibration is a stronger interface demand: every admissible $\chi$ must fix the signed units correctly. Pass 279 notes that repaired prime-pair admissibility alone does not force this. Global orientation is the intermediate target: each admissible character is pointwise identity-oriented or reciprocal-oriented everywhere.

proof idea

Pure term composition of two already-proved bridges. First apply the lemma that signed-unit calibration implies the global-orientation target (itself via signed global propagation plus the proved prime-to-global orientation propagation). Feed that orientation hypothesis into the lemma that admissible global orientation implies native-cost character rigidity: case-split on same vs inverse orientation at each orbit and transport the canonical cost by orbit congruence. No new algebra is done here.

why it matters

This closes the calibration-to-rigidity leg of the native-cost uniqueness stack. The immediate parent is the strengthened native-cost uniqueness theorem that assumes character factorization, two-calibration forcing prime calibration, and admissible signed-unit calibration; that parent reduces uniqueness to factorization plus two-calibration plus this rigidity target.

In the broader RS forcing picture, uniqueness of native cost is what pins the cost side of the Recognition Composition Law to $J(x)=(x+x^{-1})/2-1$ (T5) before $\phi$, the eight-tick octave, and $D=3$ are forced. The declaration does not invent new physics; it packages the interface reduction so uniqueness proofs can assume only signed-unit calibration rather than full orientation by hand.

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