PRCPrimeCalibrationForcesTwoPrimeReciprocalTraceConnectedTarget_iff_forces
plain-language theorem explainer
Equivalence of two formulations of the reciprocal-branch globalization target under prime calibration: the finite δ-trace transport form versus the direct “orbit-2 forces every native prime” form. Native-cost uniqueness and universal-foundation certificate work cite this to collapse the two blocker statements. Proof is a pure bidirectional term wrapper from the two already-proved one-way implications.
Claim. The following are equivalent. (i) Every prime-direction-calibrated PRC ratio character has reciprocal orientation at the orbit-$2$ prime axis transporting along any finite $\delta$-trace connection to a native prime axis. (ii) Every such character, once the orbit-$2$ prime axis lies on the reciprocal branch, places every native prime axis on the reciprocal branch.
background
In the Primitive Recognition Calculus, a ratio character is a map on ratio orbits that encodes orientation data for the native cost. Prime-direction calibration fixes how the character sits on distinguished prime axes, notably the orbit-$2$ axis. Reciprocal orientation means the character is on the reciprocal branch rather than the identity branch at that axis.
Two target Props package the desired globalization. The trace-connected target asks that reciprocal orientation at orbit $2$, once forced by calibration, transport along any finite $\delta$-trace path to an arbitrary native prime axis. The distinguished-axis target asks the shorter statement: reciprocal at orbit $2$ forces reciprocal at every native prime axis. The module isolates these as twin blockers for native-cost uniqueness.
Upstream, each direction is already a theorem: the forces-target follows from the trace-connected target by specializing the transport lemma, and conversely the trace-connected target follows from the forces-target by the matching “respects trace-connected of forces” lemma.
proof idea
Term-mode construction of $\leftrightarrow$. The left-to-right arrow is the existing theorem that the forces-target follows from the trace-connected target (introduces the character and calibration hypotheses, then applies the character-level transport specialization). The right-to-left arrow is the dual theorem that the trace-connected target follows from the forces-target (same intro pattern, then the character-level “respects trace-connected of forces” lemma). No new algebra; pure packaging of the two one-way results into an iff.
why it matters
Collapses two surface formulations of the same reciprocal-globalization blocker into one logical unit. Downstream, the native-cost uniqueness blocker certificate and the universal-foundation conditional certificate both sit on this uniqueness stack; equating the targets keeps the certificate surface from forking. In the broader Recognition forcing picture this is bookkeeping inside the native-cost uniqueness path that feeds J-uniqueness and the calibrated cost, not a new physical law. It closes a packaging gap rather than an open analytic question: once either formulation is discharged, the other is free.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.