PRCPrimeCalibrationForcesNonunitIdentityComparableTraceTarget_iff_successor_step_pair
plain-language theorem explainer
Equivalence of two formulations of the prime-calibration force on nonunit identity orientation: the comparable finite δ-orbit-trace form, and the split one-step successor-pair form (extends ∧ contracts). Cited by anyone closing native-cost uniqueness blockers or the universal-foundation certificate. Proof is a pure ↔ packaging of the two already-proved directions.
Claim. The following are equivalent. (i) Every prime-direction-calibrated ratio character has identity orientation that respects comparability of finite $\delta$-orbit traces on nonunit directions. (ii) Prime calibration forces both the extends and the contracts one-step successor targets on the prime-floor identity branch.
background
In the Primitive Recognition Calculus, ratio characters $\chi$ act on ratio orbits and encode orientation choices along multiplicative directions. Prime-direction calibration is the constraint that $\chi$ is already fixed on prime axes; the remaining work is to transport that orientation to every nonunit direction.
The comparable-trace target asks that, once calibrated, identity-branch orientation respect order-comparability of finite $\delta$-orbit traces on nonunit directions (a trace-order sharpening of nonunit identity-branch transport). The successor-step-pair target is the split one-step form of the corrected prime-floor successor obligation: identity orientation both extends and contracts under a single successor step on the prime floor.
This module sits in the native-cost uniqueness development: characters, doubled-trace displays, and d'Alembert-type identities are used to force the Recognition cost $J$ as the unique native cost compatible with calibration.
proof idea
Term-mode ↔ introduction. The forward direction applies the existing lemma that identity-comparable-trace forces the prime-floor successor-step pair; the reverse applies the lemma that the successor-step pair forces the nonunit identity comparable-trace target. No new algebra is done here; the declaration only packages the two one-way implications into a single equivalence.
why it matters
Native-cost uniqueness needs a clean blocker interface: several intermediate Prop targets must be interchangeable without changing the certificate surface. This iff lets the comparable-trace formulation and the split successor-pair formulation be swapped freely.
Downstream it is consumed by prc_native_cost_uniqueness_blocker_certificate (the assembled uniqueness blocker) and by prc_universal_foundation_conditional_certificate (kernel, real-complete ordered field, and trace-logic bundle). In the broader RS chain this is foundation scaffolding under T5 J-uniqueness and the Recognition Composition Law: forcing orientation coherence on nonunit directions is part of locking the native cost before constants and the mass ladder are read off.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.