PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget_iff_mixed_composite_cost_consistency
plain-language theorem explainer
Equivalence of two prime-calibration targets for ratio characters: forcing identity on the orbit-2 axis from identity on any calibrated prime axis is equivalent to mixed-orientation cost consistency on composites 2p. Cited when collapsing the one-sided distinguished-axis formulation into the cost-visible 2p blocker. Proof is pure Iff.trans through the two-prime reciprocal-exclusion intermediate.
Claim. The following are equivalent for ratio-orbit characters. (i) Prime-direction calibration forces: if any calibrated prime axis is sent to the identity branch, then the orbit-$2$ prime axis is also identity. (ii) Under prime-direction calibration, whenever orbit $2$ is reciprocal and a distinct native prime $p$ is identity, the composite direction $2p$ is still cost-calibrated (cross-equality holds on that composite).
background
In the Primitive Recognition Calculus native-cost uniqueness development, a ratio character $\chi$ is a map on ratio orbits obeying the multiplicative character laws of the PRC kernel. Prime-direction calibration means $\chi$ is fixed on native prime axes in the sense required by the cost functional (the J-cost side of the Recognition Composition Law).
Two target propositions package different faces of the same obstruction. The one-sided distinguished-axis target says calibration forces identity on the orbit-$2$ axis whenever any calibrated prime axis is identity. The mixed-composite cost-consistency target is the cost-visible blocker: even under mixed orientation data (orbit $2$ reciprocal, a distinct native prime $p$ identity), the composite direction $2p$ must still satisfy the cross-equality that makes the native cost well-defined.
An intermediate target sits between them: if calibration leaves orbit $2$ on the reciprocal branch, no native prime axis may remain on identity (two-prime reciprocal exclusion of an identity witness).
proof idea
One-line term proof by Iff.trans of two already-proved equivalences in the same module.
First apply the equivalence of the identity-forces-two target with the two-prime reciprocal-exclusion target. Then apply the equivalence of that reciprocal-exclusion target with the mixed-composite cost-consistency target. No new case analysis; the chain closes the three formulations.
why it matters
Closes a link in the native-cost uniqueness ladder: the one-sided orbit-2 forcing statement may be swapped for the mixed $2p$ cost blocker wherever either is more convenient.
Downstream, the absurdity theorem for a prime-calibrated two-adic axis-twist character consumes the left-to-right direction (via the mixed-composite form). A sibling iff then routes the prime-pair product cost-consistency target through this same mixed-composite node. The universal-foundation conditional certificate in UniversalFoundation lists related PRC certificates in the same forcing stack.
In framework terms this is foundation work under the Recognition Composition Law and J-uniqueness (T5), not yet the T6--T8 geometric forcing; it polices which ratio characters can carry a native cost before the phi ladder and eight-tick structure are imposed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.