Pith. sign in
theorem

PRCPrimeCalibrationForcesPrimeIdentityTraceCoherenceTarget_of_comparable_trace

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

plain-language theorem explainer

If prime calibration forces identity orientation to respect comparability of finite δ-orbit traces, then it also forces identity orientation to propagate coherently across prime axes. Native-cost uniqueness and the universal-foundation certificate cite this reduction when collapsing the remaining trace-coherence obligation. The proof is a pointwise one-line application of the character-level comparable-trace-to-coherence lemma.

Claim. Assume that every ratio character $\chi$ that is prime-direction calibrated has identity orientation respecting comparability of finite $\delta$-orbit traces. Then every such $\chi$ is prime-identity trace coherent: identity orientation propagates across prime axes under prime calibration.

background

In the Primitive Recognition Calculus, a ratio character $\chi$ is a map on ratio orbits encoding how recognition orients multiplicative structure. Prime-direction calibration means $\chi$ is locked to the native prime axes in the identity sense. Two residual targets remain for native-cost uniqueness: a sharper order target (identity orientation respects comparability of finite $\delta$-orbit traces) and a coherence target (identity orientation propagates across prime axes).

The comparable-trace property is strictly about ordered finite traces along $\delta$-orbits. Trace coherence asks that once identity orientation is fixed on one prime axis, it transfers to the others. Upstream, the character-level lemma already shows that respecting comparable traces implies full prime-identity trace coherence, because any two orbit-position traces are comparable by construction.

This module packages those character facts into global calibration targets used by the native-cost uniqueness blocker and the conditional universal-foundation certificate.

proof idea

One-line pointwise reduction. Introduce a ratio character $\chi$ together with the hypotheses that it is a ratio character and prime-direction calibrated. Apply the assumed comparable-trace target at $\chi$ to obtain that identity orientation respects comparable traces. Feed that fact into the upstream lemma PRCCharacterPrimeIdentityTraceCoherent_of_comparable_trace, which upgrades comparable-trace respect to full prime-identity trace coherence (using that orbit-position traces are always comparable). Discharge the coherence target.

why it matters

Closes one direction of the equivalence between the comparable-trace target and the exact remaining trace-coherence target, so the uniqueness chain may track either formulation. Downstream it is half of the iff linking the two targets, and it is recorded in the native-cost uniqueness blocker certificate and the conditional universal-foundation certificate.

In the Recognition Science forcing picture this is bookkeeping inside the foundation layer that pins the native cost (the J-cost side of T5) before phi, the eight-tick octave, and $D=3$ are forced. It does not itself force J-uniqueness; it ensures the prime-calibration residual is coherent enough for those later steps to sit on a single native cost.

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