PRCPrimeCalibrationForcesPrimeIdentityTraceCoherenceTarget_iff_comparable_trace
plain-language theorem explainer
The remaining prime-calibration trace-coherence target is equivalent to the sharper comparable-trace target: both assert that every prime-direction-calibrated ratio character has identity orientation behaving coherently on prime axes. Anyone tracking native-cost uniqueness blockers or the later refutation of the comparable-trace target will cite this bridge. The proof is a two-constructor iff built from the two one-line implication lemmas already in the module.
Claim. The following two statements are equivalent. (A) Every ratio character that is prime-direction calibrated is identity-trace-coherent on prime axes. (B) Every such character has identity orientation that respects comparability of finite $\delta$-orbit traces. In other words, the exact remaining trace-coherence target holds if and only if the sharper trace-order target holds.
background
In the Primitive Recognition Calculus, a ratio character $\chi$ is a map on ratio orbits that encodes how recognition cost orients along multiplicative directions. Prime-direction calibration means $\chi$ is already fixed on the native prime axes in the identity-compatible way. Two residual targets remain for native-cost uniqueness: identity-trace coherence (identity orientation propagates across prime axes) and the sharper comparable-trace condition (identity orientation respects order comparisons of finite $\delta$-orbit traces).
The module packages each residual as a universal Prop over characters: if $\chi$ is a ratio character and prime-direction calibrated, then either $\chi$ is prime-identity-trace-coherent, or $\chi$ respects comparable traces. Upstream one-direction lemmas already show each target implies the other by specializing the corresponding character-level coherence/comparability lemmas.
This sits inside the native-cost uniqueness development that feeds the universal foundation certificate chain; the targets are the last structural constraints before uniqueness of the native $J$-style cost on the recognition side.
proof idea
Term-mode iff constructor. The forward direction is the existing lemma that assumes the trace-coherence target and, for any calibrated character, applies the character-level fact that trace coherence yields comparable-trace respect. The reverse direction is the dual lemma: from the comparable-trace target, the character-level fact that comparable-trace respect yields trace coherence recovers the coherence target. No new algebra is done here; the declaration only packages the two implications as a single biconditional.
why it matters
This biconditional is the bookkeeping hinge that lets the development refute one residual target by refuting the other. Downstream, the comparable-trace target is refuted by transporting the already-proved refutation of the coherence target across this iff (via .mpr). The same equivalence is visible to the native-cost uniqueness blocker certificate and to the conditional universal-foundation certificate, which assemble proved and refuted residual targets into a single status object.
In Recognition Science terms, these targets sit under the uniqueness story for the native cost that eventually forces the $J$-functional (T5: $J(x)=(x+x^{-1})/2-1$) and the Recognition Composition Law. Closing or refuting them is part of showing which calibration hypotheses actually pin the cost, rather than leaving an open orientation branch on prime axes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.